TM: 0 B1R 0 E1L 0 C1R 0 F1R 0 D1L 0 B0R 0 E1R 0 C0L 0 A1L 0 D0R 0 G1L 0 C1R
tape / proofs; generated by unibb prover; 2010-Jul-24 05:59:22
PROOF #1
22. {10}3 <E {1}2
24. {10}2 <E {1}4
0. {10}3:F|a <E {1}2:F|b
1. {10}2:T|a - 1 1T <A {1}3:T|b + 1
2. {10}2:T|a - 1 <E {1}4:T|b + 2
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 2...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #2
67. {{1}3 0}2 {10}3 <E {1}2
69. {{1}3 0}2 {10}2 <E {1}4
0. {{1}3 0}2:F {10}3:F|a <E {1}2:F|b
1. {{1}3 0}2:F {10}2:T|a - 1 1T <A {1}3:T|b + 1
2. {{1}3 0}2:F {10}2:T|a - 1 <E {1}4:T|b + 2
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 2...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #3
169. {10}4 {01}4 {1}2 {01}3 0 <E {1}2
171. {10}4 {01}4 {1}2 {01}2 0 <E {1}4
0. {10}4:F {01}4:F {1}2:F {01}3:F|a 0F <E {1}2:F|b
1. {10}4:F {01}4:F {1}2:F {01}3:F|a <A {1}3:T|b + 1
2. {10}4:F {01}4:F {1}2:F {01}2:T|a - 1 0T <E {1}4:T|b + 2
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 2...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #4
181. {10}4 {01}3 <D {10}2 {1}9
183. {10}4 {01}2 <D {10}3 {1}9
0. {10}4:F {01}3:F|a <D {10}2:F|b {1}9:F
1. {10}4:F {01}2:T|a - 1 0T <C 0T {10}2:F|b {1}9:F
2. {10}4:F {01}2:T|a - 1 <D {10}3:T|b + 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 1...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #5
191. {10}3 {1}2 {01}2 E> {10}3 {1}9
193. {10}3 {1}2 {01}3 E> {10}2 {1}9
0. {10}3:F {1}2:F {01}2:F|a E> {10}3:F|b {1}9:F
1. {10}3:F {1}2:F {01}2:F|a 0T D> 0T {10}2:T|b - 1 {1}9:F
2. {10}3:F {1}2:F {01}3:T|a + 1 E> {10}2:T|b - 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #6
209. {10}3 {01}2 C> {10}5 {1}7
211. {10}3 {01}3 C> {10}4 {1}7
0. {10}3:F {01}2:F|a C> {10}5:F|b {1}7:F
1. {10}3:F {01}2:F|a 0T B> 0T {10}4:T|b - 1 {1}7:F
2. {10}3:F {01}3:T|a + 1 C> {10}4:T|b - 1 {1}7:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #7
212. {10}3 {01}6 C> {10}1 {1}7
285. {10}2 {01}10 C> {10}1 {1}7
0. {10}3:F|b {01}6:F|a C> {10}1:F {1}7:F
1. {10}3:F|b {01}6:F|a 0T B> 0T {1}7:F
2. {10}3:F|b {01}7:T|a + 1 C> {1}7:F
3. {10}3:F|b {01}7:T|a + 1 0T B> {1}6:T
4. {10}3:F|b {01}8:T|a + 2 F> {1}5:T
5. {10}3:F|b {01}8:T|a + 2 1T C> {1}4:T
6. {10}3:F|b {01}8:T|a + 2 1T0T B> {1}3:T
7. {10}3:F|b {01}8:T|a + 2 1T0T1T F> {1}2:T
8. {10}3:F|b {01}8:T|a + 2 1T0T {1}2:T C> 1T
9. {10}3:F|b {01}8:T|a + 2 1T0T {1}2:T 0T B>
10. {10}3:F|b {01}8:T|a + 2 1T0T {1}2:T 0T1T C>
11. {10}3:F|b {01}8:T|a + 2 1T0T {1}2:T 0T1T <D 1T
12. {10}3:F|b {01}8:T|a + 2 1T0T {1}2:T 0T <C 0T1T
13. {10}3:F|b {01}8:T|a + 2 1T0T {1}2:T <D 1T0T1T
14. {10}3:F|b {01}8:T|a + 2 1T0T1T <C {01}2:T
15. {10}3:F|b {01}8:T|a + 2 1T {0}2:T B> {01}2:T
16. {10}3:F|b {01}8:T|a + 2 1T {0}2:T 1T C> 1T0T1T
17. {10}3:F|b {01}8:T|a + 2 1T {0}2:T 1T0T B> 0T1T
18. {10}3:F|b {01}8:T|a + 2 1T {0}2:T 1T0T1T C> 1T
19. {10}3:F|b {01}8:T|a + 2 1T {0}2:T {10}2:T B>
20. {10}3:F|b {01}8:T|a + 2 1T {0}2:T {10}2:T 1T C>
21. {10}3:F|b {01}8:T|a + 2 1T {0}2:T {10}2:T 1T <D 1T
22. {10}3:F|b {01}8:T|a + 2 1T {0}2:T {10}2:T <C 0T1T
23. {10}3:F|b {01}8:T|a + 2 1T {0}2:T 1T0T1T <D 1T0T1T
24. {10}3:F|b {01}8:T|a + 2 1T {0}2:T 1T0T <C {01}2:T
25. {10}3:F|b {01}8:T|a + 2 1T {0}2:T 1T <D 1T {01}2:T
26. {10}3:F|b {01}8:T|a + 2 1T {0}2:T <C {01}3:T
27. {10}3:F|b {01}8:T|a + 2 1T0T <D 1T {01}3:T
28. {10}3:F|b {01}8:T|a + 2 {1}2:T E> 1T {01}3:T
29. {10}3:F|b {01}8:T|a + 2 {1}2:T 0T D> {01}3:T
30. {10}3:F|b {01}8:T|a + 2 {1}2:T 0T1T E> 1T {01}2:T
31. {10}3:F|b {01}8:T|a + 2 {1}2:T 0T1T0T D> {01}2:T
32. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}2:T E> 1T0T1T
33. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}2:T 0T D> 0T1T
34. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}3:T E> 1T
35. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}3:T 0T D>
36. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}4:T E>
37. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}4:T <A 1T
38. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}3:T 0T <E {1}2:T proof used (3)
39. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}1:T 0T <E {1}6:T
40. {10}3:F|b {01}8:T|a + 2 {1}2:T {01}1:T <A {1}7:T
41. {10}3:F|b {01}8:T|a + 2 {1}2:T 0T <E {1}8:T
42. {10}3:F|b {01}8:T|a + 2 {1}2:T <A {1}9:T
43. {10}3:F|b {01}8:T|a + 2 1T <E {1}10:T
44. {10}3:F|b {01}8:T|a + 2 0T D> {1}10:T
45. {10}3:F|b {01}8:T|a + 2 0T <C 0T {1}9:T
46. {10}3:F|b {01}8:T|a + 2 <D 1T0T {1}9:T
47. {10}3:F|b {01}7:T|a + 1 0T <C 0T1T0T {1}9:T
xmod: 1
xvar_min: a + 0 val=1 remaining exponent: 1 part_down=1
xmod taken from proof:
48. {10}3:F|b {01}7:T|a + 1 <D {10}2:T {1}9:T proof used (4)
49. {10}3:F|b {01}1:T <D {10}8:T|a + 2 {1}9:T
50. {10}3:F|b 0T <C 0T {10}8:T|a + 2 {1}9:T
51. {10}3:F|b <D {10}9:T|a + 3 {1}9:T
52. {10}2:T|b - 1 {1}2:T E> {10}9:T|a + 3 {1}9:T
53. {10}2:T|b - 1 {1}2:T 0T D> 0T {10}8:T|a + 2 {1}9:T
54. {10}2:T|b - 1 {1}2:T 0T1T E> {10}8:T|a + 2 {1}9:T
55. {10}2:T|b - 1 {1}2:T 0T1T0T D> 0T {10}7:T|a + 1 {1}9:T
xmod: 1
xvar_min: a + 0 val=1 remaining exponent: 1 part_down=1
xmod taken from proof:
56. {10}2:T|b - 1 {1}2:T {01}2:T E> {10}7:T|a + 1 {1}9:T proof used (5)
57. {10}2:T|b - 1 {1}2:T {01}8:T|a + 2 E> {10}1:T {1}9:T
58. {10}2:T|b - 1 {1}2:T {01}8:T|a + 2 0T D> 0T {1}9:T
59. {10}2:T|b - 1 {1}2:T {01}9:T|a + 3 E> {1}9:T
60. {10}2:T|b - 1 {1}2:T {01}9:T|a + 3 0T D> {1}8:T
61. {10}2:T|b - 1 {1}2:T {01}9:T|a + 3 0T <C 0T {1}7:T
62. {10}2:T|b - 1 {1}2:T {01}9:T|a + 3 <D 1T0T {1}7:T
63. {10}2:T|b - 1 {1}2:T {01}8:T|a + 2 0T <C 0T1T0T {1}7:T
xmod: 1
xvar_min: a + 1 val=0 remaining exponent: 1 part_down=1
xmod taken from proof:
64. {10}2:T|b - 1 {1}2:T {01}8:T|a + 2 <D {10}2:T {1}7:T proof used (4)
65. {10}2:T|b - 1 {1}2:T {01}1:T <D {10}9:T|a + 3 {1}7:T
66. {10}2:T|b - 1 {1}2:T 0T <C 0T {10}9:T|a + 3 {1}7:T
67. {10}2:T|b - 1 {1}2:T <D {10}10:T|a + 4 {1}7:T
68. {10}2:T|b - 1 1T <C 0T {10}10:T|a + 4 {1}7:T
69. {10}2:T|b - 1 0T B> 0T {10}10:T|a + 4 {1}7:T
70. {10}2:T|b - 1 0T1T C> {10}10:T|a + 4 {1}7:T
71. {10}2:T|b - 1 0T1T0T B> 0T {10}9:T|a + 3 {1}7:T
xmod: 1
xvar_min: a + 2 val=-1 remaining exponent: 1 part_down=1
xmod taken from proof:
72. {10}2:T|b - 1 {01}2:T C> {10}9:T|a + 3 {1}7:T proof used (6)
73. {10}2:T|b - 1 {01}10:T|a + 4 C> {10}1:T {1}7:T
XSTEPS: 68 =
STEPS: 126
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 4...
linearity OK
minimum a + 0 => 1
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #8
358. {01}2 C> {10}17 {1}7
360. {01}3 C> {10}16 {1}7
0. {01}2:F|a C> {10}17:F|b {1}7:F
1. {01}2:F|a 0T B> 0T {10}16:T|b - 1 {1}7:F
2. {01}3:T|a + 1 C> {10}16:T|b - 1 {1}7:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #9
409. {01}19 <D {10}2 {1}9
411. {01}18 <D {10}3 {1}9
0. {01}19:F|a <D {10}2:F|b {1}9:F
1. {01}18:T|a - 1 0T <C 0T {10}2:F|b {1}9:F
2. {01}18:T|a - 1 <D {10}3:T|b + 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 1...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #10
418. {10}2 D> 0 {10}19 {1}9
420. {10}3 D> 0 {10}18 {1}9
0. {10}2:F|a D> 0F {10}19:F|b {1}9:F
1. {10}2:F|a 1T E> {10}19:F|b {1}9:F
2. {10}3:T|a + 1 D> 0T {10}18:T|b - 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #11
429. {10}20 1 <D {10}2 {1}7
431. {10}19 1 <D {10}3 {1}7
0. {10}20:F|a 1F <D {10}2:F|b {1}7:F
1. {10}20:F|a <C 0T {10}2:F|b {1}7:F
2. {10}19:T|a - 1 1T <D {10}3:T|b + 1 {1}7:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 1...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #12
432. {10}1 1 <D {10}21 {1}7
450. {10}1 1 <D {10}23 {1}5
0. {10}1:F 1F <D {10}21:F|a {1}7:F|b
1. {10}1:F <C 0T {10}21:F|a {1}7:F|b
2. 1T <D {10}22:T|a + 1 {1}7:F|b
3. <C 0T {10}22:T|a + 1 {1}7:F|b
4. <D {10}23:T|a + 2 {1}7:F|b
5. 1T E> {10}23:T|a + 2 {1}7:F|b
6. 1T0T D> 0T {10}22:T|a + 1 {1}7:F|b
7. 1T0T1T E> {10}22:T|a + 1 {1}7:F|b
xmod: 1
xvar_min: a + -1 val=2 remaining exponent: 1 part_down=1
xmod taken from proof:
8. {10}2:T D> 0T {10}21:T|a + 0 {1}7:F|b proof used (10)
9. {10}22:T|a + 1 D> 0T {10}1:T {1}7:F|b
10. {10}22:T|a + 1 1T E> {10}1:T {1}7:F|b
11. {10}23:T|a + 2 D> 0T {1}7:F|b
12. {10}23:T|a + 2 1T E> {1}7:F|b
13. {10}24:T|a + 3 D> {1}6:T|b - 1
14. {10}24:T|a + 3 <C 0T {1}5:T|b - 2
15. {10}23:T|a + 2 1T <D 1T0T {1}5:T|b - 2
16. {10}23:T|a + 2 <C 0T1T0T {1}5:T|b - 2
xmod: 1
xvar_min: a + 0 val=1 remaining exponent: 1 part_down=1
xmod taken from proof:
17. {10}22:T|a + 1 1T <D {10}2:T {1}5:T|b - 2 proof used (11)
18. {10}1:T 1T <D {10}23:T|a + 2 {1}5:T|b - 2
XSTEPS: 16 =
STEPS: 98
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 2...
linearity OK
minimum a + -1 => 2
2. variable = b - 2...
linearity OK
minimum b - 2 => 3
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #13
480. {1}3 {0 {1}2}2 C> {1}55
483. {1}3 {0 {1}2}3 C> {1}52
0. {1}3:F {0 {1}2}2:F|a C> {1}55:F|b
1. {1}3:F {0 {1}2}2:F|a 0T B> {1}54:T|b - 1
2. {1}3:F {0 {1}2}2:F|a 0T1T F> {1}53:T|b - 2
3. {1}3:F {0 {1}2}3:T|a + 1 C> {1}52:T|b - 3
XSTEPS: 3 =
STEPS: 3
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 3...
linearity OK
minimum b - 3 => 4
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #14
574. {1}3 {0 {1}2}17 {0}2 {10}3 {01}2 0 B> 0 {1}7
647. {1}3 {0 {1}2}17 {0}2 {10}2 {01}6 0 B> 0 {1}7
0. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}2:F|a 0F B> 0F {1}7:F
1. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}3:T|a + 1 C> {1}7:F
2. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}3:T|a + 1 0T B> {1}6:T
3. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 F> {1}5:T
4. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T C> {1}4:T
5. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T B> {1}3:T
6. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T1T F> {1}2:T
7. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T {1}2:T C> 1T
8. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T {1}2:T 0T B>
9. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T {1}2:T 0T1T C>
10. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T {1}2:T 0T1T <D 1T
11. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T {1}2:T 0T <C 0T1T
12. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T {1}2:T <D 1T0T1T
13. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T1T <C {01}2:T
14. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T B> {01}2:T
15. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T 1T C> 1T0T1T
16. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T 1T0T B> 0T1T
17. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T 1T0T1T C> 1T
18. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T {10}2:T B>
19. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T {10}2:T 1T C>
20. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T {10}2:T 1T <D 1T
21. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T {10}2:T <C 0T1T
22. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T 1T0T1T <D 1T0T1T
23. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T 1T0T <C {01}2:T
24. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T 1T <D 1T {01}2:T
25. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T {0}2:T <C {01}3:T
26. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T0T <D 1T {01}3:T
27. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T E> 1T {01}3:T
28. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T 0T D> {01}3:T
29. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T 0T1T E> 1T {01}2:T
30. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T 0T1T0T D> {01}2:T
31. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}2:T E> 1T0T1T
32. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}2:T 0T D> 0T1T
33. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}3:T E> 1T
34. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}3:T 0T D>
35. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}4:T E>
36. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}4:T <A 1T
37. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}3:T 0T <E {1}2:T proof used (3)
38. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}1:T 0T <E {1}6:T
39. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T {01}1:T <A {1}7:T
40. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T 0T <E {1}8:T
41. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 {1}2:T <A {1}9:T
42. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 1T <E {1}10:T
43. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 0T D> {1}10:T
44. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 0T <C 0T {1}9:T
45. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}4:T|a + 2 <D 1T0T {1}9:T
46. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}3:T|a + 1 0T <C 0T1T0T {1}9:T
xmod: 1
xvar_min: a + 0 val=1 remaining exponent: 1 part_down=1
xmod taken from proof:
47. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}3:T|a + 1 <D {10}2:T {1}9:T proof used (4)
48. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b {01}1:T <D {10}4:T|a + 2 {1}9:T
49. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b 0T <C 0T {10}4:T|a + 2 {1}9:T
50. {1}3:F {0 {1}2}17:F {0}2:F {10}3:F|b <D {10}5:T|a + 3 {1}9:T
51. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T E> {10}5:T|a + 3 {1}9:T
52. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T 0T D> 0T {10}4:T|a + 2 {1}9:T
53. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T 0T1T E> {10}4:T|a + 2 {1}9:T
54. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T 0T1T0T D> 0T {10}3:T|a + 1 {1}9:T
xmod: 1
xvar_min: a + 0 val=1 remaining exponent: 1 part_down=1
xmod taken from proof:
55. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}2:T E> {10}3:T|a + 1 {1}9:T proof used (5)
56. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}4:T|a + 2 E> {10}1:T {1}9:T
57. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}4:T|a + 2 0T D> 0T {1}9:T
58. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}5:T|a + 3 E> {1}9:T
59. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}5:T|a + 3 0T D> {1}8:T
60. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}5:T|a + 3 0T <C 0T {1}7:T
61. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}5:T|a + 3 <D 1T0T {1}7:T
62. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}4:T|a + 2 0T <C 0T1T0T {1}7:T
xmod: 1
xvar_min: a + 1 val=0 remaining exponent: 1 part_down=1
xmod taken from proof:
63. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}4:T|a + 2 <D {10}2:T {1}7:T proof used (4)
64. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T {01}1:T <D {10}5:T|a + 3 {1}7:T
65. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T 0T <C 0T {10}5:T|a + 3 {1}7:T
66. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {1}2:T <D {10}6:T|a + 4 {1}7:T
67. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 1T <C 0T {10}6:T|a + 4 {1}7:T
68. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 0T B> 0T {10}6:T|a + 4 {1}7:T
69. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 0T1T C> {10}6:T|a + 4 {1}7:T
70. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 0T1T0T B> 0T {10}5:T|a + 3 {1}7:T
xmod: 1
xvar_min: a + 2 val=-1 remaining exponent: 1 part_down=1
xmod taken from proof:
71. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {01}2:T C> {10}5:T|a + 3 {1}7:T proof used (6)
72. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {01}6:T|a + 4 C> {10}1:T {1}7:T
73. {1}3:F {0 {1}2}17:F {0}2:F {10}2:T|b - 1 {01}6:T|a + 4 0T B> 0T {1}7:T
XSTEPS: 68 =
STEPS: 94
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 4...
linearity OK
minimum a + 0 => 1
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #15
720. {1}3 {0 {1}2}17 {0}3 {10}2 B> 0 {10}12 {1}7
722. {1}3 {0 {1}2}17 {0}3 {10}3 B> 0 {10}11 {1}7
0. {1}3:F {0 {1}2}17:F {0}3:F {10}2:F|a B> 0F {10}12:F|b {1}7:F
1. {1}3:F {0 {1}2}17:F {0}3:F {10}2:F|a 1T C> {10}12:F|b {1}7:F
2. {1}3:F {0 {1}2}17:F {0}3:F {10}3:T|a + 1 B> 0T {10}11:T|b - 1 {1}7:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #16
772. {1}3 {0 {1}2}17 {0}3 {10}14 1 <D {10}2 {1}9
774. {1}3 {0 {1}2}17 {0}3 {10}13 1 <D {10}3 {1}9
0. {1}3:F {0 {1}2}17:F {0}3:F {10}14:F|a 1F <D {10}2:F|b {1}9:F
1. {1}3:F {0 {1}2}17:F {0}3:F {10}14:F|a <C 0T {10}2:F|b {1}9:F
2. {1}3:F {0 {1}2}17:F {0}3:F {10}13:T|a - 1 1T <D {10}3:T|b + 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 1...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #17
858. {1}3 {0 {1}2}16 {10}2 D> 0 {10}20 {1}9
860. {1}3 {0 {1}2}16 {10}3 D> 0 {10}19 {1}9
0. {1}3:F {0 {1}2}16:F {10}2:F|a D> 0F {10}20:F|b {1}9:F
1. {1}3:F {0 {1}2}16:F {10}2:F|a 1T E> {10}20:F|b {1}9:F
2. {1}3:F {0 {1}2}16:F {10}3:T|a + 1 D> 0T {10}19:T|b - 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #18
861. {1}3 {0 {1}2}16 {10}21 D> 0 {10}1 {1}9
1190. {1}3 {0 {1}2}13 {10}121 D> 0 {10}1 {1}9
0. {1}3:F {0 {1}2}16:F|b {10}21:F|a D> 0F {10}1:F {1}9:F
1. {1}3:F {0 {1}2}16:F|b {10}21:F|a 1T E> {10}1:F {1}9:F
2. {1}3:F {0 {1}2}16:F|b {10}22:T|a + 1 D> 0T {1}9:F
3. {1}3:F {0 {1}2}16:F|b {10}22:T|a + 1 1T E> {1}9:F
4. {1}3:F {0 {1}2}16:F|b {10}23:T|a + 2 D> {1}8:T
5. {1}3:F {0 {1}2}16:F|b {10}23:T|a + 2 <C 0T {1}7:T
6. {1}3:F {0 {1}2}16:F|b {10}22:T|a + 1 1T <D 1T0T {1}7:T
7. {1}3:F {0 {1}2}16:F|b {10}22:T|a + 1 <C 0T1T0T {1}7:T
xmod: 1
xvar_min: a + -1 val=2 remaining exponent: 1 part_down=1
xmod taken from proof:
8. {1}3:F {0 {1}2}16:F|b {10}21:T|a + 0 1T <D {10}2:T {1}7:T proof used (16)
9. {1}3:F {0 {1}2}16:F|b {10}1:T 1T <D {10}22:T|a + 1 {1}7:T
10. {1}3:F {0 {1}2}16:F|b {10}1:T <C 0T {10}22:T|a + 1 {1}7:T
11. {1}3:F {0 {1}2}16:F|b 1T <D {10}23:T|a + 2 {1}7:T
12. {1}3:F {0 {1}2}16:F|b <C 0T {10}23:T|a + 2 {1}7:T
13. {1}3:F {0 {1}2}15:T|b - 1 0T1T0T B> 0T {10}23:T|a + 2 {1}7:T
xmod: 1
xvar_min: a + 1 val=0 remaining exponent: 1 part_down=1
xmod taken from proof:
14. {1}3:F {0 {1}2}15:T|b - 1 {01}2:T C> {10}23:T|a + 2 {1}7:T proof used (6)
15. {1}3:F {0 {1}2}15:T|b - 1 {01}24:T|a + 3 C> {10}1:T {1}7:T
16. {1}3:F {0 {1}2}15:T|b - 1 {01}24:T|a + 3 0T B> 0T {1}7:T
17. {1}3:F {0 {1}2}15:T|b - 1 {01}25:T|a + 4 C> {1}7:T
18. {1}3:F {0 {1}2}15:T|b - 1 {01}25:T|a + 4 0T B> {1}6:T
19. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 F> {1}5:T
20. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T C> {1}4:T
21. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T B> {1}3:T
22. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T1T F> {1}2:T
23. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T {1}2:T C> 1T
24. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T {1}2:T 0T B>
25. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T {1}2:T 0T1T C>
26. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T {1}2:T 0T1T <D 1T
27. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T {1}2:T 0T <C 0T1T
28. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T {1}2:T <D 1T0T1T
29. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T1T <C {01}2:T
30. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T B> {01}2:T
31. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T 1T C> 1T0T1T
32. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T 1T0T B> 0T1T
33. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T 1T0T1T C> 1T
34. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T {10}2:T B>
35. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T {10}2:T 1T C>
36. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T {10}2:T 1T <D 1T
37. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T {10}2:T <C 0T1T
38. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T 1T0T1T <D 1T0T1T
39. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T 1T0T <C {01}2:T
40. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T 1T <D 1T {01}2:T
41. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T {0}2:T <C {01}3:T
42. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T0T <D 1T {01}3:T
43. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T E> 1T {01}3:T
44. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T 0T D> {01}3:T
45. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T 0T1T E> 1T {01}2:T
46. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T 0T1T0T D> {01}2:T
47. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}2:T E> 1T0T1T
48. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}2:T 0T D> 0T1T
49. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}3:T E> 1T
50. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}3:T 0T D>
51. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}4:T E>
52. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}4:T <A 1T
53. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}3:T 0T <E {1}2:T proof used (3)
54. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}1:T 0T <E {1}6:T
55. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T {01}1:T <A {1}7:T
56. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T 0T <E {1}8:T
57. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 {1}2:T <A {1}9:T
58. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 1T <E {1}10:T
59. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 0T D> {1}10:T
60. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 0T <C 0T {1}9:T
61. {1}3:F {0 {1}2}15:T|b - 1 {01}26:T|a + 5 <D 1T0T {1}9:T
62. {1}3:F {0 {1}2}15:T|b - 1 {01}25:T|a + 4 0T <C 0T1T0T {1}9:T
xmod: 1
xvar_min: a + 3 val=-2 remaining exponent: 1 part_down=1
xmod taken from proof:
63. {1}3:F {0 {1}2}15:T|b - 1 {01}25:T|a + 4 <D {10}2:T {1}9:T proof used (4)
64. {1}3:F {0 {1}2}15:T|b - 1 {01}1:T <D {10}26:T|a + 5 {1}9:T
65. {1}3:F {0 {1}2}15:T|b - 1 0T <C 0T {10}26:T|a + 5 {1}9:T
66. {1}3:F {0 {1}2}15:T|b - 1 <D {10}27:T|a + 6 {1}9:T
67. {1}3:F {0 {1}2}14:T|b - 2 0T1T <C 0T {10}27:T|a + 6 {1}9:T
68. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T B> 0T {10}27:T|a + 6 {1}9:T
69. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T 1T C> {10}27:T|a + 6 {1}9:T
70. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T 1T0T B> 0T {10}26:T|a + 5 {1}9:T
71. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T 1T0T1T C> {10}26:T|a + 5 {1}9:T
xmod: 1
xvar_min: a + 3 val=-2 remaining exponent: 1 part_down=1
xmod taken from proof:
72. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}2:T B> 0T {10}25:T|a + 4 {1}9:T proof used (15)
73. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}26:T|a + 5 B> 0T {10}1:T {1}9:T
74. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}26:T|a + 5 1T C> {10}1:T {1}9:T
75. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}27:T|a + 6 B> 0T {1}9:T
76. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}27:T|a + 6 1T C> {1}9:T
77. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 B> {1}8:T
78. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 1T F> {1}7:T
79. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T C> {1}6:T
80. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T B> {1}5:T
81. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T1T F> {1}4:T
82. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}2:T C> {1}3:T
83. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T B> {1}2:T
84. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 1T F> 1T
85. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T {1}2:T C>
86. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T {1}2:T <D 1T
87. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 1T <C 0T1T
88. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 0T B> 0T1T
89. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 0T1T C> 1T
90. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 0T1T0T B>
91. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T {01}2:T C>
92. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T {01}2:T <D 1T
93. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 0T1T0T <C 0T1T
94. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 0T1T <D 1T0T1T
95. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T 0T <C {01}2:T
96. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {{1}2 0}2:T <D 1T {01}2:T
97. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T E> 1T {01}2:T
98. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T 0T D> {01}2:T
99. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T 0T1T E> 1T0T1T
100. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T 0T1T0T D> 0T1T
101. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}2:T E> 1T
102. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}2:T 0T D>
103. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}3:T E>
104. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}3:T <A 1T
105. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}2:T 0T <E {1}2:T proof used (3)
106. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}1:T 0T <E {1}4:T
107. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T {01}1:T <A {1}5:T
108. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T 0T <E {1}6:T
109. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}3:T <A {1}7:T
110. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T {1}2:T <E {1}8:T
111. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T1T0T D> {1}8:T
112. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T1T0T <C 0T {1}7:T
113. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T1T <D 1T0T {1}7:T
114. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T 0T <C 0T1T0T {1}7:T
115. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {1}2:T <D {10}2:T {1}7:T
116. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 1T <C 0T {10}2:T {1}7:T
117. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 0T B> 0T {10}2:T {1}7:T
118. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 0T1T C> {10}2:T {1}7:T
119. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 0T1T0T B> 0T1T0T {1}7:T
120. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {01}2:T C> 1T0T {1}7:T
xmod: 1
xvar_min: a + 6 val=-5 remaining exponent: 1 part_down=1
xmod taken from proof:
121. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}28:T|a + 7 {01}2:T 0T B> 0T {1}7:T proof used (14)
122. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}110:T|a + 6 * 4 + 2 0T B> 0T {1}7:T
123. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}111:T|a + 6 * 4 + 3 C> {1}7:T
124. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}111:T|a + 6 * 4 + 3 0T B> {1}6:T
125. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 F> {1}5:T
126. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T C> {1}4:T
127. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T B> {1}3:T
128. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T1T F> {1}2:T
129. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T {1}2:T C> 1T
130. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T {1}2:T 0T B>
131. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T {1}2:T 0T1T C>
132. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T {1}2:T 0T1T <D 1T
133. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T {1}2:T 0T <C 0T1T
134. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T {1}2:T <D 1T0T1T
135. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T1T <C {01}2:T
136. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T B> {01}2:T
137. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T 1T C> 1T0T1T
138. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T 1T0T B> 0T1T
139. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T 1T0T1T C> 1T
140. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T {10}2:T B>
141. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T {10}2:T 1T C>
142. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T {10}2:T 1T <D 1T
143. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T {10}2:T <C 0T1T
144. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T 1T0T1T <D 1T0T1T
145. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T 1T0T <C {01}2:T
146. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T 1T <D 1T {01}2:T
147. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T {0}2:T <C {01}3:T
148. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T0T <D 1T {01}3:T
149. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T E> 1T {01}3:T
150. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T 0T D> {01}3:T
151. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T 0T1T E> 1T {01}2:T
152. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T 0T1T0T D> {01}2:T
153. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}2:T E> 1T0T1T
154. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}2:T 0T D> 0T1T
155. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}3:T E> 1T
156. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}3:T 0T D>
157. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}4:T E>
158. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}4:T <A 1T
159. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}3:T 0T <E {1}2:T proof used (3)
160. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}1:T 0T <E {1}6:T
161. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T {01}1:T <A {1}7:T
162. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T 0T <E {1}8:T
163. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 {1}2:T <A {1}9:T
164. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 1T <E {1}10:T
165. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 0T D> {1}10:T
166. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 0T <C 0T {1}9:T
167. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}112:T|a + 6 * 4 + 4 <D 1T0T {1}9:T
168. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}111:T|a + 6 * 4 + 3 0T <C 0T1T0T {1}9:T
xmod: 1
xvar_min: a + 6 * 4 + 2 val=-6 remaining exponent: 1 part_down=1
xmod taken from proof:
169. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}111:T|a + 6 * 4 + 3 <D {10}2:T {1}9:T proof used (4)
170. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T {01}1:T <D {10}112:T|a + 6 * 4 + 4 {1}9:T
171. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T 0T <C 0T {10}112:T|a + 6 * 4 + 4 {1}9:T
172. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {10}1:T <D {10}113:T|a + 6 * 4 + 5 {1}9:T
173. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T E> {10}113:T|a + 6 * 4 + 5 {1}9:T
174. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T 0T D> 0T {10}112:T|a + 6 * 4 + 4 {1}9:T
175. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T 0T1T E> {10}112:T|a + 6 * 4 + 4 {1}9:T
176. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T 0T1T0T D> 0T {10}111:T|a + 6 * 4 + 3 {1}9:T
xmod: 1
xvar_min: a + 6 * 4 + 2 val=-6 remaining exponent: 1 part_down=1
xmod taken from proof:
177. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}2:T E> {10}111:T|a + 6 * 4 + 3 {1}9:T proof used (5)
178. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}112:T|a + 6 * 4 + 4 E> {10}1:T {1}9:T
179. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}112:T|a + 6 * 4 + 4 0T D> 0T {1}9:T
180. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}113:T|a + 6 * 4 + 5 E> {1}9:T
181. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}113:T|a + 6 * 4 + 5 0T D> {1}8:T
182. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}113:T|a + 6 * 4 + 5 0T <C 0T {1}7:T
183. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}113:T|a + 6 * 4 + 5 <D 1T0T {1}7:T
184. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}112:T|a + 6 * 4 + 4 0T <C 0T1T0T {1}7:T
xmod: 1
xvar_min: a + 6 * 4 + 3 val=-6 remaining exponent: 1 part_down=1
xmod taken from proof:
185. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}112:T|a + 6 * 4 + 4 <D {10}2:T {1}7:T proof used (4)
186. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T {01}1:T <D {10}113:T|a + 6 * 4 + 5 {1}7:T
187. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T 0T <C 0T {10}113:T|a + 6 * 4 + 5 {1}7:T
188. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T {1}2:T <D {10}114:T|a + 6 * 4 + 6 {1}7:T
189. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T 1T <C 0T {10}114:T|a + 6 * 4 + 6 {1}7:T
190. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T B> 0T {10}114:T|a + 6 * 4 + 6 {1}7:T
191. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T 1T C> {10}114:T|a + 6 * 4 + 6 {1}7:T
192. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T 1T0T B> 0T {10}113:T|a + 6 * 4 + 5 {1}7:T
193. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T 1T0T1T C> {10}113:T|a + 6 * 4 + 5 {1}7:T
xmod: 1
xvar_min: a + 6 * 4 + 3 val=-6 remaining exponent: 1 part_down=1
xmod taken from proof:
194. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}2:T B> 0T {10}112:T|a + 6 * 4 + 4 {1}7:T proof used (15)
195. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}113:T|a + 6 * 4 + 5 B> 0T {10}1:T {1}7:T
196. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}113:T|a + 6 * 4 + 5 1T C> {10}1:T {1}7:T
197. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}114:T|a + 6 * 4 + 6 B> 0T {1}7:T
198. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}114:T|a + 6 * 4 + 6 1T C> {1}7:T
199. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 B> {1}6:T
200. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 1T F> {1}5:T
201. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T C> {1}4:T
202. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T 0T B> {1}3:T
203. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T 0T1T F> {1}2:T
204. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T 0T {1}2:T C> 1T
205. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {{1}2 0}2:T B>
206. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {{1}2 0}2:T 1T C>
207. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {{1}2 0}2:T 1T <D 1T
208. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {{1}2 0}2:T <C 0T1T
209. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T 0T {1}2:T <D 1T0T1T
210. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T 0T1T <C {01}2:T
211. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T B> {01}2:T
212. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T 1T C> 1T0T1T
213. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T 1T0T B> 0T1T
214. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T 1T0T1T C> 1T
215. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T {10}2:T B>
216. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T {10}2:T 1T C>
217. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T {10}2:T 1T <D 1T
218. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T {10}2:T <C 0T1T
219. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T 1T0T1T <D 1T0T1T
220. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T 1T0T <C {01}2:T
221. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T 1T <D 1T {01}2:T
222. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T {0}2:T <C {01}3:T
223. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T 0T <D 1T {01}3:T
224. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T E> 1T {01}3:T
225. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T 0T D> {01}3:T
226. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T 0T1T E> 1T {01}2:T
227. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T 0T1T0T D> {01}2:T
228. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}2:T E> 1T0T1T
229. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}2:T 0T D> 0T1T
230. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}3:T E> 1T
231. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}3:T 0T D>
232. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}4:T E>
233. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}4:T <A 1T
234. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}3:T 0T <E {1}2:T proof used (3)
235. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}1:T 0T <E {1}6:T
236. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T {01}1:T <A {1}7:T
237. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T 0T <E {1}8:T
238. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}3:T <A {1}9:T
239. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 {1}2:T <E {1}10:T
240. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}116:T|a + 6 * 4 + 8 D> {1}10:T
241. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}116:T|a + 6 * 4 + 8 <C 0T {1}9:T
242. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 1T <D 1T0T {1}9:T
243. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}115:T|a + 6 * 4 + 7 <C 0T1T0T {1}9:T
xmod: 1
xvar_min: a + 6 * 4 + 5 val=-7 remaining exponent: 1 part_down=1
xmod taken from proof:
244. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}114:T|a + 6 * 4 + 6 1T <D {10}2:T {1}9:T proof used (16)
245. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}1:T 1T <D {10}115:T|a + 6 * 4 + 7 {1}9:T
246. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T {10}1:T <C 0T {10}115:T|a + 6 * 4 + 7 {1}9:T
247. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T 1T <D {10}116:T|a + 6 * 4 + 8 {1}9:T
248. {1}3:F {0 {1}2}14:T|b - 2 {0}3:T <C 0T {10}116:T|a + 6 * 4 + 8 {1}9:T
249. {1}3:F {0 {1}2}14:T|b - 2 {0}2:T <D {10}117:T|a + 6 * 4 + 9 {1}9:T
250. {1}3:F {0 {1}2}14:T|b - 2 0T1T E> {10}117:T|a + 6 * 4 + 9 {1}9:T
251. {1}3:F {0 {1}2}14:T|b - 2 0T1T0T D> 0T {10}116:T|a + 6 * 4 + 8 {1}9:T
xmod: 1
xvar_min: a + 6 * 4 + 7 val=-7 remaining exponent: 1 part_down=1
xmod taken from proof:
252. {1}3:F {0 {1}2}14:T|b - 2 {01}2:T E> {10}116:T|a + 6 * 4 + 8 {1}9:T proof used (5)
253. {1}3:F {0 {1}2}14:T|b - 2 {01}117:T|a + 6 * 4 + 9 E> {10}1:T {1}9:T
254. {1}3:F {0 {1}2}14:T|b - 2 {01}117:T|a + 6 * 4 + 9 0T D> 0T {1}9:T
255. {1}3:F {0 {1}2}14:T|b - 2 {01}118:T|a + 6 * 4 + 10 E> {1}9:T
256. {1}3:F {0 {1}2}14:T|b - 2 {01}118:T|a + 6 * 4 + 10 0T D> {1}8:T
257. {1}3:F {0 {1}2}14:T|b - 2 {01}118:T|a + 6 * 4 + 10 0T <C 0T {1}7:T
258. {1}3:F {0 {1}2}14:T|b - 2 {01}118:T|a + 6 * 4 + 10 <D 1T0T {1}7:T
259. {1}3:F {0 {1}2}14:T|b - 2 {01}117:T|a + 6 * 4 + 9 0T <C 0T1T0T {1}7:T
xmod: 1
xvar_min: a + 6 * 4 + 8 val=-7 remaining exponent: 1 part_down=1
xmod taken from proof:
260. {1}3:F {0 {1}2}14:T|b - 2 {01}117:T|a + 6 * 4 + 9 <D {10}2:T {1}7:T proof used (4)
261. {1}3:F {0 {1}2}14:T|b - 2 {01}1:T <D {10}118:T|a + 6 * 4 + 10 {1}7:T
262. {1}3:F {0 {1}2}14:T|b - 2 0T <C 0T {10}118:T|a + 6 * 4 + 10 {1}7:T
263. {1}3:F {0 {1}2}14:T|b - 2 <D {10}119:T|a + 6 * 4 + 11 {1}7:T
264. {1}3:F {0 {1}2}13:T|b - 3 0T1T <C 0T {10}119:T|a + 6 * 4 + 11 {1}7:T
265. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T B> 0T {10}119:T|a + 6 * 4 + 11 {1}7:T
266. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T 1T C> {10}119:T|a + 6 * 4 + 11 {1}7:T
267. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T 1T0T B> 0T {10}118:T|a + 6 * 4 + 10 {1}7:T
268. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T 1T0T1T C> {10}118:T|a + 6 * 4 + 10 {1}7:T
xmod: 1
xvar_min: a + 6 * 4 + 8 val=-7 remaining exponent: 1 part_down=1
xmod taken from proof:
269. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}2:T B> 0T {10}117:T|a + 6 * 4 + 9 {1}7:T proof used (15)
270. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}118:T|a + 6 * 4 + 10 B> 0T {10}1:T {1}7:T
271. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}118:T|a + 6 * 4 + 10 1T C> {10}1:T {1}7:T
272. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}119:T|a + 6 * 4 + 11 B> 0T {1}7:T
273. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}119:T|a + 6 * 4 + 11 1T C> {1}7:T
274. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 B> {1}6:T
275. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 1T F> {1}5:T
276. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T C> {1}4:T
277. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T 0T B> {1}3:T
278. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T 0T1T F> {1}2:T
279. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T 0T {1}2:T C> 1T
280. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {{1}2 0}2:T B>
281. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {{1}2 0}2:T 1T C>
282. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {{1}2 0}2:T 1T <D 1T
283. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {{1}2 0}2:T <C 0T1T
284. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T 0T {1}2:T <D 1T0T1T
285. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T 0T1T <C {01}2:T
286. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T B> {01}2:T
287. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T 1T C> 1T0T1T
288. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T 1T0T B> 0T1T
289. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T 1T0T1T C> 1T
290. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T {10}2:T B>
291. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T {10}2:T 1T C>
292. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T {10}2:T 1T <D 1T
293. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T {10}2:T <C 0T1T
294. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T 1T0T1T <D 1T0T1T
295. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T 1T0T <C {01}2:T
296. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T 1T <D 1T {01}2:T
297. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T {0}2:T <C {01}3:T
298. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T 0T <D 1T {01}3:T
299. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T E> 1T {01}3:T
300. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T 0T D> {01}3:T
301. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T 0T1T E> 1T {01}2:T
302. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T 0T1T0T D> {01}2:T
303. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}2:T E> 1T0T1T
304. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}2:T 0T D> 0T1T
305. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}3:T E> 1T
306. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}3:T 0T D>
307. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}4:T E>
308. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}4:T <A 1T
309. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}3:T 0T <E {1}2:T proof used (3)
310. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}1:T 0T <E {1}6:T
311. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T {01}1:T <A {1}7:T
312. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T 0T <E {1}8:T
313. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}3:T <A {1}9:T
314. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 {1}2:T <E {1}10:T
315. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}121:T|a + 6 * 4 + 13 D> {1}10:T
316. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}121:T|a + 6 * 4 + 13 <C 0T {1}9:T
317. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 1T <D 1T0T {1}9:T
318. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}120:T|a + 6 * 4 + 12 <C 0T1T0T {1}9:T
xmod: 1
xvar_min: a + 6 * 4 + 10 val=-8 remaining exponent: 1 part_down=1
xmod taken from proof:
319. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}119:T|a + 6 * 4 + 11 1T <D {10}2:T {1}9:T proof used (16)
320. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}1:T 1T <D {10}120:T|a + 6 * 4 + 12 {1}9:T
321. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T {10}1:T <C 0T {10}120:T|a + 6 * 4 + 12 {1}9:T
322. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T 1T <D {10}121:T|a + 6 * 4 + 13 {1}9:T
323. {1}3:F {0 {1}2}13:T|b - 3 {0}2:T <C 0T {10}121:T|a + 6 * 4 + 13 {1}9:T
324. {1}3:F {0 {1}2}13:T|b - 3 0T <D {10}122:T|a + 6 * 4 + 14 {1}9:T
325. {1}3:F {0 {1}2}13:T|b - 3 1T E> {10}122:T|a + 6 * 4 + 14 {1}9:T
326. {1}3:F {0 {1}2}13:T|b - 3 1T0T D> 0T {10}121:T|a + 6 * 4 + 13 {1}9:T
327. {1}3:F {0 {1}2}13:T|b - 3 1T0T1T E> {10}121:T|a + 6 * 4 + 13 {1}9:T
xmod: 1
xvar_min: a + 6 * 4 + 11 val=-8 remaining exponent: 1 part_down=1
xmod taken from proof:
328. {1}3:F {0 {1}2}13:T|b - 3 {10}2:T D> 0T {10}120:T|a + 6 * 4 + 12 {1}9:T proof used (17)
329. {1}3:F {0 {1}2}13:T|b - 3 {10}121:T|a + 6 * 4 + 13 D> 0T {10}1:T {1}9:T
XSTEPS: 309 =
STEPS: 4621
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 6 * 4 + 13...
linearity KO
minimum a + -1 => 2
2. variable = b - 3...
linearity OK
minimum b - 3 => 4
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #19
1264. {10}2 B> 0 {10}34126 {1}9
1266. {10}3 B> 0 {10}34125 {1}9
0. {10}2:F|a B> 0F {10}34126:F|b {1}9:F
1. {10}2:F|a 1T C> {10}34126:F|b {1}9:F
2. {10}3:T|a + 1 B> 0T {10}34125:T|b - 1 {1}9:F
XSTEPS: 2 =
STEPS: 2
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 1...
linearity OK
minimum --
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
proved - normal proof