blob: 5bcd22759705f5d4bf942725fa16f40dc78e2fec (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
1:(input ((not #1:(= a a))))
2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a) #9:(bitof 2 a)])))
3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8) #10:(= #9 #9)))) 2 2)
4:(equiv2 (#1 (not #4)) 3)
5:(resolution ((not #4)) 1 4)
6:(not_and ((not #5) (not #6) (not #10)) 5)
7:(equiv_neg1 (#5 (not #7)))
8:(equiv_neg2 (#5 #7))
9:(resolution ((not #6) (not #10)) 7 8 6)
10:(equiv_neg1 (#6 (not #8)))
11:(equiv_neg2 (#6 #8))
12:(resolution ((not #10)) 10 11 9)
13:(equiv_neg1 (#10 (not #9)))
14:(equiv_neg2 (#10 #9))
15:(resolution () 13 14 12)
|
