off rlabout;



rlset ibalp;



{}


% The formula toilet_a_04_01.4.qdimacs of Castellini's encoding of the
% bomb in the toilet problem http://www.qbflib.org
toilet_a_04_01_4 :=
ex(var43,all(var50,all(var49,all(var48,all(var51,ex(var1,ex(var2,ex(var3,ex(var4
,ex(var5,ex(var6,ex(var7,ex(var8,ex(var9,ex(var10,ex(var11,ex(var12,ex(var52,ex(
var55,ex(var56,ex(var57,ex(var58,ex(var59,ex(var60,(not(var49 = 1) or not(var50
= 1) or not(var51 = 1) or var48 = 1 or var52 = 1) and (not(var49 = 1) or not(
var50 = 1) or not(var51 = 1) or var48 = 1 or var53 = 1) and (not(var49 = 1) or
not(var50 = 1) or not(var51 = 1) or var48 = 1 or var54 = 1) and (not(var49 = 1)
or not(var50 = 1) or not(var51 = 1) or not(var55 = 1) or var48 = 1) and (not(
var49 = 1) or not(var50 = 1) or not(var52 = 1) or var48 = 1 or var51 = 1) and (
not(var49 = 1) or not(var50 = 1) or var48 = 1 or var51 = 1 or var53 = 1) and (
not(var49 = 1) or not(var50 = 1) or var48 = 1 or var51 = 1 or var54 = 1) and (
not(var49 = 1) or not(var50 = 1) or var48 = 1 or var51 = 1 or var55 = 1) and (
not(var48 = 1) or not(var50 = 1) or not(var51 = 1) or not(var52 = 1) or var49 =
1) and (not(var48 = 1) or not(var50 = 1) or not(var51 = 1) or var49 = 1 or var53
 = 1) and (not(var48 = 1) or not(var50 = 1) or not(var51 = 1) or var49 = 1 or
var54 = 1) and (not(var48 = 1) or not(var50 = 1) or not(var51 = 1) or not(var55
= 1) or var49 = 1) and (not(var48 = 1) or not(var50 = 1) or var49 = 1 or var51 =
 1 or var52 = 1) and (not(var48 = 1) or not(var50 = 1) or not(var53 = 1) or
var49 = 1 or var51 = 1) and (not(var48 = 1) or not(var50 = 1) or var49 = 1 or
var51 = 1 or var54 = 1) and (not(var48 = 1) or not(var50 = 1) or var49 = 1 or
var51 = 1 or var55 = 1) and (not(var50 = 1) or not(var51 = 1) or var48 = 1 or
var49 = 1 or var52 = 1) and (not(var50 = 1) or not(var51 = 1) or not(var53 = 1)
or var48 = 1 or var49 = 1) and (not(var50 = 1) or not(var51 = 1) or var48 = 1 or
 var49 = 1 or var54 = 1) and (not(var50 = 1) or not(var51 = 1) or not(var55 = 1)
 or var48 = 1 or var49 = 1) and (not(var50 = 1) or not(var52 = 1) or var48 = 1
or var49 = 1 or var51 = 1) and (not(var50 = 1) or not(var53 = 1) or var48 = 1 or
 var49 = 1 or var51 = 1) and (not(var50 = 1) or var48 = 1 or var49 = 1 or var51
= 1 or var54 = 1) and (not(var50 = 1) or var48 = 1 or var49 = 1 or var51 = 1 or
var55 = 1) and (not(var48 = 1) or not(var49 = 1) or not(var51 = 1) or not(var52
= 1) or var50 = 1) and (not(var48 = 1) or not(var49 = 1) or not(var51 = 1) or
not(var53 = 1) or var50 = 1) and (not(var48 = 1) or not(var49 = 1) or not(var51
= 1) or var50 = 1 or var54 = 1) and (not(var48 = 1) or not(var49 = 1) or not(
var51 = 1) or not(var55 = 1) or var50 = 1) and (not(var48 = 1) or not(var49 = 1)
 or var50 = 1 or var51 = 1 or var52 = 1) and (not(var48 = 1) or not(var49 = 1)
or var50 = 1 or var51 = 1 or var53 = 1) and (not(var48 = 1) or not(var49 = 1) or
 not(var54 = 1) or var50 = 1 or var51 = 1) and (not(var48 = 1) or not(var49 = 1)
 or var50 = 1 or var51 = 1 or var55 = 1) and (not(var49 = 1) or not(var51 = 1)
or var48 = 1 or var50 = 1 or var52 = 1) and (not(var49 = 1) or not(var51 = 1) or
 var48 = 1 or var50 = 1 or var53 = 1) and (not(var49 = 1) or not(var51 = 1) or
not(var54 = 1) or var48 = 1 or var50 = 1) and (not(var49 = 1) or not(var51 = 1)
or not(var55 = 1) or var48 = 1 or var50 = 1) and (not(var49 = 1) or not(var52 =
1) or var48 = 1 or var50 = 1 or var51 = 1) and (not(var49 = 1) or var48 = 1 or
var50 = 1 or var51 = 1 or var53 = 1) and (not(var49 = 1) or not(var54 = 1) or
var48 = 1 or var50 = 1 or var51 = 1) and (not(var49 = 1) or var48 = 1 or var50 =
 1 or var51 = 1 or var55 = 1) and (not(var48 = 1) or not(var51 = 1) or not(var52
 = 1) or var49 = 1 or var50 = 1) and (not(var48 = 1) or not(var51 = 1) or var49
= 1 or var50 = 1 or var53 = 1) and (not(var48 = 1) or not(var51 = 1) or not(
var54 = 1) or var49 = 1 or var50 = 1) and (not(var48 = 1) or not(var51 = 1) or
not(var55 = 1) or var49 = 1 or var50 = 1) and (not(var48 = 1) or var49 = 1 or
var50 = 1 or var51 = 1 or var52 = 1) and (not(var48 = 1) or not(var53 = 1) or
var49 = 1 or var50 = 1 or var51 = 1) and (not(var48 = 1) or not(var54 = 1) or
var49 = 1 or var50 = 1 or var51 = 1) and (not(var48 = 1) or var49 = 1 or var50 =
 1 or var51 = 1 or var55 = 1) and (not(var51 = 1) or var48 = 1 or var49 = 1 or
var50 = 1 or var52 = 1) and (not(var51 = 1) or not(var53 = 1) or var48 = 1 or
var49 = 1 or var50 = 1) and (not(var51 = 1) or not(var54 = 1) or var48 = 1 or
var49 = 1 or var50 = 1) and (not(var51 = 1) or not(var55 = 1) or var48 = 1 or
var49 = 1 or var50 = 1) and (not(var52 = 1) or var48 = 1 or var49 = 1 or var50 =
 1 or var51 = 1) and (not(var53 = 1) or var48 = 1 or var49 = 1 or var50 = 1 or
var51 = 1) and (not(var54 = 1) or var48 = 1 or var49 = 1 or var50 = 1 or var51 =
 1) and (var48 = 1 or var49 = 1 or var50 = 1 or var51 = 1 or var55 = 1) and (not
(var48 = 1) or not(var49 = 1) or not(var50 = 1) or var51 = 1 or var52 = 1) and (
not(var48 = 1) or not(var49 = 1) or not(var50 = 1) or var51 = 1 or var53 = 1)
and (not(var48 = 1) or not(var49 = 1) or not(var50 = 1) or var51 = 1 or var54 =
1) and (not(var48 = 1) or not(var49 = 1) or not(var50 = 1) or var51 = 1 or var55
 = 1) and not(var56 = 1) and not(var57 = 1) and not(var58 = 1) and not(var59 = 1
) and not(var60 = 1) and (not(var24 = 1) or not(var60 = 1)) and (not(var24 = 1)
or not(var56 = 1)) and (not(var4 = 1) or not(var25 = 1)) and (not(var1 = 1) or
not(var25 = 1)) and (not(var5 = 1) or not(var26 = 1)) and (not(var2 = 1) or not(
var26 = 1)) and (not(var28 = 1) or not(var57 = 1)) and (not(var28 = 1) or not(
var60 = 1)) and (not(var9 = 1) or not(var29 = 1)) and (not(var4 = 1) or not(
var29 = 1)) and (not(var10 = 1) or not(var30 = 1)) and (not(var5 = 1) or not(
var30 = 1)) and (not(var32 = 1) or not(var58 = 1)) and (not(var32 = 1) or not(
var60 = 1)) and (not(var14 = 1) or not(var33 = 1)) and (not(var4 = 1) or not(
var33 = 1)) and (not(var15 = 1) or not(var34 = 1)) and (not(var5 = 1) or not(
var34 = 1)) and (not(var36 = 1) or not(var59 = 1)) and (not(var36 = 1) or not(
var60 = 1)) and (not(var19 = 1) or not(var38 = 1)) and (not(var4 = 1) or not(
var38 = 1)) and (not(var20 = 1) or not(var40 = 1)) and (not(var5 = 1) or not(
var40 = 1)) and (not(var37 = 1) or var60 = 1) and (not(var39 = 1) or var4 = 1)
and (not(var41 = 1) or var5 = 1) and (not(var24 = 1) or var4 = 1) and (not(var7
= 1) or not(var24 = 1)) and (not(var24 = 1) or var1 = 1) and (not(var25 = 1) or
var5 = 1) and (not(var8 = 1) or not(var25 = 1)) and (not(var25 = 1) or var2 = 1)
 and (not(var26 = 1) or var6 = 1) and (not(var26 = 1) or not(var44 = 1)) and (
not(var26 = 1) or var3 = 1) and (not(var28 = 1) or var9 = 1) and (not(var12 = 1)
 or not(var28 = 1)) and (not(var28 = 1) or var4 = 1) and (not(var29 = 1) or
var10 = 1) and (not(var13 = 1) or not(var29 = 1)) and (not(var29 = 1) or var5 =
1) and (not(var30 = 1) or var11 = 1) and (not(var30 = 1) or not(var45 = 1)) and
(not(var30 = 1) or var6 = 1) and (not(var32 = 1) or var14 = 1) and (not(var17 =
1) or not(var32 = 1)) and (not(var32 = 1) or var4 = 1) and (not(var33 = 1) or
var15 = 1) and (not(var18 = 1) or not(var33 = 1)) and (not(var33 = 1) or var5 =
1) and (not(var34 = 1) or var16 = 1) and (not(var34 = 1) or not(var46 = 1)) and
(not(var34 = 1) or var6 = 1) and (not(var36 = 1) or var19 = 1) and (not(var22 =
1) or not(var36 = 1)) and (not(var36 = 1) or var4 = 1) and (not(var38 = 1) or
var20 = 1) and (not(var23 = 1) or not(var38 = 1)) and (not(var38 = 1) or var5 =
1) and (not(var40 = 1) or var21 = 1) and (not(var40 = 1) or not(var47 = 1)) and
(not(var40 = 1) or var6 = 1) and (not(var4 = 1) or not(var37 = 1)) and (not(var5
 = 1) or not(var39 = 1)) and (not(var6 = 1) or not(var41 = 1)) and (not(var1 = 1
) or var24 = 1 or var56 = 1) and (not(var2 = 1) or var1 = 1 or var25 = 1) and (
not(var3 = 1) or var2 = 1 or var26 = 1) and (not(var56 = 1) or var1 = 1) and (
not(var1 = 1) or var2 = 1) and (not(var2 = 1) or var3 = 1) and (not(var4 = 1) or
 var24 = 1 or var28 = 1 or var32 = 1 or var36 = 1 or var60 = 1) and (not(var5 =
1) or var4 = 1 or var25 = 1 or var29 = 1 or var33 = 1 or var38 = 1) and (not(
var6 = 1) or var5 = 1 or var26 = 1 or var30 = 1 or var34 = 1 or var40 = 1) and (
not(var60 = 1) or var4 = 1 or var37 = 1) and (not(var4 = 1) or var5 = 1 or var39
 = 1) and (not(var5 = 1) or var6 = 1 or var41 = 1) and (not(var7 = 1) or var55 =
 1) and (not(var8 = 1) or var7 = 1) and (not(var44 = 1) or var8 = 1) and (not(
var55 = 1) or var7 = 1 or var24 = 1) and (not(var7 = 1) or var8 = 1 or var25 = 1
) and (not(var8 = 1) or var26 = 1 or var44 = 1) and (not(var9 = 1) or var28 = 1
or var57 = 1) and (not(var10 = 1) or var9 = 1 or var29 = 1) and (not(var11 = 1)
or var10 = 1 or var30 = 1) and (not(var57 = 1) or var9 = 1) and (not(var9 = 1)
or var10 = 1) and (not(var10 = 1) or var11 = 1) and (not(var12 = 1) or var52 = 1
) and (not(var13 = 1) or var12 = 1) and (not(var45 = 1) or var13 = 1) and (not(
var52 = 1) or var12 = 1 or var28 = 1) and (not(var12 = 1) or var13 = 1 or var29
= 1) and (not(var13 = 1) or var30 = 1 or var45 = 1) and (not(var14 = 1) or var32
 = 1 or var58 = 1) and (not(var15 = 1) or var14 = 1 or var33 = 1) and (not(var16
 = 1) or var15 = 1 or var34 = 1) and (not(var58 = 1) or var14 = 1) and (not(
var14 = 1) or var15 = 1) and (not(var15 = 1) or var16 = 1) and (not(var17 = 1)
or var53 = 1) and (not(var18 = 1) or var17 = 1) and (not(var46 = 1) or var18 = 1
) and (not(var53 = 1) or var17 = 1 or var32 = 1) and (not(var17 = 1) or var18 =
1 or var33 = 1) and (not(var18 = 1) or var34 = 1 or var46 = 1) and (not(var19 =
1) or var36 = 1 or var59 = 1) and (not(var20 = 1) or var19 = 1 or var38 = 1) and
 (not(var21 = 1) or var20 = 1 or var40 = 1) and (not(var59 = 1) or var19 = 1)
and (not(var19 = 1) or var20 = 1) and (not(var20 = 1) or var21 = 1) and (not(
var22 = 1) or var54 = 1) and (not(var23 = 1) or var22 = 1) and (not(var47 = 1)
or var23 = 1) and (not(var54 = 1) or var22 = 1 or var36 = 1) and (not(var22 = 1)
 or var23 = 1 or var38 = 1) and (not(var23 = 1) or var40 = 1 or var47 = 1) and (
not(var24 = 1) or not(var28 = 1)) and (not(var25 = 1) or not(var29 = 1)) and (
not(var26 = 1) or not(var30 = 1)) and (not(var27 = 1) or not(var31 = 1)) and (
not(var24 = 1) or not(var32 = 1)) and (not(var25 = 1) or not(var33 = 1)) and (
not(var26 = 1) or not(var34 = 1)) and (not(var27 = 1) or not(var35 = 1)) and (
not(var24 = 1) or not(var36 = 1)) and (not(var25 = 1) or not(var38 = 1)) and (
not(var26 = 1) or not(var40 = 1)) and (not(var27 = 1) or not(var42 = 1)) and (
not(var24 = 1) or not(var37 = 1)) and (not(var25 = 1) or not(var39 = 1)) and (
not(var26 = 1) or not(var41 = 1)) and (not(var27 = 1) or not(var43 = 1)) and (
not(var28 = 1) or not(var32 = 1)) and (not(var29 = 1) or not(var33 = 1)) and (
not(var30 = 1) or not(var34 = 1)) and (not(var31 = 1) or not(var35 = 1)) and (
not(var28 = 1) or not(var36 = 1)) and (not(var29 = 1) or not(var38 = 1)) and (
not(var30 = 1) or not(var40 = 1)) and (not(var31 = 1) or not(var42 = 1)) and (
not(var28 = 1) or not(var37 = 1)) and (not(var29 = 1) or not(var39 = 1)) and (
not(var30 = 1) or not(var41 = 1)) and (not(var31 = 1) or not(var43 = 1)) and (
not(var32 = 1) or not(var36 = 1)) and (not(var33 = 1) or not(var38 = 1)) and (
not(var34 = 1) or not(var40 = 1)) and (not(var35 = 1) or not(var42 = 1)) and (
not(var32 = 1) or not(var37 = 1)) and (not(var33 = 1) or not(var39 = 1)) and (
not(var34 = 1) or not(var41 = 1)) and (not(var35 = 1) or not(var43 = 1)) and (
not(var36 = 1) or not(var37 = 1)) and (not(var38 = 1) or not(var39 = 1)) and (
not(var40 = 1) or not(var41 = 1)) and (not(var42 = 1) or not(var43 = 1)) and not
(var44 = 1) and not(var45 = 1) and not(var46 = 1) and not(var47 = 1)))))))))))))
))))))))))))$



rlqsat toilet_a_04_01_4;


false


end;

