Theorem: SatStress.t6
Proof state before:
x : Bool
x✝⁶³ : x = true
x1 x0 : Bool
x✝⁶² : (x0 && x1) = x
x11 x10 : Bool
x✝⁶¹ : (x10 && x11) = x1
x111 x110 : Bool
x✝⁶⁰ : (x110 && x111) = x11
x1111 x1110 : Bool
x✝⁵⁹ : (x1110 && x1111) = x111
x11111 x11110 : Bool
x✝⁵⁸ : (x11110 && x11111) = x1111
x111111 x111110 : Bool
x✝⁵⁷ : (x111110 && x111111) = x11111
x111101 x111100 : Bool
x✝⁵⁶ : (x111100 && x111101) = x11110
x11101 x11100 : Bool
x✝⁵⁵ : (x11100 && x11101) = x1110
x111011 x111010 : Bool
x✝⁵⁴ : (x111010 && x111011) = x11101
x111001 x111000 : Bool
x✝⁵³ : (x111000 && x111001) = x11100
x1101 x1100 : Bool
x✝⁵² : (x1100 && x1101) = x110
x11011 x11010 : Bool
x✝⁵¹ : (x11010 && x11011) = x1101
x110111 x110110 : Bool
x✝⁵⁰ : (x110110 && x110111) = x11011
x110101 x110100 : Bool
x✝⁴⁹ : (x110100 && x110101) = x11010
x11001 x11000 : Bool
x✝⁴⁸ : (x11000 && x11001) = x1100
x110011 x110010 : Bool
x✝⁴⁷ : (x110010 && x110011) = x11001
x110001 x110000 : Bool
x✝⁴⁶ : (x110000 && x110001) = x11000
x101 x100 : Bool
x✝⁴⁵ : (x100 && x101) = x10
x1011 x1010 : Bool
x✝⁴⁴ : (x1010 && x1011) = x101
x10111 x10110 : Bool
x✝⁴³ : (x10110 && x10111) = x1011
x101111 x101110 : Bool
x✝⁴² : (x101110 && x101111) = x10111
x101101 x101100 : Bool
x✝⁴¹ : (x101100 && x101101) = x10110
x10101 x10100 : Bool
x✝⁴⁰ : (x10100 && x10101) = x1010
x101011 x101010 : Bool
x✝³⁹ : (x101010 && x101011) = x10101
x101001 x101000 : Bool
x✝³⁸ : (x101000 && x101001) = x10100
x1001 x1000 : Bool
x✝³⁷ : (x1000 && x1001) = x100
x10011 x10010 : Bool
x✝³⁶ : (x10010 && x10011) = x1001
x100111 x100110 : Bool
x✝³⁵ : (x100110 && x100111) = x10011
x100101 x100100 : Bool
x✝³⁴ : (x100100 && x100101) = x10010
x10001 x10000 : Bool
x✝³³ : (x10000 && x10001) = x1000
x100011 x100010 : Bool
x✝³² : (x100010 && x100011) = x10001
x100001 x100000 : Bool
x✝³¹ : (x100000 && x100001) = x10000
x01 x00 : Bool
x✝³⁰ : (x00 && x01) = x0
x011 x010 : Bool
x✝²⁹ : (x010 && x011) = x01
x0111 x0110 : Bool
x✝²⁸ : (x0110 && x0111) = x011
x01111 x01110 : Bool
x✝²⁷ : (x01110 && x01111) = x0111
x011111 x011110 : Bool
x✝²⁶ : (x011110 && x011111) = x01111
x011101 x011100 : Bool
x✝²⁵ : (x011100 && x011101) = x01110
x01101 x01100 : Bool
x✝²⁴ : (x01100 && x01101) = x0110
x011011 x011010 : Bool
x✝²³ : (x011010 && x011011) = x01101
x011001 x011000 : Bool
x✝²² : (x011000 && x011001) = x01100
x0101 x0100 : Bool
x✝²¹ : (x0100 && x0101) = x010
x01011 x01010 : Bool
x✝²⁰ : (x01010 && x01011) = x0101
x010111 x010110 : Bool
x✝¹⁹ : (x010110 && x010111) = x01011
x010101 x010100 : Bool
x✝¹⁸ : (x010100 && x010101) = x01010
x01001 x01000 : Bool
x✝¹⁷ : (x01000 && x01001) = x0100
x010011 x010010 : Bool
x✝¹⁶ : (x010010 && x010011) = x01001
x010001 x010000 : Bool
x✝¹⁵ : (x010000 && x010001) = x01000
x001 x000 : Bool
x✝¹⁴ : (x000 && x001) = x00
x0011 x0010 : Bool
x✝¹³ : (x0010 && x0011) = x001
x00111 x00110 : Bool
x✝¹² : (x00110 && x00111) = x0011
x001111 x001110 : Bool
x✝¹¹ : (x001110 && x001111) = x00111
x001101 x001100 : Bool
x✝¹⁰ : (x001100 && x001101) = x00110
x00101 x00100 : Bool
x✝⁹ : (x00100 && x00101) = x0010
x001011 x001010 : Bool
x✝⁸ : (x001010 && x001011) = x00101
x001001 x001000 : Bool
x✝⁷ : (x001000 && x001001) = x00100
x0001 x0000 : Bool
x✝⁶ : (x0000 && x0001) = x000
x00011 x00010 : Bool
x✝⁵ : (x00010 && x00011) = x0001
x000111 x000110 : Bool
x✝⁴ : (x000110 && x000111) = x00011
x000101 x000100 : Bool
x✝³ : (x000100 && x000101) = x00010
x00001 x00000 : Bool
x✝² : (x00000 && x00001) = x0000
x000011 x000010 : Bool
x✝¹ : (x000010 && x000011) = x00001
x000001 x000000 : Bool
x✝ : (x000000 && x000001) = x00000
⊢ x000000 = true
Tactic:
bv_decide
Proof state after:
no goals