```(def-cartesian-product addresses
(octet octet octet octet)
(accessors octet_1 octet_2 octet_3 octet_4)
(theory octets))
```

```
logand(octet_2(x),octet_2(y)),
logand(octet_3(x),octet_3(y)),
logand(octet_4(x),octet_4(y))))"
(usages rewrite)
(theory octets))
```

```
logxor(octet_2(x),octet_2(y)),
logxor(octet_3(x),octet_3(y)),
logxor(octet_4(x),octet_4(y))))"
(usages rewrite)
(theory octets))
```

```
(usages d-r-convergence)
(theory octets)
(proof
(
insistent-direct-inference
simplify
)))

```

```
(usages d-r-convergence)
(theory octets)
(proof
(
insistent-direct-inference
simplify
)))

```

```
a_1 = a_2
iff
(logxor(octet_1(a_1),octet_1(a_2)) = 0#8
and
logxor(octet_2(a_1),octet_2(a_2)) = 0#8
and
logxor(octet_3(a_1),octet_3(a_2)) = 0#8
and
logxor(octet_4(a_1),octet_4(a_2)) = 0#8))"
(theory octets)
(proof
(
direct-inference
direct-inference
simplify
(block
(script-comment "`direct-inference' at (1)")
(cut-with-single-formula
octet_2(a_1),
octet_3(a_1),
octet_4(a_1))
and
octet_2(a_2),
octet_3(a_2),
octet_4(a_2))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p and p);")
(backchain
octet_2(a_2),
octet_3(a_2),
octet_4(a_2)));")
(backchain
octet_2(a_1),
octet_3(a_1),
octet_4(a_1)));")
(weaken (1 0))
simplify)
simplify)
)))
```

```
(series
simplify))
```

```
octet%lt(octet_1(a_1), octet_1(a_2))
or
(octet_1(a_1) = octet_1(a_2)
and
(octet%lt(octet_2(a_1), octet_2(a_2))
or
(octet_2(a_1) = octet_2(a_2)
and
(octet%lt(octet_3(a_1), octet_3(a_2))
or
(octet_3(a_1) = octet_3(a_2)
and
octet%lt(octet_4(a_1), octet_4(a_2))))))))"
(usages rewrite)
(theory octets))
```

```
(usages rewrite)
(theory octets))
```

```
(theory octets)
(proof
(
direct-inference
direct-inference
(antecedent-inference-strategy (0))
(block
(script-comment "`antecedent-inference-strategy' at (0 0 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises octet%lt-transitivity)
auto-instantiate-existential)
(block
(script-comment "`antecedent-inference-strategy' at (0 0 1 0 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(backchain "with(o:octet,o=o);"))
(block
(script-comment "`antecedent-inference-strategy' at (0 0 1 0 1 0 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(block
(script-comment "`antecedent-inference-strategy' at (0 0 1 0 1 0 1 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(block
(script-comment "`antecedent-inference-strategy' at (0 1 0 0 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(backchain-backwards "with(o:octet,o=o);"))
(block
(script-comment "`antecedent-inference-strategy' at (0 1 0 0 1 0 0)")
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_2(a_1),octet_2(a_3))));")
(apply-macete-with-minor-premises octet%lt-transitivity)
auto-instantiate-existential)
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 0 1 0 1 0 0)")
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_2(a_1),octet_2(a_3))));")
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 0 1 0 1 0 1 0)")
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_2(a_1),octet_2(a_3))));")
(block
(script-comment "`antecedent-inference-strategy' at (0 1 0 1 0 0 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(backchain-backwards
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 1 0 0 1 0 0)")
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_2(a_1),octet_2(a_3))));")
(backchain-backwards
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 1 0 0 1 0 1 0 0)")
direct-inference
direct-inference
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_3(a_1),octet_3(a_3))));")
(apply-macete-with-minor-premises octet%lt-transitivity)
auto-instantiate-existential)
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 1 0 0 1 0 1 0 1 0)")
direct-inference
direct-inference
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_3(a_1),octet_3(a_3))));")
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 1 0 1 0 0)")
direct-inference
(contrapose "with(p:prop,not(p));")
(backchain-backwards
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 1 0 1 0 1 0 0)")
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_2(a_1),octet_2(a_3))));")
(backchain-backwards
(block
(script-comment
"`antecedent-inference-strategy' at (0 1 0 1 0 1 0 1 0 1 0 0)")
direct-inference
direct-inference
direct-inference
direct-inference
direct-inference
(contrapose
not(octet%lt(octet_3(a_1),octet_3(a_3))));")
(backchain-backwards