cnf( bit_domain, axiom,
  X = o | X = i
).

cnf( bit_inverse, axiom,
  inv(X) != X
).

cnf( unpack1, axiom, 
  unpack1(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(inv(X1), X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(X1, inv(X2), X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(X1, X2, inv(X3), X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(X1, X2, X3, inv(X4), pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(X1, X2, X3, X4, inv(pack1(X1, X2, X3, X4)), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(X1, X2, X3, X4, pack1(X1, X2, X3, X4), inv(pack2(X1, X2, X3, X4)), pack3(X1, X2, X3, X4)) = X1
).

cnf( unpack1, axiom, 
  unpack1(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), inv(pack3(X1, X2, X3, X4))) = X1
).

cnf( unpack2, axiom, 
  unpack2(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(inv(X1), X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(X1, inv(X2), X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(X1, X2, inv(X3), X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(X1, X2, X3, inv(X4), pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(X1, X2, X3, X4, inv(pack1(X1, X2, X3, X4)), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(X1, X2, X3, X4, pack1(X1, X2, X3, X4), inv(pack2(X1, X2, X3, X4)), pack3(X1, X2, X3, X4)) = X2
).

cnf( unpack2, axiom, 
  unpack2(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), inv(pack3(X1, X2, X3, X4))) = X2
).

cnf( unpack3, axiom, 
  unpack3(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(inv(X1), X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(X1, inv(X2), X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(X1, X2, inv(X3), X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(X1, X2, X3, inv(X4), pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(X1, X2, X3, X4, inv(pack1(X1, X2, X3, X4)), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(X1, X2, X3, X4, pack1(X1, X2, X3, X4), inv(pack2(X1, X2, X3, X4)), pack3(X1, X2, X3, X4)) = X3
).

cnf( unpack3, axiom, 
  unpack3(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), inv(pack3(X1, X2, X3, X4))) = X3
).

cnf( unpack4, axiom, 
  unpack4(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(inv(X1), X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(X1, inv(X2), X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(X1, X2, inv(X3), X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(X1, X2, X3, inv(X4), pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(X1, X2, X3, X4, inv(pack1(X1, X2, X3, X4)), pack2(X1, X2, X3, X4), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(X1, X2, X3, X4, pack1(X1, X2, X3, X4), inv(pack2(X1, X2, X3, X4)), pack3(X1, X2, X3, X4)) = X4
).

cnf( unpack4, axiom, 
  unpack4(X1, X2, X3, X4, pack1(X1, X2, X3, X4), pack2(X1, X2, X3, X4), inv(pack3(X1, X2, X3, X4))) = X4
).