blob: 76b63d264da91085ab02754cf111984ae4a594a7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(benchmark iso_icl_repgen004.smt
:source {
http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
}
:status unsat
:difficulty { 1 }
:category { crafted }
:logic QF_UF
:extrasorts (I)
:extrafuns ((op1 I I I))
:extrafuns ((op I I I))
:extrafuns ((e5 I))
:extrafuns ((e4 I))
:extrafuns ((e3 I))
:extrafuns ((e2 I))
:extrafuns ((e1 I))
:extrafuns ((e0 I))
:assumption
(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_2 (op e0 e2)) (let (?cvc_3 (op e0 e3)) (let (?cvc_4 (op e0 e4)) (let (?cvc_5 (op e0 e5)) (let (?cvc_6 (op e1 e0)) (let (?cvc_7 (op e1 e1)) (let (?cvc_8 (op e1 e2)) (let (?cvc_9 (op e1 e3)) (let (?cvc_10 (op e1 e4)) (let (?cvc_11 (op e1 e5)) (let (?cvc_12 (op e2 e0)) (let (?cvc_13 (op e2 e1)) (let (?cvc_14 (op e2 e2)) (let (?cvc_15 (op e2 e3)) (let (?cvc_16 (op e2 e4)) (let (?cvc_17 (op e2 e5)) (let (?cvc_18 (op e3 e0)) (let (?cvc_19 (op e3 e1)) (let (?cvc_20 (op e3 e2)) (let (?cvc_21 (op e3 e3)) (let (?cvc_22 (op e3 e4)) (let (?cvc_23 (op e3 e5)) (let (?cvc_24 (op e4 e0)) (let (?cvc_25 (op e4 e1)) (let (?cvc_26 (op e4 e2)) (let (?cvc_27 (op e4 e3)) (let (?cvc_28 (op e4 e4)) (let (?cvc_29 (op e4 e5)) (let (?cvc_30 (op e5 e0)) (let (?cvc_31 (op e5 e1)) (let (?cvc_32 (op e5 e2)) (let (?cvc_33 (op e5 e3)) (let (?cvc_34 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (= ?cvc_0 e0) (= ?cvc_0 e1) ) (= ?cvc_0 e2) ) (= ?cvc_0 e3) ) (= ?cvc_0 e4) ) (= ?cvc_0 e5) ) (or (or (or (or (or (= ?cvc_1 e0) (= ?cvc_1 e1) ) (= ?cvc_1 e2) ) (= ?cvc_1 e3) ) (= ?cvc_1 e4) ) (= ?cvc_1 e5) )) (or (or (or (or (or (= ?cvc_2 e0) (= ?cvc_2 e1) ) (= ?cvc_2 e2) ) (= ?cvc_2 e3) ) (= ?cvc_2 e4) ) (= ?cvc_2 e5) )) (or (or (or (or (or (= ?cvc_3 e0) (= ?cvc_3 e1) ) (= ?cvc_3 e2) ) (= ?cvc_3 e3) ) (= ?cvc_3 e4) ) (= ?cvc_3 e5) )) (or (or (or (or (or (= ?cvc_4 e0) (= ?cvc_4 e1) ) (= ?cvc_4 e2) ) (= ?cvc_4 e3) ) (= ?cvc_4 e4) ) (= ?cvc_4 e5) )) (or (or (or (or (or (= ?cvc_5 e0) (= ?cvc_5 e1) ) (= ?cvc_5 e2) ) (= ?cvc_5 e3) ) (= ?cvc_5 e4) ) (= ?cvc_5 e5) )) (and (and (and (and (and (or (or (or (or (or (= ?cvc_6 e0) (= ?cvc_6 e1) ) (= ?cvc_6 e2) ) (= ?cvc_6 e3) ) (= ?cvc_6 e4) ) (= ?cvc_6 e5) ) (or (or (or (or (or (= ?cvc_7 e0) (= ?cvc_7 e1) ) (= ?cvc_7 e2) ) (= ?cvc_7 e3) ) (= ?cvc_7 e4) ) (= ?cvc_7 e5) )) (or (or (or (or (or (= ?cvc_8 e0) (= ?cvc_8 e1) ) (= ?cvc_8 e2) ) (= ?cvc_8 e3) ) (= ?cvc_8 e4) ) (= ?cvc_8 e5) )) (or (or (or (or (or (= ?cvc_9 e0) (= ?cvc_9 e1) ) (= ?cvc_9 e2) ) (= ?cvc_9 e3) ) (= ?cvc_9 e4) ) (= ?cvc_9 e5) )) (or (or (or (or (or (= ?cvc_10 e0) (= ?cvc_10 e1) ) (= ?cvc_10 e2) ) (= ?cvc_10 e3) ) (= ?cvc_10 e4) ) (= ?cvc_10 e5) )) (or (or (or (or (or (= ?cvc_11 e0) (= ?cvc_11 e1) ) (= ?cvc_11 e2) ) (= ?cvc_11 e3) ) (= ?cvc_11 e4) ) (= ?cvc_11 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_12 e0) (= ?cvc_12 e1) ) (= ?cvc_12 e2) ) (= ?cvc_12 e3) ) (= ?cvc_12 e4) ) (= ?cvc_12 e5) ) (or (or (or (or (or (= ?cvc_13 e0) (= ?cvc_13 e1) ) (= ?cvc_13 e2) ) (= ?cvc_13 e3) ) (= ?cvc_13 e4) ) (= ?cvc_13 e5) )) (or (or (or (or (or (= ?cvc_14 e0) (= ?cvc_14 e1) ) (= ?cvc_14 e2) ) (= ?cvc_14 e3) ) (= ?cvc_14 e4) ) (= ?cvc_14 e5) )) (or (or (or (or (or (= ?cvc_15 e0) (= ?cvc_15 e1) ) (= ?cvc_15 e2) ) (= ?cvc_15 e3) ) (= ?cvc_15 e4) ) (= ?cvc_15 e5) )) (or (or (or (or (or (= ?cvc_16 e0) (= ?cvc_16 e1) ) (= ?cvc_16 e2) ) (= ?cvc_16 e3) ) (= ?cvc_16 e4) ) (= ?cvc_16 e5) )) (or (or (or (or (or (= ?cvc_17 e0) (= ?cvc_17 e1) ) (= ?cvc_17 e2) ) (= ?cvc_17 e3) ) (= ?cvc_17 e4) ) (= ?cvc_17 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_18 e0) (= ?cvc_18 e1) ) (= ?cvc_18 e2) ) (= ?cvc_18 e3) ) (= ?cvc_18 e4) ) (= ?cvc_18 e5) ) (or (or (or (or (or (= ?cvc_19 e0) (= ?cvc_19 e1) ) (= ?cvc_19 e2) ) (= ?cvc_19 e3) ) (= ?cvc_19 e4) ) (= ?cvc_19 e5) )) (or (or (or (or (or (= ?cvc_20 e0) (= ?cvc_20 e1) ) (= ?cvc_20 e2) ) (= ?cvc_20 e3) ) (= ?cvc_20 e4) ) (= ?cvc_20 e5) )) (or (or (or (or (or (= ?cvc_21 e0) (= ?cvc_21 e1) ) (= ?cvc_21 e2) ) (= ?cvc_21 e3) ) (= ?cvc_21 e4) ) (= ?cvc_21 e5) )) (or (or (or (or (or (= ?cvc_22 e0) (= ?cvc_22 e1) ) (= ?cvc_22 e2) ) (= ?cvc_22 e3) ) (= ?cvc_22 e4) ) (= ?cvc_22 e5) )) (or (or (or (or (or (= ?cvc_23 e0) (= ?cvc_23 e1) ) (= ?cvc_23 e2) ) (= ?cvc_23 e3) ) (= ?cvc_23 e4) ) (= ?cvc_23 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_24 e0) (= ?cvc_24 e1) ) (= ?cvc_24 e2) ) (= ?cvc_24 e3) ) (= ?cvc_24 e4) ) (= ?cvc_24 e5) ) (or (or (or (or (or (= ?cvc_25 e0) (= ?cvc_25 e1) ) (= ?cvc_25 e2) ) (= ?cvc_25 e3) ) (= ?cvc_25 e4) ) (= ?cvc_25 e5) )) (or (or (or (or (or (= ?cvc_26 e0) (= ?cvc_26 e1) ) (= ?cvc_26 e2) ) (= ?cvc_26 e3) ) (= ?cvc_26 e4) ) (= ?cvc_26 e5) )) (or (or (or (or (or (= ?cvc_27 e0) (= ?cvc_27 e1) ) (= ?cvc_27 e2) ) (= ?cvc_27 e3) ) (= ?cvc_27 e4) ) (= ?cvc_27 e5) )) (or (or (or (or (or (= ?cvc_28 e0) (= ?cvc_28 e1) ) (= ?cvc_28 e2) ) (= ?cvc_28 e3) ) (= ?cvc_28 e4) ) (= ?cvc_28 e5) )) (or (or (or (or (or (= ?cvc_29 e0) (= ?cvc_29 e1) ) (= ?cvc_29 e2) ) (= ?cvc_29 e3) ) (= ?cvc_29 e4) ) (= ?cvc_29 e5) ))) (and (and (and (and (and (or (or (or (or (or (= ?cvc_30 e0) (= ?cvc_30 e1) ) (= ?cvc_30 e2) ) (= ?cvc_30 e3) ) (= ?cvc_30 e4) ) (= ?cvc_30 e5) ) (or (or (or (or (or (= ?cvc_31 e0) (= ?cvc_31 e1) ) (= ?cvc_31 e2) ) (= ?cvc_31 e3) ) (= ?cvc_31 e4) ) (= ?cvc_31 e5) )) (or (or (or (or (or (= ?cvc_32 e0) (= ?cvc_32 e1) ) (= ?cvc_32 e2) ) (= ?cvc_32 e3) ) (= ?cvc_32 e4) ) (= ?cvc_32 e5) )) (or (or (or (or (or (= ?cvc_33 e0) (= ?cvc_33 e1) ) (= ?cvc_33 e2) ) (= ?cvc_33 e3) ) (= ?cvc_33 e4) ) (= ?cvc_33 e5) )) (or (or (or (or (or (= ?cvc_34 e0) (= ?cvc_34 e1) ) (= ?cvc_34 e2) ) (= ?cvc_34 e3) ) (= ?cvc_34 e4) ) (= ?cvc_34 e5) )) (or (or (or (or (or (= ?cvc_35 e0) (= ?cvc_35 e1) ) (= ?cvc_35 e2) ) (= ?cvc_35 e3) ) (= ?cvc_35 e4) ) (= ?cvc_35 e5) )))))))))))))))))))))))))))))))))))))))
:assumption
(let (?cvc_1 (op e0 e0)) (flet ($cvc_0 (= ?cvc_1 e0)) (flet ($cvc_7 (= ?cvc_1 e1)) (flet ($cvc_13 (= ?cvc_1 e2)) (flet ($cvc_14 (= ?cvc_1 e3)) (flet ($cvc_15 (= ?cvc_1 e4)) (flet ($cvc_16 (= ?cvc_1 e5)) (let (?cvc_2 (op e0 e1)) (flet ($cvc_18 (= ?cvc_2 e0)) (flet ($cvc_26 (= ?cvc_2 e1)) (flet ($cvc_33 (= ?cvc_2 e2)) (flet ($cvc_36 (= ?cvc_2 e3)) (flet ($cvc_39 (= ?cvc_2 e4)) (flet ($cvc_42 (= ?cvc_2 e5)) (let (?cvc_3 (op e0 e2)) (flet ($cvc_46 (= ?cvc_3 e0)) (flet ($cvc_55 (= ?cvc_3 e1)) (flet ($cvc_63 (= ?cvc_3 e2)) (flet ($cvc_68 (= ?cvc_3 e3)) (flet ($cvc_73 (= ?cvc_3 e4)) (flet ($cvc_78 (= ?cvc_3 e5)) (let (?cvc_4 (op e0 e3)) (flet ($cvc_84 (= ?cvc_4 e0)) (flet ($cvc_94 (= ?cvc_4 e1)) (flet ($cvc_103 (= ?cvc_4 e2)) (flet ($cvc_110 (= ?cvc_4 e3)) (flet ($cvc_117 (= ?cvc_4 e4)) (flet ($cvc_124 (= ?cvc_4 e5)) (let (?cvc_5 (op e0 e4)) (flet ($cvc_132 (= ?cvc_5 e0)) (flet ($cvc_143 (= ?cvc_5 e1)) (flet ($cvc_153 (= ?cvc_5 e2)) (flet ($cvc_162 (= ?cvc_5 e3)) (flet ($cvc_171 (= ?cvc_5 e4)) (flet ($cvc_180 (= ?cvc_5 e5)) (let (?cvc_6 (op e0 e5)) (flet ($cvc_190 (= ?cvc_6 e0)) (flet ($cvc_202 (= ?cvc_6 e1)) (flet ($cvc_213 (= ?cvc_6 e2)) (flet ($cvc_224 (= ?cvc_6 e3)) (flet ($cvc_235 (= ?cvc_6 e4)) (flet ($cvc_246 (= ?cvc_6 e5)) (let (?cvc_8 (op e1 e0)) (flet ($cvc_17 (= ?cvc_8 e0)) (flet ($cvc_20 (= ?cvc_8 e1)) (flet ($cvc_32 (= ?cvc_8 e2)) (flet ($cvc_35 (= ?cvc_8 e3)) (flet ($cvc_38 (= ?cvc_8 e4)) (flet ($cvc_41 (= ?cvc_8 e5)) (let (?cvc_21 (op e1 e1)) (flet ($cvc_19 (= ?cvc_21 e0)) (flet ($cvc_27 (= ?cvc_21 e1)) (flet ($cvc_34 (= ?cvc_21 e2)) (flet ($cvc_37 (= ?cvc_21 e3)) (flet ($cvc_40 (= ?cvc_21 e4)) (flet ($cvc_43 (= ?cvc_21 e5)) (let (?cvc_22 (op e1 e2)) (flet ($cvc_47 (= ?cvc_22 e0)) (flet ($cvc_56 (= ?cvc_22 e1)) (flet ($cvc_64 (= ?cvc_22 e2)) (flet ($cvc_69 (= ?cvc_22 e3)) (flet ($cvc_74 (= ?cvc_22 e4)) (flet ($cvc_79 (= ?cvc_22 e5)) (let (?cvc_23 (op e1 e3)) (flet ($cvc_85 (= ?cvc_23 e0)) (flet ($cvc_95 (= ?cvc_23 e1)) (flet ($cvc_104 (= ?cvc_23 e2)) (flet ($cvc_111 (= ?cvc_23 e3)) (flet ($cvc_118 (= ?cvc_23 e4)) (flet ($cvc_125 (= ?cvc_23 e5)) (let (?cvc_24 (op e1 e4)) (flet ($cvc_133 (= ?cvc_24 e0)) (flet ($cvc_144 (= ?cvc_24 e1)) (flet ($cvc_154 (= ?cvc_24 e2)) (flet ($cvc_163 (= ?cvc_24 e3)) (flet ($cvc_172 (= ?cvc_24 e4)) (flet ($cvc_181 (= ?cvc_24 e5)) (let (?cvc_25 (op e1 e5)) (flet ($cvc_191 (= ?cvc_25 e0)) (flet ($cvc_203 (= ?cvc_25 e1)) (flet ($cvc_214 (= ?cvc_25 e2)) (flet ($cvc_225 (= ?cvc_25 e3)) (flet ($cvc_236 (= ?cvc_25 e4)) (flet ($cvc_247 (= ?cvc_25 e5)) (let (?cvc_9 (op e2 e0)) (flet ($cvc_44 (= ?cvc_9 e0)) (flet ($cvc_49 (= ?cvc_9 e1)) (flet ($cvc_61 (= ?cvc_9 e2)) (flet ($cvc_66 (= ?cvc_9 e3)) (flet ($cvc_71 (= ?cvc_9 e4)) (flet ($cvc_76 (= ?cvc_9 e5)) (let (?cvc_28 (op e2 e1)) (flet ($cvc_45 (= ?cvc_28 e0)) (flet ($cvc_50 (= ?cvc_28 e1)) (flet ($cvc_62 (= ?cvc_28 e2)) (flet ($cvc_67 (= ?cvc_28 e3)) (flet ($cvc_72 (= ?cvc_28 e4)) (flet ($cvc_77 (= ?cvc_28 e5)) (let (?cvc_51 (op e2 e2)) (flet ($cvc_48 (= ?cvc_51 e0)) (flet ($cvc_57 (= ?cvc_51 e1)) (flet ($cvc_65 (= ?cvc_51 e2)) (flet ($cvc_70 (= ?cvc_51 e3)) (flet ($cvc_75 (= ?cvc_51 e4)) (flet ($cvc_80 (= ?cvc_51 e5)) (let (?cvc_52 (op e2 e3)) (flet ($cvc_86 (= ?cvc_52 e0)) (flet ($cvc_96 (= ?cvc_52 e1)) (flet ($cvc_105 (= ?cvc_52 e2)) (flet ($cvc_112 (= ?cvc_52 e3)) (flet ($cvc_119 (= ?cvc_52 e4)) (flet ($cvc_126 (= ?cvc_52 e5)) (let (?cvc_53 (op e2 e4)) (flet ($cvc_134 (= ?cvc_53 e0)) (flet ($cvc_145 (= ?cvc_53 e1)) (flet ($cvc_155 (= ?cvc_53 e2)) (flet ($cvc_164 (= ?cvc_53 e3)) (flet ($cvc_173 (= ?cvc_53 e4)) (flet ($cvc_182 (= ?cvc_53 e5)) (let (?cvc_54 (op e2 e5)) (flet ($cvc_192 (= ?cvc_54 e0)) (flet ($cvc_204 (= ?cvc_54 e1)) (flet ($cvc_215 (= ?cvc_54 e2)) (flet ($cvc_226 (= ?cvc_54 e3)) (flet ($cvc_237 (= ?cvc_54 e4)) (flet ($cvc_248 (= ?cvc_54 e5)) (let (?cvc_10 (op e3 e0)) (flet ($cvc_81 (= ?cvc_10 e0)) (flet ($cvc_88 (= ?cvc_10 e1)) (flet ($cvc_100 (= ?cvc_10 e2)) (flet ($cvc_107 (= ?cvc_10 e3)) (flet ($cvc_114 (= ?cvc_10 e4)) (flet ($cvc_121 (= ?cvc_10 e5)) (let (?cvc_29 (op e3 e1)) (flet ($cvc_82 (= ?cvc_29 e0)) (flet ($cvc_89 (= ?cvc_29 e1)) (flet ($cvc_101 (= ?cvc_29 e2)) (flet ($cvc_108 (= ?cvc_29 e3)) (flet ($cvc_115 (= ?cvc_29 e4)) (flet ($cvc_122 (= ?cvc_29 e5)) (let (?cvc_58 (op e3 e2)) (flet ($cvc_83 (= ?cvc_58 e0)) (flet ($cvc_90 (= ?cvc_58 e1)) (flet ($cvc_102 (= ?cvc_58 e2)) (flet ($cvc_109 (= ?cvc_58 e3)) (flet ($cvc_116 (= ?cvc_58 e4)) (flet ($cvc_123 (= ?cvc_58 e5)) (let (?cvc_91 (op e3 e3)) (flet ($cvc_87 (= ?cvc_91 e0)) (flet ($cvc_97 (= ?cvc_91 e1)) (flet ($cvc_106 (= ?cvc_91 e2)) (flet ($cvc_113 (= ?cvc_91 e3)) (flet ($cvc_120 (= ?cvc_91 e4)) (flet ($cvc_127 (= ?cvc_91 e5)) (let (?cvc_92 (op e3 e4)) (flet ($cvc_135 (= ?cvc_92 e0)) (flet ($cvc_146 (= ?cvc_92 e1)) (flet ($cvc_156 (= ?cvc_92 e2)) (flet ($cvc_165 (= ?cvc_92 e3)) (flet ($cvc_174 (= ?cvc_92 e4)) (flet ($cvc_183 (= ?cvc_92 e5)) (let (?cvc_93 (op e3 e5)) (flet ($cvc_193 (= ?cvc_93 e0)) (flet ($cvc_205 (= ?cvc_93 e1)) (flet ($cvc_216 (= ?cvc_93 e2)) (flet ($cvc_227 (= ?cvc_93 e3)) (flet ($cvc_238 (= ?cvc_93 e4)) (flet ($cvc_249 (= ?cvc_93 e5)) (let (?cvc_11 (op e4 e0)) (flet ($cvc_128 (= ?cvc_11 e0)) (flet ($cvc_137 (= ?cvc_11 e1)) (flet ($cvc_149 (= ?cvc_11 e2)) (flet ($cvc_158 (= ?cvc_11 e3)) (flet ($cvc_167 (= ?cvc_11 e4)) (flet ($cvc_176 (= ?cvc_11 e5)) (let (?cvc_30 (op e4 e1)) (flet ($cvc_129 (= ?cvc_30 e0)) (flet ($cvc_138 (= ?cvc_30 e1)) (flet ($cvc_150 (= ?cvc_30 e2)) (flet ($cvc_159 (= ?cvc_30 e3)) (flet ($cvc_168 (= ?cvc_30 e4)) (flet ($cvc_177 (= ?cvc_30 e5)) (let (?cvc_59 (op e4 e2)) (flet ($cvc_130 (= ?cvc_59 e0)) (flet ($cvc_139 (= ?cvc_59 e1)) (flet ($cvc_151 (= ?cvc_59 e2)) (flet ($cvc_160 (= ?cvc_59 e3)) (flet ($cvc_169 (= ?cvc_59 e4)) (flet ($cvc_178 (= ?cvc_59 e5)) (let (?cvc_98 (op e4 e3)) (flet ($cvc_131 (= ?cvc_98 e0)) (flet ($cvc_140 (= ?cvc_98 e1)) (flet ($cvc_152 (= ?cvc_98 e2)) (flet ($cvc_161 (= ?cvc_98 e3)) (flet ($cvc_170 (= ?cvc_98 e4)) (flet ($cvc_179 (= ?cvc_98 e5)) (let (?cvc_141 (op e4 e4)) (flet ($cvc_136 (= ?cvc_141 e0)) (flet ($cvc_147 (= ?cvc_141 e1)) (flet ($cvc_157 (= ?cvc_141 e2)) (flet ($cvc_166 (= ?cvc_141 e3)) (flet ($cvc_175 (= ?cvc_141 e4)) (flet ($cvc_184 (= ?cvc_141 e5)) (let (?cvc_142 (op e4 e5)) (flet ($cvc_194 (= ?cvc_142 e0)) (flet ($cvc_206 (= ?cvc_142 e1)) (flet ($cvc_217 (= ?cvc_142 e2)) (flet ($cvc_228 (= ?cvc_142 e3)) (flet ($cvc_239 (= ?cvc_142 e4)) (flet ($cvc_250 (= ?cvc_142 e5)) (let (?cvc_12 (op e5 e0)) (flet ($cvc_185 (= ?cvc_12 e0)) (flet ($cvc_196 (= ?cvc_12 e1)) (flet ($cvc_208 (= ?cvc_12 e2)) (flet ($cvc_219 (= ?cvc_12 e3)) (flet ($cvc_230 (= ?cvc_12 e4)) (flet ($cvc_241 (= ?cvc_12 e5)) (let (?cvc_31 (op e5 e1)) (flet ($cvc_186 (= ?cvc_31 e0)) (flet ($cvc_197 (= ?cvc_31 e1)) (flet ($cvc_209 (= ?cvc_31 e2)) (flet ($cvc_220 (= ?cvc_31 e3)) (flet ($cvc_231 (= ?cvc_31 e4)) (flet ($cvc_242 (= ?cvc_31 e5)) (let (?cvc_60 (op e5 e2)) (flet ($cvc_187 (= ?cvc_60 e0)) (flet ($cvc_198 (= ?cvc_60 e1)) (flet ($cvc_210 (= ?cvc_60 e2)) (flet ($cvc_221 (= ?cvc_60 e3)) (flet ($cvc_232 (= ?cvc_60 e4)) (flet ($cvc_243 (= ?cvc_60 e5)) (let (?cvc_99 (op e5 e3)) (flet ($cvc_188 (= ?cvc_99 e0)) (flet ($cvc_199 (= ?cvc_99 e1)) (flet ($cvc_211 (= ?cvc_99 e2)) (flet ($cvc_222 (= ?cvc_99 e3)) (flet ($cvc_233 (= ?cvc_99 e4)) (flet ($cvc_244 (= ?cvc_99 e5)) (let (?cvc_148 (op e5 e4)) (flet ($cvc_189 (= ?cvc_148 e0)) (flet ($cvc_200 (= ?cvc_148 e1)) (flet ($cvc_212 (= ?cvc_148 e2)) (flet ($cvc_223 (= ?cvc_148 e3)) (flet ($cvc_234 (= ?cvc_148 e4)) (flet ($cvc_245 (= ?cvc_148 e5)) (let (?cvc_201 (op e5 e5)) (flet ($cvc_195 (= ?cvc_201 e0)) (flet ($cvc_207 (= ?cvc_201 e1)) (flet ($cvc_218 (= ?cvc_201 e2)) (flet ($cvc_229 (= ?cvc_201 e3)) (flet ($cvc_240 (= ?cvc_201 e4)) (flet ($cvc_251 (= ?cvc_201 e5)) (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or $cvc_0 $cvc_18 ) $cvc_46 ) $cvc_84 ) $cvc_132 ) $cvc_190 ) (or (or (or (or (or $cvc_0 $cvc_17 ) $cvc_44 ) $cvc_81 ) $cvc_128 ) $cvc_185 )) (and (or (or (or (or (or $cvc_7 $cvc_26 ) $cvc_55 ) $cvc_94 ) $cvc_143 ) $cvc_202 ) (or (or (or (or (or $cvc_7 $cvc_20 ) $cvc_49 ) $cvc_88 ) $cvc_137 ) $cvc_196 ))) (and (or (or (or (or (or $cvc_13 $cvc_33 ) $cvc_63 ) $cvc_103 ) $cvc_153 ) $cvc_213 ) (or (or (or (or (or $cvc_13 $cvc_32 ) $cvc_61 ) $cvc_100 ) $cvc_149 ) $cvc_208 ))) (and (or (or (or (or (or $cvc_14 $cvc_36 ) $cvc_68 ) $cvc_110 ) $cvc_162 ) $cvc_224 ) (or (or (or (or (or $cvc_14 $cvc_35 ) $cvc_66 ) $cvc_107 ) $cvc_158 ) $cvc_219 ))) (and (or (or (or (or (or $cvc_15 $cvc_39 ) $cvc_73 ) $cvc_117 ) $cvc_171 ) $cvc_235 ) (or (or (or (or (or $cvc_15 $cvc_38 ) $cvc_71 ) $cvc_114 ) $cvc_167 ) $cvc_230 ))) (and (or (or (or (or (or $cvc_16 $cvc_42 ) $cvc_78 ) $cvc_124 ) $cvc_180 ) $cvc_246 ) (or (or (or (or (or $cvc_16 $cvc_41 ) $cvc_76 ) $cvc_121 ) $cvc_176 ) $cvc_241 ))) (and (and (and (and (and (and (or (or (or (or (or $cvc_17 $cvc_19 ) $cvc_47 ) $cvc_85 ) $cvc_133 ) $cvc_191 ) (or (or (or (or (or $cvc_18 $cvc_19 ) $cvc_45 ) $cvc_82 ) $cvc_129 ) $cvc_186 )) (and (or (or (or (or (or $cvc_20 $cvc_27 ) $cvc_56 ) $cvc_95 ) $cvc_144 ) $cvc_203 ) (or (or (or (or (or $cvc_26 $cvc_27 ) $cvc_50 ) $cvc_89 ) $cvc_138 ) $cvc_197 ))) (and (or (or (or (or (or $cvc_32 $cvc_34 ) $cvc_64 ) $cvc_104 ) $cvc_154 ) $cvc_214 ) (or (or (or (or (or $cvc_33 $cvc_34 ) $cvc_62 ) $cvc_101 ) $cvc_150 ) $cvc_209 ))) (and (or (or (or (or (or $cvc_35 $cvc_37 ) $cvc_69 ) $cvc_111 ) $cvc_163 ) $cvc_225 ) (or (or (or (or (or $cvc_36 $cvc_37 ) $cvc_67 ) $cvc_108 ) $cvc_159 ) $cvc_220 ))) (and (or (or (or (or (or $cvc_38 $cvc_40 ) $cvc_74 ) $cvc_118 ) $cvc_172 ) $cvc_236 ) (or (or (or (or (or $cvc_39 $cvc_40 ) $cvc_72 ) $cvc_115 ) $cvc_168 ) $cvc_231 ))) (and (or (or (or (or (or $cvc_41 $cvc_43 ) $cvc_79 ) $cvc_125 ) $cvc_181 ) $cvc_247 ) (or (or (or (or (or $cvc_42 $cvc_43 ) $cvc_77 ) $cvc_122 ) $cvc_177 ) $cvc_242 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_44 $cvc_45 ) $cvc_48 ) $cvc_86 ) $cvc_134 ) $cvc_192 ) (or (or (or (or (or $cvc_46 $cvc_47 ) $cvc_48 ) $cvc_83 ) $cvc_130 ) $cvc_187 )) (and (or (or (or (or (or $cvc_49 $cvc_50 ) $cvc_57 ) $cvc_96 ) $cvc_145 ) $cvc_204 ) (or (or (or (or (or $cvc_55 $cvc_56 ) $cvc_57 ) $cvc_90 ) $cvc_139 ) $cvc_198 ))) (and (or (or (or (or (or $cvc_61 $cvc_62 ) $cvc_65 ) $cvc_105 ) $cvc_155 ) $cvc_215 ) (or (or (or (or (or $cvc_63 $cvc_64 ) $cvc_65 ) $cvc_102 ) $cvc_151 ) $cvc_210 ))) (and (or (or (or (or (or $cvc_66 $cvc_67 ) $cvc_70 ) $cvc_112 ) $cvc_164 ) $cvc_226 ) (or (or (or (or (or $cvc_68 $cvc_69 ) $cvc_70 ) $cvc_109 ) $cvc_160 ) $cvc_221 ))) (and (or (or (or (or (or $cvc_71 $cvc_72 ) $cvc_75 ) $cvc_119 ) $cvc_173 ) $cvc_237 ) (or (or (or (or (or $cvc_73 $cvc_74 ) $cvc_75 ) $cvc_116 ) $cvc_169 ) $cvc_232 ))) (and (or (or (or (or (or $cvc_76 $cvc_77 ) $cvc_80 ) $cvc_126 ) $cvc_182 ) $cvc_248 ) (or (or (or (or (or $cvc_78 $cvc_79 ) $cvc_80 ) $cvc_123 ) $cvc_178 ) $cvc_243 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_81 $cvc_82 ) $cvc_83 ) $cvc_87 ) $cvc_135 ) $cvc_193 ) (or (or (or (or (or $cvc_84 $cvc_85 ) $cvc_86 ) $cvc_87 ) $cvc_131 ) $cvc_188 )) (and (or (or (or (or (or $cvc_88 $cvc_89 ) $cvc_90 ) $cvc_97 ) $cvc_146 ) $cvc_205 ) (or (or (or (or (or $cvc_94 $cvc_95 ) $cvc_96 ) $cvc_97 ) $cvc_140 ) $cvc_199 ))) (and (or (or (or (or (or $cvc_100 $cvc_101 ) $cvc_102 ) $cvc_106 ) $cvc_156 ) $cvc_216 ) (or (or (or (or (or $cvc_103 $cvc_104 ) $cvc_105 ) $cvc_106 ) $cvc_152 ) $cvc_211 ))) (and (or (or (or (or (or $cvc_107 $cvc_108 ) $cvc_109 ) $cvc_113 ) $cvc_165 ) $cvc_227 ) (or (or (or (or (or $cvc_110 $cvc_111 ) $cvc_112 ) $cvc_113 ) $cvc_161 ) $cvc_222 ))) (and (or (or (or (or (or $cvc_114 $cvc_115 ) $cvc_116 ) $cvc_120 ) $cvc_174 ) $cvc_238 ) (or (or (or (or (or $cvc_117 $cvc_118 ) $cvc_119 ) $cvc_120 ) $cvc_170 ) $cvc_233 ))) (and (or (or (or (or (or $cvc_121 $cvc_122 ) $cvc_123 ) $cvc_127 ) $cvc_183 ) $cvc_249 ) (or (or (or (or (or $cvc_124 $cvc_125 ) $cvc_126 ) $cvc_127 ) $cvc_179 ) $cvc_244 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_128 $cvc_129 ) $cvc_130 ) $cvc_131 ) $cvc_136 ) $cvc_194 ) (or (or (or (or (or $cvc_132 $cvc_133 ) $cvc_134 ) $cvc_135 ) $cvc_136 ) $cvc_189 )) (and (or (or (or (or (or $cvc_137 $cvc_138 ) $cvc_139 ) $cvc_140 ) $cvc_147 ) $cvc_206 ) (or (or (or (or (or $cvc_143 $cvc_144 ) $cvc_145 ) $cvc_146 ) $cvc_147 ) $cvc_200 ))) (and (or (or (or (or (or $cvc_149 $cvc_150 ) $cvc_151 ) $cvc_152 ) $cvc_157 ) $cvc_217 ) (or (or (or (or (or $cvc_153 $cvc_154 ) $cvc_155 ) $cvc_156 ) $cvc_157 ) $cvc_212 ))) (and (or (or (or (or (or $cvc_158 $cvc_159 ) $cvc_160 ) $cvc_161 ) $cvc_166 ) $cvc_228 ) (or (or (or (or (or $cvc_162 $cvc_163 ) $cvc_164 ) $cvc_165 ) $cvc_166 ) $cvc_223 ))) (and (or (or (or (or (or $cvc_167 $cvc_168 ) $cvc_169 ) $cvc_170 ) $cvc_175 ) $cvc_239 ) (or (or (or (or (or $cvc_171 $cvc_172 ) $cvc_173 ) $cvc_174 ) $cvc_175 ) $cvc_234 ))) (and (or (or (or (or (or $cvc_176 $cvc_177 ) $cvc_178 ) $cvc_179 ) $cvc_184 ) $cvc_250 ) (or (or (or (or (or $cvc_180 $cvc_181 ) $cvc_182 ) $cvc_183 ) $cvc_184 ) $cvc_245 )))) (and (and (and (and (and (and (or (or (or (or (or $cvc_185 $cvc_186 ) $cvc_187 ) $cvc_188 ) $cvc_189 ) $cvc_195 ) (or (or (or (or (or $cvc_190 $cvc_191 ) $cvc_192 ) $cvc_193 ) $cvc_194 ) $cvc_195 )) (and (or (or (or (or (or $cvc_196 $cvc_197 ) $cvc_198 ) $cvc_199 ) $cvc_200 ) $cvc_207 ) (or (or (or (or (or $cvc_202 $cvc_203 ) $cvc_204 ) $cvc_205 ) $cvc_206 ) $cvc_207 ))) (and (or (or (or (or (or $cvc_208 $cvc_209 ) $cvc_210 ) $cvc_211 ) $cvc_212 ) $cvc_218 ) (or (or (or (or (or $cvc_213 $cvc_214 ) $cvc_215 ) $cvc_216 ) $cvc_217 ) $cvc_218 ))) (and (or (or (or (or (or $cvc_219 $cvc_220 ) $cvc_221 ) $cvc_222 ) $cvc_223 ) $cvc_229 ) (or (or (or (or (or $cvc_224 $cvc_225 ) $cvc_226 ) $cvc_227 ) $cvc_228 ) $cvc_229 ))) (and (or (or (or (or (or $cvc_230 $cvc_231 ) $cvc_232 ) $cvc_233 ) $cvc_234 ) $cvc_240 ) (or (or (or (or (or $cvc_235 $cvc_236 ) $cvc_237 ) $cvc_238 ) $cvc_239 ) $cvc_240 ))) (and (or (or (or (or (or $cvc_241 $cvc_242 ) $cvc_243 ) $cvc_244 ) $cvc_245 ) $cvc_251 ) (or (or (or (or (or $cvc_246 $cvc_247 ) $cvc_248 ) $cvc_249 ) $cvc_250 ) $cvc_251 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
:assumption
(let (?cvc_0 (op e0 e0)) (let (?cvc_1 (op e0 e1)) (let (?cvc_4 (op e0 e2)) (let (?cvc_9 (op e0 e3)) (let (?cvc_16 (op e0 e4)) (let (?cvc_25 (op e0 e5)) (let (?cvc_2 (op e1 e0)) (let (?cvc_3 (op e1 e1)) (let (?cvc_6 (op e1 e2)) (let (?cvc_11 (op e1 e3)) (let (?cvc_18 (op e1 e4)) (let (?cvc_27 (op e1 e5)) (let (?cvc_5 (op e2 e0)) (let (?cvc_7 (op e2 e1)) (let (?cvc_8 (op e2 e2)) (let (?cvc_13 (op e2 e3)) (let (?cvc_20 (op e2 e4)) (let (?cvc_29 (op e2 e5)) (let (?cvc_10 (op e3 e0)) (let (?cvc_12 (op e3 e1)) (let (?cvc_14 (op e3 e2)) (let (?cvc_15 (op e3 e3)) (let (?cvc_22 (op e3 e4)) (let (?cvc_31 (op e3 e5)) (let (?cvc_17 (op e4 e0)) (let (?cvc_19 (op e4 e1)) (let (?cvc_21 (op e4 e2)) (let (?cvc_23 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (let (?cvc_33 (op e4 e5)) (let (?cvc_26 (op e5 e0)) (let (?cvc_28 (op e5 e1)) (let (?cvc_30 (op e5 e2)) (let (?cvc_32 (op e5 e3)) (let (?cvc_34 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (or (or (or (or (or (and (and (and (and (and (= (op ?cvc_0 ?cvc_0) e0) (= (op ?cvc_2 ?cvc_1) e1)) (= (op ?cvc_5 ?cvc_4) e2)) (= (op ?cvc_10 ?cvc_9) e3)) (= (op ?cvc_17 ?cvc_16) e4)) (= (op ?cvc_26 ?cvc_25) e5)) (and (and (and (and (and (= (op ?cvc_1 ?cvc_2) e0) (= (op ?cvc_3 ?cvc_3) e1)) (= (op ?cvc_7 ?cvc_6) e2)) (= (op ?cvc_12 ?cvc_11) e3)) (= (op ?cvc_19 ?cvc_18) e4)) (= (op ?cvc_28 ?cvc_27) e5)) ) (and (and (and (and (and (= (op ?cvc_4 ?cvc_5) e0) (= (op ?cvc_6 ?cvc_7) e1)) (= (op ?cvc_8 ?cvc_8) e2)) (= (op ?cvc_14 ?cvc_13) e3)) (= (op ?cvc_21 ?cvc_20) e4)) (= (op ?cvc_30 ?cvc_29) e5)) ) (and (and (and (and (and (= (op ?cvc_9 ?cvc_10) e0) (= (op ?cvc_11 ?cvc_12) e1)) (= (op ?cvc_13 ?cvc_14) e2)) (= (op ?cvc_15 ?cvc_15) e3)) (= (op ?cvc_23 ?cvc_22) e4)) (= (op ?cvc_32 ?cvc_31) e5)) ) (and (and (and (and (and (= (op ?cvc_16 ?cvc_17) e0) (= (op ?cvc_18 ?cvc_19) e1)) (= (op ?cvc_20 ?cvc_21) e2)) (= (op ?cvc_22 ?cvc_23) e3)) (= (op ?cvc_24 ?cvc_24) e4)) (= (op ?cvc_34 ?cvc_33) e5)) ) (and (and (and (and (and (= (op ?cvc_25 ?cvc_26) e0) (= (op ?cvc_27 ?cvc_28) e1)) (= (op ?cvc_29 ?cvc_30) e2)) (= (op ?cvc_31 ?cvc_32) e3)) (= (op ?cvc_33 ?cvc_34) e4)) (= (op ?cvc_35 ?cvc_35) e5)) )))))))))))))))))))))))))))))))))))))
:assumption
(and (and (and (and (and (not (= (op e0 e0) e0)) (not (= (op e1 e1) e1))) (not (= (op e2 e2) e2))) (not (= (op e3 e3) e3))) (not (= (op e4 e4) e4))) (not (= (op e5 e5) e5)))
:assumption
(let (?cvc_0 (op e0 e0)) (let (?cvc_6 (op e0 e1)) (let (?cvc_12 (op e0 e2)) (let (?cvc_18 (op e0 e3)) (let (?cvc_24 (op e0 e4)) (let (?cvc_30 (op e0 e5)) (let (?cvc_1 (op e1 e0)) (let (?cvc_7 (op e1 e1)) (let (?cvc_13 (op e1 e2)) (let (?cvc_19 (op e1 e3)) (let (?cvc_25 (op e1 e4)) (let (?cvc_31 (op e1 e5)) (let (?cvc_2 (op e2 e0)) (let (?cvc_8 (op e2 e1)) (let (?cvc_14 (op e2 e2)) (let (?cvc_20 (op e2 e3)) (let (?cvc_26 (op e2 e4)) (let (?cvc_32 (op e2 e5)) (let (?cvc_3 (op e3 e0)) (let (?cvc_9 (op e3 e1)) (let (?cvc_15 (op e3 e2)) (let (?cvc_21 (op e3 e3)) (let (?cvc_27 (op e3 e4)) (let (?cvc_33 (op e3 e5)) (let (?cvc_4 (op e4 e0)) (let (?cvc_10 (op e4 e1)) (let (?cvc_16 (op e4 e2)) (let (?cvc_22 (op e4 e3)) (let (?cvc_28 (op e4 e4)) (let (?cvc_34 (op e4 e5)) (let (?cvc_5 (op e5 e0)) (let (?cvc_11 (op e5 e1)) (let (?cvc_17 (op e5 e2)) (let (?cvc_23 (op e5 e3)) (let (?cvc_29 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (or (or (or (or (or (and (and (and (and (and (not (= (op ?cvc_0 e0) ?cvc_0)) (not (= (op ?cvc_1 e1) ?cvc_1))) (not (= (op ?cvc_2 e2) ?cvc_2))) (not (= (op ?cvc_3 e3) ?cvc_3))) (not (= (op ?cvc_4 e4) ?cvc_4))) (not (= (op ?cvc_5 e5) ?cvc_5))) (and (and (and (and (and (not (= (op ?cvc_6 e0) ?cvc_6)) (not (= (op ?cvc_7 e1) ?cvc_7))) (not (= (op ?cvc_8 e2) ?cvc_8))) (not (= (op ?cvc_9 e3) ?cvc_9))) (not (= (op ?cvc_10 e4) ?cvc_10))) (not (= (op ?cvc_11 e5) ?cvc_11))) ) (and (and (and (and (and (not (= (op ?cvc_12 e0) ?cvc_12)) (not (= (op ?cvc_13 e1) ?cvc_13))) (not (= (op ?cvc_14 e2) ?cvc_14))) (not (= (op ?cvc_15 e3) ?cvc_15))) (not (= (op ?cvc_16 e4) ?cvc_16))) (not (= (op ?cvc_17 e5) ?cvc_17))) ) (and (and (and (and (and (not (= (op ?cvc_18 e0) ?cvc_18)) (not (= (op ?cvc_19 e1) ?cvc_19))) (not (= (op ?cvc_20 e2) ?cvc_20))) (not (= (op ?cvc_21 e3) ?cvc_21))) (not (= (op ?cvc_22 e4) ?cvc_22))) (not (= (op ?cvc_23 e5) ?cvc_23))) ) (and (and (and (and (and (not (= (op ?cvc_24 e0) ?cvc_24)) (not (= (op ?cvc_25 e1) ?cvc_25))) (not (= (op ?cvc_26 e2) ?cvc_26))) (not (= (op ?cvc_27 e3) ?cvc_27))) (not (= (op ?cvc_28 e4) ?cvc_28))) (not (= (op ?cvc_29 e5) ?cvc_29))) ) (and (and (and (and (and (not (= (op ?cvc_30 e0) ?cvc_30)) (not (= (op ?cvc_31 e1) ?cvc_31))) (not (= (op ?cvc_32 e2) ?cvc_32))) (not (= (op ?cvc_33 e3) ?cvc_33))) (not (= (op ?cvc_34 e4) ?cvc_34))) (not (= (op ?cvc_35 e5) ?cvc_35))) )))))))))))))))))))))))))))))))))))))
:assumption
(and (and (and (and (and (or (or (or (or (or (= (op e0 (op e0 e0)) e0) (= (op e0 (op e0 e1)) e1) ) (= (op e0 (op e0 e2)) e2) ) (= (op e0 (op e0 e3)) e3) ) (= (op e0 (op e0 e4)) e4) ) (= (op e0 (op e0 e5)) e5) ) (or (or (or (or (or (= (op e1 (op e1 e0)) e0) (= (op e1 (op e1 e1)) e1) ) (= (op e1 (op e1 e2)) e2) ) (= (op e1 (op e1 e3)) e3) ) (= (op e1 (op e1 e4)) e4) ) (= (op e1 (op e1 e5)) e5) )) (or (or (or (or (or (= (op e2 (op e2 e0)) e0) (= (op e2 (op e2 e1)) e1) ) (= (op e2 (op e2 e2)) e2) ) (= (op e2 (op e2 e3)) e3) ) (= (op e2 (op e2 e4)) e4) ) (= (op e2 (op e2 e5)) e5) )) (or (or (or (or (or (= (op e3 (op e3 e0)) e0) (= (op e3 (op e3 e1)) e1) ) (= (op e3 (op e3 e2)) e2) ) (= (op e3 (op e3 e3)) e3) ) (= (op e3 (op e3 e4)) e4) ) (= (op e3 (op e3 e5)) e5) )) (or (or (or (or (or (= (op e4 (op e4 e0)) e0) (= (op e4 (op e4 e1)) e1) ) (= (op e4 (op e4 e2)) e2) ) (= (op e4 (op e4 e3)) e3) ) (= (op e4 (op e4 e4)) e4) ) (= (op e4 (op e4 e5)) e5) )) (or (or (or (or (or (= (op e5 (op e5 e0)) e0) (= (op e5 (op e5 e1)) e1) ) (= (op e5 (op e5 e2)) e2) ) (= (op e5 (op e5 e3)) e3) ) (= (op e5 (op e5 e4)) e4) ) (= (op e5 (op e5 e5)) e5) ))
:assumption
(or (or (or (or (or (= (op e0 (op e0 e0)) e0) (= (op e1 (op e1 e1)) e1) ) (= (op e2 (op e2 e2)) e2) ) (= (op e3 (op e3 e3)) e3) ) (= (op e4 (op e4 e4)) e4) ) (= (op e5 (op e5 e5)) e5) )
:assumption
(and (and (and (and (and (or (or (or (or (or (= (op (op e0 e0) e0) e0) (= (op (op e1 e0) e0) e1) ) (= (op (op e2 e0) e0) e2) ) (= (op (op e3 e0) e0) e3) ) (= (op (op e4 e0) e0) e4) ) (= (op (op e5 e0) e0) e5) ) (or (or (or (or (or (= (op (op e0 e1) e1) e0) (= (op (op e1 e1) e1) e1) ) (= (op (op e2 e1) e1) e2) ) (= (op (op e3 e1) e1) e3) ) (= (op (op e4 e1) e1) e4) ) (= (op (op e5 e1) e1) e5) )) (or (or (or (or (or (= (op (op e0 e2) e2) e0) (= (op (op e1 e2) e2) e1) ) (= (op (op e2 e2) e2) e2) ) (= (op (op e3 e2) e2) e3) ) (= (op (op e4 e2) e2) e4) ) (= (op (op e5 e2) e2) e5) )) (or (or (or (or (or (= (op (op e0 e3) e3) e0) (= (op (op e1 e3) e3) e1) ) (= (op (op e2 e3) e3) e2) ) (= (op (op e3 e3) e3) e3) ) (= (op (op e4 e3) e3) e4) ) (= (op (op e5 e3) e3) e5) )) (or (or (or (or (or (= (op (op e0 e4) e4) e0) (= (op (op e1 e4) e4) e1) ) (= (op (op e2 e4) e4) e2) ) (= (op (op e3 e4) e4) e3) ) (= (op (op e4 e4) e4) e4) ) (= (op (op e5 e4) e4) e5) )) (or (or (or (or (or (= (op (op e0 e5) e5) e0) (= (op (op e1 e5) e5) e1) ) (= (op (op e2 e5) e5) e2) ) (= (op (op e3 e5) e5) e3) ) (= (op (op e4 e5) e5) e4) ) (= (op (op e5 e5) e5) e5) ))
:assumption
(let (?cvc_0 (op e0 e0)) (let (?cvc_6 (op e0 e1)) (let (?cvc_12 (op e0 e2)) (let (?cvc_18 (op e0 e3)) (let (?cvc_24 (op e0 e4)) (let (?cvc_30 (op e0 e5)) (let (?cvc_1 (op e1 e0)) (let (?cvc_7 (op e1 e1)) (let (?cvc_13 (op e1 e2)) (let (?cvc_19 (op e1 e3)) (let (?cvc_25 (op e1 e4)) (let (?cvc_31 (op e1 e5)) (let (?cvc_2 (op e2 e0)) (let (?cvc_8 (op e2 e1)) (let (?cvc_14 (op e2 e2)) (let (?cvc_20 (op e2 e3)) (let (?cvc_26 (op e2 e4)) (let (?cvc_32 (op e2 e5)) (let (?cvc_3 (op e3 e0)) (let (?cvc_9 (op e3 e1)) (let (?cvc_15 (op e3 e2)) (let (?cvc_21 (op e3 e3)) (let (?cvc_27 (op e3 e4)) (let (?cvc_33 (op e3 e5)) (let (?cvc_4 (op e4 e0)) (let (?cvc_10 (op e4 e1)) (let (?cvc_16 (op e4 e2)) (let (?cvc_22 (op e4 e3)) (let (?cvc_28 (op e4 e4)) (let (?cvc_34 (op e4 e5)) (let (?cvc_5 (op e5 e0)) (let (?cvc_11 (op e5 e1)) (let (?cvc_17 (op e5 e2)) (let (?cvc_23 (op e5 e3)) (let (?cvc_29 (op e5 e4)) (let (?cvc_35 (op e5 e5)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_1)) (not (= ?cvc_0 ?cvc_2))) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_5))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 ?cvc_4))) (not (= ?cvc_1 ?cvc_5))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_5))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_5))) (not (= ?cvc_4 ?cvc_5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_6 ?cvc_7)) (not (= ?cvc_6 ?cvc_8))) (not (= ?cvc_6 ?cvc_9))) (not (= ?cvc_6 ?cvc_10))) (not (= ?cvc_6 ?cvc_11))) (not (= ?cvc_7 ?cvc_8))) (not (= ?cvc_7 ?cvc_9))) (not (= ?cvc_7 ?cvc_10))) (not (= ?cvc_7 ?cvc_11))) (not (= ?cvc_8 ?cvc_9))) (not (= ?cvc_8 ?cvc_10))) (not (= ?cvc_8 ?cvc_11))) (not (= ?cvc_9 ?cvc_10))) (not (= ?cvc_9 ?cvc_11))) (not (= ?cvc_10 ?cvc_11)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_12 ?cvc_13)) (not (= ?cvc_12 ?cvc_14))) (not (= ?cvc_12 ?cvc_15))) (not (= ?cvc_12 ?cvc_16))) (not (= ?cvc_12 ?cvc_17))) (not (= ?cvc_13 ?cvc_14))) (not (= ?cvc_13 ?cvc_15))) (not (= ?cvc_13 ?cvc_16))) (not (= ?cvc_13 ?cvc_17))) (not (= ?cvc_14 ?cvc_15))) (not (= ?cvc_14 ?cvc_16))) (not (= ?cvc_14 ?cvc_17))) (not (= ?cvc_15 ?cvc_16))) (not (= ?cvc_15 ?cvc_17))) (not (= ?cvc_16 ?cvc_17)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_18 ?cvc_19)) (not (= ?cvc_18 ?cvc_20))) (not (= ?cvc_18 ?cvc_21))) (not (= ?cvc_18 ?cvc_22))) (not (= ?cvc_18 ?cvc_23))) (not (= ?cvc_19 ?cvc_20))) (not (= ?cvc_19 ?cvc_21))) (not (= ?cvc_19 ?cvc_22))) (not (= ?cvc_19 ?cvc_23))) (not (= ?cvc_20 ?cvc_21))) (not (= ?cvc_20 ?cvc_22))) (not (= ?cvc_20 ?cvc_23))) (not (= ?cvc_21 ?cvc_22))) (not (= ?cvc_21 ?cvc_23))) (not (= ?cvc_22 ?cvc_23)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_24 ?cvc_25)) (not (= ?cvc_24 ?cvc_26))) (not (= ?cvc_24 ?cvc_27))) (not (= ?cvc_24 ?cvc_28))) (not (= ?cvc_24 ?cvc_29))) (not (= ?cvc_25 ?cvc_26))) (not (= ?cvc_25 ?cvc_27))) (not (= ?cvc_25 ?cvc_28))) (not (= ?cvc_25 ?cvc_29))) (not (= ?cvc_26 ?cvc_27))) (not (= ?cvc_26 ?cvc_28))) (not (= ?cvc_26 ?cvc_29))) (not (= ?cvc_27 ?cvc_28))) (not (= ?cvc_27 ?cvc_29))) (not (= ?cvc_28 ?cvc_29)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_30 ?cvc_31)) (not (= ?cvc_30 ?cvc_32))) (not (= ?cvc_30 ?cvc_33))) (not (= ?cvc_30 ?cvc_34))) (not (= ?cvc_30 ?cvc_35))) (not (= ?cvc_31 ?cvc_32))) (not (= ?cvc_31 ?cvc_33))) (not (= ?cvc_31 ?cvc_34))) (not (= ?cvc_31 ?cvc_35))) (not (= ?cvc_32 ?cvc_33))) (not (= ?cvc_32 ?cvc_34))) (not (= ?cvc_32 ?cvc_35))) (not (= ?cvc_33 ?cvc_34))) (not (= ?cvc_33 ?cvc_35))) (not (= ?cvc_34 ?cvc_35)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_6)) (not (= ?cvc_0 ?cvc_12))) (not (= ?cvc_0 ?cvc_18))) (not (= ?cvc_0 ?cvc_24))) (not (= ?cvc_0 ?cvc_30))) (not (= ?cvc_6 ?cvc_12))) (not (= ?cvc_6 ?cvc_18))) (not (= ?cvc_6 ?cvc_24))) (not (= ?cvc_6 ?cvc_30))) (not (= ?cvc_12 ?cvc_18))) (not (= ?cvc_12 ?cvc_24))) (not (= ?cvc_12 ?cvc_30))) (not (= ?cvc_18 ?cvc_24))) (not (= ?cvc_18 ?cvc_30))) (not (= ?cvc_24 ?cvc_30))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_1 ?cvc_7)) (not (= ?cvc_1 ?cvc_13))) (not (= ?cvc_1 ?cvc_19))) (not (= ?cvc_1 ?cvc_25))) (not (= ?cvc_1 ?cvc_31))) (not (= ?cvc_7 ?cvc_13))) (not (= ?cvc_7 ?cvc_19))) (not (= ?cvc_7 ?cvc_25))) (not (= ?cvc_7 ?cvc_31))) (not (= ?cvc_13 ?cvc_19))) (not (= ?cvc_13 ?cvc_25))) (not (= ?cvc_13 ?cvc_31))) (not (= ?cvc_19 ?cvc_25))) (not (= ?cvc_19 ?cvc_31))) (not (= ?cvc_25 ?cvc_31)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_2 ?cvc_8)) (not (= ?cvc_2 ?cvc_14))) (not (= ?cvc_2 ?cvc_20))) (not (= ?cvc_2 ?cvc_26))) (not (= ?cvc_2 ?cvc_32))) (not (= ?cvc_8 ?cvc_14))) (not (= ?cvc_8 ?cvc_20))) (not (= ?cvc_8 ?cvc_26))) (not (= ?cvc_8 ?cvc_32))) (not (= ?cvc_14 ?cvc_20))) (not (= ?cvc_14 ?cvc_26))) (not (= ?cvc_14 ?cvc_32))) (not (= ?cvc_20 ?cvc_26))) (not (= ?cvc_20 ?cvc_32))) (not (= ?cvc_26 ?cvc_32)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_3 ?cvc_9)) (not (= ?cvc_3 ?cvc_15))) (not (= ?cvc_3 ?cvc_21))) (not (= ?cvc_3 ?cvc_27))) (not (= ?cvc_3 ?cvc_33))) (not (= ?cvc_9 ?cvc_15))) (not (= ?cvc_9 ?cvc_21))) (not (= ?cvc_9 ?cvc_27))) (not (= ?cvc_9 ?cvc_33))) (not (= ?cvc_15 ?cvc_21))) (not (= ?cvc_15 ?cvc_27))) (not (= ?cvc_15 ?cvc_33))) (not (= ?cvc_21 ?cvc_27))) (not (= ?cvc_21 ?cvc_33))) (not (= ?cvc_27 ?cvc_33)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_4 ?cvc_10)) (not (= ?cvc_4 ?cvc_16))) (not (= ?cvc_4 ?cvc_22))) (not (= ?cvc_4 ?cvc_28))) (not (= ?cvc_4 ?cvc_34))) (not (= ?cvc_10 ?cvc_16))) (not (= ?cvc_10 ?cvc_22))) (not (= ?cvc_10 ?cvc_28))) (not (= ?cvc_10 ?cvc_34))) (not (= ?cvc_16 ?cvc_22))) (not (= ?cvc_16 ?cvc_28))) (not (= ?cvc_16 ?cvc_34))) (not (= ?cvc_22 ?cvc_28))) (not (= ?cvc_22 ?cvc_34))) (not (= ?cvc_28 ?cvc_34)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_5 ?cvc_11)) (not (= ?cvc_5 ?cvc_17))) (not (= ?cvc_5 ?cvc_23))) (not (= ?cvc_5 ?cvc_29))) (not (= ?cvc_5 ?cvc_35))) (not (= ?cvc_11 ?cvc_17))) (not (= ?cvc_11 ?cvc_23))) (not (= ?cvc_11 ?cvc_29))) (not (= ?cvc_11 ?cvc_35))) (not (= ?cvc_17 ?cvc_23))) (not (= ?cvc_17 ?cvc_29))) (not (= ?cvc_17 ?cvc_35))) (not (= ?cvc_23 ?cvc_29))) (not (= ?cvc_23 ?cvc_35))) (not (= ?cvc_29 ?cvc_35)))))))))))))))))))))))))))))))))))))))))
:assumption
(and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e0 e5))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e1 e5))) (not (= e2 e3))) (not (= e2 e4))) (not (= e2 e5))) (not (= e3 e4))) (not (= e3 e5))) (not (= e4 e5)))
:assumption
(let (?cvc_0 (op e5 e5)) (let (?cvc_3 (op e5 ?cvc_0)) (let (?cvc_1 (op e5 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e5 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e5 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e5))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e5))) (= e5 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e5 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e5))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e5 ?cvc_4))) (= e5 (op e5 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e5 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e5))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e5 (op ?cvc_1 e5))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e5))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e5))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e5))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e5 ?cvc_0))) (not (= e5 ?cvc_2))) (not (= e5 ?cvc_3))) (not (= e5 ?cvc_4))) (not (= e5 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e5))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e5))) (not (= ?cvc_1 ?cvc_4))))))))))
:assumption
(let (?cvc_0 (op e4 e4)) (let (?cvc_3 (op e4 ?cvc_0)) (let (?cvc_1 (op e4 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e4 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e4 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e4))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e4))) (= e4 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e4 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e4))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e4 ?cvc_4))) (= e4 (op e4 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e4 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e4))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e4 (op ?cvc_1 e4))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e4))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e4))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e4))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e4 ?cvc_0))) (not (= e4 ?cvc_2))) (not (= e4 ?cvc_3))) (not (= e4 ?cvc_4))) (not (= e4 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e4))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e4))) (not (= ?cvc_1 ?cvc_4))))))))))
:assumption
(let (?cvc_0 (op e3 e3)) (let (?cvc_3 (op e3 ?cvc_0)) (let (?cvc_1 (op e3 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e3 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e3 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e3))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e3))) (= e3 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e3 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e3))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e3 ?cvc_4))) (= e3 (op e3 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e3 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e3))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e3 (op ?cvc_1 e3))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e3))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e3))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e3 ?cvc_0))) (not (= e3 ?cvc_2))) (not (= e3 ?cvc_3))) (not (= e3 ?cvc_4))) (not (= e3 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e3))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e3))) (not (= ?cvc_1 ?cvc_4))))))))))
:assumption
(let (?cvc_0 (op e2 e2)) (let (?cvc_3 (op e2 ?cvc_0)) (let (?cvc_1 (op e2 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e2 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e2 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e2))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e2))) (= e2 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e2 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e2))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e2 ?cvc_4))) (= e2 (op e2 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e2 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e2))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e2 (op ?cvc_1 e2))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e2))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e2))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e2))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e2 ?cvc_0))) (not (= e2 ?cvc_2))) (not (= e2 ?cvc_3))) (not (= e2 ?cvc_4))) (not (= e2 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e2))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e2))) (not (= ?cvc_1 ?cvc_4))))))))))
:assumption
(let (?cvc_0 (op e1 e1)) (let (?cvc_3 (op e1 ?cvc_0)) (let (?cvc_1 (op e1 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e1 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e1 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e1))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e1))) (= e1 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e1 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e1))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e1 ?cvc_4))) (= e1 (op e1 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e1 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e1))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e1 (op ?cvc_1 e1))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e1))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e1))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e1))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e1 ?cvc_0))) (not (= e1 ?cvc_2))) (not (= e1 ?cvc_3))) (not (= e1 ?cvc_4))) (not (= e1 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e1))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e1))) (not (= ?cvc_1 ?cvc_4))))))))))
:assumption
(let (?cvc_0 (op e0 e0)) (let (?cvc_3 (op e0 ?cvc_0)) (let (?cvc_1 (op e0 ?cvc_3)) (let (?cvc_2 (op ?cvc_1 ?cvc_1)) (let (?cvc_4 (op e0 ?cvc_2)) (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= e0 (op ?cvc_0 ?cvc_0)) (= ?cvc_2 (op ?cvc_0 ?cvc_2))) (= ?cvc_4 (op ?cvc_0 ?cvc_3))) (= ?cvc_3 (op ?cvc_0 e0))) (= ?cvc_1 (op ?cvc_0 ?cvc_4))) (= ?cvc_0 (op ?cvc_0 ?cvc_1))) (= ?cvc_0 (op ?cvc_2 ?cvc_0))) (= ?cvc_3 (op ?cvc_2 ?cvc_2))) (= ?cvc_2 (op ?cvc_2 ?cvc_3))) (= ?cvc_1 (op ?cvc_2 e0))) (= e0 (op ?cvc_2 ?cvc_4))) (= ?cvc_4 (op ?cvc_2 ?cvc_1))) (= ?cvc_4 (op ?cvc_3 ?cvc_0))) (= ?cvc_1 (op ?cvc_3 ?cvc_2))) (= e0 (op ?cvc_3 ?cvc_3))) (= ?cvc_2 (op ?cvc_3 e0))) (= ?cvc_0 (op ?cvc_3 ?cvc_4))) (= ?cvc_3 (op ?cvc_3 ?cvc_1))) (= ?cvc_3 ?cvc_3)) (= ?cvc_4 ?cvc_4)) (= ?cvc_1 ?cvc_1)) (= ?cvc_0 ?cvc_0)) (= ?cvc_2 (op e0 ?cvc_4))) (= e0 (op e0 ?cvc_1))) (= ?cvc_2 (op ?cvc_4 ?cvc_0))) (= e0 (op ?cvc_4 ?cvc_2))) (= ?cvc_0 (op ?cvc_4 ?cvc_3))) (= ?cvc_4 (op ?cvc_4 e0))) (= ?cvc_3 (op ?cvc_4 ?cvc_4))) (= ?cvc_1 (op ?cvc_4 ?cvc_1))) (= ?cvc_1 (op ?cvc_1 ?cvc_0))) (= ?cvc_0 (op ?cvc_1 ?cvc_2))) (= ?cvc_3 (op ?cvc_1 ?cvc_3))) (= e0 (op ?cvc_1 e0))) (= ?cvc_4 (op ?cvc_1 ?cvc_4))) (= ?cvc_2 ?cvc_2)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_2)) (not (= ?cvc_0 ?cvc_3))) (not (= ?cvc_0 e0))) (not (= ?cvc_0 ?cvc_4))) (not (= ?cvc_0 ?cvc_1))) (not (= ?cvc_2 ?cvc_0))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 e0))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_2 ?cvc_1))) (not (= ?cvc_3 ?cvc_0))) (not (= ?cvc_3 ?cvc_2))) (not (= ?cvc_3 e0))) (not (= ?cvc_3 ?cvc_4))) (not (= ?cvc_3 ?cvc_1))) (not (= e0 ?cvc_0))) (not (= e0 ?cvc_2))) (not (= e0 ?cvc_3))) (not (= e0 ?cvc_4))) (not (= e0 ?cvc_1))) (not (= ?cvc_4 ?cvc_0))) (not (= ?cvc_4 ?cvc_2))) (not (= ?cvc_4 ?cvc_3))) (not (= ?cvc_4 e0))) (not (= ?cvc_4 ?cvc_1))) (not (= ?cvc_1 ?cvc_0))) (not (= ?cvc_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 e0))) (not (= ?cvc_1 ?cvc_4))))))))))
:formula
(not false)
)
|
