blob: db1efdfcef7d4e1906b70939366ea96fd29ae3e6 (
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
|
(benchmark iso_brn001.smt
:source {
http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
}
:status sat
:difficulty { 0 }
:category { crafted }
:logic QF_UF
:extrasorts (I)
:extrafuns ((op1 I I I))
:extrafuns ((op I I 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 e1 e0)) (let (?cvc_6 (op e1 e1)) (let (?cvc_7 (op e1 e2)) (let (?cvc_8 (op e1 e3)) (let (?cvc_9 (op e1 e4)) (let (?cvc_10 (op e2 e0)) (let (?cvc_11 (op e2 e1)) (let (?cvc_12 (op e2 e2)) (let (?cvc_13 (op e2 e3)) (let (?cvc_14 (op e2 e4)) (let (?cvc_15 (op e3 e0)) (let (?cvc_16 (op e3 e1)) (let (?cvc_17 (op e3 e2)) (let (?cvc_18 (op e3 e3)) (let (?cvc_19 (op e3 e4)) (let (?cvc_20 (op e4 e0)) (let (?cvc_21 (op e4 e1)) (let (?cvc_22 (op e4 e2)) (let (?cvc_23 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (and (and (and (and (and (and (and (and (or (or (or (or (= ?cvc_0 e0) (= ?cvc_0 e1) ) (= ?cvc_0 e2) ) (= ?cvc_0 e3) ) (= ?cvc_0 e4) ) (or (or (or (or (= ?cvc_1 e0) (= ?cvc_1 e1) ) (= ?cvc_1 e2) ) (= ?cvc_1 e3) ) (= ?cvc_1 e4) )) (or (or (or (or (= ?cvc_2 e0) (= ?cvc_2 e1) ) (= ?cvc_2 e2) ) (= ?cvc_2 e3) ) (= ?cvc_2 e4) )) (or (or (or (or (= ?cvc_3 e0) (= ?cvc_3 e1) ) (= ?cvc_3 e2) ) (= ?cvc_3 e3) ) (= ?cvc_3 e4) )) (or (or (or (or (= ?cvc_4 e0) (= ?cvc_4 e1) ) (= ?cvc_4 e2) ) (= ?cvc_4 e3) ) (= ?cvc_4 e4) )) (and (and (and (and (or (or (or (or (= ?cvc_5 e0) (= ?cvc_5 e1) ) (= ?cvc_5 e2) ) (= ?cvc_5 e3) ) (= ?cvc_5 e4) ) (or (or (or (or (= ?cvc_6 e0) (= ?cvc_6 e1) ) (= ?cvc_6 e2) ) (= ?cvc_6 e3) ) (= ?cvc_6 e4) )) (or (or (or (or (= ?cvc_7 e0) (= ?cvc_7 e1) ) (= ?cvc_7 e2) ) (= ?cvc_7 e3) ) (= ?cvc_7 e4) )) (or (or (or (or (= ?cvc_8 e0) (= ?cvc_8 e1) ) (= ?cvc_8 e2) ) (= ?cvc_8 e3) ) (= ?cvc_8 e4) )) (or (or (or (or (= ?cvc_9 e0) (= ?cvc_9 e1) ) (= ?cvc_9 e2) ) (= ?cvc_9 e3) ) (= ?cvc_9 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_10 e0) (= ?cvc_10 e1) ) (= ?cvc_10 e2) ) (= ?cvc_10 e3) ) (= ?cvc_10 e4) ) (or (or (or (or (= ?cvc_11 e0) (= ?cvc_11 e1) ) (= ?cvc_11 e2) ) (= ?cvc_11 e3) ) (= ?cvc_11 e4) )) (or (or (or (or (= ?cvc_12 e0) (= ?cvc_12 e1) ) (= ?cvc_12 e2) ) (= ?cvc_12 e3) ) (= ?cvc_12 e4) )) (or (or (or (or (= ?cvc_13 e0) (= ?cvc_13 e1) ) (= ?cvc_13 e2) ) (= ?cvc_13 e3) ) (= ?cvc_13 e4) )) (or (or (or (or (= ?cvc_14 e0) (= ?cvc_14 e1) ) (= ?cvc_14 e2) ) (= ?cvc_14 e3) ) (= ?cvc_14 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_15 e0) (= ?cvc_15 e1) ) (= ?cvc_15 e2) ) (= ?cvc_15 e3) ) (= ?cvc_15 e4) ) (or (or (or (or (= ?cvc_16 e0) (= ?cvc_16 e1) ) (= ?cvc_16 e2) ) (= ?cvc_16 e3) ) (= ?cvc_16 e4) )) (or (or (or (or (= ?cvc_17 e0) (= ?cvc_17 e1) ) (= ?cvc_17 e2) ) (= ?cvc_17 e3) ) (= ?cvc_17 e4) )) (or (or (or (or (= ?cvc_18 e0) (= ?cvc_18 e1) ) (= ?cvc_18 e2) ) (= ?cvc_18 e3) ) (= ?cvc_18 e4) )) (or (or (or (or (= ?cvc_19 e0) (= ?cvc_19 e1) ) (= ?cvc_19 e2) ) (= ?cvc_19 e3) ) (= ?cvc_19 e4) ))) (and (and (and (and (or (or (or (or (= ?cvc_20 e0) (= ?cvc_20 e1) ) (= ?cvc_20 e2) ) (= ?cvc_20 e3) ) (= ?cvc_20 e4) ) (or (or (or (or (= ?cvc_21 e0) (= ?cvc_21 e1) ) (= ?cvc_21 e2) ) (= ?cvc_21 e3) ) (= ?cvc_21 e4) )) (or (or (or (or (= ?cvc_22 e0) (= ?cvc_22 e1) ) (= ?cvc_22 e2) ) (= ?cvc_22 e3) ) (= ?cvc_22 e4) )) (or (or (or (or (= ?cvc_23 e0) (= ?cvc_23 e1) ) (= ?cvc_23 e2) ) (= ?cvc_23 e3) ) (= ?cvc_23 e4) )) (or (or (or (or (= ?cvc_24 e0) (= ?cvc_24 e1) ) (= ?cvc_24 e2) ) (= ?cvc_24 e3) ) (= ?cvc_24 e4) ))))))))))))))))))))))))))))
:assumption
(let (?cvc_1 (op e0 e0)) (flet ($cvc_0 (= ?cvc_1 e0)) (flet ($cvc_6 (= ?cvc_1 e1)) (flet ($cvc_11 (= ?cvc_1 e2)) (flet ($cvc_12 (= ?cvc_1 e3)) (flet ($cvc_13 (= ?cvc_1 e4)) (let (?cvc_2 (op e0 e1)) (flet ($cvc_15 (= ?cvc_2 e0)) (flet ($cvc_22 (= ?cvc_2 e1)) (flet ($cvc_28 (= ?cvc_2 e2)) (flet ($cvc_31 (= ?cvc_2 e3)) (flet ($cvc_34 (= ?cvc_2 e4)) (let (?cvc_3 (op e0 e2)) (flet ($cvc_38 (= ?cvc_3 e0)) (flet ($cvc_46 (= ?cvc_3 e1)) (flet ($cvc_53 (= ?cvc_3 e2)) (flet ($cvc_58 (= ?cvc_3 e3)) (flet ($cvc_63 (= ?cvc_3 e4)) (let (?cvc_4 (op e0 e3)) (flet ($cvc_69 (= ?cvc_4 e0)) (flet ($cvc_78 (= ?cvc_4 e1)) (flet ($cvc_86 (= ?cvc_4 e2)) (flet ($cvc_93 (= ?cvc_4 e3)) (flet ($cvc_100 (= ?cvc_4 e4)) (let (?cvc_5 (op e0 e4)) (flet ($cvc_108 (= ?cvc_5 e0)) (flet ($cvc_118 (= ?cvc_5 e1)) (flet ($cvc_127 (= ?cvc_5 e2)) (flet ($cvc_136 (= ?cvc_5 e3)) (flet ($cvc_145 (= ?cvc_5 e4)) (let (?cvc_7 (op e1 e0)) (flet ($cvc_14 (= ?cvc_7 e0)) (flet ($cvc_17 (= ?cvc_7 e1)) (flet ($cvc_27 (= ?cvc_7 e2)) (flet ($cvc_30 (= ?cvc_7 e3)) (flet ($cvc_33 (= ?cvc_7 e4)) (let (?cvc_18 (op e1 e1)) (flet ($cvc_16 (= ?cvc_18 e0)) (flet ($cvc_23 (= ?cvc_18 e1)) (flet ($cvc_29 (= ?cvc_18 e2)) (flet ($cvc_32 (= ?cvc_18 e3)) (flet ($cvc_35 (= ?cvc_18 e4)) (let (?cvc_19 (op e1 e2)) (flet ($cvc_39 (= ?cvc_19 e0)) (flet ($cvc_47 (= ?cvc_19 e1)) (flet ($cvc_54 (= ?cvc_19 e2)) (flet ($cvc_59 (= ?cvc_19 e3)) (flet ($cvc_64 (= ?cvc_19 e4)) (let (?cvc_20 (op e1 e3)) (flet ($cvc_70 (= ?cvc_20 e0)) (flet ($cvc_79 (= ?cvc_20 e1)) (flet ($cvc_87 (= ?cvc_20 e2)) (flet ($cvc_94 (= ?cvc_20 e3)) (flet ($cvc_101 (= ?cvc_20 e4)) (let (?cvc_21 (op e1 e4)) (flet ($cvc_109 (= ?cvc_21 e0)) (flet ($cvc_119 (= ?cvc_21 e1)) (flet ($cvc_128 (= ?cvc_21 e2)) (flet ($cvc_137 (= ?cvc_21 e3)) (flet ($cvc_146 (= ?cvc_21 e4)) (let (?cvc_8 (op e2 e0)) (flet ($cvc_36 (= ?cvc_8 e0)) (flet ($cvc_41 (= ?cvc_8 e1)) (flet ($cvc_51 (= ?cvc_8 e2)) (flet ($cvc_56 (= ?cvc_8 e3)) (flet ($cvc_61 (= ?cvc_8 e4)) (let (?cvc_24 (op e2 e1)) (flet ($cvc_37 (= ?cvc_24 e0)) (flet ($cvc_42 (= ?cvc_24 e1)) (flet ($cvc_52 (= ?cvc_24 e2)) (flet ($cvc_57 (= ?cvc_24 e3)) (flet ($cvc_62 (= ?cvc_24 e4)) (let (?cvc_43 (op e2 e2)) (flet ($cvc_40 (= ?cvc_43 e0)) (flet ($cvc_48 (= ?cvc_43 e1)) (flet ($cvc_55 (= ?cvc_43 e2)) (flet ($cvc_60 (= ?cvc_43 e3)) (flet ($cvc_65 (= ?cvc_43 e4)) (let (?cvc_44 (op e2 e3)) (flet ($cvc_71 (= ?cvc_44 e0)) (flet ($cvc_80 (= ?cvc_44 e1)) (flet ($cvc_88 (= ?cvc_44 e2)) (flet ($cvc_95 (= ?cvc_44 e3)) (flet ($cvc_102 (= ?cvc_44 e4)) (let (?cvc_45 (op e2 e4)) (flet ($cvc_110 (= ?cvc_45 e0)) (flet ($cvc_120 (= ?cvc_45 e1)) (flet ($cvc_129 (= ?cvc_45 e2)) (flet ($cvc_138 (= ?cvc_45 e3)) (flet ($cvc_147 (= ?cvc_45 e4)) (let (?cvc_9 (op e3 e0)) (flet ($cvc_66 (= ?cvc_9 e0)) (flet ($cvc_73 (= ?cvc_9 e1)) (flet ($cvc_83 (= ?cvc_9 e2)) (flet ($cvc_90 (= ?cvc_9 e3)) (flet ($cvc_97 (= ?cvc_9 e4)) (let (?cvc_25 (op e3 e1)) (flet ($cvc_67 (= ?cvc_25 e0)) (flet ($cvc_74 (= ?cvc_25 e1)) (flet ($cvc_84 (= ?cvc_25 e2)) (flet ($cvc_91 (= ?cvc_25 e3)) (flet ($cvc_98 (= ?cvc_25 e4)) (let (?cvc_49 (op e3 e2)) (flet ($cvc_68 (= ?cvc_49 e0)) (flet ($cvc_75 (= ?cvc_49 e1)) (flet ($cvc_85 (= ?cvc_49 e2)) (flet ($cvc_92 (= ?cvc_49 e3)) (flet ($cvc_99 (= ?cvc_49 e4)) (let (?cvc_76 (op e3 e3)) (flet ($cvc_72 (= ?cvc_76 e0)) (flet ($cvc_81 (= ?cvc_76 e1)) (flet ($cvc_89 (= ?cvc_76 e2)) (flet ($cvc_96 (= ?cvc_76 e3)) (flet ($cvc_103 (= ?cvc_76 e4)) (let (?cvc_77 (op e3 e4)) (flet ($cvc_111 (= ?cvc_77 e0)) (flet ($cvc_121 (= ?cvc_77 e1)) (flet ($cvc_130 (= ?cvc_77 e2)) (flet ($cvc_139 (= ?cvc_77 e3)) (flet ($cvc_148 (= ?cvc_77 e4)) (let (?cvc_10 (op e4 e0)) (flet ($cvc_104 (= ?cvc_10 e0)) (flet ($cvc_113 (= ?cvc_10 e1)) (flet ($cvc_123 (= ?cvc_10 e2)) (flet ($cvc_132 (= ?cvc_10 e3)) (flet ($cvc_141 (= ?cvc_10 e4)) (let (?cvc_26 (op e4 e1)) (flet ($cvc_105 (= ?cvc_26 e0)) (flet ($cvc_114 (= ?cvc_26 e1)) (flet ($cvc_124 (= ?cvc_26 e2)) (flet ($cvc_133 (= ?cvc_26 e3)) (flet ($cvc_142 (= ?cvc_26 e4)) (let (?cvc_50 (op e4 e2)) (flet ($cvc_106 (= ?cvc_50 e0)) (flet ($cvc_115 (= ?cvc_50 e1)) (flet ($cvc_125 (= ?cvc_50 e2)) (flet ($cvc_134 (= ?cvc_50 e3)) (flet ($cvc_143 (= ?cvc_50 e4)) (let (?cvc_82 (op e4 e3)) (flet ($cvc_107 (= ?cvc_82 e0)) (flet ($cvc_116 (= ?cvc_82 e1)) (flet ($cvc_126 (= ?cvc_82 e2)) (flet ($cvc_135 (= ?cvc_82 e3)) (flet ($cvc_144 (= ?cvc_82 e4)) (let (?cvc_117 (op e4 e4)) (flet ($cvc_112 (= ?cvc_117 e0)) (flet ($cvc_122 (= ?cvc_117 e1)) (flet ($cvc_131 (= ?cvc_117 e2)) (flet ($cvc_140 (= ?cvc_117 e3)) (flet ($cvc_149 (= ?cvc_117 e4)) (and (and (and (and (and (and (and (and (and (or (or (or (or $cvc_0 $cvc_15 ) $cvc_38 ) $cvc_69 ) $cvc_108 ) (or (or (or (or $cvc_0 $cvc_14 ) $cvc_36 ) $cvc_66 ) $cvc_104 )) (and (or (or (or (or $cvc_6 $cvc_22 ) $cvc_46 ) $cvc_78 ) $cvc_118 ) (or (or (or (or $cvc_6 $cvc_17 ) $cvc_41 ) $cvc_73 ) $cvc_113 ))) (and (or (or (or (or $cvc_11 $cvc_28 ) $cvc_53 ) $cvc_86 ) $cvc_127 ) (or (or (or (or $cvc_11 $cvc_27 ) $cvc_51 ) $cvc_83 ) $cvc_123 ))) (and (or (or (or (or $cvc_12 $cvc_31 ) $cvc_58 ) $cvc_93 ) $cvc_136 ) (or (or (or (or $cvc_12 $cvc_30 ) $cvc_56 ) $cvc_90 ) $cvc_132 ))) (and (or (or (or (or $cvc_13 $cvc_34 ) $cvc_63 ) $cvc_100 ) $cvc_145 ) (or (or (or (or $cvc_13 $cvc_33 ) $cvc_61 ) $cvc_97 ) $cvc_141 ))) (and (and (and (and (and (or (or (or (or $cvc_14 $cvc_16 ) $cvc_39 ) $cvc_70 ) $cvc_109 ) (or (or (or (or $cvc_15 $cvc_16 ) $cvc_37 ) $cvc_67 ) $cvc_105 )) (and (or (or (or (or $cvc_17 $cvc_23 ) $cvc_47 ) $cvc_79 ) $cvc_119 ) (or (or (or (or $cvc_22 $cvc_23 ) $cvc_42 ) $cvc_74 ) $cvc_114 ))) (and (or (or (or (or $cvc_27 $cvc_29 ) $cvc_54 ) $cvc_87 ) $cvc_128 ) (or (or (or (or $cvc_28 $cvc_29 ) $cvc_52 ) $cvc_84 ) $cvc_124 ))) (and (or (or (or (or $cvc_30 $cvc_32 ) $cvc_59 ) $cvc_94 ) $cvc_137 ) (or (or (or (or $cvc_31 $cvc_32 ) $cvc_57 ) $cvc_91 ) $cvc_133 ))) (and (or (or (or (or $cvc_33 $cvc_35 ) $cvc_64 ) $cvc_101 ) $cvc_146 ) (or (or (or (or $cvc_34 $cvc_35 ) $cvc_62 ) $cvc_98 ) $cvc_142 )))) (and (and (and (and (and (or (or (or (or $cvc_36 $cvc_37 ) $cvc_40 ) $cvc_71 ) $cvc_110 ) (or (or (or (or $cvc_38 $cvc_39 ) $cvc_40 ) $cvc_68 ) $cvc_106 )) (and (or (or (or (or $cvc_41 $cvc_42 ) $cvc_48 ) $cvc_80 ) $cvc_120 ) (or (or (or (or $cvc_46 $cvc_47 ) $cvc_48 ) $cvc_75 ) $cvc_115 ))) (and (or (or (or (or $cvc_51 $cvc_52 ) $cvc_55 ) $cvc_88 ) $cvc_129 ) (or (or (or (or $cvc_53 $cvc_54 ) $cvc_55 ) $cvc_85 ) $cvc_125 ))) (and (or (or (or (or $cvc_56 $cvc_57 ) $cvc_60 ) $cvc_95 ) $cvc_138 ) (or (or (or (or $cvc_58 $cvc_59 ) $cvc_60 ) $cvc_92 ) $cvc_134 ))) (and (or (or (or (or $cvc_61 $cvc_62 ) $cvc_65 ) $cvc_102 ) $cvc_147 ) (or (or (or (or $cvc_63 $cvc_64 ) $cvc_65 ) $cvc_99 ) $cvc_143 )))) (and (and (and (and (and (or (or (or (or $cvc_66 $cvc_67 ) $cvc_68 ) $cvc_72 ) $cvc_111 ) (or (or (or (or $cvc_69 $cvc_70 ) $cvc_71 ) $cvc_72 ) $cvc_107 )) (and (or (or (or (or $cvc_73 $cvc_74 ) $cvc_75 ) $cvc_81 ) $cvc_121 ) (or (or (or (or $cvc_78 $cvc_79 ) $cvc_80 ) $cvc_81 ) $cvc_116 ))) (and (or (or (or (or $cvc_83 $cvc_84 ) $cvc_85 ) $cvc_89 ) $cvc_130 ) (or (or (or (or $cvc_86 $cvc_87 ) $cvc_88 ) $cvc_89 ) $cvc_126 ))) (and (or (or (or (or $cvc_90 $cvc_91 ) $cvc_92 ) $cvc_96 ) $cvc_139 ) (or (or (or (or $cvc_93 $cvc_94 ) $cvc_95 ) $cvc_96 ) $cvc_135 ))) (and (or (or (or (or $cvc_97 $cvc_98 ) $cvc_99 ) $cvc_103 ) $cvc_148 ) (or (or (or (or $cvc_100 $cvc_101 ) $cvc_102 ) $cvc_103 ) $cvc_144 )))) (and (and (and (and (and (or (or (or (or $cvc_104 $cvc_105 ) $cvc_106 ) $cvc_107 ) $cvc_112 ) (or (or (or (or $cvc_108 $cvc_109 ) $cvc_110 ) $cvc_111 ) $cvc_112 )) (and (or (or (or (or $cvc_113 $cvc_114 ) $cvc_115 ) $cvc_116 ) $cvc_122 ) (or (or (or (or $cvc_118 $cvc_119 ) $cvc_120 ) $cvc_121 ) $cvc_122 ))) (and (or (or (or (or $cvc_123 $cvc_124 ) $cvc_125 ) $cvc_126 ) $cvc_131 ) (or (or (or (or $cvc_127 $cvc_128 ) $cvc_129 ) $cvc_130 ) $cvc_131 ))) (and (or (or (or (or $cvc_132 $cvc_133 ) $cvc_134 ) $cvc_135 ) $cvc_140 ) (or (or (or (or $cvc_136 $cvc_137 ) $cvc_138 ) $cvc_139 ) $cvc_140 ))) (and (or (or (or (or $cvc_141 $cvc_142 ) $cvc_143 ) $cvc_144 ) $cvc_149 ) (or (or (or (or $cvc_145 $cvc_146 ) $cvc_147 ) $cvc_148 ) $cvc_149 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
:assumption
(let (?cvc_0 (op e0 e0)) (let (?cvc_5 (op e0 e1)) (let (?cvc_10 (op e0 e2)) (let (?cvc_15 (op e0 e3)) (let (?cvc_20 (op e0 e4)) (let (?cvc_1 (op e1 e0)) (let (?cvc_6 (op e1 e1)) (let (?cvc_11 (op e1 e2)) (let (?cvc_16 (op e1 e3)) (let (?cvc_21 (op e1 e4)) (let (?cvc_2 (op e2 e0)) (let (?cvc_7 (op e2 e1)) (let (?cvc_12 (op e2 e2)) (let (?cvc_17 (op e2 e3)) (let (?cvc_22 (op e2 e4)) (let (?cvc_3 (op e3 e0)) (let (?cvc_8 (op e3 e1)) (let (?cvc_13 (op e3 e2)) (let (?cvc_18 (op e3 e3)) (let (?cvc_23 (op e3 e4)) (let (?cvc_4 (op e4 e0)) (let (?cvc_9 (op e4 e1)) (let (?cvc_14 (op e4 e2)) (let (?cvc_19 (op e4 e3)) (let (?cvc_24 (op e4 e4)) (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_1 ?cvc_2))) (not (= ?cvc_1 ?cvc_3))) (not (= ?cvc_1 ?cvc_4))) (not (= ?cvc_2 ?cvc_3))) (not (= ?cvc_2 ?cvc_4))) (not (= ?cvc_3 ?cvc_4))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_5 ?cvc_6)) (not (= ?cvc_5 ?cvc_7))) (not (= ?cvc_5 ?cvc_8))) (not (= ?cvc_5 ?cvc_9))) (not (= ?cvc_6 ?cvc_7))) (not (= ?cvc_6 ?cvc_8))) (not (= ?cvc_6 ?cvc_9))) (not (= ?cvc_7 ?cvc_8))) (not (= ?cvc_7 ?cvc_9))) (not (= ?cvc_8 ?cvc_9)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_10 ?cvc_11)) (not (= ?cvc_10 ?cvc_12))) (not (= ?cvc_10 ?cvc_13))) (not (= ?cvc_10 ?cvc_14))) (not (= ?cvc_11 ?cvc_12))) (not (= ?cvc_11 ?cvc_13))) (not (= ?cvc_11 ?cvc_14))) (not (= ?cvc_12 ?cvc_13))) (not (= ?cvc_12 ?cvc_14))) (not (= ?cvc_13 ?cvc_14)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_15 ?cvc_16)) (not (= ?cvc_15 ?cvc_17))) (not (= ?cvc_15 ?cvc_18))) (not (= ?cvc_15 ?cvc_19))) (not (= ?cvc_16 ?cvc_17))) (not (= ?cvc_16 ?cvc_18))) (not (= ?cvc_16 ?cvc_19))) (not (= ?cvc_17 ?cvc_18))) (not (= ?cvc_17 ?cvc_19))) (not (= ?cvc_18 ?cvc_19)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_20 ?cvc_21)) (not (= ?cvc_20 ?cvc_22))) (not (= ?cvc_20 ?cvc_23))) (not (= ?cvc_20 ?cvc_24))) (not (= ?cvc_21 ?cvc_22))) (not (= ?cvc_21 ?cvc_23))) (not (= ?cvc_21 ?cvc_24))) (not (= ?cvc_22 ?cvc_23))) (not (= ?cvc_22 ?cvc_24))) (not (= ?cvc_23 ?cvc_24)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?cvc_0 ?cvc_5)) (not (= ?cvc_0 ?cvc_10))) (not (= ?cvc_0 ?cvc_15))) (not (= ?cvc_0 ?cvc_20))) (not (= ?cvc_5 ?cvc_10))) (not (= ?cvc_5 ?cvc_15))) (not (= ?cvc_5 ?cvc_20))) (not (= ?cvc_10 ?cvc_15))) (not (= ?cvc_10 ?cvc_20))) (not (= ?cvc_15 ?cvc_20))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_1 ?cvc_6)) (not (= ?cvc_1 ?cvc_11))) (not (= ?cvc_1 ?cvc_16))) (not (= ?cvc_1 ?cvc_21))) (not (= ?cvc_6 ?cvc_11))) (not (= ?cvc_6 ?cvc_16))) (not (= ?cvc_6 ?cvc_21))) (not (= ?cvc_11 ?cvc_16))) (not (= ?cvc_11 ?cvc_21))) (not (= ?cvc_16 ?cvc_21)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_2 ?cvc_7)) (not (= ?cvc_2 ?cvc_12))) (not (= ?cvc_2 ?cvc_17))) (not (= ?cvc_2 ?cvc_22))) (not (= ?cvc_7 ?cvc_12))) (not (= ?cvc_7 ?cvc_17))) (not (= ?cvc_7 ?cvc_22))) (not (= ?cvc_12 ?cvc_17))) (not (= ?cvc_12 ?cvc_22))) (not (= ?cvc_17 ?cvc_22)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_3 ?cvc_8)) (not (= ?cvc_3 ?cvc_13))) (not (= ?cvc_3 ?cvc_18))) (not (= ?cvc_3 ?cvc_23))) (not (= ?cvc_8 ?cvc_13))) (not (= ?cvc_8 ?cvc_18))) (not (= ?cvc_8 ?cvc_23))) (not (= ?cvc_13 ?cvc_18))) (not (= ?cvc_13 ?cvc_23))) (not (= ?cvc_18 ?cvc_23)))) (and (and (and (and (and (and (and (and (and (not (= ?cvc_4 ?cvc_9)) (not (= ?cvc_4 ?cvc_14))) (not (= ?cvc_4 ?cvc_19))) (not (= ?cvc_4 ?cvc_24))) (not (= ?cvc_9 ?cvc_14))) (not (= ?cvc_9 ?cvc_19))) (not (= ?cvc_9 ?cvc_24))) (not (= ?cvc_14 ?cvc_19))) (not (= ?cvc_14 ?cvc_24))) (not (= ?cvc_19 ?cvc_24))))))))))))))))))))))))))))))
:assumption
(and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e2 e3))) (not (= e2 e4))) (not (= e3 e4)))
:assumption
(and (and (and (= e0 (op e4 e4)) (= e1 (op e3 e4))) (= e2 (op e3 e1))) (= e4 (op e3 e3)))
:assumption
(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 (= (op e0 e0) e2) (= (op e0 e1) e0)) (= (op e0 e2) e1)) (= (op e0 e3) e3)) (= (op e0 e4) e4)) (= (op e1 e0) e0)) (= (op e1 e1) e1)) (= (op e1 e2) e4)) (= (op e1 e3) e2)) (= (op e1 e4) e3)) (= (op e2 e0) e1)) (= (op e2 e1) e4)) (= (op e2 e2) e3)) (= (op e2 e3) e0)) (= (op e2 e4) e2)) (= (op e3 e0) e3)) (= (op e3 e1) e2)) (= (op e3 e2) e0)) (= (op e3 e3) e4)) (= (op e3 e4) e1)) (= (op e4 e0) e4)) (= (op e4 e1) e3)) (= (op e4 e2) e2)) (= (op e4 e3) e1)) (= (op e4 e4) e0)))
:assumption
(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 (= (op e0 e0) e1) (= (op e0 e1) e0)) (= (op e0 e2) e4)) (= (op e0 e3) e3)) (= (op e0 e4) e2)) (= (op e1 e0) e0)) (= (op e1 e1) e3)) (= (op e1 e2) e1)) (= (op e1 e3) e2)) (= (op e1 e4) e4)) (= (op e2 e0) e4)) (= (op e2 e1) e1)) (= (op e2 e2) e2)) (= (op e2 e3) e0)) (= (op e2 e4) e3)) (= (op e3 e0) e3)) (= (op e3 e1) e2)) (= (op e3 e2) e0)) (= (op e3 e3) e4)) (= (op e3 e4) e1)) (= (op e4 e0) e2)) (= (op e4 e1) e4)) (= (op e4 e2) e3)) (= (op e4 e3) e1)) (= (op e4 e4) e0)))
:formula
(not false)
)
|
