-
-
Save nikotan/5876743852414602ed19d854dc16f77f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(int hr_0_0 0 1) | |
(int hl_0_0 0 1) | |
(<= (+ hr_0_0 hl_0_0) 1) | |
(int hr_1_0 0 1) | |
(int hl_1_0 0 1) | |
(<= (+ hr_1_0 hl_1_0) 1) | |
(int hr_2_0 0 1) | |
(int hl_2_0 0 1) | |
(<= (+ hr_2_0 hl_2_0) 1) | |
(int hr_3_0 0 1) | |
(int hl_3_0 0 1) | |
(<= (+ hr_3_0 hl_3_0) 1) | |
(int hr_4_0 0 1) | |
(int hl_4_0 0 1) | |
(<= (+ hr_4_0 hl_4_0) 1) | |
(int hr_0_1 0 1) | |
(int hl_0_1 0 1) | |
(<= (+ hr_0_1 hl_0_1) 1) | |
(int hr_1_1 0 1) | |
(int hl_1_1 0 1) | |
(<= (+ hr_1_1 hl_1_1) 1) | |
(int hr_2_1 0 1) | |
(int hl_2_1 0 1) | |
(<= (+ hr_2_1 hl_2_1) 1) | |
(int hr_3_1 0 1) | |
(int hl_3_1 0 1) | |
(<= (+ hr_3_1 hl_3_1) 1) | |
(int hr_4_1 0 1) | |
(int hl_4_1 0 1) | |
(<= (+ hr_4_1 hl_4_1) 1) | |
(int hr_0_2 0 1) | |
(int hl_0_2 0 1) | |
(<= (+ hr_0_2 hl_0_2) 1) | |
(int hr_1_2 0 1) | |
(int hl_1_2 0 1) | |
(<= (+ hr_1_2 hl_1_2) 1) | |
(int hr_2_2 0 1) | |
(int hl_2_2 0 1) | |
(<= (+ hr_2_2 hl_2_2) 1) | |
(int hr_3_2 0 1) | |
(int hl_3_2 0 1) | |
(<= (+ hr_3_2 hl_3_2) 1) | |
(int hr_4_2 0 1) | |
(int hl_4_2 0 1) | |
(<= (+ hr_4_2 hl_4_2) 1) | |
(int hr_0_3 0 1) | |
(int hl_0_3 0 1) | |
(<= (+ hr_0_3 hl_0_3) 1) | |
(int hr_1_3 0 1) | |
(int hl_1_3 0 1) | |
(<= (+ hr_1_3 hl_1_3) 1) | |
(int hr_2_3 0 1) | |
(int hl_2_3 0 1) | |
(<= (+ hr_2_3 hl_2_3) 1) | |
(int hr_3_3 0 1) | |
(int hl_3_3 0 1) | |
(<= (+ hr_3_3 hl_3_3) 1) | |
(int hr_4_3 0 1) | |
(int hl_4_3 0 1) | |
(<= (+ hr_4_3 hl_4_3) 1) | |
(int hr_0_4 0 1) | |
(int hl_0_4 0 1) | |
(<= (+ hr_0_4 hl_0_4) 1) | |
(int hr_1_4 0 1) | |
(int hl_1_4 0 1) | |
(<= (+ hr_1_4 hl_1_4) 1) | |
(int hr_2_4 0 1) | |
(int hl_2_4 0 1) | |
(<= (+ hr_2_4 hl_2_4) 1) | |
(int hr_3_4 0 1) | |
(int hl_3_4 0 1) | |
(<= (+ hr_3_4 hl_3_4) 1) | |
(int hr_4_4 0 1) | |
(int hl_4_4 0 1) | |
(<= (+ hr_4_4 hl_4_4) 1) | |
(int hr_0_5 0 1) | |
(int hl_0_5 0 1) | |
(<= (+ hr_0_5 hl_0_5) 1) | |
(int hr_1_5 0 1) | |
(int hl_1_5 0 1) | |
(<= (+ hr_1_5 hl_1_5) 1) | |
(int hr_2_5 0 1) | |
(int hl_2_5 0 1) | |
(<= (+ hr_2_5 hl_2_5) 1) | |
(int hr_3_5 0 1) | |
(int hl_3_5 0 1) | |
(<= (+ hr_3_5 hl_3_5) 1) | |
(int hr_4_5 0 1) | |
(int hl_4_5 0 1) | |
(<= (+ hr_4_5 hl_4_5) 1) | |
(int vu_0_0 0 1) | |
(int vd_0_0 0 1) | |
(<= (+ vu_0_0 vd_0_0) 1) | |
(int vu_1_0 0 1) | |
(int vd_1_0 0 1) | |
(<= (+ vu_1_0 vd_1_0) 1) | |
(int vu_2_0 0 1) | |
(int vd_2_0 0 1) | |
(<= (+ vu_2_0 vd_2_0) 1) | |
(int vu_3_0 0 1) | |
(int vd_3_0 0 1) | |
(<= (+ vu_3_0 vd_3_0) 1) | |
(int vu_4_0 0 1) | |
(int vd_4_0 0 1) | |
(<= (+ vu_4_0 vd_4_0) 1) | |
(int vu_5_0 0 1) | |
(int vd_5_0 0 1) | |
(<= (+ vu_5_0 vd_5_0) 1) | |
(int vu_0_1 0 1) | |
(int vd_0_1 0 1) | |
(<= (+ vu_0_1 vd_0_1) 1) | |
(int vu_1_1 0 1) | |
(int vd_1_1 0 1) | |
(<= (+ vu_1_1 vd_1_1) 1) | |
(int vu_2_1 0 1) | |
(int vd_2_1 0 1) | |
(<= (+ vu_2_1 vd_2_1) 1) | |
(int vu_3_1 0 1) | |
(int vd_3_1 0 1) | |
(<= (+ vu_3_1 vd_3_1) 1) | |
(int vu_4_1 0 1) | |
(int vd_4_1 0 1) | |
(<= (+ vu_4_1 vd_4_1) 1) | |
(int vu_5_1 0 1) | |
(int vd_5_1 0 1) | |
(<= (+ vu_5_1 vd_5_1) 1) | |
(int vu_0_2 0 1) | |
(int vd_0_2 0 1) | |
(<= (+ vu_0_2 vd_0_2) 1) | |
(int vu_1_2 0 1) | |
(int vd_1_2 0 1) | |
(<= (+ vu_1_2 vd_1_2) 1) | |
(int vu_2_2 0 1) | |
(int vd_2_2 0 1) | |
(<= (+ vu_2_2 vd_2_2) 1) | |
(int vu_3_2 0 1) | |
(int vd_3_2 0 1) | |
(<= (+ vu_3_2 vd_3_2) 1) | |
(int vu_4_2 0 1) | |
(int vd_4_2 0 1) | |
(<= (+ vu_4_2 vd_4_2) 1) | |
(int vu_5_2 0 1) | |
(int vd_5_2 0 1) | |
(<= (+ vu_5_2 vd_5_2) 1) | |
(int vu_0_3 0 1) | |
(int vd_0_3 0 1) | |
(<= (+ vu_0_3 vd_0_3) 1) | |
(int vu_1_3 0 1) | |
(int vd_1_3 0 1) | |
(<= (+ vu_1_3 vd_1_3) 1) | |
(int vu_2_3 0 1) | |
(int vd_2_3 0 1) | |
(<= (+ vu_2_3 vd_2_3) 1) | |
(int vu_3_3 0 1) | |
(int vd_3_3 0 1) | |
(<= (+ vu_3_3 vd_3_3) 1) | |
(int vu_4_3 0 1) | |
(int vd_4_3 0 1) | |
(<= (+ vu_4_3 vd_4_3) 1) | |
(int vu_5_3 0 1) | |
(int vd_5_3 0 1) | |
(<= (+ vu_5_3 vd_5_3) 1) | |
(int vu_0_4 0 1) | |
(int vd_0_4 0 1) | |
(<= (+ vu_0_4 vd_0_4) 1) | |
(int vu_1_4 0 1) | |
(int vd_1_4 0 1) | |
(<= (+ vu_1_4 vd_1_4) 1) | |
(int vu_2_4 0 1) | |
(int vd_2_4 0 1) | |
(<= (+ vu_2_4 vd_2_4) 1) | |
(int vu_3_4 0 1) | |
(int vd_3_4 0 1) | |
(<= (+ vu_3_4 vd_3_4) 1) | |
(int vu_4_4 0 1) | |
(int vd_4_4 0 1) | |
(<= (+ vu_4_4 vd_4_4) 1) | |
(int vu_5_4 0 1) | |
(int vd_5_4 0 1) | |
(<= (+ vu_5_4 vd_5_4) 1) | |
(int di_0_0 0 1) | |
(int do_0_0 0 1) | |
(= di_0_0 (+ hl_0_0 vu_0_0)) | |
(= do_0_0 (+ hr_0_0 vd_0_0)) | |
(int o_0_0 -1 36) | |
(int di_1_0 0 1) | |
(int do_1_0 0 1) | |
(= di_1_0 (+ hr_0_0 hl_1_0 vu_1_0)) | |
(= do_1_0 (+ hl_0_0 hr_1_0 vd_1_0)) | |
(int o_1_0 -1 36) | |
(int di_2_0 0 1) | |
(int do_2_0 0 1) | |
(= di_2_0 (+ hr_1_0 hl_2_0 vu_2_0)) | |
(= do_2_0 (+ hl_1_0 hr_2_0 vd_2_0)) | |
(int o_2_0 -1 36) | |
(int di_3_0 0 1) | |
(int do_3_0 0 1) | |
(= di_3_0 (+ hr_2_0 hl_3_0 vu_3_0)) | |
(= do_3_0 (+ hl_2_0 hr_3_0 vd_3_0)) | |
(int o_3_0 -1 36) | |
(int di_4_0 0 1) | |
(int do_4_0 0 1) | |
(= di_4_0 (+ hr_3_0 hl_4_0 vu_4_0)) | |
(= do_4_0 (+ hl_3_0 hr_4_0 vd_4_0)) | |
(int o_4_0 -1 36) | |
(int di_5_0 0 1) | |
(int do_5_0 0 1) | |
(= di_5_0 (+ hr_4_0 vu_5_0)) | |
(= do_5_0 (+ hl_4_0 vd_5_0)) | |
(int o_5_0 -1 36) | |
(int di_0_1 0 1) | |
(int do_0_1 0 1) | |
(= di_0_1 (+ hl_0_1 vd_0_0 vu_0_1)) | |
(= do_0_1 (+ hr_0_1 vu_0_0 vd_0_1)) | |
(int o_0_1 -1 36) | |
(int di_1_1 0 1) | |
(int do_1_1 0 1) | |
(= di_1_1 (+ hr_0_1 hl_1_1 vd_1_0 vu_1_1)) | |
(= do_1_1 (+ hl_0_1 hr_1_1 vu_1_0 vd_1_1)) | |
(int o_1_1 -1 36) | |
(int di_2_1 0 1) | |
(int do_2_1 0 1) | |
(= di_2_1 (+ hr_1_1 hl_2_1 vd_2_0 vu_2_1)) | |
(= do_2_1 (+ hl_1_1 hr_2_1 vu_2_0 vd_2_1)) | |
(int o_2_1 -1 36) | |
(int di_3_1 0 1) | |
(int do_3_1 0 1) | |
(= di_3_1 (+ hr_2_1 hl_3_1 vd_3_0 vu_3_1)) | |
(= do_3_1 (+ hl_2_1 hr_3_1 vu_3_0 vd_3_1)) | |
(int o_3_1 -1 36) | |
(int di_4_1 0 1) | |
(int do_4_1 0 1) | |
(= di_4_1 (+ hr_3_1 hl_4_1 vd_4_0 vu_4_1)) | |
(= do_4_1 (+ hl_3_1 hr_4_1 vu_4_0 vd_4_1)) | |
(int o_4_1 -1 36) | |
(int di_5_1 0 1) | |
(int do_5_1 0 1) | |
(= di_5_1 (+ hr_4_1 vd_5_0 vu_5_1)) | |
(= do_5_1 (+ hl_4_1 vu_5_0 vd_5_1)) | |
(int o_5_1 -1 36) | |
(int di_0_2 0 1) | |
(int do_0_2 0 1) | |
(= di_0_2 (+ hl_0_2 vd_0_1 vu_0_2)) | |
(= do_0_2 (+ hr_0_2 vu_0_1 vd_0_2)) | |
(int o_0_2 -1 36) | |
(int di_1_2 0 1) | |
(int do_1_2 0 1) | |
(= di_1_2 (+ hr_0_2 hl_1_2 vd_1_1 vu_1_2)) | |
(= do_1_2 (+ hl_0_2 hr_1_2 vu_1_1 vd_1_2)) | |
(int o_1_2 -1 36) | |
(int di_2_2 0 1) | |
(int do_2_2 0 1) | |
(= di_2_2 (+ hr_1_2 hl_2_2 vd_2_1 vu_2_2)) | |
(= do_2_2 (+ hl_1_2 hr_2_2 vu_2_1 vd_2_2)) | |
(int o_2_2 -1 36) | |
(int di_3_2 0 1) | |
(int do_3_2 0 1) | |
(= di_3_2 (+ hr_2_2 hl_3_2 vd_3_1 vu_3_2)) | |
(= do_3_2 (+ hl_2_2 hr_3_2 vu_3_1 vd_3_2)) | |
(int o_3_2 -1 36) | |
(int di_4_2 0 1) | |
(int do_4_2 0 1) | |
(= di_4_2 (+ hr_3_2 hl_4_2 vd_4_1 vu_4_2)) | |
(= do_4_2 (+ hl_3_2 hr_4_2 vu_4_1 vd_4_2)) | |
(int o_4_2 -1 36) | |
(int di_5_2 0 1) | |
(int do_5_2 0 1) | |
(= di_5_2 (+ hr_4_2 vd_5_1 vu_5_2)) | |
(= do_5_2 (+ hl_4_2 vu_5_1 vd_5_2)) | |
(int o_5_2 -1 36) | |
(int di_0_3 0 1) | |
(int do_0_3 0 1) | |
(= di_0_3 (+ hl_0_3 vd_0_2 vu_0_3)) | |
(= do_0_3 (+ hr_0_3 vu_0_2 vd_0_3)) | |
(int o_0_3 -1 36) | |
(int di_1_3 0 1) | |
(int do_1_3 0 1) | |
(= di_1_3 (+ hr_0_3 hl_1_3 vd_1_2 vu_1_3)) | |
(= do_1_3 (+ hl_0_3 hr_1_3 vu_1_2 vd_1_3)) | |
(int o_1_3 -1 36) | |
(int di_2_3 0 1) | |
(int do_2_3 0 1) | |
(= di_2_3 (+ hr_1_3 hl_2_3 vd_2_2 vu_2_3)) | |
(= do_2_3 (+ hl_1_3 hr_2_3 vu_2_2 vd_2_3)) | |
(int o_2_3 -1 36) | |
(int di_3_3 0 1) | |
(int do_3_3 0 1) | |
(= di_3_3 (+ hr_2_3 hl_3_3 vd_3_2 vu_3_3)) | |
(= do_3_3 (+ hl_2_3 hr_3_3 vu_3_2 vd_3_3)) | |
(int o_3_3 -1 36) | |
(int di_4_3 0 1) | |
(int do_4_3 0 1) | |
(= di_4_3 (+ hr_3_3 hl_4_3 vd_4_2 vu_4_3)) | |
(= do_4_3 (+ hl_3_3 hr_4_3 vu_4_2 vd_4_3)) | |
(int o_4_3 -1 36) | |
(int di_5_3 0 1) | |
(int do_5_3 0 1) | |
(= di_5_3 (+ hr_4_3 vd_5_2 vu_5_3)) | |
(= do_5_3 (+ hl_4_3 vu_5_2 vd_5_3)) | |
(int o_5_3 -1 36) | |
(int di_0_4 0 1) | |
(int do_0_4 0 1) | |
(= di_0_4 (+ hl_0_4 vd_0_3 vu_0_4)) | |
(= do_0_4 (+ hr_0_4 vu_0_3 vd_0_4)) | |
(int o_0_4 -1 36) | |
(int di_1_4 0 1) | |
(int do_1_4 0 1) | |
(= di_1_4 (+ hr_0_4 hl_1_4 vd_1_3 vu_1_4)) | |
(= do_1_4 (+ hl_0_4 hr_1_4 vu_1_3 vd_1_4)) | |
(int o_1_4 -1 36) | |
(int di_2_4 0 1) | |
(int do_2_4 0 1) | |
(= di_2_4 (+ hr_1_4 hl_2_4 vd_2_3 vu_2_4)) | |
(= do_2_4 (+ hl_1_4 hr_2_4 vu_2_3 vd_2_4)) | |
(int o_2_4 -1 36) | |
(int di_3_4 0 1) | |
(int do_3_4 0 1) | |
(= di_3_4 (+ hr_2_4 hl_3_4 vd_3_3 vu_3_4)) | |
(= do_3_4 (+ hl_2_4 hr_3_4 vu_3_3 vd_3_4)) | |
(int o_3_4 -1 36) | |
(int di_4_4 0 1) | |
(int do_4_4 0 1) | |
(= di_4_4 (+ hr_3_4 hl_4_4 vd_4_3 vu_4_4)) | |
(= do_4_4 (+ hl_3_4 hr_4_4 vu_4_3 vd_4_4)) | |
(int o_4_4 -1 36) | |
(int di_5_4 0 1) | |
(int do_5_4 0 1) | |
(= di_5_4 (+ hr_4_4 vd_5_3 vu_5_4)) | |
(= do_5_4 (+ hl_4_4 vu_5_3 vd_5_4)) | |
(int o_5_4 -1 36) | |
(int di_0_5 0 1) | |
(int do_0_5 0 1) | |
(= di_0_5 (+ hl_0_5 vd_0_4)) | |
(= do_0_5 (+ hr_0_5 vu_0_4)) | |
(int o_0_5 -1 36) | |
(int di_1_5 0 1) | |
(int do_1_5 0 1) | |
(= di_1_5 (+ hr_0_5 hl_1_5 vd_1_4)) | |
(= do_1_5 (+ hl_0_5 hr_1_5 vu_1_4)) | |
(int o_1_5 -1 36) | |
(int di_2_5 0 1) | |
(int do_2_5 0 1) | |
(= di_2_5 (+ hr_1_5 hl_2_5 vd_2_4)) | |
(= do_2_5 (+ hl_1_5 hr_2_5 vu_2_4)) | |
(int o_2_5 -1 36) | |
(int di_3_5 0 1) | |
(int do_3_5 0 1) | |
(= di_3_5 (+ hr_2_5 hl_3_5 vd_3_4)) | |
(= do_3_5 (+ hl_2_5 hr_3_5 vu_3_4)) | |
(int o_3_5 -1 36) | |
(int di_4_5 0 1) | |
(int do_4_5 0 1) | |
(= di_4_5 (+ hr_3_5 hl_4_5 vd_4_4)) | |
(= do_4_5 (+ hl_3_5 hr_4_5 vu_4_4)) | |
(int o_4_5 -1 36) | |
(int di_5_5 0 1) | |
(int do_5_5 0 1) | |
(= di_5_5 (+ hr_4_5 vd_5_4)) | |
(= do_5_5 (+ hl_4_5 vu_5_4)) | |
(int o_5_5 -1 36) | |
(domain number (0 2 1)) | |
(= di_0_0 do_0_0) | |
(int x_0_0 number) | |
(int i_0_0 0) | |
(=> (= x_0_0 0) (= di_0_0 0)) | |
(=> (= x_0_0 0) (= do_0_0 0)) | |
(=> (= x_0_0 0) (= o_0_0 -1)) | |
(= di_1_0 do_1_0) | |
(int x_1_0 number) | |
(int i_1_0 0) | |
(=> (= x_1_0 0) (= di_1_0 0)) | |
(=> (= x_1_0 0) (= do_1_0 0)) | |
(=> (= x_1_0 0) (= o_1_0 -1)) | |
(= di_2_0 do_2_0) | |
(int x_2_0 number) | |
(int i_2_0 0) | |
(=> (= x_2_0 0) (= di_2_0 0)) | |
(=> (= x_2_0 0) (= do_2_0 0)) | |
(=> (= x_2_0 0) (= o_2_0 -1)) | |
(= di_3_0 do_3_0) | |
(int x_3_0 number) | |
(int i_3_0 0) | |
(=> (= x_3_0 0) (= di_3_0 0)) | |
(=> (= x_3_0 0) (= do_3_0 0)) | |
(=> (= x_3_0 0) (= o_3_0 -1)) | |
(= di_4_0 do_4_0) | |
(int x_4_0 number) | |
(int i_4_0 0) | |
(=> (= x_4_0 0) (= di_4_0 0)) | |
(=> (= x_4_0 0) (= do_4_0 0)) | |
(=> (= x_4_0 0) (= o_4_0 -1)) | |
(= di_5_0 do_5_0) | |
(int x_5_0 number) | |
(int i_5_0 0) | |
(=> (= x_5_0 0) (= di_5_0 0)) | |
(=> (= x_5_0 0) (= do_5_0 0)) | |
(=> (= x_5_0 0) (= o_5_0 -1)) | |
(= di_0_1 do_0_1) | |
(int x_0_1 number) | |
(int i_0_1 0) | |
(=> (= x_0_1 0) (= di_0_1 0)) | |
(=> (= x_0_1 0) (= do_0_1 0)) | |
(=> (= x_0_1 0) (= o_0_1 -1)) | |
(= di_2_1 do_2_1) | |
(int x_2_1 number) | |
(int i_2_1 0) | |
(=> (= x_2_1 0) (= di_2_1 0)) | |
(=> (= x_2_1 0) (= do_2_1 0)) | |
(=> (= x_2_1 0) (= o_2_1 -1)) | |
(= di_3_1 do_3_1) | |
(int x_3_1 number) | |
(int i_3_1 0) | |
(=> (= x_3_1 0) (= di_3_1 0)) | |
(=> (= x_3_1 0) (= do_3_1 0)) | |
(=> (= x_3_1 0) (= o_3_1 -1)) | |
(= di_4_1 do_4_1) | |
(int x_4_1 number) | |
(int i_4_1 0) | |
(=> (= x_4_1 0) (= di_4_1 0)) | |
(=> (= x_4_1 0) (= do_4_1 0)) | |
(=> (= x_4_1 0) (= o_4_1 -1)) | |
(= di_5_1 do_5_1) | |
(int x_5_1 number) | |
(int i_5_1 0) | |
(=> (= x_5_1 0) (= di_5_1 0)) | |
(=> (= x_5_1 0) (= do_5_1 0)) | |
(=> (= x_5_1 0) (= o_5_1 -1)) | |
(= di_0_2 do_0_2) | |
(int x_0_2 number) | |
(int i_0_2 0) | |
(=> (= x_0_2 0) (= di_0_2 0)) | |
(=> (= x_0_2 0) (= do_0_2 0)) | |
(=> (= x_0_2 0) (= o_0_2 -1)) | |
(= di_2_2 do_2_2) | |
(int x_2_2 number) | |
(int i_2_2 0) | |
(=> (= x_2_2 0) (= di_2_2 0)) | |
(=> (= x_2_2 0) (= do_2_2 0)) | |
(=> (= x_2_2 0) (= o_2_2 -1)) | |
(= di_3_2 do_3_2) | |
(int x_3_2 number) | |
(int i_3_2 0) | |
(=> (= x_3_2 0) (= di_3_2 0)) | |
(=> (= x_3_2 0) (= do_3_2 0)) | |
(=> (= x_3_2 0) (= o_3_2 -1)) | |
(= di_4_2 do_4_2) | |
(int x_4_2 number) | |
(int i_4_2 0) | |
(=> (= x_4_2 0) (= di_4_2 0)) | |
(=> (= x_4_2 0) (= do_4_2 0)) | |
(=> (= x_4_2 0) (= o_4_2 -1)) | |
(= di_5_2 do_5_2) | |
(int x_5_2 number) | |
(int i_5_2 0) | |
(=> (= x_5_2 0) (= di_5_2 0)) | |
(=> (= x_5_2 0) (= do_5_2 0)) | |
(=> (= x_5_2 0) (= o_5_2 -1)) | |
(= di_1_3 do_1_3) | |
(int x_1_3 number) | |
(int i_1_3 0) | |
(=> (= x_1_3 0) (= di_1_3 0)) | |
(=> (= x_1_3 0) (= do_1_3 0)) | |
(=> (= x_1_3 0) (= o_1_3 -1)) | |
(= di_3_3 do_3_3) | |
(int x_3_3 number) | |
(int i_3_3 0) | |
(=> (= x_3_3 0) (= di_3_3 0)) | |
(=> (= x_3_3 0) (= do_3_3 0)) | |
(=> (= x_3_3 0) (= o_3_3 -1)) | |
(= di_4_3 do_4_3) | |
(int x_4_3 number) | |
(int i_4_3 0) | |
(=> (= x_4_3 0) (= di_4_3 0)) | |
(=> (= x_4_3 0) (= do_4_3 0)) | |
(=> (= x_4_3 0) (= o_4_3 -1)) | |
(= di_0_4 do_0_4) | |
(int x_0_4 number) | |
(int i_0_4 0) | |
(=> (= x_0_4 0) (= di_0_4 0)) | |
(=> (= x_0_4 0) (= do_0_4 0)) | |
(=> (= x_0_4 0) (= o_0_4 -1)) | |
(= di_1_4 do_1_4) | |
(int x_1_4 number) | |
(int i_1_4 0) | |
(=> (= x_1_4 0) (= di_1_4 0)) | |
(=> (= x_1_4 0) (= do_1_4 0)) | |
(=> (= x_1_4 0) (= o_1_4 -1)) | |
(= di_5_4 do_5_4) | |
(int x_5_4 number) | |
(int i_5_4 0) | |
(=> (= x_5_4 0) (= di_5_4 0)) | |
(=> (= x_5_4 0) (= do_5_4 0)) | |
(=> (= x_5_4 0) (= o_5_4 -1)) | |
(= di_1_5 do_1_5) | |
(int x_1_5 number) | |
(int i_1_5 0) | |
(=> (= x_1_5 0) (= di_1_5 0)) | |
(=> (= x_1_5 0) (= do_1_5 0)) | |
(=> (= x_1_5 0) (= o_1_5 -1)) | |
(= di_2_5 do_2_5) | |
(int x_2_5 number) | |
(int i_2_5 0) | |
(=> (= x_2_5 0) (= di_2_5 0)) | |
(=> (= x_2_5 0) (= do_2_5 0)) | |
(=> (= x_2_5 0) (= o_2_5 -1)) | |
(= di_3_5 do_3_5) | |
(int x_3_5 number) | |
(int i_3_5 0) | |
(=> (= x_3_5 0) (= di_3_5 0)) | |
(=> (= x_3_5 0) (= do_3_5 0)) | |
(=> (= x_3_5 0) (= o_3_5 -1)) | |
(= di_4_5 do_4_5) | |
(int x_4_5 number) | |
(int i_4_5 0) | |
(=> (= x_4_5 0) (= di_4_5 0)) | |
(=> (= x_4_5 0) (= do_4_5 0)) | |
(=> (= x_4_5 0) (= o_4_5 -1)) | |
(int x_1_1 2) | |
(int i_1_1 2) | |
(=> (and (= di_1_1 0) (= do_1_1 1)) (= o_1_1 0)) | |
(=> (and (= di_1_1 1) (= do_1_1 0)) (= o_1_1 4)) | |
(int x_2_3 2) | |
(int i_2_3 2) | |
(=> (and (= di_2_3 0) (= do_2_3 1)) (= o_2_3 0)) | |
(=> (and (= di_2_3 1) (= do_2_3 0)) (= o_2_3 4)) | |
(int x_2_4 2) | |
(int i_2_4 2) | |
(=> (and (= di_2_4 0) (= do_2_4 1)) (= o_2_4 0)) | |
(=> (and (= di_2_4 1) (= do_2_4 0)) (= o_2_4 4)) | |
(int x_4_4 2) | |
(int i_4_4 2) | |
(=> (and (= di_4_4 0) (= do_4_4 1)) (= o_4_4 0)) | |
(=> (and (= di_4_4 1) (= do_4_4 0)) (= o_4_4 4)) | |
(int x_0_5 2) | |
(int i_0_5 2) | |
(=> (and (= di_0_5 0) (= do_0_5 1)) (= o_0_5 0)) | |
(=> (and (= di_0_5 1) (= do_0_5 0)) (= o_0_5 4)) | |
(count 0 (di_1_1 di_2_3 di_2_4 di_4_4 di_0_5) eq 1) | |
(count 0 (do_1_1 do_2_3 do_2_4 do_4_4 do_0_5) eq 1) | |
(count 1 ((+ di_1_1 do_1_1) (+ di_2_3 do_2_3) (+ di_2_4 do_2_4) (+ di_4_4 do_4_4) (+ di_0_5 do_0_5)) eq 2) | |
(int x_1_2 1) | |
(int i_1_2 1) | |
(=> (and (= di_1_2 0) (= do_1_2 1)) (= o_1_2 0)) | |
(=> (and (= di_1_2 1) (= do_1_2 0)) (= o_1_2 4)) | |
(int x_0_3 1) | |
(int i_0_3 1) | |
(=> (and (= di_0_3 0) (= do_0_3 1)) (= o_0_3 0)) | |
(=> (and (= di_0_3 1) (= do_0_3 0)) (= o_0_3 4)) | |
(int x_5_3 1) | |
(int i_5_3 1) | |
(=> (and (= di_5_3 0) (= do_5_3 1)) (= o_5_3 0)) | |
(=> (and (= di_5_3 1) (= do_5_3 0)) (= o_5_3 4)) | |
(int x_3_4 1) | |
(int i_3_4 1) | |
(=> (and (= di_3_4 0) (= do_3_4 1)) (= o_3_4 0)) | |
(=> (and (= di_3_4 1) (= do_3_4 0)) (= o_3_4 4)) | |
(int x_5_5 1) | |
(int i_5_5 1) | |
(=> (and (= di_5_5 0) (= do_5_5 1)) (= o_5_5 0)) | |
(=> (and (= di_5_5 1) (= do_5_5 0)) (= o_5_5 4)) | |
(count 0 (di_1_2 di_0_3 di_5_3 di_3_4 di_5_5) eq 1) | |
(count 0 (do_1_2 do_0_3 do_5_3 do_3_4 do_5_5) eq 1) | |
(count 1 ((+ di_1_2 do_1_2) (+ di_0_3 do_0_3) (+ di_5_3 do_5_3) (+ di_3_4 do_3_4) (+ di_5_5 do_5_5)) eq 2) | |
(=> (> hr_0_0 0) (= x_0_0 x_1_0)) | |
(=> (> hl_0_0 0) (= x_0_0 x_1_0)) | |
(=> (and (> hr_0_0 0) (= i_1_0 0)) (= o_0_0 o_1_0)) | |
(=> (and (> hl_0_0 0) (= i_0_0 0)) (= o_0_0 o_1_0)) | |
(=> (and (> hr_0_0 0) (> i_1_0 0)) (= o_1_0 (+ o_0_0 1))) | |
(=> (and (> hl_0_0 0) (> i_0_0 0)) (= o_0_0 (+ o_1_0 1))) | |
(=> (> hr_1_0 0) (= x_1_0 x_2_0)) | |
(=> (> hl_1_0 0) (= x_1_0 x_2_0)) | |
(=> (and (> hr_1_0 0) (= i_2_0 0)) (= o_1_0 o_2_0)) | |
(=> (and (> hl_1_0 0) (= i_1_0 0)) (= o_1_0 o_2_0)) | |
(=> (and (> hr_1_0 0) (> i_2_0 0)) (= o_2_0 (+ o_1_0 1))) | |
(=> (and (> hl_1_0 0) (> i_1_0 0)) (= o_1_0 (+ o_2_0 1))) | |
(=> (> hr_2_0 0) (= x_2_0 x_3_0)) | |
(=> (> hl_2_0 0) (= x_2_0 x_3_0)) | |
(=> (and (> hr_2_0 0) (= i_3_0 0)) (= o_2_0 o_3_0)) | |
(=> (and (> hl_2_0 0) (= i_2_0 0)) (= o_2_0 o_3_0)) | |
(=> (and (> hr_2_0 0) (> i_3_0 0)) (= o_3_0 (+ o_2_0 1))) | |
(=> (and (> hl_2_0 0) (> i_2_0 0)) (= o_2_0 (+ o_3_0 1))) | |
(=> (> hr_3_0 0) (= x_3_0 x_4_0)) | |
(=> (> hl_3_0 0) (= x_3_0 x_4_0)) | |
(=> (and (> hr_3_0 0) (= i_4_0 0)) (= o_3_0 o_4_0)) | |
(=> (and (> hl_3_0 0) (= i_3_0 0)) (= o_3_0 o_4_0)) | |
(=> (and (> hr_3_0 0) (> i_4_0 0)) (= o_4_0 (+ o_3_0 1))) | |
(=> (and (> hl_3_0 0) (> i_3_0 0)) (= o_3_0 (+ o_4_0 1))) | |
(=> (> hr_4_0 0) (= x_4_0 x_5_0)) | |
(=> (> hl_4_0 0) (= x_4_0 x_5_0)) | |
(=> (and (> hr_4_0 0) (= i_5_0 0)) (= o_4_0 o_5_0)) | |
(=> (and (> hl_4_0 0) (= i_4_0 0)) (= o_4_0 o_5_0)) | |
(=> (and (> hr_4_0 0) (> i_5_0 0)) (= o_5_0 (+ o_4_0 1))) | |
(=> (and (> hl_4_0 0) (> i_4_0 0)) (= o_4_0 (+ o_5_0 1))) | |
(=> (> hr_0_1 0) (= x_0_1 x_1_1)) | |
(=> (> hl_0_1 0) (= x_0_1 x_1_1)) | |
(=> (and (> hr_0_1 0) (= i_1_1 0)) (= o_0_1 o_1_1)) | |
(=> (and (> hl_0_1 0) (= i_0_1 0)) (= o_0_1 o_1_1)) | |
(=> (and (> hr_0_1 0) (> i_1_1 0)) (= o_1_1 (+ o_0_1 1))) | |
(=> (and (> hl_0_1 0) (> i_0_1 0)) (= o_0_1 (+ o_1_1 1))) | |
(=> (> hr_1_1 0) (= x_1_1 x_2_1)) | |
(=> (> hl_1_1 0) (= x_1_1 x_2_1)) | |
(=> (and (> hr_1_1 0) (= i_2_1 0)) (= o_1_1 o_2_1)) | |
(=> (and (> hl_1_1 0) (= i_1_1 0)) (= o_1_1 o_2_1)) | |
(=> (and (> hr_1_1 0) (> i_2_1 0)) (= o_2_1 (+ o_1_1 1))) | |
(=> (and (> hl_1_1 0) (> i_1_1 0)) (= o_1_1 (+ o_2_1 1))) | |
(=> (> hr_2_1 0) (= x_2_1 x_3_1)) | |
(=> (> hl_2_1 0) (= x_2_1 x_3_1)) | |
(=> (and (> hr_2_1 0) (= i_3_1 0)) (= o_2_1 o_3_1)) | |
(=> (and (> hl_2_1 0) (= i_2_1 0)) (= o_2_1 o_3_1)) | |
(=> (and (> hr_2_1 0) (> i_3_1 0)) (= o_3_1 (+ o_2_1 1))) | |
(=> (and (> hl_2_1 0) (> i_2_1 0)) (= o_2_1 (+ o_3_1 1))) | |
(=> (> hr_3_1 0) (= x_3_1 x_4_1)) | |
(=> (> hl_3_1 0) (= x_3_1 x_4_1)) | |
(=> (and (> hr_3_1 0) (= i_4_1 0)) (= o_3_1 o_4_1)) | |
(=> (and (> hl_3_1 0) (= i_3_1 0)) (= o_3_1 o_4_1)) | |
(=> (and (> hr_3_1 0) (> i_4_1 0)) (= o_4_1 (+ o_3_1 1))) | |
(=> (and (> hl_3_1 0) (> i_3_1 0)) (= o_3_1 (+ o_4_1 1))) | |
(=> (> hr_4_1 0) (= x_4_1 x_5_1)) | |
(=> (> hl_4_1 0) (= x_4_1 x_5_1)) | |
(=> (and (> hr_4_1 0) (= i_5_1 0)) (= o_4_1 o_5_1)) | |
(=> (and (> hl_4_1 0) (= i_4_1 0)) (= o_4_1 o_5_1)) | |
(=> (and (> hr_4_1 0) (> i_5_1 0)) (= o_5_1 (+ o_4_1 1))) | |
(=> (and (> hl_4_1 0) (> i_4_1 0)) (= o_4_1 (+ o_5_1 1))) | |
(=> (> hr_0_2 0) (= x_0_2 x_1_2)) | |
(=> (> hl_0_2 0) (= x_0_2 x_1_2)) | |
(=> (and (> hr_0_2 0) (= i_1_2 0)) (= o_0_2 o_1_2)) | |
(=> (and (> hl_0_2 0) (= i_0_2 0)) (= o_0_2 o_1_2)) | |
(=> (and (> hr_0_2 0) (> i_1_2 0)) (= o_1_2 (+ o_0_2 1))) | |
(=> (and (> hl_0_2 0) (> i_0_2 0)) (= o_0_2 (+ o_1_2 1))) | |
(=> (> hr_1_2 0) (= x_1_2 x_2_2)) | |
(=> (> hl_1_2 0) (= x_1_2 x_2_2)) | |
(=> (and (> hr_1_2 0) (= i_2_2 0)) (= o_1_2 o_2_2)) | |
(=> (and (> hl_1_2 0) (= i_1_2 0)) (= o_1_2 o_2_2)) | |
(=> (and (> hr_1_2 0) (> i_2_2 0)) (= o_2_2 (+ o_1_2 1))) | |
(=> (and (> hl_1_2 0) (> i_1_2 0)) (= o_1_2 (+ o_2_2 1))) | |
(=> (> hr_2_2 0) (= x_2_2 x_3_2)) | |
(=> (> hl_2_2 0) (= x_2_2 x_3_2)) | |
(=> (and (> hr_2_2 0) (= i_3_2 0)) (= o_2_2 o_3_2)) | |
(=> (and (> hl_2_2 0) (= i_2_2 0)) (= o_2_2 o_3_2)) | |
(=> (and (> hr_2_2 0) (> i_3_2 0)) (= o_3_2 (+ o_2_2 1))) | |
(=> (and (> hl_2_2 0) (> i_2_2 0)) (= o_2_2 (+ o_3_2 1))) | |
(=> (> hr_3_2 0) (= x_3_2 x_4_2)) | |
(=> (> hl_3_2 0) (= x_3_2 x_4_2)) | |
(=> (and (> hr_3_2 0) (= i_4_2 0)) (= o_3_2 o_4_2)) | |
(=> (and (> hl_3_2 0) (= i_3_2 0)) (= o_3_2 o_4_2)) | |
(=> (and (> hr_3_2 0) (> i_4_2 0)) (= o_4_2 (+ o_3_2 1))) | |
(=> (and (> hl_3_2 0) (> i_3_2 0)) (= o_3_2 (+ o_4_2 1))) | |
(=> (> hr_4_2 0) (= x_4_2 x_5_2)) | |
(=> (> hl_4_2 0) (= x_4_2 x_5_2)) | |
(=> (and (> hr_4_2 0) (= i_5_2 0)) (= o_4_2 o_5_2)) | |
(=> (and (> hl_4_2 0) (= i_4_2 0)) (= o_4_2 o_5_2)) | |
(=> (and (> hr_4_2 0) (> i_5_2 0)) (= o_5_2 (+ o_4_2 1))) | |
(=> (and (> hl_4_2 0) (> i_4_2 0)) (= o_4_2 (+ o_5_2 1))) | |
(=> (> hr_0_3 0) (= x_0_3 x_1_3)) | |
(=> (> hl_0_3 0) (= x_0_3 x_1_3)) | |
(=> (and (> hr_0_3 0) (= i_1_3 0)) (= o_0_3 o_1_3)) | |
(=> (and (> hl_0_3 0) (= i_0_3 0)) (= o_0_3 o_1_3)) | |
(=> (and (> hr_0_3 0) (> i_1_3 0)) (= o_1_3 (+ o_0_3 1))) | |
(=> (and (> hl_0_3 0) (> i_0_3 0)) (= o_0_3 (+ o_1_3 1))) | |
(=> (> hr_1_3 0) (= x_1_3 x_2_3)) | |
(=> (> hl_1_3 0) (= x_1_3 x_2_3)) | |
(=> (and (> hr_1_3 0) (= i_2_3 0)) (= o_1_3 o_2_3)) | |
(=> (and (> hl_1_3 0) (= i_1_3 0)) (= o_1_3 o_2_3)) | |
(=> (and (> hr_1_3 0) (> i_2_3 0)) (= o_2_3 (+ o_1_3 1))) | |
(=> (and (> hl_1_3 0) (> i_1_3 0)) (= o_1_3 (+ o_2_3 1))) | |
(=> (> hr_2_3 0) (= x_2_3 x_3_3)) | |
(=> (> hl_2_3 0) (= x_2_3 x_3_3)) | |
(=> (and (> hr_2_3 0) (= i_3_3 0)) (= o_2_3 o_3_3)) | |
(=> (and (> hl_2_3 0) (= i_2_3 0)) (= o_2_3 o_3_3)) | |
(=> (and (> hr_2_3 0) (> i_3_3 0)) (= o_3_3 (+ o_2_3 1))) | |
(=> (and (> hl_2_3 0) (> i_2_3 0)) (= o_2_3 (+ o_3_3 1))) | |
(=> (> hr_3_3 0) (= x_3_3 x_4_3)) | |
(=> (> hl_3_3 0) (= x_3_3 x_4_3)) | |
(=> (and (> hr_3_3 0) (= i_4_3 0)) (= o_3_3 o_4_3)) | |
(=> (and (> hl_3_3 0) (= i_3_3 0)) (= o_3_3 o_4_3)) | |
(=> (and (> hr_3_3 0) (> i_4_3 0)) (= o_4_3 (+ o_3_3 1))) | |
(=> (and (> hl_3_3 0) (> i_3_3 0)) (= o_3_3 (+ o_4_3 1))) | |
(=> (> hr_4_3 0) (= x_4_3 x_5_3)) | |
(=> (> hl_4_3 0) (= x_4_3 x_5_3)) | |
(=> (and (> hr_4_3 0) (= i_5_3 0)) (= o_4_3 o_5_3)) | |
(=> (and (> hl_4_3 0) (= i_4_3 0)) (= o_4_3 o_5_3)) | |
(=> (and (> hr_4_3 0) (> i_5_3 0)) (= o_5_3 (+ o_4_3 1))) | |
(=> (and (> hl_4_3 0) (> i_4_3 0)) (= o_4_3 (+ o_5_3 1))) | |
(=> (> hr_0_4 0) (= x_0_4 x_1_4)) | |
(=> (> hl_0_4 0) (= x_0_4 x_1_4)) | |
(=> (and (> hr_0_4 0) (= i_1_4 0)) (= o_0_4 o_1_4)) | |
(=> (and (> hl_0_4 0) (= i_0_4 0)) (= o_0_4 o_1_4)) | |
(=> (and (> hr_0_4 0) (> i_1_4 0)) (= o_1_4 (+ o_0_4 1))) | |
(=> (and (> hl_0_4 0) (> i_0_4 0)) (= o_0_4 (+ o_1_4 1))) | |
(=> (> hr_1_4 0) (= x_1_4 x_2_4)) | |
(=> (> hl_1_4 0) (= x_1_4 x_2_4)) | |
(=> (and (> hr_1_4 0) (= i_2_4 0)) (= o_1_4 o_2_4)) | |
(=> (and (> hl_1_4 0) (= i_1_4 0)) (= o_1_4 o_2_4)) | |
(=> (and (> hr_1_4 0) (> i_2_4 0)) (= o_2_4 (+ o_1_4 1))) | |
(=> (and (> hl_1_4 0) (> i_1_4 0)) (= o_1_4 (+ o_2_4 1))) | |
(=> (> hr_2_4 0) (= x_2_4 x_3_4)) | |
(=> (> hl_2_4 0) (= x_2_4 x_3_4)) | |
(=> (and (> hr_2_4 0) (= i_3_4 0)) (= o_2_4 o_3_4)) | |
(=> (and (> hl_2_4 0) (= i_2_4 0)) (= o_2_4 o_3_4)) | |
(=> (and (> hr_2_4 0) (> i_3_4 0)) (= o_3_4 (+ o_2_4 1))) | |
(=> (and (> hl_2_4 0) (> i_2_4 0)) (= o_2_4 (+ o_3_4 1))) | |
(=> (> hr_3_4 0) (= x_3_4 x_4_4)) | |
(=> (> hl_3_4 0) (= x_3_4 x_4_4)) | |
(=> (and (> hr_3_4 0) (= i_4_4 0)) (= o_3_4 o_4_4)) | |
(=> (and (> hl_3_4 0) (= i_3_4 0)) (= o_3_4 o_4_4)) | |
(=> (and (> hr_3_4 0) (> i_4_4 0)) (= o_4_4 (+ o_3_4 1))) | |
(=> (and (> hl_3_4 0) (> i_3_4 0)) (= o_3_4 (+ o_4_4 1))) | |
(=> (> hr_4_4 0) (= x_4_4 x_5_4)) | |
(=> (> hl_4_4 0) (= x_4_4 x_5_4)) | |
(=> (and (> hr_4_4 0) (= i_5_4 0)) (= o_4_4 o_5_4)) | |
(=> (and (> hl_4_4 0) (= i_4_4 0)) (= o_4_4 o_5_4)) | |
(=> (and (> hr_4_4 0) (> i_5_4 0)) (= o_5_4 (+ o_4_4 1))) | |
(=> (and (> hl_4_4 0) (> i_4_4 0)) (= o_4_4 (+ o_5_4 1))) | |
(=> (> hr_0_5 0) (= x_0_5 x_1_5)) | |
(=> (> hl_0_5 0) (= x_0_5 x_1_5)) | |
(=> (and (> hr_0_5 0) (= i_1_5 0)) (= o_0_5 o_1_5)) | |
(=> (and (> hl_0_5 0) (= i_0_5 0)) (= o_0_5 o_1_5)) | |
(=> (and (> hr_0_5 0) (> i_1_5 0)) (= o_1_5 (+ o_0_5 1))) | |
(=> (and (> hl_0_5 0) (> i_0_5 0)) (= o_0_5 (+ o_1_5 1))) | |
(=> (> hr_1_5 0) (= x_1_5 x_2_5)) | |
(=> (> hl_1_5 0) (= x_1_5 x_2_5)) | |
(=> (and (> hr_1_5 0) (= i_2_5 0)) (= o_1_5 o_2_5)) | |
(=> (and (> hl_1_5 0) (= i_1_5 0)) (= o_1_5 o_2_5)) | |
(=> (and (> hr_1_5 0) (> i_2_5 0)) (= o_2_5 (+ o_1_5 1))) | |
(=> (and (> hl_1_5 0) (> i_1_5 0)) (= o_1_5 (+ o_2_5 1))) | |
(=> (> hr_2_5 0) (= x_2_5 x_3_5)) | |
(=> (> hl_2_5 0) (= x_2_5 x_3_5)) | |
(=> (and (> hr_2_5 0) (= i_3_5 0)) (= o_2_5 o_3_5)) | |
(=> (and (> hl_2_5 0) (= i_2_5 0)) (= o_2_5 o_3_5)) | |
(=> (and (> hr_2_5 0) (> i_3_5 0)) (= o_3_5 (+ o_2_5 1))) | |
(=> (and (> hl_2_5 0) (> i_2_5 0)) (= o_2_5 (+ o_3_5 1))) | |
(=> (> hr_3_5 0) (= x_3_5 x_4_5)) | |
(=> (> hl_3_5 0) (= x_3_5 x_4_5)) | |
(=> (and (> hr_3_5 0) (= i_4_5 0)) (= o_3_5 o_4_5)) | |
(=> (and (> hl_3_5 0) (= i_3_5 0)) (= o_3_5 o_4_5)) | |
(=> (and (> hr_3_5 0) (> i_4_5 0)) (= o_4_5 (+ o_3_5 1))) | |
(=> (and (> hl_3_5 0) (> i_3_5 0)) (= o_3_5 (+ o_4_5 1))) | |
(=> (> hr_4_5 0) (= x_4_5 x_5_5)) | |
(=> (> hl_4_5 0) (= x_4_5 x_5_5)) | |
(=> (and (> hr_4_5 0) (= i_5_5 0)) (= o_4_5 o_5_5)) | |
(=> (and (> hl_4_5 0) (= i_4_5 0)) (= o_4_5 o_5_5)) | |
(=> (and (> hr_4_5 0) (> i_5_5 0)) (= o_5_5 (+ o_4_5 1))) | |
(=> (and (> hl_4_5 0) (> i_4_5 0)) (= o_4_5 (+ o_5_5 1))) | |
(=> (> vu_0_0 0) (= x_0_0 x_0_1)) | |
(=> (> vd_0_0 0) (= x_0_0 x_0_1)) | |
(=> (and (> vu_0_0 0) (= i_0_0 0)) (= o_0_0 o_0_1)) | |
(=> (and (> vd_0_0 0) (= i_0_1 0)) (= o_0_0 o_0_1)) | |
(=> (and (> vu_0_0 0) (> i_0_0 0)) (= o_0_0 (+ o_0_1 1))) | |
(=> (and (> vd_0_0 0) (> i_0_1 0)) (= o_0_1 (+ o_0_0 1))) | |
(=> (> vu_1_0 0) (= x_1_0 x_1_1)) | |
(=> (> vd_1_0 0) (= x_1_0 x_1_1)) | |
(=> (and (> vu_1_0 0) (= i_1_0 0)) (= o_1_0 o_1_1)) | |
(=> (and (> vd_1_0 0) (= i_1_1 0)) (= o_1_0 o_1_1)) | |
(=> (and (> vu_1_0 0) (> i_1_0 0)) (= o_1_0 (+ o_1_1 1))) | |
(=> (and (> vd_1_0 0) (> i_1_1 0)) (= o_1_1 (+ o_1_0 1))) | |
(=> (> vu_2_0 0) (= x_2_0 x_2_1)) | |
(=> (> vd_2_0 0) (= x_2_0 x_2_1)) | |
(=> (and (> vu_2_0 0) (= i_2_0 0)) (= o_2_0 o_2_1)) | |
(=> (and (> vd_2_0 0) (= i_2_1 0)) (= o_2_0 o_2_1)) | |
(=> (and (> vu_2_0 0) (> i_2_0 0)) (= o_2_0 (+ o_2_1 1))) | |
(=> (and (> vd_2_0 0) (> i_2_1 0)) (= o_2_1 (+ o_2_0 1))) | |
(=> (> vu_3_0 0) (= x_3_0 x_3_1)) | |
(=> (> vd_3_0 0) (= x_3_0 x_3_1)) | |
(=> (and (> vu_3_0 0) (= i_3_0 0)) (= o_3_0 o_3_1)) | |
(=> (and (> vd_3_0 0) (= i_3_1 0)) (= o_3_0 o_3_1)) | |
(=> (and (> vu_3_0 0) (> i_3_0 0)) (= o_3_0 (+ o_3_1 1))) | |
(=> (and (> vd_3_0 0) (> i_3_1 0)) (= o_3_1 (+ o_3_0 1))) | |
(=> (> vu_4_0 0) (= x_4_0 x_4_1)) | |
(=> (> vd_4_0 0) (= x_4_0 x_4_1)) | |
(=> (and (> vu_4_0 0) (= i_4_0 0)) (= o_4_0 o_4_1)) | |
(=> (and (> vd_4_0 0) (= i_4_1 0)) (= o_4_0 o_4_1)) | |
(=> (and (> vu_4_0 0) (> i_4_0 0)) (= o_4_0 (+ o_4_1 1))) | |
(=> (and (> vd_4_0 0) (> i_4_1 0)) (= o_4_1 (+ o_4_0 1))) | |
(=> (> vu_5_0 0) (= x_5_0 x_5_1)) | |
(=> (> vd_5_0 0) (= x_5_0 x_5_1)) | |
(=> (and (> vu_5_0 0) (= i_5_0 0)) (= o_5_0 o_5_1)) | |
(=> (and (> vd_5_0 0) (= i_5_1 0)) (= o_5_0 o_5_1)) | |
(=> (and (> vu_5_0 0) (> i_5_0 0)) (= o_5_0 (+ o_5_1 1))) | |
(=> (and (> vd_5_0 0) (> i_5_1 0)) (= o_5_1 (+ o_5_0 1))) | |
(=> (> vu_0_1 0) (= x_0_1 x_0_2)) | |
(=> (> vd_0_1 0) (= x_0_1 x_0_2)) | |
(=> (and (> vu_0_1 0) (= i_0_1 0)) (= o_0_1 o_0_2)) | |
(=> (and (> vd_0_1 0) (= i_0_2 0)) (= o_0_1 o_0_2)) | |
(=> (and (> vu_0_1 0) (> i_0_1 0)) (= o_0_1 (+ o_0_2 1))) | |
(=> (and (> vd_0_1 0) (> i_0_2 0)) (= o_0_2 (+ o_0_1 1))) | |
(=> (> vu_1_1 0) (= x_1_1 x_1_2)) | |
(=> (> vd_1_1 0) (= x_1_1 x_1_2)) | |
(=> (and (> vu_1_1 0) (= i_1_1 0)) (= o_1_1 o_1_2)) | |
(=> (and (> vd_1_1 0) (= i_1_2 0)) (= o_1_1 o_1_2)) | |
(=> (and (> vu_1_1 0) (> i_1_1 0)) (= o_1_1 (+ o_1_2 1))) | |
(=> (and (> vd_1_1 0) (> i_1_2 0)) (= o_1_2 (+ o_1_1 1))) | |
(=> (> vu_2_1 0) (= x_2_1 x_2_2)) | |
(=> (> vd_2_1 0) (= x_2_1 x_2_2)) | |
(=> (and (> vu_2_1 0) (= i_2_1 0)) (= o_2_1 o_2_2)) | |
(=> (and (> vd_2_1 0) (= i_2_2 0)) (= o_2_1 o_2_2)) | |
(=> (and (> vu_2_1 0) (> i_2_1 0)) (= o_2_1 (+ o_2_2 1))) | |
(=> (and (> vd_2_1 0) (> i_2_2 0)) (= o_2_2 (+ o_2_1 1))) | |
(=> (> vu_3_1 0) (= x_3_1 x_3_2)) | |
(=> (> vd_3_1 0) (= x_3_1 x_3_2)) | |
(=> (and (> vu_3_1 0) (= i_3_1 0)) (= o_3_1 o_3_2)) | |
(=> (and (> vd_3_1 0) (= i_3_2 0)) (= o_3_1 o_3_2)) | |
(=> (and (> vu_3_1 0) (> i_3_1 0)) (= o_3_1 (+ o_3_2 1))) | |
(=> (and (> vd_3_1 0) (> i_3_2 0)) (= o_3_2 (+ o_3_1 1))) | |
(=> (> vu_4_1 0) (= x_4_1 x_4_2)) | |
(=> (> vd_4_1 0) (= x_4_1 x_4_2)) | |
(=> (and (> vu_4_1 0) (= i_4_1 0)) (= o_4_1 o_4_2)) | |
(=> (and (> vd_4_1 0) (= i_4_2 0)) (= o_4_1 o_4_2)) | |
(=> (and (> vu_4_1 0) (> i_4_1 0)) (= o_4_1 (+ o_4_2 1))) | |
(=> (and (> vd_4_1 0) (> i_4_2 0)) (= o_4_2 (+ o_4_1 1))) | |
(=> (> vu_5_1 0) (= x_5_1 x_5_2)) | |
(=> (> vd_5_1 0) (= x_5_1 x_5_2)) | |
(=> (and (> vu_5_1 0) (= i_5_1 0)) (= o_5_1 o_5_2)) | |
(=> (and (> vd_5_1 0) (= i_5_2 0)) (= o_5_1 o_5_2)) | |
(=> (and (> vu_5_1 0) (> i_5_1 0)) (= o_5_1 (+ o_5_2 1))) | |
(=> (and (> vd_5_1 0) (> i_5_2 0)) (= o_5_2 (+ o_5_1 1))) | |
(=> (> vu_0_2 0) (= x_0_2 x_0_3)) | |
(=> (> vd_0_2 0) (= x_0_2 x_0_3)) | |
(=> (and (> vu_0_2 0) (= i_0_2 0)) (= o_0_2 o_0_3)) | |
(=> (and (> vd_0_2 0) (= i_0_3 0)) (= o_0_2 o_0_3)) | |
(=> (and (> vu_0_2 0) (> i_0_2 0)) (= o_0_2 (+ o_0_3 1))) | |
(=> (and (> vd_0_2 0) (> i_0_3 0)) (= o_0_3 (+ o_0_2 1))) | |
(=> (> vu_1_2 0) (= x_1_2 x_1_3)) | |
(=> (> vd_1_2 0) (= x_1_2 x_1_3)) | |
(=> (and (> vu_1_2 0) (= i_1_2 0)) (= o_1_2 o_1_3)) | |
(=> (and (> vd_1_2 0) (= i_1_3 0)) (= o_1_2 o_1_3)) | |
(=> (and (> vu_1_2 0) (> i_1_2 0)) (= o_1_2 (+ o_1_3 1))) | |
(=> (and (> vd_1_2 0) (> i_1_3 0)) (= o_1_3 (+ o_1_2 1))) | |
(=> (> vu_2_2 0) (= x_2_2 x_2_3)) | |
(=> (> vd_2_2 0) (= x_2_2 x_2_3)) | |
(=> (and (> vu_2_2 0) (= i_2_2 0)) (= o_2_2 o_2_3)) | |
(=> (and (> vd_2_2 0) (= i_2_3 0)) (= o_2_2 o_2_3)) | |
(=> (and (> vu_2_2 0) (> i_2_2 0)) (= o_2_2 (+ o_2_3 1))) | |
(=> (and (> vd_2_2 0) (> i_2_3 0)) (= o_2_3 (+ o_2_2 1))) | |
(=> (> vu_3_2 0) (= x_3_2 x_3_3)) | |
(=> (> vd_3_2 0) (= x_3_2 x_3_3)) | |
(=> (and (> vu_3_2 0) (= i_3_2 0)) (= o_3_2 o_3_3)) | |
(=> (and (> vd_3_2 0) (= i_3_3 0)) (= o_3_2 o_3_3)) | |
(=> (and (> vu_3_2 0) (> i_3_2 0)) (= o_3_2 (+ o_3_3 1))) | |
(=> (and (> vd_3_2 0) (> i_3_3 0)) (= o_3_3 (+ o_3_2 1))) | |
(=> (> vu_4_2 0) (= x_4_2 x_4_3)) | |
(=> (> vd_4_2 0) (= x_4_2 x_4_3)) | |
(=> (and (> vu_4_2 0) (= i_4_2 0)) (= o_4_2 o_4_3)) | |
(=> (and (> vd_4_2 0) (= i_4_3 0)) (= o_4_2 o_4_3)) | |
(=> (and (> vu_4_2 0) (> i_4_2 0)) (= o_4_2 (+ o_4_3 1))) | |
(=> (and (> vd_4_2 0) (> i_4_3 0)) (= o_4_3 (+ o_4_2 1))) | |
(=> (> vu_5_2 0) (= x_5_2 x_5_3)) | |
(=> (> vd_5_2 0) (= x_5_2 x_5_3)) | |
(=> (and (> vu_5_2 0) (= i_5_2 0)) (= o_5_2 o_5_3)) | |
(=> (and (> vd_5_2 0) (= i_5_3 0)) (= o_5_2 o_5_3)) | |
(=> (and (> vu_5_2 0) (> i_5_2 0)) (= o_5_2 (+ o_5_3 1))) | |
(=> (and (> vd_5_2 0) (> i_5_3 0)) (= o_5_3 (+ o_5_2 1))) | |
(=> (> vu_0_3 0) (= x_0_3 x_0_4)) | |
(=> (> vd_0_3 0) (= x_0_3 x_0_4)) | |
(=> (and (> vu_0_3 0) (= i_0_3 0)) (= o_0_3 o_0_4)) | |
(=> (and (> vd_0_3 0) (= i_0_4 0)) (= o_0_3 o_0_4)) | |
(=> (and (> vu_0_3 0) (> i_0_3 0)) (= o_0_3 (+ o_0_4 1))) | |
(=> (and (> vd_0_3 0) (> i_0_4 0)) (= o_0_4 (+ o_0_3 1))) | |
(=> (> vu_1_3 0) (= x_1_3 x_1_4)) | |
(=> (> vd_1_3 0) (= x_1_3 x_1_4)) | |
(=> (and (> vu_1_3 0) (= i_1_3 0)) (= o_1_3 o_1_4)) | |
(=> (and (> vd_1_3 0) (= i_1_4 0)) (= o_1_3 o_1_4)) | |
(=> (and (> vu_1_3 0) (> i_1_3 0)) (= o_1_3 (+ o_1_4 1))) | |
(=> (and (> vd_1_3 0) (> i_1_4 0)) (= o_1_4 (+ o_1_3 1))) | |
(=> (> vu_2_3 0) (= x_2_3 x_2_4)) | |
(=> (> vd_2_3 0) (= x_2_3 x_2_4)) | |
(=> (and (> vu_2_3 0) (= i_2_3 0)) (= o_2_3 o_2_4)) | |
(=> (and (> vd_2_3 0) (= i_2_4 0)) (= o_2_3 o_2_4)) | |
(=> (and (> vu_2_3 0) (> i_2_3 0)) (= o_2_3 (+ o_2_4 1))) | |
(=> (and (> vd_2_3 0) (> i_2_4 0)) (= o_2_4 (+ o_2_3 1))) | |
(=> (> vu_3_3 0) (= x_3_3 x_3_4)) | |
(=> (> vd_3_3 0) (= x_3_3 x_3_4)) | |
(=> (and (> vu_3_3 0) (= i_3_3 0)) (= o_3_3 o_3_4)) | |
(=> (and (> vd_3_3 0) (= i_3_4 0)) (= o_3_3 o_3_4)) | |
(=> (and (> vu_3_3 0) (> i_3_3 0)) (= o_3_3 (+ o_3_4 1))) | |
(=> (and (> vd_3_3 0) (> i_3_4 0)) (= o_3_4 (+ o_3_3 1))) | |
(=> (> vu_4_3 0) (= x_4_3 x_4_4)) | |
(=> (> vd_4_3 0) (= x_4_3 x_4_4)) | |
(=> (and (> vu_4_3 0) (= i_4_3 0)) (= o_4_3 o_4_4)) | |
(=> (and (> vd_4_3 0) (= i_4_4 0)) (= o_4_3 o_4_4)) | |
(=> (and (> vu_4_3 0) (> i_4_3 0)) (= o_4_3 (+ o_4_4 1))) | |
(=> (and (> vd_4_3 0) (> i_4_4 0)) (= o_4_4 (+ o_4_3 1))) | |
(=> (> vu_5_3 0) (= x_5_3 x_5_4)) | |
(=> (> vd_5_3 0) (= x_5_3 x_5_4)) | |
(=> (and (> vu_5_3 0) (= i_5_3 0)) (= o_5_3 o_5_4)) | |
(=> (and (> vd_5_3 0) (= i_5_4 0)) (= o_5_3 o_5_4)) | |
(=> (and (> vu_5_3 0) (> i_5_3 0)) (= o_5_3 (+ o_5_4 1))) | |
(=> (and (> vd_5_3 0) (> i_5_4 0)) (= o_5_4 (+ o_5_3 1))) | |
(=> (> vu_0_4 0) (= x_0_4 x_0_5)) | |
(=> (> vd_0_4 0) (= x_0_4 x_0_5)) | |
(=> (and (> vu_0_4 0) (= i_0_4 0)) (= o_0_4 o_0_5)) | |
(=> (and (> vd_0_4 0) (= i_0_5 0)) (= o_0_4 o_0_5)) | |
(=> (and (> vu_0_4 0) (> i_0_4 0)) (= o_0_4 (+ o_0_5 1))) | |
(=> (and (> vd_0_4 0) (> i_0_5 0)) (= o_0_5 (+ o_0_4 1))) | |
(=> (> vu_1_4 0) (= x_1_4 x_1_5)) | |
(=> (> vd_1_4 0) (= x_1_4 x_1_5)) | |
(=> (and (> vu_1_4 0) (= i_1_4 0)) (= o_1_4 o_1_5)) | |
(=> (and (> vd_1_4 0) (= i_1_5 0)) (= o_1_4 o_1_5)) | |
(=> (and (> vu_1_4 0) (> i_1_4 0)) (= o_1_4 (+ o_1_5 1))) | |
(=> (and (> vd_1_4 0) (> i_1_5 0)) (= o_1_5 (+ o_1_4 1))) | |
(=> (> vu_2_4 0) (= x_2_4 x_2_5)) | |
(=> (> vd_2_4 0) (= x_2_4 x_2_5)) | |
(=> (and (> vu_2_4 0) (= i_2_4 0)) (= o_2_4 o_2_5)) | |
(=> (and (> vd_2_4 0) (= i_2_5 0)) (= o_2_4 o_2_5)) | |
(=> (and (> vu_2_4 0) (> i_2_4 0)) (= o_2_4 (+ o_2_5 1))) | |
(=> (and (> vd_2_4 0) (> i_2_5 0)) (= o_2_5 (+ o_2_4 1))) | |
(=> (> vu_3_4 0) (= x_3_4 x_3_5)) | |
(=> (> vd_3_4 0) (= x_3_4 x_3_5)) | |
(=> (and (> vu_3_4 0) (= i_3_4 0)) (= o_3_4 o_3_5)) | |
(=> (and (> vd_3_4 0) (= i_3_5 0)) (= o_3_4 o_3_5)) | |
(=> (and (> vu_3_4 0) (> i_3_4 0)) (= o_3_4 (+ o_3_5 1))) | |
(=> (and (> vd_3_4 0) (> i_3_5 0)) (= o_3_5 (+ o_3_4 1))) | |
(=> (> vu_4_4 0) (= x_4_4 x_4_5)) | |
(=> (> vd_4_4 0) (= x_4_4 x_4_5)) | |
(=> (and (> vu_4_4 0) (= i_4_4 0)) (= o_4_4 o_4_5)) | |
(=> (and (> vd_4_4 0) (= i_4_5 0)) (= o_4_4 o_4_5)) | |
(=> (and (> vu_4_4 0) (> i_4_4 0)) (= o_4_4 (+ o_4_5 1))) | |
(=> (and (> vd_4_4 0) (> i_4_5 0)) (= o_4_5 (+ o_4_4 1))) | |
(=> (> vu_5_4 0) (= x_5_4 x_5_5)) | |
(=> (> vd_5_4 0) (= x_5_4 x_5_5)) | |
(=> (and (> vu_5_4 0) (= i_5_4 0)) (= o_5_4 o_5_5)) | |
(=> (and (> vd_5_4 0) (= i_5_5 0)) (= o_5_4 o_5_5)) | |
(=> (and (> vu_5_4 0) (> i_5_4 0)) (= o_5_4 (+ o_5_5 1))) | |
(=> (and (> vd_5_4 0) (> i_5_5 0)) (= o_5_5 (+ o_5_4 1))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment