%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:19:23 AM UTC 2026
% Result : Unsatisfiable 6.89s 1.34s
% Output : Proof 10.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n026.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sun Sep 27 10:54:56 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.38 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.89/1.34 Command-line arguments: --flatten --complete-subsets
% 6.89/1.34
% 6.89/1.34 % SZS status Unsatisfiable
% 6.89/1.34
% 9.28/1.66 % SZS output start Proof
% 9.28/1.66 Axiom 1 (ll0_inverse): not(ll0) = ll1.
% 9.28/1.66 Axiom 2 (ll1_inverse): not(ll1) = ll0.
% 9.28/1.66 Axiom 3 (not_involution): not(not(X)) = X.
% 9.28/1.66 Axiom 4 (xor_commutative): xor(X, Y) = xor(Y, X).
% 9.28/1.66 Axiom 5 (or_commutative): or(X, Y) = or(Y, X).
% 9.28/1.66 Axiom 6 (or_identity): or(X, ll0) = X.
% 9.28/1.66 Axiom 7 (or_boundedness): or(X, ll1) = ll1.
% 9.28/1.66 Axiom 8 (or_complement): or(X, not(X)) = ll1.
% 9.28/1.66 Axiom 9 (and_commutative): and(X, Y) = and(Y, X).
% 9.28/1.66 Axiom 10 (and_boundedness): and(X, ll0) = ll0.
% 9.28/1.66 Axiom 11 (and_identity): and(X, ll1) = X.
% 9.28/1.66 Axiom 12 (and_complement): and(X, not(X)) = ll0.
% 9.28/1.66 Axiom 13 (or_demorgan): not(or(X, Y)) = and(not(X), not(Y)).
% 9.28/1.66 Axiom 14 (and_demorgan): not(and(X, Y)) = or(not(X), not(Y)).
% 9.28/1.66 Axiom 15 (t4): not(and(t2, t3)) = t4.
% 9.28/1.66 Axiom 16 (sum): not(and(t6, t7)) = sum.
% 9.28/1.66 Axiom 17 (t6): not(and(t4, t5)) = t6.
% 9.28/1.66 Axiom 18 (t5): not(and(t4, cin)) = t5.
% 9.28/1.66 Axiom 19 (carry): not(and(t1, t5)) = carry.
% 9.28/1.66 Axiom 20 (t7): not(and(t5, cin)) = t7.
% 9.28/1.66 Axiom 21 (t2): not(and(a, t1)) = t2.
% 9.28/1.66 Axiom 22 (t1): not(and(a, b)) = t1.
% 9.28/1.66 Axiom 23 (t3): not(and(b, t1)) = t3.
% 9.28/1.66 Axiom 24 (xor_associative): xor(X, xor(Y, Z)) = xor(xor(X, Y), Z).
% 9.28/1.66 Axiom 25 (sum_def): xor(xor(a, b), cin) = sum_def.
% 9.28/1.66 Axiom 26 (or_absorption): or(X, and(X, Y)) = X.
% 9.28/1.66 Axiom 27 (or_associative): or(or(X, Y), Z) = or(X, or(Y, Z)).
% 9.28/1.66 Axiom 28 (and_absorption): and(X, or(X, Y)) = X.
% 9.28/1.66 Axiom 29 (and_associative): and(and(X, Y), Z) = and(X, and(Y, Z)).
% 9.28/1.66 Axiom 30 (or_distributive): and(X, or(Y, Z)) = or(and(X, Y), and(X, Z)).
% 9.28/1.66 Axiom 31 (xor_definition): or(and(not(X), Y), and(X, not(Y))) = xor(X, Y).
% 9.28/1.66 Axiom 32 (and_distributive): or(X, and(Y, Z)) = and(or(X, Y), or(X, Z)).
% 9.28/1.66 Axiom 33 (carry_def): or(and(cin, or(a, b)), and(not(cin), and(a, b))) = carry_def.
% 9.28/1.66
% 9.28/1.66 Lemma 34: or(X, not(X)) = not(ll0).
% 9.28/1.66 Proof:
% 9.28/1.66 or(X, not(X))
% 9.28/1.66 = { by axiom 8 (or_complement) }
% 9.28/1.66 ll1
% 9.28/1.66 = { by axiom 1 (ll0_inverse) R->L }
% 9.28/1.66 not(ll0)
% 9.28/1.66
% 9.28/1.66 Lemma 35: or(X, not(ll1)) = X.
% 9.28/1.66 Proof:
% 9.28/1.66 or(X, not(ll1))
% 9.28/1.66 = { by axiom 2 (ll1_inverse) }
% 9.28/1.66 or(X, ll0)
% 9.28/1.66 = { by axiom 6 (or_identity) }
% 9.28/1.66 X
% 9.28/1.66
% 9.28/1.66 Lemma 36: or(not(X), X) = not(ll0).
% 9.28/1.66 Proof:
% 9.28/1.66 or(not(X), X)
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(X, not(X))
% 9.28/1.66 = { by lemma 34 }
% 9.28/1.66 not(ll0)
% 9.28/1.66
% 9.28/1.66 Lemma 37: or(not(ll1), X) = X.
% 9.28/1.66 Proof:
% 9.28/1.66 or(not(ll1), X)
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(X, not(ll1))
% 9.28/1.66 = { by lemma 35 }
% 9.28/1.66 X
% 9.28/1.66
% 9.28/1.66 Lemma 38: and(X, not(X)) = not(ll1).
% 9.28/1.66 Proof:
% 9.28/1.66 and(X, not(X))
% 9.28/1.66 = { by axiom 12 (and_complement) }
% 9.28/1.66 ll0
% 9.28/1.66 = { by axiom 2 (ll1_inverse) R->L }
% 9.28/1.66 not(ll1)
% 9.28/1.66
% 9.28/1.66 Lemma 39: and(X, not(ll0)) = X.
% 9.28/1.66 Proof:
% 9.28/1.66 and(X, not(ll0))
% 9.28/1.66 = { by axiom 1 (ll0_inverse) }
% 9.28/1.66 and(X, ll1)
% 9.28/1.66 = { by axiom 11 (and_identity) }
% 9.28/1.66 X
% 9.28/1.66
% 9.28/1.66 Lemma 40: and(X, not(ll1)) = not(ll1).
% 9.28/1.66 Proof:
% 9.28/1.66 and(X, not(ll1))
% 9.28/1.66 = { by axiom 2 (ll1_inverse) }
% 9.28/1.66 and(X, ll0)
% 9.28/1.66 = { by axiom 10 (and_boundedness) }
% 9.28/1.66 ll0
% 9.28/1.66 = { by axiom 2 (ll1_inverse) R->L }
% 9.28/1.66 not(ll1)
% 9.28/1.66
% 9.28/1.66 Lemma 41: or(and(a, t1), and(b, t1)) = not(and(t2, t3)).
% 9.28/1.66 Proof:
% 9.28/1.66 or(and(a, t1), and(b, t1))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(and(b, t1), and(a, t1))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 or(and(b, t1), not(not(and(a, t1))))
% 9.28/1.66 = { by axiom 21 (t2) }
% 9.28/1.66 or(and(b, t1), not(t2))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 or(not(not(and(b, t1))), not(t2))
% 9.28/1.66 = { by axiom 23 (t3) }
% 9.28/1.66 or(not(t3), not(t2))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(not(t2), not(t3))
% 9.28/1.66 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.66 not(and(t2, t3))
% 9.28/1.66
% 9.28/1.66 Lemma 42: and(not(and(a, b)), X) = not(not(and(X, t1))).
% 9.28/1.66 Proof:
% 9.28/1.66 and(not(and(a, b)), X)
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 and(not(and(a, b)), not(not(X)))
% 9.28/1.66 = { by axiom 22 (t1) }
% 9.28/1.66 and(t1, not(not(X)))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 and(not(not(t1)), not(not(X)))
% 9.28/1.66 = { by axiom 13 (or_demorgan) R->L }
% 9.28/1.66 not(or(not(t1), not(X)))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 not(or(not(X), not(t1)))
% 9.28/1.66 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.66 not(not(and(X, t1)))
% 9.28/1.66
% 9.28/1.66 Lemma 43: or(and(X, not(Y)), and(not(X), Y)) = xor(X, Y).
% 9.28/1.66 Proof:
% 9.28/1.66 or(and(X, not(Y)), and(not(X), Y))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(and(not(X), Y), and(X, not(Y)))
% 9.28/1.66 = { by axiom 31 (xor_definition) }
% 9.28/1.66 xor(X, Y)
% 9.28/1.66
% 9.28/1.66 Lemma 44: xor(X, not(ll0)) = not(X).
% 9.28/1.66 Proof:
% 9.28/1.66 xor(X, not(ll0))
% 9.28/1.66 = { by lemma 43 R->L }
% 9.28/1.66 or(and(X, not(not(ll0))), and(not(X), not(ll0)))
% 9.28/1.66 = { by axiom 1 (ll0_inverse) }
% 9.28/1.66 or(and(X, not(ll1)), and(not(X), not(ll0)))
% 9.28/1.66 = { by lemma 40 }
% 9.28/1.66 or(not(ll1), and(not(X), not(ll0)))
% 9.28/1.66 = { by lemma 37 }
% 9.28/1.66 and(not(X), not(ll0))
% 9.28/1.66 = { by lemma 39 }
% 9.28/1.66 not(X)
% 9.28/1.66
% 9.28/1.66 Lemma 45: not(xor(X, Y)) = xor(X, not(Y)).
% 9.28/1.66 Proof:
% 9.28/1.66 not(xor(X, Y))
% 9.28/1.66 = { by lemma 44 R->L }
% 9.28/1.66 xor(xor(X, Y), not(ll0))
% 9.28/1.66 = { by axiom 24 (xor_associative) R->L }
% 9.28/1.66 xor(X, xor(Y, not(ll0)))
% 9.28/1.66 = { by lemma 44 }
% 9.28/1.66 xor(X, not(Y))
% 9.28/1.66
% 9.28/1.66 Lemma 46: and(or(X, Y), not(and(X, Y))) = xor(X, Y).
% 9.28/1.66 Proof:
% 9.28/1.66 and(or(X, Y), not(and(X, Y)))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 and(not(and(X, Y)), or(X, Y))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 and(not(and(X, Y)), not(not(or(X, Y))))
% 9.28/1.66 = { by axiom 13 (or_demorgan) R->L }
% 9.28/1.66 not(or(and(X, Y), not(or(X, Y))))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 not(or(not(or(X, Y)), and(X, Y)))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 not(or(not(or(X, Y)), and(not(not(X)), Y)))
% 9.28/1.66 = { by axiom 13 (or_demorgan) }
% 9.28/1.66 not(or(and(not(X), not(Y)), and(not(not(X)), Y)))
% 9.28/1.66 = { by lemma 43 }
% 9.28/1.66 not(xor(not(X), Y))
% 9.28/1.66 = { by axiom 4 (xor_commutative) }
% 9.28/1.66 not(xor(Y, not(X)))
% 9.28/1.66 = { by lemma 45 }
% 9.28/1.66 xor(Y, not(not(X)))
% 9.28/1.66 = { by axiom 3 (not_involution) }
% 9.28/1.66 xor(Y, X)
% 9.28/1.66 = { by axiom 4 (xor_commutative) }
% 9.28/1.66 xor(X, Y)
% 9.28/1.66
% 9.28/1.66 Lemma 47: not(and(t2, t3)) = xor(a, b).
% 9.28/1.66 Proof:
% 9.28/1.66 not(and(t2, t3))
% 9.28/1.66 = { by lemma 41 R->L }
% 9.28/1.66 or(and(a, t1), and(b, t1))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(and(b, t1), and(a, t1))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 or(and(b, t1), not(not(and(a, t1))))
% 9.28/1.66 = { by lemma 42 R->L }
% 9.28/1.66 or(and(b, t1), and(not(and(a, b)), a))
% 9.28/1.66 = { by axiom 22 (t1) }
% 9.28/1.66 or(and(b, t1), and(t1, a))
% 9.28/1.66 = { by axiom 9 (and_commutative) }
% 9.28/1.66 or(and(t1, b), and(t1, a))
% 9.28/1.66 = { by axiom 30 (or_distributive) R->L }
% 9.28/1.66 and(t1, or(b, a))
% 9.28/1.66 = { by axiom 22 (t1) R->L }
% 9.28/1.66 and(not(and(a, b)), or(b, a))
% 9.28/1.66 = { by axiom 5 (or_commutative) }
% 9.28/1.66 and(not(and(a, b)), or(a, b))
% 9.28/1.66 = { by axiom 9 (and_commutative) }
% 9.28/1.66 and(or(a, b), not(and(a, b)))
% 9.28/1.66 = { by lemma 46 }
% 9.28/1.66 xor(a, b)
% 9.28/1.66
% 9.28/1.66 Lemma 48: xor(not(ll0), X) = not(X).
% 9.28/1.66 Proof:
% 9.28/1.66 xor(not(ll0), X)
% 9.28/1.66 = { by axiom 4 (xor_commutative) R->L }
% 9.28/1.66 xor(X, not(ll0))
% 9.28/1.66 = { by lemma 44 }
% 9.28/1.66 not(X)
% 9.28/1.66
% 9.28/1.66 Lemma 49: xor(Y, not(X)) = xor(X, not(Y)).
% 9.28/1.66 Proof:
% 9.28/1.66 xor(Y, not(X))
% 9.28/1.66 = { by axiom 4 (xor_commutative) R->L }
% 9.28/1.66 xor(not(X), Y)
% 9.28/1.66 = { by lemma 48 R->L }
% 9.28/1.66 xor(xor(not(ll0), X), Y)
% 9.28/1.66 = { by axiom 24 (xor_associative) R->L }
% 9.28/1.66 xor(not(ll0), xor(X, Y))
% 9.28/1.66 = { by lemma 48 }
% 9.28/1.66 not(xor(X, Y))
% 9.28/1.66 = { by lemma 45 }
% 9.28/1.66 xor(X, not(Y))
% 9.28/1.66
% 9.28/1.66 Lemma 50: or(X, and(Y, X)) = X.
% 9.28/1.66 Proof:
% 9.28/1.66 or(X, and(Y, X))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 or(X, and(X, Y))
% 9.28/1.66 = { by axiom 26 (or_absorption) }
% 9.28/1.66 X
% 9.28/1.66
% 9.28/1.66 Lemma 51: or(Y, or(X, Z)) = or(X, or(Y, Z)).
% 9.28/1.66 Proof:
% 9.28/1.66 or(Y, or(X, Z))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 or(or(X, Z), Y)
% 9.28/1.66 = { by axiom 27 (or_associative) }
% 9.28/1.66 or(X, or(Z, Y))
% 9.28/1.66 = { by axiom 5 (or_commutative) }
% 9.28/1.66 or(X, or(Y, Z))
% 9.28/1.66
% 9.28/1.66 Lemma 52: or(Z, or(X, Y)) = or(X, or(Y, Z)).
% 9.28/1.66 Proof:
% 9.28/1.66 or(Z, or(X, Y))
% 9.28/1.66 = { by lemma 51 }
% 9.28/1.66 or(X, or(Z, Y))
% 9.28/1.66 = { by axiom 5 (or_commutative) }
% 9.28/1.66 or(X, or(Y, Z))
% 9.28/1.66
% 9.28/1.66 Lemma 53: or(Z, or(Y, X)) = or(X, or(Y, Z)).
% 9.28/1.66 Proof:
% 9.28/1.66 or(Z, or(Y, X))
% 9.28/1.66 = { by lemma 52 R->L }
% 9.28/1.66 or(X, or(Z, Y))
% 9.28/1.66 = { by axiom 5 (or_commutative) }
% 9.28/1.66 or(X, or(Y, Z))
% 9.28/1.66
% 9.28/1.66 Lemma 54: and(X, or(Y, X)) = X.
% 9.28/1.66 Proof:
% 9.28/1.66 and(X, or(Y, X))
% 9.28/1.66 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.66 and(X, or(X, Y))
% 9.28/1.66 = { by axiom 28 (and_absorption) }
% 9.28/1.66 X
% 9.28/1.66
% 9.28/1.66 Lemma 55: and(Y, and(X, Z)) = and(X, and(Y, Z)).
% 9.28/1.66 Proof:
% 9.28/1.66 and(Y, and(X, Z))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 and(and(X, Z), Y)
% 9.28/1.66 = { by axiom 29 (and_associative) }
% 9.28/1.66 and(X, and(Z, Y))
% 9.28/1.66 = { by axiom 9 (and_commutative) }
% 9.28/1.66 and(X, and(Y, Z))
% 9.28/1.66
% 9.28/1.66 Lemma 56: and(Z, and(X, Y)) = and(X, and(Y, Z)).
% 9.28/1.66 Proof:
% 9.28/1.66 and(Z, and(X, Y))
% 9.28/1.66 = { by lemma 55 }
% 9.28/1.66 and(X, and(Z, Y))
% 9.28/1.66 = { by axiom 9 (and_commutative) }
% 9.28/1.66 and(X, and(Y, Z))
% 9.28/1.66
% 9.28/1.66 Lemma 57: and(or(X, Y), X) = X.
% 9.28/1.66 Proof:
% 9.28/1.66 and(or(X, Y), X)
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 and(X, or(X, Y))
% 9.28/1.66 = { by axiom 28 (and_absorption) }
% 9.28/1.66 X
% 9.28/1.66
% 9.28/1.66 Lemma 58: not(and(not(Y), X)) = or(not(X), Y).
% 9.28/1.66 Proof:
% 9.28/1.66 not(and(not(Y), X))
% 9.28/1.66 = { by axiom 9 (and_commutative) }
% 9.28/1.66 not(and(X, not(Y)))
% 9.28/1.66 = { by axiom 14 (and_demorgan) }
% 9.28/1.66 or(not(X), not(not(Y)))
% 9.28/1.66 = { by axiom 3 (not_involution) }
% 9.28/1.66 or(not(X), Y)
% 9.28/1.66
% 9.28/1.66 Lemma 59: and(X, or(Y, not(X))) = and(X, Y).
% 9.28/1.66 Proof:
% 9.28/1.66 and(X, or(Y, not(X)))
% 9.28/1.66 = { by axiom 30 (or_distributive) }
% 9.28/1.66 or(and(X, Y), and(X, not(X)))
% 9.28/1.66 = { by lemma 38 }
% 9.28/1.66 or(and(X, Y), not(ll1))
% 9.28/1.66 = { by lemma 35 }
% 9.28/1.66 and(X, Y)
% 9.28/1.66
% 9.28/1.66 Lemma 60: xor(X, and(X, Y)) = and(X, not(Y)).
% 9.28/1.66 Proof:
% 9.28/1.66 xor(X, and(X, Y))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 xor(X, and(Y, X))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 xor(X, and(Y, not(not(X))))
% 9.28/1.66 = { by lemma 43 R->L }
% 9.28/1.66 or(and(X, not(and(Y, not(not(X))))), and(not(X), and(Y, not(not(X)))))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 or(and(X, not(and(Y, not(not(X))))), and(not(X), and(not(not(X)), Y)))
% 9.28/1.66 = { by axiom 29 (and_associative) R->L }
% 9.28/1.66 or(and(X, not(and(Y, not(not(X))))), and(and(not(X), not(not(X))), Y))
% 9.28/1.66 = { by lemma 38 }
% 9.28/1.66 or(and(X, not(and(Y, not(not(X))))), and(not(ll1), Y))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 or(and(X, not(and(Y, not(not(X))))), and(Y, not(ll1)))
% 9.28/1.66 = { by lemma 40 }
% 9.28/1.66 or(and(X, not(and(Y, not(not(X))))), not(ll1))
% 9.28/1.66 = { by lemma 35 }
% 9.28/1.66 and(X, not(and(Y, not(not(X)))))
% 9.28/1.66 = { by axiom 14 (and_demorgan) }
% 9.28/1.66 and(X, or(not(Y), not(not(not(X)))))
% 9.28/1.66 = { by axiom 3 (not_involution) }
% 9.28/1.66 and(X, or(not(Y), not(X)))
% 9.28/1.66 = { by lemma 59 }
% 9.28/1.66 and(X, not(Y))
% 9.28/1.66
% 9.28/1.66 Lemma 61: xor(X, and(Y, X)) = and(X, not(Y)).
% 9.28/1.66 Proof:
% 9.28/1.66 xor(X, and(Y, X))
% 9.28/1.66 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.66 xor(X, and(X, Y))
% 9.28/1.66 = { by lemma 60 }
% 9.28/1.66 and(X, not(Y))
% 9.28/1.66
% 9.28/1.66 Lemma 62: xor(X, xor(Y, Z)) = xor(Y, xor(X, Z)).
% 9.28/1.66 Proof:
% 9.28/1.66 xor(X, xor(Y, Z))
% 9.28/1.66 = { by axiom 4 (xor_commutative) R->L }
% 9.28/1.66 xor(xor(Y, Z), X)
% 9.28/1.66 = { by axiom 24 (xor_associative) R->L }
% 9.28/1.66 xor(Y, xor(Z, X))
% 9.28/1.66 = { by axiom 4 (xor_commutative) }
% 9.28/1.66 xor(Y, xor(X, Z))
% 9.28/1.66
% 9.28/1.66 Lemma 63: xor(X, xor(Y, X)) = Y.
% 9.28/1.66 Proof:
% 9.28/1.66 xor(X, xor(Y, X))
% 9.28/1.66 = { by lemma 62 R->L }
% 9.28/1.66 xor(Y, xor(X, X))
% 9.28/1.66 = { by axiom 3 (not_involution) R->L }
% 9.28/1.66 xor(Y, xor(X, not(not(X))))
% 9.28/1.66 = { by lemma 43 R->L }
% 9.28/1.66 xor(Y, or(and(X, not(not(not(X)))), and(not(X), not(not(X)))))
% 9.28/1.66 = { by lemma 38 }
% 9.28/1.66 xor(Y, or(and(X, not(not(not(X)))), not(ll1)))
% 9.28/1.66 = { by lemma 35 }
% 9.28/1.66 xor(Y, and(X, not(not(not(X)))))
% 9.28/1.66 = { by axiom 3 (not_involution) }
% 9.28/1.66 xor(Y, and(X, not(X)))
% 9.28/1.66 = { by lemma 38 }
% 9.28/1.66 xor(Y, not(ll1))
% 9.28/1.66 = { by axiom 2 (ll1_inverse) }
% 9.28/1.66 xor(Y, ll0)
% 9.28/1.66 = { by lemma 43 R->L }
% 9.28/1.66 or(and(Y, not(ll0)), and(not(Y), ll0))
% 9.28/1.66 = { by lemma 39 }
% 9.28/1.66 or(Y, and(not(Y), ll0))
% 9.28/1.66 = { by axiom 2 (ll1_inverse) R->L }
% 9.28/1.66 or(Y, and(not(Y), not(ll1)))
% 9.28/1.66 = { by lemma 40 }
% 9.28/1.66 or(Y, not(ll1))
% 9.28/1.66 = { by lemma 35 }
% 9.28/1.66 Y
% 9.28/1.66
% 9.28/1.66 Lemma 64: xor(X, xor(X, Y)) = Y.
% 9.28/1.66 Proof:
% 9.28/1.66 xor(X, xor(X, Y))
% 9.28/1.66 = { by axiom 4 (xor_commutative) R->L }
% 9.28/1.66 xor(X, xor(Y, X))
% 9.28/1.66 = { by lemma 63 }
% 9.28/1.67 Y
% 9.28/1.67
% 9.28/1.67 Lemma 65: or(X, and(Y, not(X))) = or(X, Y).
% 9.28/1.67 Proof:
% 9.28/1.67 or(X, and(Y, not(X)))
% 9.28/1.67 = { by axiom 32 (and_distributive) }
% 9.28/1.67 and(or(X, Y), or(X, not(X)))
% 9.28/1.67 = { by lemma 34 }
% 9.28/1.67 and(or(X, Y), not(ll0))
% 9.28/1.67 = { by lemma 39 }
% 9.28/1.67 or(X, Y)
% 9.28/1.67
% 9.28/1.67 Lemma 66: and(not(and(t2, t3)), and(X, not(and(t4, cin)))) = and(X, and(t4, t5)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t2, t3)), and(X, not(and(t4, cin))))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(not(and(t4, cin)), X))
% 9.28/1.67 = { by axiom 18 (t5) }
% 9.28/1.67 and(not(and(t2, t3)), and(t5, X))
% 9.28/1.67 = { by axiom 15 (t4) }
% 9.28/1.67 and(t4, and(t5, X))
% 9.28/1.67 = { by axiom 29 (and_associative) R->L }
% 9.28/1.67 and(and(t4, t5), X)
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 and(X, and(t4, t5))
% 9.28/1.67
% 9.28/1.67 Lemma 67: and(not(and(t2, t3)), and(not(and(t4, cin)), X)) = and(X, and(t4, t5)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t2, t3)), and(not(and(t4, cin)), X))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(X, not(and(t4, cin))))
% 9.28/1.67 = { by lemma 66 }
% 9.28/1.67 and(X, and(t4, t5))
% 9.28/1.67
% 9.28/1.67 Lemma 68: and(not(and(t4, cin)), X) = and(t5, X).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t4, cin)), X)
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(X, not(and(t4, cin)))
% 9.28/1.67 = { by axiom 18 (t5) }
% 9.28/1.67 and(X, t5)
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(t5, X)
% 9.28/1.67
% 9.28/1.67 Lemma 69: and(not(and(t2, t3)), and(X, Y)) = and(X, and(t4, Y)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t2, t3)), and(X, Y))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(Y, X))
% 9.28/1.67 = { by axiom 15 (t4) }
% 9.28/1.67 and(t4, and(Y, X))
% 9.28/1.67 = { by axiom 29 (and_associative) R->L }
% 9.28/1.67 and(and(t4, Y), X)
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 and(X, and(t4, Y))
% 9.28/1.67
% 9.28/1.67 Lemma 70: or(and(t4, t5), not(cin)) = not(cin).
% 9.28/1.67 Proof:
% 9.28/1.67 or(and(t4, t5), not(cin))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(not(cin), and(t4, t5))
% 9.28/1.67 = { by lemma 39 R->L }
% 9.28/1.67 and(or(not(cin), and(t4, t5)), not(ll0))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 and(not(ll0), or(not(cin), and(t4, t5)))
% 9.28/1.67 = { by lemma 36 R->L }
% 9.28/1.67 and(or(not(cin), cin), or(not(cin), and(t4, t5)))
% 9.28/1.67 = { by axiom 32 (and_distributive) R->L }
% 9.28/1.67 or(not(cin), and(cin, and(t4, t5)))
% 9.28/1.67 = { by lemma 67 R->L }
% 9.28/1.67 or(not(cin), and(not(and(t2, t3)), and(not(and(t4, cin)), cin)))
% 9.28/1.67 = { by lemma 68 }
% 9.28/1.67 or(not(cin), and(not(and(t2, t3)), and(t5, cin)))
% 9.28/1.67 = { by lemma 69 }
% 9.28/1.67 or(not(cin), and(t5, and(t4, cin)))
% 9.28/1.67 = { by axiom 18 (t5) R->L }
% 9.28/1.67 or(not(cin), and(not(and(t4, cin)), and(t4, cin)))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 or(not(cin), and(and(t4, cin), not(and(t4, cin))))
% 9.28/1.67 = { by lemma 38 }
% 9.28/1.67 or(not(cin), not(ll1))
% 9.28/1.67 = { by lemma 35 }
% 9.28/1.67 not(cin)
% 9.28/1.67
% 9.28/1.67 Lemma 71: and(not(X), or(Y, X)) = and(Y, not(X)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(X), or(Y, X))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 and(not(X), or(X, Y))
% 9.28/1.67 = { by axiom 30 (or_distributive) }
% 9.28/1.67 or(and(not(X), X), and(not(X), Y))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 or(and(X, not(X)), and(not(X), Y))
% 9.28/1.67 = { by lemma 38 }
% 9.28/1.67 or(not(ll1), and(not(X), Y))
% 9.28/1.67 = { by lemma 37 }
% 9.28/1.67 and(not(X), Y)
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 and(Y, not(X))
% 9.28/1.67
% 9.28/1.67 Lemma 72: or(not(X), not(not(and(t2, t3)))) = not(and(t4, X)).
% 9.28/1.67 Proof:
% 9.28/1.67 or(not(X), not(not(and(t2, t3))))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(not(not(and(t2, t3))), not(X))
% 9.28/1.67 = { by axiom 15 (t4) }
% 9.28/1.67 or(not(t4), not(X))
% 9.28/1.67 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.67 not(and(t4, X))
% 9.28/1.67
% 9.28/1.67 Lemma 73: and(not(and(t4, X)), not(X)) = not(X).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t4, X)), not(X))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(X), not(and(t4, X)))
% 9.28/1.67 = { by lemma 72 R->L }
% 9.28/1.67 and(not(X), or(not(X), not(not(and(t2, t3)))))
% 9.28/1.67 = { by axiom 28 (and_absorption) }
% 9.28/1.67 not(X)
% 9.28/1.67
% 9.28/1.67 Lemma 74: and(not(and(t2, t3)), not(cin)) = and(and(t4, t5), not(cin)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t2, t3)), not(cin))
% 9.28/1.67 = { by lemma 73 R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(not(and(t4, cin)), not(cin)))
% 9.28/1.67 = { by lemma 67 }
% 9.28/1.67 and(not(cin), and(t4, t5))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 and(and(t4, t5), not(cin))
% 9.28/1.67
% 9.28/1.67 Lemma 75: and(not(and(t5, X)), not(X)) = not(X).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t5, X)), not(X))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(X), not(and(t5, X)))
% 9.28/1.67 = { by axiom 14 (and_demorgan) }
% 9.28/1.67 and(not(X), or(not(t5), not(X)))
% 9.28/1.67 = { by axiom 18 (t5) R->L }
% 9.28/1.67 and(not(X), or(not(not(and(t4, cin))), not(X)))
% 9.28/1.67 = { by axiom 5 (or_commutative) }
% 9.28/1.67 and(not(X), or(not(X), not(not(and(t4, cin)))))
% 9.28/1.67 = { by axiom 28 (and_absorption) }
% 9.28/1.67 not(X)
% 9.28/1.67
% 9.28/1.67 Lemma 76: and(and(X, and(Y, Z)), Y) = and(X, and(Y, Z)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(and(X, and(Y, Z)), Y)
% 9.28/1.67 = { by axiom 26 (or_absorption) R->L }
% 9.28/1.67 and(and(X, and(Y, Z)), or(Y, and(Y, and(and(X, and(Y, Z)), Z))))
% 9.28/1.67 = { by lemma 55 R->L }
% 9.28/1.67 and(and(X, and(Y, Z)), or(Y, and(and(X, and(Y, Z)), and(Y, Z))))
% 9.28/1.67 = { by axiom 26 (or_absorption) R->L }
% 9.28/1.67 and(and(X, and(Y, Z)), or(Y, and(and(X, and(Y, Z)), or(and(Y, Z), and(and(Y, Z), X)))))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(and(X, and(Y, Z)), or(Y, and(and(X, and(Y, Z)), or(and(Y, Z), and(X, and(Y, Z))))))
% 9.28/1.67 = { by axiom 5 (or_commutative) }
% 9.28/1.67 and(and(X, and(Y, Z)), or(Y, and(and(X, and(Y, Z)), or(and(X, and(Y, Z)), and(Y, Z)))))
% 9.28/1.67 = { by axiom 28 (and_absorption) }
% 9.28/1.67 and(and(X, and(Y, Z)), or(Y, and(X, and(Y, Z))))
% 9.28/1.67 = { by axiom 5 (or_commutative) }
% 9.28/1.67 and(and(X, and(Y, Z)), or(and(X, and(Y, Z)), Y))
% 9.28/1.67 = { by axiom 28 (and_absorption) }
% 9.28/1.67 and(X, and(Y, Z))
% 9.28/1.67
% 9.28/1.67 Lemma 77: or(or(a, b), not(and(t2, t3))) = or(a, b).
% 9.28/1.67 Proof:
% 9.28/1.67 or(or(a, b), not(and(t2, t3)))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(not(and(t2, t3)), or(a, b))
% 9.28/1.67 = { by lemma 41 R->L }
% 9.28/1.67 or(or(and(a, t1), and(b, t1)), or(a, b))
% 9.28/1.67 = { by axiom 27 (or_associative) }
% 9.28/1.67 or(and(a, t1), or(and(b, t1), or(a, b)))
% 9.28/1.67 = { by lemma 51 }
% 9.28/1.67 or(and(a, t1), or(a, or(and(b, t1), b)))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(and(a, t1), or(a, or(b, and(b, t1))))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 or(and(a, t1), or(a, or(b, and(t1, b))))
% 9.28/1.67 = { by lemma 50 }
% 9.28/1.67 or(and(a, t1), or(a, b))
% 9.28/1.67 = { by axiom 5 (or_commutative) }
% 9.28/1.67 or(or(a, b), and(a, t1))
% 9.28/1.67 = { by axiom 3 (not_involution) R->L }
% 9.28/1.67 or(or(a, b), not(not(and(a, t1))))
% 9.28/1.67 = { by lemma 42 R->L }
% 9.28/1.67 or(or(a, b), and(not(and(a, b)), a))
% 9.28/1.67 = { by lemma 57 R->L }
% 9.28/1.67 or(or(a, b), and(not(and(a, b)), and(or(a, b), a)))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 or(or(a, b), and(not(and(a, b)), and(a, or(a, b))))
% 9.28/1.67 = { by axiom 22 (t1) }
% 9.28/1.67 or(or(a, b), and(t1, and(a, or(a, b))))
% 9.28/1.67 = { by axiom 29 (and_associative) R->L }
% 9.28/1.67 or(or(a, b), and(and(t1, a), or(a, b)))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 or(or(a, b), and(and(a, t1), or(a, b)))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 or(or(a, b), and(or(a, b), and(a, t1)))
% 9.28/1.67 = { by axiom 26 (or_absorption) }
% 9.28/1.67 or(a, b)
% 9.28/1.67
% 9.28/1.67 Lemma 78: or(and(t4, X), not(and(t2, t3))) = not(and(t2, t3)).
% 9.28/1.67 Proof:
% 9.28/1.67 or(and(t4, X), not(and(t2, t3)))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(not(and(t2, t3)), and(t4, X))
% 9.28/1.67 = { by axiom 15 (t4) }
% 9.28/1.67 or(t4, and(t4, X))
% 9.28/1.67 = { by axiom 26 (or_absorption) }
% 9.28/1.67 t4
% 9.28/1.67 = { by axiom 15 (t4) R->L }
% 9.28/1.67 not(and(t2, t3))
% 9.28/1.67
% 9.28/1.67 Lemma 79: or(not(and(X, Y)), xor(X, Y)) = not(and(X, Y)).
% 9.28/1.67 Proof:
% 9.28/1.67 or(not(and(X, Y)), xor(X, Y))
% 9.28/1.67 = { by lemma 46 R->L }
% 9.28/1.67 or(not(and(X, Y)), and(or(X, Y), not(and(X, Y))))
% 9.28/1.67 = { by lemma 50 }
% 9.28/1.67 not(and(X, Y))
% 9.28/1.67
% 9.28/1.67 Lemma 80: and(and(X, t5), not(and(t2, t3))) = and(and(X, t5), and(t4, t5)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(and(X, t5), not(and(t2, t3)))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(X, t5))
% 9.28/1.67 = { by axiom 28 (and_absorption) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), or(and(X, t5), not(and(t4, cin)))))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), or(not(and(t4, cin)), and(X, t5))))
% 9.28/1.67 = { by axiom 3 (not_involution) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), or(not(and(t4, cin)), not(not(and(X, t5))))))
% 9.28/1.67 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(and(and(t4, cin), not(and(X, t5))))))
% 9.28/1.67 = { by axiom 3 (not_involution) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(and(not(not(and(t4, cin))), not(and(X, t5))))))
% 9.28/1.67 = { by axiom 14 (and_demorgan) }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(and(not(not(and(t4, cin))), or(not(X), not(t5))))))
% 9.28/1.67 = { by axiom 18 (t5) R->L }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(and(not(not(and(t4, cin))), or(not(X), not(not(and(t4, cin))))))))
% 9.28/1.67 = { by axiom 5 (or_commutative) }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(and(not(not(and(t4, cin))), or(not(not(and(t4, cin))), not(X))))))
% 9.28/1.67 = { by axiom 28 (and_absorption) }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(not(not(and(t4, cin))))))
% 9.28/1.67 = { by axiom 3 (not_involution) }
% 9.28/1.67 and(not(and(t2, t3)), and(and(X, t5), not(and(t4, cin))))
% 9.28/1.67 = { by lemma 66 }
% 9.28/1.67 and(and(X, t5), and(t4, t5))
% 9.28/1.67
% 9.28/1.67 Lemma 81: and(and(a, b), not(and(X, t1))) = and(a, b).
% 9.28/1.67 Proof:
% 9.28/1.67 and(and(a, b), not(and(X, t1)))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(and(X, t1)), and(a, b))
% 9.28/1.67 = { by axiom 3 (not_involution) R->L }
% 9.28/1.67 and(not(and(X, t1)), not(not(and(a, b))))
% 9.28/1.67 = { by axiom 13 (or_demorgan) R->L }
% 9.28/1.67 not(or(and(X, t1), not(and(a, b))))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 not(or(not(and(a, b)), and(X, t1)))
% 9.28/1.67 = { by axiom 22 (t1) }
% 9.28/1.67 not(or(t1, and(X, t1)))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 not(or(t1, and(t1, X)))
% 9.28/1.67 = { by axiom 26 (or_absorption) }
% 9.28/1.67 not(t1)
% 9.28/1.67 = { by axiom 22 (t1) R->L }
% 9.28/1.67 not(not(and(a, b)))
% 9.28/1.67 = { by axiom 3 (not_involution) }
% 9.28/1.67 and(a, b)
% 9.28/1.67
% 9.28/1.67 Lemma 82: xor(and(t2, t3), not(and(t4, cin))) = and(t4, t5).
% 9.28/1.67 Proof:
% 9.28/1.67 xor(and(t2, t3), not(and(t4, cin)))
% 9.28/1.67 = { by lemma 49 }
% 9.28/1.67 xor(and(t4, cin), not(and(t2, t3)))
% 9.28/1.67 = { by axiom 4 (xor_commutative) R->L }
% 9.28/1.67 xor(not(and(t2, t3)), and(t4, cin))
% 9.28/1.67 = { by axiom 15 (t4) }
% 9.28/1.67 xor(t4, and(t4, cin))
% 9.28/1.67 = { by lemma 60 }
% 9.28/1.67 and(t4, not(cin))
% 9.28/1.67 = { by axiom 15 (t4) R->L }
% 9.28/1.67 and(not(and(t2, t3)), not(cin))
% 9.28/1.67 = { by lemma 74 }
% 9.28/1.67 and(and(t4, t5), not(cin))
% 9.28/1.67 = { by lemma 70 R->L }
% 9.28/1.67 and(and(t4, t5), or(and(t4, t5), not(cin)))
% 9.28/1.67 = { by axiom 28 (and_absorption) }
% 9.28/1.67 and(t4, t5)
% 9.28/1.67
% 9.28/1.67 Lemma 83: or(not(and(a, b)), not(and(t2, t3))) = not(and(a, b)).
% 9.28/1.67 Proof:
% 9.28/1.67 or(not(and(a, b)), not(and(t2, t3)))
% 9.28/1.67 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.67 not(and(and(a, b), and(t2, t3)))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 not(and(and(t2, t3), and(a, b)))
% 9.28/1.67 = { by axiom 29 (and_associative) }
% 9.28/1.67 not(and(t2, and(t3, and(a, b))))
% 9.28/1.67 = { by axiom 21 (t2) R->L }
% 9.28/1.67 not(and(not(and(a, t1)), and(t3, and(a, b))))
% 9.28/1.67 = { by axiom 23 (t3) R->L }
% 9.28/1.67 not(and(not(and(a, t1)), and(not(and(b, t1)), and(a, b))))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 not(and(not(and(a, t1)), and(and(a, b), not(and(b, t1)))))
% 9.28/1.67 = { by lemma 81 }
% 9.28/1.67 not(and(not(and(a, t1)), and(a, b)))
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 not(and(and(a, b), not(and(a, t1))))
% 9.28/1.67 = { by lemma 81 }
% 9.28/1.67 not(and(a, b))
% 9.28/1.67
% 9.28/1.67 Lemma 84: or(and(t4, X), or(Y, not(and(t2, t3)))) = or(Y, not(and(t2, t3))).
% 9.28/1.67 Proof:
% 9.28/1.67 or(and(t4, X), or(Y, not(and(t2, t3))))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(and(t4, X), or(not(and(t2, t3)), Y))
% 9.28/1.67 = { by axiom 27 (or_associative) R->L }
% 9.28/1.67 or(or(and(t4, X), not(and(t2, t3))), Y)
% 9.28/1.67 = { by lemma 78 }
% 9.28/1.67 or(not(and(t2, t3)), Y)
% 9.28/1.67 = { by axiom 5 (or_commutative) }
% 9.28/1.67 or(Y, not(and(t2, t3)))
% 9.28/1.67
% 9.28/1.67 Lemma 85: and(not(and(t4, t5)), and(X, not(and(t5, cin)))) = and(X, and(t6, t7)).
% 9.28/1.67 Proof:
% 9.28/1.67 and(not(and(t4, t5)), and(X, not(and(t5, cin))))
% 9.28/1.67 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.67 and(not(and(t4, t5)), and(not(and(t5, cin)), X))
% 9.28/1.67 = { by axiom 20 (t7) }
% 9.28/1.67 and(not(and(t4, t5)), and(t7, X))
% 9.28/1.67 = { by axiom 17 (t6) }
% 9.28/1.67 and(t6, and(t7, X))
% 9.28/1.67 = { by axiom 29 (and_associative) R->L }
% 9.28/1.67 and(and(t6, t7), X)
% 9.28/1.67 = { by axiom 9 (and_commutative) }
% 9.28/1.67 and(X, and(t6, t7))
% 9.28/1.67
% 9.28/1.67 Lemma 86: or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), and(t2, t3)) = not(and(t4, t5)).
% 9.28/1.67 Proof:
% 9.28/1.67 or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), and(t2, t3))
% 9.28/1.67 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.67 or(and(t2, t3), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 9.28/1.67 = { by lemma 53 }
% 9.28/1.68 or(and(not(cin), and(a, b)), or(and(cin, or(a, b)), and(t2, t3)))
% 9.28/1.68 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), or(and(t2, t3), and(cin, or(a, b))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), or(and(t2, t3), not(not(and(cin, or(a, b))))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), or(not(not(and(t2, t3))), not(not(and(cin, or(a, b))))))
% 9.28/1.68 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(and(not(and(t2, t3)), not(and(cin, or(a, b))))))
% 9.28/1.68 = { by lemma 61 R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(and(cin, or(a, b)), not(and(t2, t3))))))
% 9.28/1.68 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(not(and(t2, t3)), and(cin, or(a, b))))))
% 9.28/1.68 = { by axiom 9 (and_commutative) }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(not(and(t2, t3)), and(or(a, b), cin)))))
% 9.28/1.68 = { by lemma 69 }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(or(a, b), and(t4, cin)))))
% 9.28/1.68 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(and(t4, cin), or(a, b)))))
% 9.28/1.68 = { by lemma 77 R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(and(t4, cin), or(or(a, b), not(and(t2, t3)))))))
% 9.28/1.68 = { by lemma 84 R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(and(t4, cin), or(and(t4, cin), or(or(a, b), not(and(t2, t3))))))))
% 9.28/1.68 = { by lemma 77 }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(and(t4, cin), or(and(t4, cin), or(a, b))))))
% 9.28/1.68 = { by axiom 5 (or_commutative) }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(and(t4, cin), or(or(a, b), and(t4, cin))))))
% 9.28/1.68 = { by lemma 54 }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(not(and(t2, t3)), and(t4, cin))))
% 9.28/1.68 = { by axiom 4 (xor_commutative) }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(and(t4, cin), not(and(t2, t3)))))
% 9.28/1.68 = { by lemma 49 R->L }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(xor(and(t2, t3), not(and(t4, cin)))))
% 9.28/1.68 = { by lemma 82 }
% 9.28/1.68 or(and(not(cin), and(a, b)), not(and(t4, t5)))
% 9.28/1.68 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(not(cin), and(a, b)))
% 9.28/1.68 = { by axiom 28 (and_absorption) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), or(and(not(cin), and(a, b)), and(t2, t3))))
% 9.28/1.68 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), or(and(t2, t3), and(not(cin), and(a, b)))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), or(and(t2, t3), not(not(and(not(cin), and(a, b)))))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), or(not(not(and(t2, t3))), not(not(and(not(cin), and(a, b)))))))
% 9.28/1.68 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(and(not(and(t2, t3)), not(and(not(cin), and(a, b)))))))
% 9.28/1.68 = { by lemma 58 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(and(not(and(t2, t3)), or(not(and(a, b)), cin)))))
% 9.28/1.68 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(and(not(and(t2, t3)), or(cin, not(and(a, b)))))))
% 9.28/1.68 = { by axiom 15 (t4) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(and(t4, or(cin, not(and(a, b)))))))
% 9.28/1.68 = { by axiom 30 (or_distributive) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(or(and(t4, cin), and(t4, not(and(a, b)))))))
% 9.28/1.68 = { by axiom 15 (t4) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(or(and(t4, cin), and(not(and(t2, t3)), not(and(a, b)))))))
% 9.28/1.68 = { by lemma 83 R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(or(and(t4, cin), and(not(and(t2, t3)), or(not(and(a, b)), not(and(t2, t3))))))))
% 9.28/1.68 = { by lemma 54 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(or(and(t4, cin), not(and(t2, t3))))))
% 9.28/1.68 = { by lemma 78 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(not(and(t2, t3)))))
% 9.28/1.68 = { by axiom 3 (not_involution) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), and(t2, t3)))
% 9.28/1.68 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(t2, t3), and(not(cin), and(a, b))))
% 9.28/1.68 = { by lemma 56 R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(and(t2, t3), not(cin))))
% 9.28/1.68 = { by lemma 71 R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), or(and(t2, t3), cin))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), or(and(t2, t3), not(not(cin))))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), or(not(not(and(t2, t3))), not(not(cin))))))
% 9.28/1.68 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), not(and(not(and(t2, t3)), not(cin))))))
% 9.28/1.68 = { by lemma 74 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), not(and(and(t4, t5), not(cin))))))
% 9.28/1.68 = { by axiom 14 (and_demorgan) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), or(not(and(t4, t5)), not(not(cin))))))
% 9.28/1.68 = { by axiom 3 (not_involution) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), or(not(and(t4, t5)), cin))))
% 9.28/1.68 = { by lemma 71 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(and(t4, t5)), not(cin))))
% 9.28/1.68 = { by lemma 75 R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(and(t4, t5)), and(not(and(t5, cin)), not(cin)))))
% 9.28/1.68 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(and(t4, t5)), and(not(cin), not(and(t5, cin))))))
% 9.28/1.68 = { by lemma 85 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(not(cin), and(t6, t7))))
% 9.28/1.68 = { by axiom 9 (and_commutative) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(a, b), and(and(t6, t7), not(cin))))
% 9.28/1.68 = { by lemma 56 }
% 9.28/1.68 or(not(and(t4, t5)), and(and(t6, t7), and(not(cin), and(a, b))))
% 9.28/1.68 = { by axiom 9 (and_commutative) }
% 9.28/1.68 or(not(and(t4, t5)), and(and(not(cin), and(a, b)), and(t6, t7)))
% 9.28/1.68 = { by lemma 85 R->L }
% 9.28/1.68 or(not(and(t4, t5)), and(not(and(t4, t5)), and(and(not(cin), and(a, b)), not(and(t5, cin)))))
% 9.28/1.68 = { by axiom 26 (or_absorption) }
% 9.28/1.68 not(and(t4, t5))
% 9.28/1.68
% 9.28/1.68 Goal 1 (prove_circuit): tuple(sum, carry) = tuple(sum_def, carry_def).
% 9.28/1.68 Proof:
% 9.28/1.68 tuple(sum, carry)
% 9.28/1.68 = { by axiom 16 (sum) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), carry)
% 9.28/1.68 = { by axiom 19 (carry) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), not(and(t1, t5)))
% 9.28/1.68 = { by lemma 54 R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(t4, t5), not(and(t1, t5)))))
% 9.28/1.68 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(not(and(t1, t5)), and(t4, t5))))
% 9.28/1.68 = { by axiom 3 (not_involution) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(not(and(t1, t5)), not(not(and(t4, t5))))))
% 9.28/1.68 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(and(t1, t5), not(and(t4, t5))))))
% 9.28/1.68 = { by lemma 60 R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(xor(and(t1, t5), and(and(t1, t5), and(t4, t5))))))
% 9.28/1.68 = { by lemma 80 R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(xor(and(t1, t5), and(and(t1, t5), not(and(t2, t3)))))))
% 9.28/1.68 = { by lemma 60 }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(and(t1, t5), not(not(and(t2, t3)))))))
% 9.28/1.68 = { by axiom 3 (not_involution) }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(and(t1, t5), and(t2, t3)))))
% 9.28/1.68 = { by axiom 29 (and_associative) }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(t1, and(t5, and(t2, t3))))))
% 9.28/1.68 = { by axiom 22 (t1) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(t5, and(t2, t3))))))
% 9.28/1.68 = { by axiom 18 (t5) R->L }
% 9.28/1.68 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(not(and(t4, cin)), and(t2, t3))))))
% 9.28/1.68 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(and(t2, t3), not(and(t4, cin)))))))
% 9.28/1.69 = { by lemma 72 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(and(t2, t3), or(not(cin), not(not(and(t2, t3)))))))))
% 9.28/1.69 = { by axiom 3 (not_involution) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(and(t2, t3), or(not(cin), and(t2, t3)))))))
% 9.28/1.69 = { by axiom 5 (or_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(and(t2, t3), or(and(t2, t3), not(cin)))))))
% 9.28/1.69 = { by axiom 28 (and_absorption) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(not(and(a, b)), and(t2, t3)))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), not(and(and(t2, t3), not(and(a, b))))))
% 9.28/1.69 = { by axiom 14 (and_demorgan) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(not(and(t2, t3)), not(not(and(a, b))))))
% 9.28/1.69 = { by axiom 3 (not_involution) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(not(and(t2, t3)), and(a, b))))
% 9.28/1.69 = { by axiom 5 (or_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(a, b), not(and(t2, t3)))))
% 9.28/1.69 = { by lemma 47 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(a, b), xor(a, b))))
% 9.28/1.69 = { by lemma 54 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(a, b), and(xor(a, b), or(not(and(a, b)), xor(a, b))))))
% 9.28/1.69 = { by lemma 79 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(a, b), and(xor(a, b), not(and(a, b))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(a, b), and(not(and(a, b)), xor(a, b)))))
% 9.28/1.69 = { by axiom 3 (not_involution) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(not(not(and(a, b))), and(not(and(a, b)), xor(a, b)))))
% 9.28/1.69 = { by lemma 79 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(not(or(not(and(a, b)), xor(a, b))), and(not(and(a, b)), xor(a, b)))))
% 9.28/1.69 = { by axiom 13 (or_demorgan) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(not(not(and(a, b))), not(xor(a, b))), and(not(and(a, b)), xor(a, b)))))
% 9.28/1.69 = { by axiom 3 (not_involution) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(and(and(a, b), not(xor(a, b))), and(not(and(a, b)), xor(a, b)))))
% 9.28/1.69 = { by lemma 43 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), xor(a, b))))
% 9.28/1.69 = { by lemma 46 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), and(or(a, b), not(and(a, b))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), and(not(and(a, b)), or(a, b)))))
% 9.28/1.69 = { by lemma 37 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(not(ll1), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by lemma 40 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, not(ll1)), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 7 (or_boundedness) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, not(or(a, ll1))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 1 (ll0_inverse) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, not(or(a, not(ll0)))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by lemma 34 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, not(or(a, or(b, not(b))))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by lemma 52 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, not(or(not(b), or(a, b)))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 5 (or_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, not(or(or(a, b), not(b)))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 13 (or_demorgan) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, and(not(or(a, b)), not(not(b)))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 3 (not_involution) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, and(not(or(a, b)), b)), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(a, and(b, not(or(a, b)))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by lemma 56 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(not(or(a, b)), and(a, b)), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), or(and(and(a, b), not(or(a, b))), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by lemma 43 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), xor(and(a, b), or(a, b)))))
% 9.28/1.69 = { by axiom 4 (xor_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), xor(and(a, b), xor(or(a, b), and(a, b)))))
% 9.28/1.69 = { by lemma 63 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(not(and(t1, t5)), or(a, b)))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(t1, t5))))
% 9.28/1.69 = { by lemma 59 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), or(not(and(t1, t5)), not(or(a, b)))))
% 9.28/1.69 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), or(not(or(a, b)), not(and(t1, t5)))))
% 9.28/1.69 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(or(a, b), and(t1, t5)))))
% 9.28/1.69 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), or(a, b)))))
% 9.28/1.69 = { by axiom 28 (and_absorption) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(and(t1, t5), or(and(t1, t5), not(and(a, b)))), or(a, b)))))
% 9.28/1.69 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(and(t1, t5), or(not(and(a, b)), and(t1, t5))), or(a, b)))))
% 9.28/1.69 = { by axiom 22 (t1) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(and(t1, t5), or(t1, and(t1, t5))), or(a, b)))))
% 9.28/1.69 = { by axiom 26 (or_absorption) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(and(t1, t5), t1), or(a, b)))))
% 9.28/1.69 = { by axiom 22 (t1) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(and(t1, t5), not(and(a, b))), or(a, b)))))
% 9.28/1.69 = { by axiom 29 (and_associative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), and(not(and(a, b)), or(a, b))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), and(or(a, b), not(and(a, b)))))))
% 9.28/1.69 = { by lemma 46 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), xor(a, b)))))
% 9.28/1.69 = { by lemma 47 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), not(and(t2, t3))))))
% 9.28/1.69 = { by lemma 80 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), and(t4, t5)))))
% 9.28/1.69 = { by axiom 3 (not_involution) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t1, t5), not(not(and(t4, t5)))))))
% 9.28/1.69 = { by axiom 3 (not_involution) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(not(not(and(t1, t5))), not(not(and(t4, t5)))))))
% 9.28/1.69 = { by axiom 13 (or_demorgan) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(or(not(and(t1, t5)), not(and(t4, t5)))))))
% 9.28/1.69 = { by axiom 14 (and_demorgan) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(and(t1, t5), and(t4, t5)))))))
% 9.28/1.69 = { by lemma 80 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(and(t1, t5), not(and(t2, t3))))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(not(and(t2, t3)), and(t1, t5)))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(not(and(t2, t3)), and(t5, t1)))))))
% 9.28/1.69 = { by axiom 18 (t5) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(not(and(t2, t3)), and(not(and(t4, cin)), t1)))))))
% 9.28/1.69 = { by axiom 22 (t1) R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(not(and(t2, t3)), and(not(and(t4, cin)), not(and(a, b)))))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(not(and(t2, t3)), and(not(and(a, b)), not(and(t4, cin)))))))))
% 9.28/1.69 = { by lemma 66 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(not(and(a, b)), and(t4, t5)))))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(not(and(and(t4, t5), not(and(a, b))))))))
% 9.28/1.69 = { by axiom 14 (and_demorgan) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(or(not(and(t4, t5)), not(not(and(a, b))))))))
% 9.28/1.69 = { by axiom 3 (not_involution) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(or(not(and(t4, t5)), and(a, b))))))
% 9.28/1.69 = { by axiom 5 (or_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(not(or(and(a, b), not(and(t4, t5)))))))
% 9.28/1.69 = { by axiom 13 (or_demorgan) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(not(and(a, b)), not(not(and(t4, t5)))))))
% 9.28/1.69 = { by axiom 3 (not_involution) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(not(and(a, b)), and(t4, t5)))))
% 9.28/1.69 = { by axiom 9 (and_commutative) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t4, t5), not(and(a, b))))))
% 9.28/1.69 = { by lemma 83 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t4, t5), or(not(and(a, b)), not(and(t2, t3)))))))
% 9.28/1.69 = { by lemma 84 R->L }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t4, t5), or(and(t4, t5), or(not(and(a, b)), not(and(t2, t3))))))))
% 9.28/1.69 = { by lemma 83 }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(and(t4, t5), or(and(t4, t5), not(and(a, b)))))))
% 9.28/1.69 = { by axiom 28 (and_absorption) }
% 9.28/1.69 tuple(not(and(t6, t7)), and(or(a, b), not(and(t4, t5))))
% 9.28/1.70 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(a, b)))
% 9.28/1.70 = { by axiom 26 (or_absorption) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(or(a, b), and(not(cin), and(a, b))))))
% 9.28/1.70 = { by lemma 76 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(or(a, b), and(and(not(cin), and(a, b)), a)))))
% 9.28/1.70 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(or(a, b), and(a, and(not(cin), and(a, b)))))))
% 9.28/1.70 = { by axiom 29 (and_associative) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(and(or(a, b), a), and(not(cin), and(a, b))))))
% 9.28/1.70 = { by lemma 57 }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(a, and(not(cin), and(a, b))))))
% 9.28/1.70 = { by axiom 9 (and_commutative) }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(and(not(cin), and(a, b)), a))))
% 9.28/1.70 = { by lemma 76 }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(a, b), and(not(cin), and(a, b)))))
% 9.28/1.70 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), or(a, b))))
% 9.28/1.70 = { by lemma 65 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), and(or(a, b), not(and(not(cin), and(a, b)))))))
% 9.28/1.70 = { by lemma 58 }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), and(or(a, b), or(not(and(a, b)), cin)))))
% 9.28/1.70 = { by axiom 5 (or_commutative) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), and(or(a, b), or(cin, not(and(a, b)))))))
% 9.28/1.70 = { by axiom 30 (or_distributive) }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), or(and(or(a, b), cin), and(or(a, b), not(and(a, b)))))))
% 9.28/1.70 = { by axiom 9 (and_commutative) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), or(and(cin, or(a, b)), and(or(a, b), not(and(a, b)))))))
% 9.28/1.70 = { by lemma 46 }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), or(and(cin, or(a, b)), xor(a, b)))))
% 9.28/1.70 = { by lemma 47 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(and(not(cin), and(a, b)), or(and(cin, or(a, b)), not(and(t2, t3))))))
% 9.28/1.70 = { by lemma 53 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(not(and(t2, t3)), or(and(cin, or(a, b)), and(not(cin), and(a, b))))))
% 9.28/1.70 = { by axiom 5 (or_commutative) }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), not(and(t2, t3)))))
% 9.28/1.70 = { by lemma 65 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), and(not(and(t2, t3)), not(or(and(cin, or(a, b)), and(not(cin), and(a, b))))))))
% 9.28/1.70 = { by lemma 61 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(or(and(cin, or(a, b)), and(not(cin), and(a, b))), not(and(t2, t3)))))))
% 9.28/1.70 = { by lemma 71 R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), and(t2, t3)))))))
% 9.28/1.70 = { by lemma 86 }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), not(and(t4, t5)))))))
% 9.28/1.70 = { by axiom 14 (and_demorgan) }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(not(t4), not(t5)))))))
% 9.28/1.70 = { by axiom 15 (t4) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(not(not(and(t2, t3))), not(t5)))))))
% 9.28/1.70 = { by axiom 3 (not_involution) }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(and(t2, t3), not(t5)))))))
% 9.28/1.70 = { by axiom 18 (t5) R->L }
% 9.28/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(and(t2, t3), not(not(and(t4, cin)))))))))
% 10.09/1.70 = { by axiom 3 (not_involution) }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(and(t2, t3), and(t4, cin)))))))
% 10.09/1.70 = { by axiom 5 (or_commutative) R->L }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(not(and(t2, t3)), or(and(t4, cin), and(t2, t3)))))))
% 10.09/1.70 = { by lemma 78 R->L }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(or(and(t4, cin), not(and(t2, t3))), or(and(t4, cin), and(t2, t3)))))))
% 10.09/1.70 = { by axiom 32 (and_distributive) R->L }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), or(and(t4, cin), and(not(and(t2, t3)), and(t2, t3)))))))
% 10.09/1.70 = { by axiom 9 (and_commutative) }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), or(and(t4, cin), and(and(t2, t3), not(and(t2, t3))))))))
% 10.09/1.70 = { by lemma 38 }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), or(and(t4, cin), not(ll1))))))
% 10.09/1.70 = { by lemma 35 }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(not(and(t2, t3)), and(t4, cin)))))
% 10.09/1.70 = { by axiom 4 (xor_commutative) }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(and(t4, cin), not(and(t2, t3))))))
% 10.09/1.70 = { by lemma 49 R->L }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), xor(and(t2, t3), not(and(t4, cin))))))
% 10.09/1.70 = { by lemma 82 }
% 10.09/1.70 tuple(not(and(t6, t7)), and(not(and(t4, t5)), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), and(t4, t5))))
% 10.09/1.70 = { by lemma 71 }
% 10.09/1.70 tuple(not(and(t6, t7)), and(or(and(cin, or(a, b)), and(not(cin), and(a, b))), not(and(t4, t5))))
% 10.09/1.70 = { by lemma 86 R->L }
% 10.09/1.70 tuple(not(and(t6, t7)), and(or(and(cin, or(a, b)), and(not(cin), and(a, b))), or(or(and(cin, or(a, b)), and(not(cin), and(a, b))), and(t2, t3))))
% 10.09/1.70 = { by axiom 28 (and_absorption) }
% 10.09/1.70 tuple(not(and(t6, t7)), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by lemma 64 R->L }
% 10.09/1.70 tuple(xor(and(t4, t5), xor(and(t4, t5), not(and(t6, t7)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by lemma 49 }
% 10.09/1.70 tuple(xor(and(t4, t5), xor(and(t6, t7), not(and(t4, t5)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 4 (xor_commutative) R->L }
% 10.09/1.70 tuple(xor(and(t4, t5), xor(not(and(t4, t5)), and(t6, t7))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 17 (t6) }
% 10.09/1.70 tuple(xor(and(t4, t5), xor(t6, and(t6, t7))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by lemma 60 }
% 10.09/1.70 tuple(xor(and(t4, t5), and(t6, not(t7))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 17 (t6) R->L }
% 10.09/1.70 tuple(xor(and(t4, t5), and(not(and(t4, t5)), not(t7))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 20 (t7) R->L }
% 10.09/1.70 tuple(xor(and(t4, t5), and(not(and(t4, t5)), not(not(and(t5, cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 3 (not_involution) }
% 10.09/1.70 tuple(xor(and(t4, t5), and(not(and(t4, t5)), and(t5, cin))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 9 (and_commutative) R->L }
% 10.09/1.70 tuple(xor(and(t4, t5), and(and(t5, cin), not(and(t4, t5)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.70 = { by axiom 29 (and_associative) }
% 10.09/1.70 tuple(xor(and(t4, t5), and(t5, and(cin, not(and(t4, t5))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 18 (t5) R->L }
% 10.09/1.71 tuple(xor(and(t4, t5), and(not(and(t4, cin)), and(cin, not(and(t4, t5))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 9 (and_commutative) }
% 10.09/1.71 tuple(xor(and(t4, t5), and(not(and(t4, cin)), and(not(and(t4, t5)), cin))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 3 (not_involution) R->L }
% 10.09/1.71 tuple(xor(and(t4, t5), and(not(and(t4, cin)), and(not(and(t4, t5)), not(not(cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 13 (or_demorgan) R->L }
% 10.09/1.71 tuple(xor(and(t4, t5), and(not(and(t4, cin)), not(or(and(t4, t5), not(cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 70 }
% 10.09/1.71 tuple(xor(and(t4, t5), and(not(and(t4, cin)), not(not(cin)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 3 (not_involution) }
% 10.09/1.71 tuple(xor(and(t4, t5), and(not(and(t4, cin)), cin)), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 68 }
% 10.09/1.71 tuple(xor(and(t4, t5), and(t5, cin)), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 4 (xor_commutative) R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), and(t4, t5)), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 82 R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(and(t2, t3), not(and(t4, cin)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 49 }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(and(t4, cin), not(and(t2, t3)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 4 (xor_commutative) R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(not(and(t2, t3)), and(t4, cin))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 47 }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), and(t4, cin))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 3 (not_involution) R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(not(and(t4, cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 39 R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(and(not(and(t4, cin)), not(ll0))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 36 R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(and(not(and(t4, cin)), or(not(cin), cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 5 (or_commutative) R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(and(not(and(t4, cin)), or(cin, not(cin)))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 18 (t5) }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(and(t5, or(cin, not(cin)))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 30 (or_distributive) }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(or(and(t5, cin), and(t5, not(cin)))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 18 (t5) R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(or(and(t5, cin), and(not(and(t4, cin)), not(cin)))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 73 }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), not(or(and(t5, cin), not(cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 13 (or_demorgan) }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), and(not(and(t5, cin)), not(not(cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 60 R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), xor(not(and(t5, cin)), and(not(and(t5, cin)), not(cin))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 75 }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), xor(not(and(t5, cin)), not(cin)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 49 R->L }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), xor(cin, not(not(and(t5, cin)))))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 3 (not_involution) }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), xor(cin, and(t5, cin)))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 4 (xor_commutative) }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(xor(a, b), xor(and(t5, cin), cin))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 62 }
% 10.09/1.71 tuple(xor(and(t5, cin), xor(and(t5, cin), xor(xor(a, b), cin))), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by lemma 64 }
% 10.09/1.71 tuple(xor(xor(a, b), cin), or(and(cin, or(a, b)), and(not(cin), and(a, b))))
% 10.09/1.71 = { by axiom 33 (carry_def) }
% 10.09/1.71 tuple(xor(xor(a, b), cin), carry_def)
% 10.09/1.71 = { by axiom 25 (sum_def) }
% 10.09/1.71 tuple(sum_def, carry_def)
% 10.09/1.71 % SZS output end Proof
% 10.09/1.71
% 10.09/1.71 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------