cube(a)
smaller(b,a)
between(c,a,d)
large(d)
larger(e,a)
tet(b)
dodec(e)
rightof(e,b)
rightof(e,b)
smaller(a,e)
backof(d,a)
samerow(b,d)
samesize(b,c)
-frontof(f,a)
rightof(f,a)&leftof(f,b)
backof(f,a)|smaller(f,a)
between(e,c,a)&between(d,c,a)
-(larger(e,c)|larger(d,c))
-(larger(e,d)|smaller(e,d))
smaller(c,a)&larger(c,e)
frontof(c,f)&smaller(c,f)
samerow(b,a)&-samecol(b,f)
-(samecol(e,c)|samecol(e,d))
small(a)|(large(c)&large(d))
backof(d,b)&backof(e,b)
backof(d,b)&backof(e,b)&larger(d,b)&larger(e,b)
cube(d)&cube(c)&-small(d)&-small(c)
-(rightof(e,c)&leftof(e,b))&-(rightof(a,c)&leftof(a,b))
-large(e)|backof(e,a)
-between(c,a,b)&-frontof(c,a)&-frontof(c,b)
(tet(a)&tet(e))|(tet(a)&tet(f))
-frontof(d,c)&-frontof(d,b)&-frontof(c,c)&-frontof(c,b)
between(c,d,f)|(smaller(c,d)&smaller(c,f))
-samerow(b,c)
samecol(b,e)&samerow(e,d)&samecol(d,a)
tet(c)-->-tet(a)
tet(b)-->-tet(d)
tet(b)-->-tet(c)
(cube(a)&dodec(b))-->leftof(a,b)
(cube(b)&cube(c))-->(samerow(b,c)&-samecol(b,c))
tet(b)-->small(b)
(cube(a)&cube(d))-->(leftof(a,d)|leftof(d,a))
cube(d)<->(medium(d)|large(d))
-(rightof(b,d)|leftof(b,d))-->(tet(b)|tet(d))
samesize(b,c)<->((tet(b)&dodec(c))|(tet(c)&dodec(b)))
tet(a)-->frontof(a,d)
(leftof(a,d)|rightof(a,d))-->cube(a)
between(c,a,e)|between(c,a,d)
small(c)-->rightof(c,a)
rightof(c,d)-->(rightof(b,c)&leftof(b,e))
tet(e)-->(rightof(e,b)<->frontof(e,b))
dodec(b)-->(-frontof(b,d)-->-backof(b,d))
backof(c,a)&frontof(c,e)
-(large(e)&tet(e))-->frontof(e,d)
cube(a)|cube(c)|cube(e)
tet(a)-->frontof(a,b)
larger(b,a)&larger(b,e)
larger(a,c)&larger(e,c)&-large(a)&-large(e)
sameshape(d,b)-->samesize(d,b)
large(a)<->cube(a)
-tet(c)-->cube(b)
-cube(e)-->(large(b)|large(d))
(tet(a)|tet(c))-->(cube(b)|cube(d))
large(a)<->small(d)
large(a)<->large(e)
tet(a)-->tet(b)
tet(b)-->tet(c)
(tet(a)&tet(c))-->(large(a)|large(c))
tet(a)&-large(c)
(small(c)&dodec(d))-->-(large(d)|small(d))
medium(c)-->(-cube(d)&-cube(e)&-cube(f))
-small(a)-->(small(d)&dodec(d))
large(e)<->(large(d)<->large(f))
samesize(d,e)
sameshape(d,e)
large(f)-->(cube(f)|dodec(f))
larger(c,e)-->larger(b,c)