%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : SYO581+1 : TPTP v6.4.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_nitpick %d %s % Computer : n035.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.36.3.el7.x86_64 % CPULimit : 300s % DateTime : Wed Jan 18 19:33:23 EST 2017 % Result : CounterSatisfiable 32.98s % Output : FiniteModel 32.98s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYO581+1 : TPTP v6.4.0. Released v5.5.0. % 0.00/0.04 % Command : isabelle tptp_nitpick %d %s % 0.03/0.24 % Computer : n035.star.cs.uiowa.edu % 0.03/0.24 % Model : x86_64 x86_64 % 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.24 % Memory : 32218.75MB % 0.03/0.24 % OS : Linux 3.10.0-327.36.3.el7.x86_64 % 0.03/0.24 % CPULimit : 300 % 0.03/0.24 % DateTime : Mon Jan 16 05:20:19 CST 2017 % 0.03/0.24 % CPUTime: % 32.98/20.27 Nitpicking formula... % 32.98/20.27 Timestamp: 05:20:28 % 32.98/20.27 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 32.98/20.27 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 32.98/20.27 Batch 1 of 20: Trying 5 scopes: % 32.98/20.27 card TPTP_Interpret.ind = 1 % 32.98/20.27 card TPTP_Interpret.ind = 2 % 32.98/20.27 card TPTP_Interpret.ind = 3 % 32.98/20.27 card TPTP_Interpret.ind = 4 % 32.98/20.27 card TPTP_Interpret.ind = 5 % 32.98/20.27 % SZS status CounterSatisfiable % SZS output start FiniteModel % 32.98/20.27 Nitpick found a counterexample for card TPTP_Interpret.ind = 4: % 32.98/20.27 % 32.98/20.27 Skolem constants: % 32.98/20.27 X1055 = i1 % 32.98/20.27 X1056 = i1 % 32.98/20.27 X1061 = i2 % 32.98/20.27 Constants: % 32.98/20.27 bnd_b48_buttercup10007 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10013 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10019 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10021 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10022 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10024 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10029 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10031 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10034 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10035 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10043 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10045 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10046 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10050 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10052 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10054 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10058 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10065 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10068 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10070 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10072 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10075 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10076 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10082 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10085 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10086 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10092 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10098 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10102 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10104 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10107 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10108 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10109 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10110 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10111 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10115 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10119 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10120 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10121 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10130 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10133 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10134 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10143 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10150 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10154 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10156 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10158 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10159 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10160 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10161 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10166 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10167 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10169 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10170 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10173 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10174 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10176 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10179 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10180 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10182 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10186 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10191 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10193 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10195 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10196 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10197 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10198 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10199 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10201 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10208 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10210 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10214 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10217 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10220 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10222 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10227 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10228 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10229 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10231 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10240 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10247 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10248 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10253 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10260 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True, i4 := False) % 32.98/20.27 bnd_b48_buttercup10261 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True, i4 := False) % 32.98/20.27 bnd_b48_buttercup10266 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10267 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10268 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10269 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10271 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10272 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10273 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10274 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10275 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10276 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10277 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10278 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10279 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10283 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10289 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10290 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10291 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10294 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10299 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10300 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10305 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10307 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10308 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10309 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10313 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10318 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10320 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10322 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10326 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10332 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10334 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10343 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10344 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10348 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10352 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10353 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10358 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10359 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10361 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10362 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10365 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10367 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10370 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10374 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10377 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10378 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10381 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10383 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10386 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10394 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10398 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10402 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10405 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10410 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10411 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10417 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10420 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10421 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10422 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10427 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10433 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10434 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10440 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10441 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10442 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True, i4 := False) % 32.98/20.27 bnd_b48_buttercup10443 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10446 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10450 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10451 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10454 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10456 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10458 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := True, i4 := True) % 32.98/20.27 bnd_b48_buttercup10460 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10465 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10466 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10467 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10469 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10471 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10474 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10478 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10479 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10483 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10487 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10489 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10490 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10493 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10496 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10502 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10507 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10512 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10513 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10514 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10515 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10518 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10519 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10520 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10521 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10522 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10526 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10530 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10531 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10538 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10541 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10542 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10545 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10548 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10549 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10552 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10561 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10562 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10563 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_b48_buttercup10570 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10572 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10574 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10575 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10579 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10582 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10589 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10596 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10604 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10605 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10606 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10609 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10612 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10616 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10624 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10629 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10632 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10636 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10638 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10640 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10642 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_b48_buttercup10646 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10000 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True, i4 := False) % 32.98/20.27 bnd_k04_buttercup10004 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True, i4 := False) % 32.98/20.27 bnd_k04_buttercup10012 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10016 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10026 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10028 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10033 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10039 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10042 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10044 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10048 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10049 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10051 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10053 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10057 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10061 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10064 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10067 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10074 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10079 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10084 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10089 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10095 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10096 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10097 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.27 bnd_k04_buttercup10100 = % 32.98/20.27 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10117 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.27 bnd_k04_buttercup10125 = % 32.98/20.27 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10132 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10135 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10139 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10142 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10147 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10153 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10164 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10172 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10181 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10184 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10190 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10200 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10204 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10206 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10213 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10219 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10221 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10225 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10234 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10236 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10238 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10244 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10252 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10255 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10259 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := True, i4 := False) % 32.98/20.28 bnd_k04_buttercup10282 = % 32.98/20.28 (\<lambda>x. _)(i1 := False, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10286 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10288 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10293 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10296 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10298 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10303 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10312 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10316 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10325 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10329 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10333 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10337 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10342 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10347 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10351 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10356 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10357 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10360 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10364 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10369 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10371 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10373 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10376 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10380 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10382 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10385 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10389 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10391 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10397 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10400 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10404 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10406 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10408 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10415 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10419 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10424 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10425 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10430 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10437 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10445 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10449 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10453 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10462 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10464 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10470 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10473 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10477 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10482 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10486 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10492 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10495 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10499 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10504 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10506 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10510 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10516 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10517 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10524 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10529 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10535 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10539 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10540 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10544 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10546 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10547 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10551 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10555 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10559 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10567 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10578 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10581 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10586 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10593 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10599 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10602 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10608 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10611 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10619 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10620 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10622 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := True) % 32.98/20.28 bnd_k04_buttercup10626 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10628 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := True, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10631 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10635 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10637 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10639 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10641 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 bnd_k04_buttercup10643 = % 32.98/20.28 (\<lambda>x. _)(i1 := True, i2 := False, i3 := False, i4 := False) % 32.98/20.28 % SZS output end FiniteModel % 32.98/20.28 Total time: 9.1 s %------------------------------------------------------------------------------