%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : HWV003-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 168.60s 26.79s
% Output : Proof 176.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV003-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.03 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/5.37 % Computer : n010.cluster.edu
% 0.07/5.37 % Model : x86_64 x86_64
% 0.07/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/5.37 % Memory : 8046.5625MB
% 0.07/5.37 % OS : Linux 6.8.0-71-generic
% 0.07/5.37 % CPULimit : 300
% 0.07/5.37 % WCLimit : 300
% 0.07/5.37 % DateTime : Sun Sep 27 10:52:06 UTC 2026
% 0.07/5.37 % CPUTime :
% 0.07/5.37 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 168.60/26.79 Command-line arguments: --stitch /export/starexec/sandbox2/solver/bin/stitch --hint-skel-cost 0 --hint-skel-factor 0.5
% 168.60/26.79
% 168.60/26.79 % SZS status Unsatisfiable
% 168.60/26.79
% 175.75/27.64 % SZS output start Proof
% 175.75/27.64 Axiom 1 (not_definition1): not(n0) = n1.
% 175.75/27.64 Axiom 2 (not_involution): not(not(X)) = X.
% 175.75/27.64 Axiom 3 (the_output_circuit): circuit(s1, c1) = true.
% 175.75/27.64 Axiom 4 (or_symmetry): or(X, Y) = or(Y, X).
% 175.75/27.64 Axiom 5 (or_definition2): or(X, n1) = n1.
% 175.75/27.64 Axiom 6 (or_definition1): or(X, n0) = X.
% 175.75/27.64 Axiom 7 (or_not_evaluation1): or(X, not(X)) = n1.
% 175.75/27.64 Axiom 8 (and_idempotency): and(X, X) = X.
% 175.75/27.64 Axiom 9 (and_symmetry): and(X, Y) = and(Y, X).
% 175.75/27.64 Axiom 10 (and_definition2): and(X, n1) = X.
% 175.75/27.64 Axiom 11 (and_not_evaluation1): and(X, not(X)) = n0.
% 175.75/27.64 Axiom 12 (demorgan2): not(or(X, Y)) = and(not(X), not(Y)).
% 175.75/27.64 Axiom 13 (demorgan1): not(and(X, Y)) = or(not(X), not(Y)).
% 175.75/27.64 Axiom 14 (circuit4): a14 = not(and(a12, a13)).
% 175.75/27.64 Axiom 15 (circuit8): s1 = not(and(a16, a17)).
% 175.75/27.64 Axiom 16 (circuit6): a16 = not(and(a14, a15)).
% 175.75/27.64 Axiom 17 (circuit5): a15 = not(and(a14, carryin)).
% 175.75/27.64 Axiom 18 (circuit9): c1 = not(and(a11, a15)).
% 175.75/27.64 Axiom 19 (circuit2): a12 = not(and(a11, a)).
% 175.75/27.64 Axiom 20 (circuit3): a13 = not(and(a11, b)).
% 175.75/27.64 Axiom 21 (circuit7): a17 = not(and(a15, carryin)).
% 175.75/27.64 Axiom 22 (circuit1): a11 = not(and(a, b)).
% 175.75/27.64 Axiom 23 (sum_definition): sum(X, Y, Z) = xor(xor(X, Y), Z).
% 175.75/27.64 Axiom 24 (or_evaluation1): or(or(X, Y), Y) = or(X, Y).
% 175.75/27.64 Axiom 25 (or_commutativity): or(or(X, Y), Z) = or(or(X, Z), Y).
% 175.75/27.64 Axiom 26 (or_not_evaluation3): or(or(X, Y), not(X)) = n1.
% 175.75/27.64 Axiom 27 (and_or_subsumption2): or(and(X, Y), X) = X.
% 175.75/27.64 Axiom 28 (and_or_subsumption1): or(and(X, Y), Y) = Y.
% 175.75/27.64 Axiom 29 (karnaugh1): or(and(X, not(Y)), Y) = or(X, Y).
% 175.75/27.64 Axiom 30 (and_evaluation1): and(and(X, Y), Y) = and(X, Y).
% 175.75/27.64 Axiom 31 (and_commutativity): and(and(X, Y), Z) = and(and(X, Z), Y).
% 175.75/27.64 Axiom 32 (and_not_evaluation3): and(and(X, Y), not(X)) = n0.
% 175.75/27.64 Axiom 33 (and_or_simplification): and(or(X, Y), Z) = or(and(X, Z), and(Y, Z)).
% 175.75/27.64 Axiom 34 (xor_definition): xor(X, Y) = or(and(X, not(Y)), and(Y, not(X))).
% 175.75/27.64 Axiom 35 (and_or_subsumption4): or(or(X, and(Y, Z)), Z) = or(X, Z).
% 175.75/27.64 Axiom 36 (and_or_subsumption3): or(or(and(X, Y), Z), Y) = or(Z, Y).
% 175.75/27.64 Axiom 37 (carryout_definition): carryout(X, Y, Z) = or(and(X, or(Y, Z)), and(not(X), and(Y, Z))).
% 175.75/27.64
% 175.75/27.64 Lemma 38: or(not(a11), not(a)) = a12.
% 175.75/27.64 Proof:
% 175.75/27.64 or(not(a11), not(a))
% 175.75/27.64 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.64 not(and(a11, a))
% 175.75/27.64 = { by axiom 19 (circuit2) R->L }
% 175.75/27.64 a12
% 175.75/27.64
% 175.75/27.64 Lemma 39: and(a11, a) = not(a12).
% 175.75/27.64 Proof:
% 175.75/27.64 and(a11, a)
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(a11, not(not(a)))
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(not(not(a11)), not(not(a)))
% 175.75/27.64 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.64 not(or(not(a11), not(a)))
% 175.75/27.64 = { by lemma 38 }
% 175.75/27.64 not(a12)
% 175.75/27.64
% 175.75/27.64 Lemma 40: or(not(a11), not(b)) = a13.
% 175.75/27.64 Proof:
% 175.75/27.64 or(not(a11), not(b))
% 175.75/27.64 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.64 not(and(a11, b))
% 175.75/27.64 = { by axiom 20 (circuit3) R->L }
% 175.75/27.64 a13
% 175.75/27.64
% 175.75/27.64 Lemma 41: and(a11, b) = not(a13).
% 175.75/27.64 Proof:
% 175.75/27.64 and(a11, b)
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(a11, not(not(b)))
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(not(not(a11)), not(not(b)))
% 175.75/27.64 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.64 not(or(not(a11), not(b)))
% 175.75/27.64 = { by lemma 40 }
% 175.75/27.64 not(a13)
% 175.75/27.64
% 175.75/27.64 Lemma 42: or(not(a11), not(a15)) = c1.
% 175.75/27.64 Proof:
% 175.75/27.64 or(not(a11), not(a15))
% 175.75/27.64 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.64 not(and(a11, a15))
% 175.75/27.64 = { by axiom 18 (circuit9) R->L }
% 175.75/27.64 c1
% 175.75/27.64
% 175.75/27.64 Lemma 43: and(a11, a15) = not(c1).
% 175.75/27.64 Proof:
% 175.75/27.64 and(a11, a15)
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(a11, not(not(a15)))
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(not(not(a11)), not(not(a15)))
% 175.75/27.64 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.64 not(or(not(a11), not(a15)))
% 175.75/27.64 = { by lemma 42 }
% 175.75/27.64 not(c1)
% 175.75/27.64
% 175.75/27.64 Lemma 44: or(not(a), not(b)) = a11.
% 175.75/27.64 Proof:
% 175.75/27.64 or(not(a), not(b))
% 175.75/27.64 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.64 not(and(a, b))
% 175.75/27.64 = { by axiom 22 (circuit1) R->L }
% 175.75/27.64 a11
% 175.75/27.64
% 175.75/27.64 Lemma 45: and(a, b) = not(a11).
% 175.75/27.64 Proof:
% 175.75/27.64 and(a, b)
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(a, not(not(b)))
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(not(not(a)), not(not(b)))
% 175.75/27.64 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.64 not(or(not(a), not(b)))
% 175.75/27.64 = { by lemma 44 }
% 175.75/27.64 not(a11)
% 175.75/27.64
% 175.75/27.64 Lemma 46: or(not(a12), not(a13)) = a14.
% 175.75/27.64 Proof:
% 175.75/27.64 or(not(a12), not(a13))
% 175.75/27.64 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.64 not(and(a12, a13))
% 175.75/27.64 = { by axiom 14 (circuit4) R->L }
% 175.75/27.64 a14
% 175.75/27.64
% 175.75/27.64 Lemma 47: and(a12, a13) = not(a14).
% 175.75/27.64 Proof:
% 175.75/27.64 and(a12, a13)
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(a12, not(not(a13)))
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(not(not(a12)), not(not(a13)))
% 175.75/27.64 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.64 not(or(not(a12), not(a13)))
% 175.75/27.64 = { by lemma 46 }
% 175.75/27.64 not(a14)
% 175.75/27.64
% 175.75/27.64 Lemma 48: and(not(X), or(X, Y)) = and(Y, not(X)).
% 175.75/27.64 Proof:
% 175.75/27.64 and(not(X), or(X, Y))
% 175.75/27.64 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.64 and(not(X), or(Y, X))
% 175.75/27.64 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.64 and(or(Y, X), not(X))
% 175.75/27.64 = { by axiom 33 (and_or_simplification) }
% 175.75/27.64 or(and(Y, not(X)), and(X, not(X)))
% 175.75/27.64 = { by axiom 11 (and_not_evaluation1) }
% 175.75/27.64 or(and(Y, not(X)), n0)
% 175.75/27.64 = { by axiom 6 (or_definition1) }
% 175.75/27.64 and(Y, not(X))
% 175.75/27.64
% 175.75/27.64 Lemma 49: or(X, and(Y, not(X))) = or(Y, X).
% 175.75/27.64 Proof:
% 175.75/27.64 or(X, and(Y, not(X)))
% 175.75/27.64 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.64 or(and(Y, not(X)), X)
% 175.75/27.64 = { by axiom 29 (karnaugh1) }
% 175.75/27.64 or(Y, X)
% 175.75/27.64
% 175.75/27.64 Lemma 50: or(not(X), and(Y, X)) = or(Y, not(X)).
% 175.75/27.64 Proof:
% 175.75/27.64 or(not(X), and(Y, X))
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 or(not(X), and(Y, not(not(X))))
% 175.75/27.64 = { by lemma 49 }
% 175.75/27.64 or(Y, not(X))
% 175.75/27.64
% 175.75/27.64 Lemma 51: and(b, not(a)) = not(a13).
% 175.75/27.64 Proof:
% 175.75/27.64 and(b, not(a))
% 175.75/27.64 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.64 and(not(a), b)
% 175.75/27.64 = { by axiom 2 (not_involution) R->L }
% 175.75/27.64 and(not(a), not(not(b)))
% 175.75/27.64 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.64 not(or(a, not(b)))
% 175.75/27.64 = { by lemma 50 R->L }
% 175.75/27.64 not(or(not(b), and(a, b)))
% 175.75/27.64 = { by lemma 45 }
% 175.75/27.64 not(or(not(b), not(a11)))
% 175.75/27.64 = { by axiom 4 (or_symmetry) }
% 175.75/27.64 not(or(not(a11), not(b)))
% 175.75/27.64 = { by lemma 40 }
% 175.75/27.64 not(a13)
% 175.75/27.64
% 175.75/27.64 Lemma 52: or(a12, not(a13)) = a12.
% 175.75/27.64 Proof:
% 175.75/27.64 or(a12, not(a13))
% 175.75/27.64 = { by lemma 51 R->L }
% 175.75/27.64 or(a12, and(b, not(a)))
% 175.75/27.64 = { by lemma 38 R->L }
% 175.75/27.64 or(or(not(a11), not(a)), and(b, not(a)))
% 175.75/27.64 = { by axiom 25 (or_commutativity) R->L }
% 175.75/27.64 or(or(not(a11), and(b, not(a))), not(a))
% 175.75/27.64 = { by axiom 35 (and_or_subsumption4) }
% 175.75/27.64 or(not(a11), not(a))
% 175.75/27.64 = { by lemma 38 }
% 175.75/27.64 a12
% 175.75/27.64
% 175.75/27.64 Lemma 53: or(X, and(Y, X)) = X.
% 175.75/27.64 Proof:
% 175.75/27.64 or(X, and(Y, X))
% 175.75/27.64 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.64 or(and(Y, X), X)
% 175.75/27.64 = { by axiom 28 (and_or_subsumption1) }
% 175.75/27.64 X
% 175.75/27.64
% 175.75/27.64 Lemma 54: and(X, or(X, Y)) = X.
% 175.75/27.64 Proof:
% 175.75/27.64 and(X, or(X, Y))
% 175.75/27.64 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.64 and(or(X, Y), X)
% 175.75/27.64 = { by axiom 33 (and_or_simplification) }
% 175.75/27.64 or(and(X, X), and(Y, X))
% 175.75/27.64 = { by axiom 8 (and_idempotency) }
% 175.75/27.64 or(X, and(Y, X))
% 175.75/27.64 = { by lemma 53 }
% 175.75/27.64 X
% 175.75/27.64
% 175.75/27.64 Lemma 55: and(X, or(Y, X)) = X.
% 175.75/27.64 Proof:
% 175.75/27.64 and(X, or(Y, X))
% 175.75/27.64 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.64 and(X, or(X, Y))
% 175.75/27.64 = { by lemma 54 }
% 175.75/27.65 X
% 175.75/27.65
% 175.75/27.65 Lemma 56: and(a12, a14) = not(a13).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a12, a14)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(a12)), a14)
% 175.75/27.65 = { by lemma 46 R->L }
% 175.75/27.65 and(not(not(a12)), or(not(a12), not(a13)))
% 175.75/27.65 = { by lemma 48 }
% 175.75/27.65 and(not(a13), not(not(a12)))
% 175.75/27.65 = { by axiom 2 (not_involution) }
% 175.75/27.65 and(not(a13), a12)
% 175.75/27.65 = { by lemma 52 R->L }
% 175.75/27.65 and(not(a13), or(a12, not(a13)))
% 175.75/27.65 = { by lemma 55 }
% 175.75/27.65 not(a13)
% 175.75/27.65
% 175.75/27.65 Lemma 57: and(X, and(Y, Z)) = and(Z, and(X, Y)).
% 175.75/27.65 Proof:
% 175.75/27.65 and(X, and(Y, Z))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(and(Y, Z), X)
% 175.75/27.65 = { by axiom 31 (and_commutativity) }
% 175.75/27.65 and(and(Y, X), Z)
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 and(Z, and(Y, X))
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 and(Z, and(X, Y))
% 175.75/27.65
% 175.75/27.65 Lemma 58: and(and(X, Y), Z) = and(X, and(Y, Z)).
% 175.75/27.65 Proof:
% 175.75/27.65 and(and(X, Y), Z)
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(Z, and(X, Y))
% 175.75/27.65 = { by lemma 57 R->L }
% 175.75/27.65 and(X, and(Y, Z))
% 175.75/27.65
% 175.75/27.65 Lemma 59: and(a11, and(X, b)) = and(X, not(a13)).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a11, and(X, b))
% 175.75/27.65 = { by lemma 58 R->L }
% 175.75/27.65 and(and(a11, X), b)
% 175.75/27.65 = { by axiom 31 (and_commutativity) R->L }
% 175.75/27.65 and(and(a11, b), X)
% 175.75/27.65 = { by lemma 41 }
% 175.75/27.65 and(not(a13), X)
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 and(X, not(a13))
% 175.75/27.65
% 175.75/27.65 Lemma 60: and(a13, a) = a.
% 175.75/27.65 Proof:
% 175.75/27.65 and(a13, a)
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(a, a13)
% 175.75/27.65 = { by axiom 6 (or_definition1) R->L }
% 175.75/27.65 and(a, or(a13, n0))
% 175.75/27.65 = { by axiom 11 (and_not_evaluation1) R->L }
% 175.75/27.65 and(a, or(a13, and(a11, not(a11))))
% 175.75/27.65 = { by lemma 45 R->L }
% 175.75/27.65 and(a, or(a13, and(a11, and(a, b))))
% 175.75/27.65 = { by lemma 59 }
% 175.75/27.65 and(a, or(a13, and(a, not(a13))))
% 175.75/27.65 = { by lemma 49 }
% 175.75/27.65 and(a, or(a, a13))
% 175.75/27.65 = { by axiom 4 (or_symmetry) }
% 175.75/27.65 and(a, or(a13, a))
% 175.75/27.65 = { by lemma 55 }
% 175.75/27.65 a
% 175.75/27.65
% 175.75/27.65 Lemma 61: and(a13, a14) = not(a12).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a13, a14)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(a13, not(not(a14)))
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(a13)), not(not(a14)))
% 175.75/27.65 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.65 not(or(not(a13), not(a14)))
% 175.75/27.65 = { by lemma 47 R->L }
% 175.75/27.65 not(or(not(a13), and(a12, a13)))
% 175.75/27.65 = { by lemma 50 }
% 175.75/27.65 not(or(a12, not(a13)))
% 175.75/27.65 = { by lemma 52 }
% 175.75/27.65 not(a12)
% 175.75/27.65
% 175.75/27.65 Lemma 62: or(not(a14), not(a15)) = a16.
% 175.75/27.65 Proof:
% 175.75/27.65 or(not(a14), not(a15))
% 175.75/27.65 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.65 not(and(a14, a15))
% 175.75/27.65 = { by axiom 16 (circuit6) R->L }
% 175.75/27.65 a16
% 175.75/27.65
% 175.75/27.65 Lemma 63: and(a14, a15) = not(a16).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a14, a15)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(a14, not(not(a15)))
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(a14)), not(not(a15)))
% 175.75/27.65 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.65 not(or(not(a14), not(a15)))
% 175.75/27.65 = { by lemma 62 }
% 175.75/27.65 not(a16)
% 175.75/27.65
% 175.75/27.65 Lemma 64: or(not(a14), not(carryin)) = a15.
% 175.75/27.65 Proof:
% 175.75/27.65 or(not(a14), not(carryin))
% 175.75/27.65 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.65 not(and(a14, carryin))
% 175.75/27.65 = { by axiom 17 (circuit5) R->L }
% 175.75/27.65 a15
% 175.75/27.65
% 175.75/27.65 Lemma 65: and(a14, carryin) = not(a15).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a14, carryin)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(a14, not(not(carryin)))
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(a14)), not(not(carryin)))
% 175.75/27.65 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.65 not(or(not(a14), not(carryin)))
% 175.75/27.65 = { by lemma 64 }
% 175.75/27.65 not(a15)
% 175.75/27.65
% 175.75/27.65 Lemma 66: and(X, and(Y, X)) = and(Y, X).
% 175.75/27.65 Proof:
% 175.75/27.65 and(X, and(Y, X))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(and(Y, X), X)
% 175.75/27.65 = { by axiom 30 (and_evaluation1) }
% 175.75/27.65 and(Y, X)
% 175.75/27.65
% 175.75/27.65 Lemma 67: and(a16, a14) = not(a15).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a16, a14)
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(a14, a16)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(a14)), a16)
% 175.75/27.65 = { by lemma 62 R->L }
% 175.75/27.65 and(not(not(a14)), or(not(a14), not(a15)))
% 175.75/27.65 = { by lemma 48 }
% 175.75/27.65 and(not(a15), not(not(a14)))
% 175.75/27.65 = { by axiom 2 (not_involution) }
% 175.75/27.65 and(not(a15), a14)
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 and(a14, not(a15))
% 175.75/27.65 = { by lemma 65 R->L }
% 175.75/27.65 and(a14, and(a14, carryin))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(a14, and(carryin, a14))
% 175.75/27.65 = { by lemma 66 }
% 175.75/27.65 and(carryin, a14)
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 and(a14, carryin)
% 175.75/27.65 = { by lemma 65 }
% 175.75/27.65 not(a15)
% 175.75/27.65
% 175.75/27.65 Lemma 68: or(X, or(Y, X)) = or(Y, X).
% 175.75/27.65 Proof:
% 175.75/27.65 or(X, or(Y, X))
% 175.75/27.65 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.65 or(or(Y, X), X)
% 175.75/27.65 = { by axiom 24 (or_evaluation1) }
% 175.75/27.65 or(Y, X)
% 175.75/27.65
% 175.75/27.65 Lemma 69: or(X, or(Y, Z)) = or(Z, or(X, Y)).
% 175.75/27.65 Proof:
% 175.75/27.65 or(X, or(Y, Z))
% 175.75/27.65 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.65 or(or(Y, Z), X)
% 175.75/27.65 = { by axiom 25 (or_commutativity) }
% 175.75/27.65 or(or(Y, X), Z)
% 175.75/27.65 = { by axiom 4 (or_symmetry) }
% 175.75/27.65 or(Z, or(Y, X))
% 175.75/27.65 = { by axiom 4 (or_symmetry) }
% 175.75/27.65 or(Z, or(X, Y))
% 175.75/27.65
% 175.75/27.65 Lemma 70: and(a12, and(a13, X)) = and(X, not(a14)).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a12, and(a13, X))
% 175.75/27.65 = { by lemma 57 R->L }
% 175.75/27.65 and(a13, and(X, a12))
% 175.75/27.65 = { by lemma 57 R->L }
% 175.75/27.65 and(X, and(a12, a13))
% 175.75/27.65 = { by lemma 47 }
% 175.75/27.65 and(X, not(a14))
% 175.75/27.65
% 175.75/27.65 Lemma 71: or(a14, a11) = a11.
% 175.75/27.65 Proof:
% 175.75/27.65 or(a14, a11)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 or(a14, not(not(a11)))
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 or(not(not(a14)), not(not(a11)))
% 175.75/27.65 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.65 not(and(not(a14), not(a11)))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 not(and(not(a11), not(a14)))
% 175.75/27.65 = { by lemma 70 R->L }
% 175.75/27.65 not(and(a12, and(a13, not(a11))))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 not(and(a12, and(not(a11), a13)))
% 175.75/27.65 = { by lemma 40 R->L }
% 175.75/27.65 not(and(a12, and(not(a11), or(not(a11), not(b)))))
% 175.75/27.65 = { by lemma 54 }
% 175.75/27.65 not(and(a12, not(a11)))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 not(and(not(a11), a12))
% 175.75/27.65 = { by lemma 38 R->L }
% 175.75/27.65 not(and(not(a11), or(not(a11), not(a))))
% 175.75/27.65 = { by lemma 54 }
% 175.75/27.65 not(not(a11))
% 175.75/27.65 = { by axiom 2 (not_involution) }
% 175.75/27.65 a11
% 175.75/27.65
% 175.75/27.65 Lemma 72: or(a14, not(b)) = a11.
% 175.75/27.65 Proof:
% 175.75/27.65 or(a14, not(b))
% 175.75/27.65 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.65 or(not(b), a14)
% 175.75/27.65 = { by lemma 46 R->L }
% 175.75/27.65 or(not(b), or(not(a12), not(a13)))
% 175.75/27.65 = { by lemma 68 R->L }
% 175.75/27.65 or(not(b), or(not(a13), or(not(a12), not(a13))))
% 175.75/27.65 = { by lemma 46 }
% 175.75/27.65 or(not(b), or(not(a13), a14))
% 175.75/27.65 = { by axiom 4 (or_symmetry) }
% 175.75/27.65 or(not(b), or(a14, not(a13)))
% 175.75/27.65 = { by lemma 69 }
% 175.75/27.65 or(not(a13), or(not(b), a14))
% 175.75/27.65 = { by lemma 69 }
% 175.75/27.65 or(a14, or(not(a13), not(b)))
% 175.75/27.65 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.65 or(a14, or(not(b), not(a13)))
% 175.75/27.65 = { by lemma 41 R->L }
% 175.75/27.65 or(a14, or(not(b), and(a11, b)))
% 175.75/27.65 = { by lemma 50 }
% 175.75/27.65 or(a14, or(a11, not(b)))
% 175.75/27.65 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.65 or(a14, or(not(b), a11))
% 175.75/27.65 = { by lemma 44 R->L }
% 175.75/27.65 or(a14, or(not(b), or(not(a), not(b))))
% 175.75/27.65 = { by lemma 68 }
% 175.75/27.65 or(a14, or(not(a), not(b)))
% 175.75/27.65 = { by lemma 44 }
% 175.75/27.65 or(a14, a11)
% 175.75/27.65 = { by lemma 71 }
% 175.75/27.65 a11
% 175.75/27.65
% 175.75/27.65 Lemma 73: and(a15, not(a14)) = not(a14).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a15, not(a14))
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(not(a14), a15)
% 175.75/27.65 = { by lemma 64 R->L }
% 175.75/27.65 and(not(a14), or(not(a14), not(carryin)))
% 175.75/27.65 = { by lemma 54 }
% 175.75/27.65 not(a14)
% 175.75/27.65
% 175.75/27.65 Lemma 74: and(c1, a11) = not(a15).
% 175.75/27.65 Proof:
% 175.75/27.65 and(c1, a11)
% 175.75/27.65 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.65 and(a11, c1)
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(a11)), c1)
% 175.75/27.65 = { by lemma 42 R->L }
% 175.75/27.65 and(not(not(a11)), or(not(a11), not(a15)))
% 175.75/27.65 = { by lemma 48 }
% 175.75/27.65 and(not(a15), not(not(a11)))
% 175.75/27.65 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.65 not(or(a15, not(a11)))
% 175.75/27.65 = { by lemma 72 R->L }
% 175.75/27.65 not(or(a15, not(or(a14, not(b)))))
% 175.75/27.65 = { by axiom 12 (demorgan2) }
% 175.75/27.65 not(or(a15, and(not(a14), not(not(b)))))
% 175.75/27.65 = { by axiom 2 (not_involution) }
% 175.75/27.65 not(or(a15, and(not(a14), b)))
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 not(or(a15, and(b, not(a14))))
% 175.75/27.65 = { by lemma 73 R->L }
% 175.75/27.65 not(or(a15, and(b, and(a15, not(a14)))))
% 175.75/27.65 = { by lemma 58 R->L }
% 175.75/27.65 not(or(a15, and(and(b, a15), not(a14))))
% 175.75/27.65 = { by axiom 31 (and_commutativity) R->L }
% 175.75/27.65 not(or(a15, and(and(b, not(a14)), a15)))
% 175.75/27.65 = { by lemma 53 }
% 175.75/27.65 not(a15)
% 175.75/27.65
% 175.75/27.65 Lemma 75: and(X, or(Y, not(X))) = and(X, Y).
% 175.75/27.65 Proof:
% 175.75/27.65 and(X, or(Y, not(X)))
% 175.75/27.65 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.65 and(X, or(not(X), Y))
% 175.75/27.65 = { by axiom 2 (not_involution) R->L }
% 175.75/27.65 and(not(not(X)), or(not(X), Y))
% 175.75/27.65 = { by lemma 48 }
% 175.75/27.65 and(Y, not(not(X)))
% 175.75/27.65 = { by axiom 2 (not_involution) }
% 175.75/27.65 and(Y, X)
% 175.75/27.65 = { by axiom 9 (and_symmetry) }
% 175.75/27.65 and(X, Y)
% 175.75/27.65
% 175.75/27.65 Lemma 76: and(a11, and(a15, X)) = and(X, not(c1)).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a11, and(a15, X))
% 175.75/27.65 = { by lemma 57 R->L }
% 175.75/27.65 and(a15, and(X, a11))
% 175.75/27.65 = { by lemma 57 R->L }
% 175.75/27.65 and(X, and(a11, a15))
% 175.75/27.65 = { by lemma 43 }
% 175.75/27.65 and(X, not(c1))
% 175.75/27.65
% 175.75/27.65 Lemma 77: and(a, not(c1)) = and(a15, not(a12)).
% 175.75/27.65 Proof:
% 175.75/27.65 and(a, not(c1))
% 175.75/27.65 = { by lemma 76 R->L }
% 175.75/27.65 and(a11, and(a15, a))
% 175.75/27.65 = { by lemma 58 R->L }
% 175.75/27.65 and(and(a11, a15), a)
% 175.75/27.65 = { by axiom 31 (and_commutativity) R->L }
% 175.75/27.66 and(and(a11, a), a15)
% 175.75/27.66 = { by lemma 39 }
% 175.75/27.66 and(not(a12), a15)
% 175.75/27.66 = { by axiom 9 (and_symmetry) }
% 175.75/27.66 and(a15, not(a12))
% 175.75/27.66
% 175.75/27.66 Lemma 78: or(X, or(X, Y)) = or(X, Y).
% 175.75/27.66 Proof:
% 175.75/27.66 or(X, or(X, Y))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(X, or(Y, X))
% 175.75/27.66 = { by lemma 68 }
% 175.75/27.66 or(Y, X)
% 175.75/27.66 = { by axiom 4 (or_symmetry) }
% 175.75/27.66 or(X, Y)
% 175.75/27.66
% 175.75/27.66 Lemma 79: or(or(X, Y), Z) = or(X, or(Y, Z)).
% 175.75/27.66 Proof:
% 175.75/27.66 or(or(X, Y), Z)
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(Z, or(X, Y))
% 175.75/27.66 = { by lemma 69 R->L }
% 175.75/27.66 or(X, or(Y, Z))
% 175.75/27.66
% 175.75/27.66 Lemma 80: or(a12, or(X, not(a))) = or(X, a12).
% 175.75/27.66 Proof:
% 175.75/27.66 or(a12, or(X, not(a)))
% 175.75/27.66 = { by lemma 79 R->L }
% 175.75/27.66 or(or(a12, X), not(a))
% 175.75/27.66 = { by axiom 25 (or_commutativity) R->L }
% 175.75/27.66 or(or(a12, not(a)), X)
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(or(not(a), a12), X)
% 175.75/27.66 = { by lemma 38 R->L }
% 175.75/27.66 or(or(not(a), or(not(a11), not(a))), X)
% 175.75/27.66 = { by lemma 68 }
% 175.75/27.66 or(or(not(a11), not(a)), X)
% 175.75/27.66 = { by lemma 38 }
% 175.75/27.66 or(a12, X)
% 175.75/27.66 = { by axiom 4 (or_symmetry) }
% 175.75/27.66 or(X, a12)
% 175.75/27.66
% 175.75/27.66 Lemma 81: or(a12, not(a15)) = or(a12, c1).
% 175.75/27.66 Proof:
% 175.75/27.66 or(a12, not(a15))
% 175.75/27.66 = { by lemma 78 R->L }
% 175.75/27.66 or(a12, or(a12, not(a15)))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(a12, or(not(a15), a12))
% 175.75/27.66 = { by axiom 2 (not_involution) R->L }
% 175.75/27.66 or(a12, or(not(a15), not(not(a12))))
% 175.75/27.66 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.66 or(a12, not(and(a15, not(a12))))
% 175.75/27.66 = { by lemma 77 R->L }
% 175.75/27.66 or(a12, not(and(a, not(c1))))
% 175.75/27.66 = { by axiom 13 (demorgan1) }
% 175.75/27.66 or(a12, or(not(a), not(not(c1))))
% 175.75/27.66 = { by axiom 2 (not_involution) }
% 175.75/27.66 or(a12, or(not(a), c1))
% 175.75/27.66 = { by axiom 4 (or_symmetry) }
% 175.75/27.66 or(a12, or(c1, not(a)))
% 175.75/27.66 = { by lemma 80 }
% 175.75/27.66 or(c1, a12)
% 175.75/27.66 = { by axiom 4 (or_symmetry) }
% 175.75/27.66 or(a12, c1)
% 175.75/27.66
% 175.75/27.66 Lemma 82: or(c1, not(a)) = or(a12, c1).
% 175.75/27.66 Proof:
% 175.75/27.66 or(c1, not(a))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(not(a), c1)
% 175.75/27.66 = { by axiom 2 (not_involution) R->L }
% 175.75/27.66 or(not(a), not(not(c1)))
% 175.75/27.66 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.66 not(and(a, not(c1)))
% 175.75/27.66 = { by lemma 77 }
% 175.75/27.66 not(and(a15, not(a12)))
% 175.75/27.66 = { by axiom 13 (demorgan1) }
% 175.75/27.66 or(not(a15), not(not(a12)))
% 175.75/27.66 = { by axiom 2 (not_involution) }
% 175.75/27.66 or(not(a15), a12)
% 175.75/27.66 = { by axiom 4 (or_symmetry) }
% 175.75/27.66 or(a12, not(a15))
% 175.75/27.66 = { by lemma 81 }
% 175.75/27.66 or(a12, c1)
% 175.75/27.66
% 175.75/27.66 Lemma 83: or(a16, not(a15)) = a16.
% 175.75/27.66 Proof:
% 175.75/27.66 or(a16, not(a15))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(not(a15), a16)
% 175.75/27.66 = { by lemma 62 R->L }
% 175.75/27.66 or(not(a15), or(not(a14), not(a15)))
% 175.75/27.66 = { by lemma 68 }
% 175.75/27.66 or(not(a14), not(a15))
% 175.75/27.66 = { by lemma 62 }
% 175.75/27.66 a16
% 175.75/27.66
% 175.75/27.66 Lemma 84: and(a12, and(a14, X)) = and(X, not(a13)).
% 175.75/27.66 Proof:
% 175.75/27.66 and(a12, and(a14, X))
% 175.75/27.66 = { by lemma 58 R->L }
% 175.75/27.66 and(and(a12, a14), X)
% 175.75/27.66 = { by lemma 56 }
% 175.75/27.66 and(not(a13), X)
% 175.75/27.66 = { by axiom 9 (and_symmetry) }
% 175.75/27.66 and(X, not(a13))
% 175.75/27.66
% 175.75/27.66 Lemma 85: and(a15, not(a13)) = and(a12, not(a16)).
% 175.75/27.66 Proof:
% 175.75/27.66 and(a15, not(a13))
% 175.75/27.66 = { by lemma 84 R->L }
% 175.75/27.66 and(a12, and(a14, a15))
% 175.75/27.66 = { by lemma 63 }
% 175.75/27.66 and(a12, not(a16))
% 175.75/27.66
% 175.75/27.66 Lemma 86: or(a12, c1) = or(a12, a16).
% 175.75/27.66 Proof:
% 175.75/27.66 or(a12, c1)
% 175.75/27.66 = { by lemma 81 R->L }
% 175.75/27.66 or(a12, not(a15))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(not(a15), a12)
% 175.75/27.66 = { by axiom 2 (not_involution) R->L }
% 175.75/27.66 or(not(a15), not(not(a12)))
% 175.75/27.66 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.66 not(and(a15, not(a12)))
% 175.75/27.66 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.66 not(and(not(a12), a15))
% 175.75/27.66 = { by lemma 61 R->L }
% 175.75/27.66 not(and(and(a13, a14), a15))
% 175.75/27.66 = { by lemma 58 }
% 175.75/27.66 not(and(a13, and(a14, a15)))
% 175.75/27.66 = { by lemma 63 }
% 175.75/27.66 not(and(a13, not(a16)))
% 175.75/27.66 = { by axiom 13 (demorgan1) }
% 175.75/27.66 or(not(a13), not(not(a16)))
% 175.75/27.66 = { by axiom 2 (not_involution) }
% 175.75/27.66 or(not(a13), a16)
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(a16, not(a13))
% 175.75/27.66 = { by lemma 83 R->L }
% 175.75/27.66 or(or(a16, not(a15)), not(a13))
% 175.75/27.66 = { by axiom 25 (or_commutativity) }
% 175.75/27.66 or(or(a16, not(a13)), not(a15))
% 175.75/27.66 = { by lemma 79 }
% 175.75/27.66 or(a16, or(not(a13), not(a15)))
% 175.75/27.66 = { by lemma 49 R->L }
% 175.75/27.66 or(a16, or(not(a15), and(not(a13), not(not(a15)))))
% 175.75/27.66 = { by lemma 69 R->L }
% 175.75/27.66 or(not(a15), or(and(not(a13), not(not(a15))), a16))
% 175.75/27.66 = { by lemma 69 R->L }
% 175.75/27.66 or(and(not(a13), not(not(a15))), or(a16, not(a15)))
% 175.75/27.66 = { by lemma 83 }
% 175.75/27.66 or(and(not(a13), not(not(a15))), a16)
% 175.75/27.66 = { by axiom 2 (not_involution) }
% 175.75/27.66 or(and(not(a13), a15), a16)
% 175.75/27.66 = { by axiom 4 (or_symmetry) }
% 175.75/27.66 or(a16, and(not(a13), a15))
% 175.75/27.66 = { by axiom 9 (and_symmetry) }
% 175.75/27.66 or(a16, and(a15, not(a13)))
% 175.75/27.66 = { by lemma 85 }
% 175.75/27.66 or(a16, and(a12, not(a16)))
% 175.75/27.66 = { by lemma 49 }
% 175.75/27.66 or(a12, a16)
% 175.75/27.66
% 175.75/27.66 Lemma 87: and(a14, and(X, a15)) = and(X, not(a16)).
% 175.75/27.66 Proof:
% 175.75/27.66 and(a14, and(X, a15))
% 175.75/27.66 = { by lemma 58 R->L }
% 175.75/27.66 and(and(a14, X), a15)
% 175.75/27.66 = { by axiom 31 (and_commutativity) R->L }
% 175.75/27.66 and(and(a14, a15), X)
% 175.75/27.66 = { by lemma 63 }
% 175.75/27.66 and(not(a16), X)
% 175.75/27.66 = { by axiom 9 (and_symmetry) }
% 175.75/27.66 and(X, not(a16))
% 175.75/27.66
% 175.75/27.66 Lemma 88: or(not(X), or(X, Y)) = n1.
% 175.75/27.66 Proof:
% 175.75/27.66 or(not(X), or(X, Y))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 or(or(X, Y), not(X))
% 175.75/27.66 = { by axiom 26 (or_not_evaluation3) }
% 175.75/27.66 n1
% 175.75/27.66
% 175.75/27.66 Lemma 89: and(a14, not(c1)) = not(a16).
% 175.75/27.66 Proof:
% 175.75/27.66 and(a14, not(c1))
% 175.75/27.66 = { by lemma 43 R->L }
% 175.75/27.66 and(a14, and(a11, a15))
% 175.75/27.66 = { by lemma 87 }
% 175.75/27.66 and(a11, not(a16))
% 175.75/27.66 = { by lemma 48 R->L }
% 175.75/27.66 and(not(a16), or(a16, a11))
% 175.75/27.66 = { by lemma 71 R->L }
% 175.75/27.66 and(not(a16), or(a16, or(a14, a11)))
% 175.75/27.66 = { by lemma 69 }
% 175.75/27.66 and(not(a16), or(a11, or(a16, a14)))
% 175.75/27.66 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.66 and(not(a16), or(a11, or(a14, a16)))
% 175.75/27.66 = { by axiom 2 (not_involution) R->L }
% 175.75/27.66 and(not(a16), or(a11, or(not(not(a14)), a16)))
% 175.75/27.66 = { by lemma 62 R->L }
% 175.75/27.66 and(not(a16), or(a11, or(not(not(a14)), or(not(a14), not(a15)))))
% 175.75/27.66 = { by lemma 88 }
% 175.75/27.66 and(not(a16), or(a11, n1))
% 175.75/27.66 = { by axiom 5 (or_definition2) }
% 175.75/27.66 and(not(a16), n1)
% 175.75/27.66 = { by axiom 10 (and_definition2) }
% 175.75/27.66 not(a16)
% 175.75/27.66
% 175.75/27.66 Lemma 90: and(a11, not(a)) = not(a).
% 175.75/27.66 Proof:
% 175.75/27.66 and(a11, not(a))
% 175.75/27.66 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.66 and(not(a), a11)
% 175.75/27.66 = { by lemma 44 R->L }
% 175.75/27.66 and(not(a), or(not(a), not(b)))
% 175.75/27.66 = { by lemma 54 }
% 175.75/27.66 not(a)
% 175.75/27.66
% 175.75/27.66 Lemma 91: and(a12, and(a11, X)) = and(X, not(a)).
% 175.75/27.66 Proof:
% 175.75/27.66 and(a12, and(a11, X))
% 175.75/27.66 = { by lemma 58 R->L }
% 175.75/27.66 and(and(a12, a11), X)
% 175.75/27.66 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 and(and(a11, a12), X)
% 175.75/27.67 = { by axiom 2 (not_involution) R->L }
% 175.75/27.67 and(and(not(not(a11)), a12), X)
% 175.75/27.67 = { by lemma 38 R->L }
% 175.75/27.67 and(and(not(not(a11)), or(not(a11), not(a))), X)
% 175.75/27.67 = { by lemma 48 }
% 175.75/27.67 and(and(not(a), not(not(a11))), X)
% 175.75/27.67 = { by axiom 2 (not_involution) }
% 175.75/27.67 and(and(not(a), a11), X)
% 175.75/27.67 = { by axiom 9 (and_symmetry) }
% 175.75/27.67 and(and(a11, not(a)), X)
% 175.75/27.67 = { by lemma 90 }
% 175.75/27.67 and(not(a), X)
% 175.75/27.67 = { by axiom 9 (and_symmetry) }
% 175.75/27.67 and(X, not(a))
% 175.75/27.67
% 175.75/27.67 Lemma 92: or(X, and(not(X), Y)) = or(X, Y).
% 175.75/27.67 Proof:
% 175.75/27.67 or(X, and(not(X), Y))
% 175.75/27.67 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 or(X, and(Y, not(X)))
% 175.75/27.67 = { by lemma 49 }
% 175.75/27.67 or(Y, X)
% 175.75/27.67 = { by axiom 4 (or_symmetry) }
% 175.75/27.67 or(X, Y)
% 175.75/27.67
% 175.75/27.67 Lemma 93: and(c1, a) = and(a16, a).
% 175.75/27.67 Proof:
% 175.75/27.67 and(c1, a)
% 175.75/27.67 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 and(a, c1)
% 175.75/27.67 = { by lemma 75 R->L }
% 175.75/27.67 and(a, or(c1, not(a)))
% 175.75/27.67 = { by lemma 82 }
% 175.75/27.67 and(a, or(a12, c1))
% 175.75/27.67 = { by lemma 86 }
% 175.75/27.67 and(a, or(a12, a16))
% 175.75/27.67 = { by lemma 49 R->L }
% 175.75/27.67 and(a, or(a16, and(a12, not(a16))))
% 175.75/27.67 = { by lemma 89 R->L }
% 175.75/27.67 and(a, or(a16, and(a12, and(a14, not(c1)))))
% 175.75/27.67 = { by lemma 43 R->L }
% 175.75/27.67 and(a, or(a16, and(a12, and(a14, and(a11, a15)))))
% 175.75/27.67 = { by lemma 87 }
% 175.75/27.67 and(a, or(a16, and(a12, and(a11, not(a16)))))
% 175.75/27.67 = { by lemma 91 }
% 175.75/27.67 and(a, or(a16, and(not(a16), not(a))))
% 175.75/27.67 = { by lemma 92 }
% 175.75/27.67 and(a, or(a16, not(a)))
% 175.75/27.67 = { by lemma 75 }
% 175.75/27.67 and(a, a16)
% 175.75/27.67 = { by axiom 9 (and_symmetry) }
% 175.75/27.67 and(a16, a)
% 175.75/27.67
% 175.75/27.67 Lemma 94: and(a, not(b)) = not(a12).
% 175.75/27.67 Proof:
% 175.75/27.67 and(a, not(b))
% 175.75/27.67 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 and(not(b), a)
% 175.75/27.67 = { by axiom 2 (not_involution) R->L }
% 175.75/27.67 and(not(b), not(not(a)))
% 175.75/27.67 = { by lemma 48 R->L }
% 175.75/27.67 and(not(not(a)), or(not(a), not(b)))
% 175.75/27.67 = { by lemma 44 }
% 175.75/27.67 and(not(not(a)), a11)
% 175.75/27.67 = { by axiom 2 (not_involution) }
% 175.75/27.67 and(a, a11)
% 175.75/27.67 = { by axiom 9 (and_symmetry) }
% 175.75/27.67 and(a11, a)
% 175.75/27.67 = { by lemma 39 }
% 175.75/27.67 not(a12)
% 175.75/27.67
% 175.75/27.67 Lemma 95: or(b, not(a12)) = or(a, b).
% 175.75/27.67 Proof:
% 175.75/27.67 or(b, not(a12))
% 175.75/27.67 = { by lemma 94 R->L }
% 175.75/27.67 or(b, and(a, not(b)))
% 175.75/27.67 = { by lemma 49 }
% 175.75/27.67 or(a, b)
% 175.75/27.67
% 175.75/27.67 Lemma 96: and(not(a12), not(b)) = not(a12).
% 175.75/27.67 Proof:
% 175.75/27.67 and(not(a12), not(b))
% 175.75/27.67 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 and(not(b), not(a12))
% 175.75/27.67 = { by lemma 94 R->L }
% 175.75/27.67 and(not(b), and(a, not(b)))
% 175.75/27.67 = { by lemma 66 }
% 175.75/27.67 and(a, not(b))
% 175.75/27.67 = { by lemma 94 }
% 175.75/27.67 not(a12)
% 175.75/27.67
% 175.75/27.67 Lemma 97: xor(Y, X) = xor(X, Y).
% 175.75/27.67 Proof:
% 175.75/27.67 xor(Y, X)
% 175.75/27.67 = { by axiom 34 (xor_definition) }
% 175.75/27.67 or(and(Y, not(X)), and(X, not(Y)))
% 175.75/27.67 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.67 or(and(X, not(Y)), and(Y, not(X)))
% 175.75/27.67 = { by axiom 34 (xor_definition) R->L }
% 175.75/27.67 xor(X, Y)
% 175.75/27.67
% 175.75/27.67 Lemma 98: or(a, b) = xor(b, not(a12)).
% 175.75/27.67 Proof:
% 175.75/27.67 or(a, b)
% 175.75/27.67 = { by lemma 95 R->L }
% 175.75/27.67 or(b, not(a12))
% 175.75/27.67 = { by lemma 49 R->L }
% 175.75/27.67 or(not(a12), and(b, not(not(a12))))
% 175.75/27.67 = { by lemma 96 R->L }
% 175.75/27.67 or(and(not(a12), not(b)), and(b, not(not(a12))))
% 175.75/27.67 = { by axiom 34 (xor_definition) R->L }
% 175.75/27.67 xor(not(a12), b)
% 175.75/27.67 = { by lemma 97 R->L }
% 175.75/27.67 xor(b, not(a12))
% 175.75/27.67
% 175.75/27.67 Lemma 99: or(X, and(X, Y)) = X.
% 175.75/27.67 Proof:
% 175.75/27.67 or(X, and(X, Y))
% 175.75/27.67 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.67 or(and(X, Y), X)
% 175.75/27.67 = { by axiom 27 (and_or_subsumption2) }
% 175.75/27.67 X
% 175.75/27.67
% 175.75/27.67 Lemma 100: or(X, or(Y, and(X, Z))) = or(X, Y).
% 175.75/27.67 Proof:
% 175.75/27.67 or(X, or(Y, and(X, Z)))
% 175.75/27.67 = { by lemma 79 R->L }
% 175.75/27.67 or(or(X, Y), and(X, Z))
% 175.75/27.67 = { by axiom 25 (or_commutativity) R->L }
% 175.75/27.67 or(or(X, and(X, Z)), Y)
% 175.75/27.67 = { by lemma 99 }
% 175.75/27.67 or(X, Y)
% 175.75/27.67
% 175.75/27.67 Lemma 101: or(a12, carryin) = or(a12, a16).
% 175.75/27.67 Proof:
% 175.75/27.67 or(a12, carryin)
% 175.75/27.67 = { by axiom 10 (and_definition2) R->L }
% 175.75/27.67 or(a12, and(carryin, n1))
% 175.75/27.67 = { by lemma 88 R->L }
% 175.75/27.67 or(a12, and(carryin, or(not(not(a12)), or(not(a12), not(a13)))))
% 175.75/27.67 = { by lemma 46 }
% 175.75/27.67 or(a12, and(carryin, or(not(not(a12)), a14)))
% 175.75/27.67 = { by axiom 2 (not_involution) }
% 175.75/27.67 or(a12, and(carryin, or(a12, a14)))
% 175.75/27.67 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.67 or(a12, and(carryin, or(a14, a12)))
% 175.75/27.67 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 or(a12, and(or(a14, a12), carryin))
% 175.75/27.67 = { by axiom 33 (and_or_simplification) }
% 175.75/27.67 or(a12, or(and(a14, carryin), and(a12, carryin)))
% 175.75/27.67 = { by lemma 65 }
% 175.75/27.67 or(a12, or(not(a15), and(a12, carryin)))
% 175.75/27.67 = { by lemma 100 }
% 175.75/27.67 or(a12, not(a15))
% 175.75/27.67 = { by lemma 81 }
% 175.75/27.67 or(a12, c1)
% 175.75/27.67 = { by lemma 86 }
% 175.75/27.67 or(a12, a16)
% 175.75/27.67
% 175.75/27.67 Lemma 102: and(a14, and(a15, X)) = and(X, not(a16)).
% 175.75/27.67 Proof:
% 175.75/27.67 and(a14, and(a15, X))
% 175.75/27.67 = { by lemma 57 R->L }
% 175.75/27.67 and(a15, and(X, a14))
% 175.75/27.67 = { by lemma 57 R->L }
% 175.75/27.67 and(X, and(a14, a15))
% 175.75/27.67 = { by lemma 63 }
% 175.75/27.67 and(X, not(a16))
% 175.75/27.67
% 175.75/27.67 Lemma 103: and(a15, not(c1)) = not(c1).
% 175.75/27.67 Proof:
% 175.75/27.67 and(a15, not(c1))
% 175.75/27.67 = { by lemma 43 R->L }
% 175.75/27.67 and(a15, and(a11, a15))
% 175.75/27.67 = { by lemma 66 }
% 175.75/27.67 and(a11, a15)
% 175.75/27.67 = { by lemma 43 }
% 175.75/27.67 not(c1)
% 175.75/27.67
% 175.75/27.67 Lemma 104: and(not(a16), not(c1)) = and(a14, not(c1)).
% 175.75/27.67 Proof:
% 175.75/27.67 and(not(a16), not(c1))
% 175.75/27.67 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.67 and(not(c1), not(a16))
% 175.75/27.67 = { by lemma 102 R->L }
% 175.75/27.67 and(a14, and(a15, not(c1)))
% 175.75/27.67 = { by lemma 103 }
% 175.75/27.67 and(a14, not(c1))
% 175.75/27.67
% 175.75/27.67 Lemma 105: or(c1, not(a16)) = or(c1, a14).
% 175.75/27.67 Proof:
% 175.75/27.67 or(c1, not(a16))
% 175.75/27.67 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.67 or(not(a16), c1)
% 175.75/27.67 = { by lemma 49 R->L }
% 175.75/27.67 or(c1, and(not(a16), not(c1)))
% 175.75/27.67 = { by lemma 104 }
% 175.75/27.67 or(c1, and(a14, not(c1)))
% 175.75/27.67 = { by lemma 49 }
% 175.75/27.67 or(a14, c1)
% 175.75/27.67 = { by axiom 4 (or_symmetry) }
% 175.75/27.67 or(c1, a14)
% 175.75/27.67
% 175.75/27.67 Lemma 106: or(c1, a14) = xor(c1, not(a16)).
% 175.75/27.67 Proof:
% 175.75/27.67 or(c1, a14)
% 175.75/27.67 = { by lemma 105 R->L }
% 175.75/27.67 or(c1, not(a16))
% 175.75/27.67 = { by lemma 49 R->L }
% 175.75/27.67 or(not(a16), and(c1, not(not(a16))))
% 175.75/27.67 = { by lemma 89 R->L }
% 175.75/27.67 or(and(a14, not(c1)), and(c1, not(not(a16))))
% 175.75/27.67 = { by lemma 103 R->L }
% 175.75/27.67 or(and(a14, and(a15, not(c1))), and(c1, not(not(a16))))
% 175.75/27.67 = { by lemma 102 }
% 175.75/27.67 or(and(not(c1), not(a16)), and(c1, not(not(a16))))
% 175.75/27.67 = { by axiom 9 (and_symmetry) }
% 175.75/27.67 or(and(not(a16), not(c1)), and(c1, not(not(a16))))
% 175.75/27.67 = { by axiom 34 (xor_definition) R->L }
% 175.75/27.67 xor(not(a16), c1)
% 175.75/27.67 = { by lemma 97 R->L }
% 175.75/27.67 xor(c1, not(a16))
% 175.75/27.67
% 175.75/27.67 Lemma 107: xor(a, b) = a14.
% 175.75/27.67 Proof:
% 175.75/27.67 xor(a, b)
% 175.75/27.67 = { by axiom 34 (xor_definition) }
% 175.75/27.67 or(and(a, not(b)), and(b, not(a)))
% 175.75/27.67 = { by lemma 94 }
% 175.75/27.67 or(not(a12), and(b, not(a)))
% 175.75/27.67 = { by lemma 51 }
% 175.75/27.67 or(not(a12), not(a13))
% 175.75/27.67 = { by lemma 46 }
% 175.75/27.67 a14
% 175.75/27.67
% 175.75/27.67 Lemma 108: xor(b, not(a12)) = xor(a, not(a13)).
% 175.75/27.67 Proof:
% 175.75/27.67 xor(b, not(a12))
% 175.75/27.67 = { by lemma 98 R->L }
% 175.75/27.67 or(a, b)
% 175.75/27.67 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.67 or(b, a)
% 175.75/27.67 = { by lemma 49 R->L }
% 175.75/27.67 or(a, and(b, not(a)))
% 175.75/27.67 = { by lemma 51 }
% 175.75/27.67 or(a, not(a13))
% 175.75/27.67 = { by lemma 49 R->L }
% 175.75/27.67 or(not(a13), and(a, not(not(a13))))
% 175.75/27.67 = { by lemma 51 R->L }
% 175.75/27.67 or(and(b, not(a)), and(a, not(not(a13))))
% 175.75/27.67 = { by lemma 66 R->L }
% 175.75/27.67 or(and(not(a), and(b, not(a))), and(a, not(not(a13))))
% 175.75/27.67 = { by lemma 51 }
% 175.75/27.67 or(and(not(a), not(a13)), and(a, not(not(a13))))
% 175.75/27.67 = { by axiom 9 (and_symmetry) }
% 175.75/27.67 or(and(not(a13), not(a)), and(a, not(not(a13))))
% 175.75/27.67 = { by axiom 34 (xor_definition) R->L }
% 175.75/27.67 xor(not(a13), a)
% 175.75/27.67 = { by lemma 97 R->L }
% 175.75/27.67 xor(a, not(a13))
% 175.75/27.67
% 175.75/27.67 Lemma 109: xor(a, not(a13)) = xor(c1, not(a16)).
% 175.75/27.67 Proof:
% 175.75/27.67 xor(a, not(a13))
% 175.75/27.67 = { by lemma 108 R->L }
% 175.75/27.67 xor(b, not(a12))
% 175.75/27.67 = { by lemma 98 R->L }
% 175.75/27.67 or(a, b)
% 175.75/27.67 = { by lemma 95 R->L }
% 175.75/27.67 or(b, not(a12))
% 175.75/27.67 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.67 or(not(a12), b)
% 175.75/27.68 = { by axiom 2 (not_involution) R->L }
% 175.75/27.68 or(not(a12), not(not(b)))
% 175.75/27.68 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.68 not(and(a12, not(b)))
% 175.75/27.68 = { by lemma 53 R->L }
% 175.75/27.68 not(and(a12, not(or(b, and(a, b)))))
% 175.75/27.68 = { by lemma 45 }
% 175.75/27.68 not(and(a12, not(or(b, not(a11)))))
% 175.75/27.68 = { by axiom 12 (demorgan2) }
% 175.75/27.68 not(and(a12, and(not(b), not(not(a11)))))
% 175.75/27.68 = { by lemma 48 R->L }
% 175.75/27.68 not(and(a12, and(not(not(a11)), or(not(a11), not(b)))))
% 175.75/27.68 = { by lemma 40 }
% 175.75/27.68 not(and(a12, and(not(not(a11)), a13)))
% 175.75/27.68 = { by axiom 2 (not_involution) }
% 175.75/27.68 not(and(a12, and(a11, a13)))
% 175.75/27.68 = { by axiom 9 (and_symmetry) }
% 175.75/27.68 not(and(a12, and(a13, a11)))
% 175.75/27.68 = { by lemma 70 }
% 175.75/27.68 not(and(a11, not(a14)))
% 175.75/27.68 = { by lemma 73 R->L }
% 175.75/27.68 not(and(a11, and(a15, not(a14))))
% 175.75/27.68 = { by lemma 76 }
% 175.75/27.68 not(and(not(a14), not(c1)))
% 175.75/27.68 = { by axiom 9 (and_symmetry) }
% 175.75/27.68 not(and(not(c1), not(a14)))
% 175.75/27.68 = { by axiom 13 (demorgan1) }
% 175.75/27.68 or(not(not(c1)), not(not(a14)))
% 175.75/27.68 = { by axiom 2 (not_involution) }
% 175.75/27.68 or(c1, not(not(a14)))
% 175.75/27.68 = { by axiom 2 (not_involution) }
% 175.75/27.68 or(c1, a14)
% 175.75/27.68 = { by lemma 106 }
% 175.75/27.68 xor(c1, not(a16))
% 175.75/27.68
% 175.75/27.68 Lemma 110: or(not(a15), not(carryin)) = a17.
% 175.75/27.68 Proof:
% 175.75/27.68 or(not(a15), not(carryin))
% 175.75/27.68 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.68 not(and(a15, carryin))
% 175.75/27.68 = { by axiom 21 (circuit7) R->L }
% 175.75/27.68 a17
% 175.75/27.68
% 175.75/27.68 Lemma 111: or(not(a16), not(a17)) = s1.
% 175.75/27.68 Proof:
% 175.75/27.68 or(not(a16), not(a17))
% 175.75/27.68 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.68 not(and(a16, a17))
% 175.75/27.68 = { by axiom 15 (circuit8) R->L }
% 175.75/27.68 s1
% 175.75/27.68
% 175.75/27.68 Lemma 112: sum(a, b, carryin) = s1.
% 175.75/27.68 Proof:
% 175.75/27.68 sum(a, b, carryin)
% 175.75/27.68 = { by axiom 23 (sum_definition) }
% 175.75/27.68 xor(xor(a, b), carryin)
% 175.75/27.68 = { by lemma 107 }
% 175.75/27.68 xor(a14, carryin)
% 175.75/27.68 = { by axiom 34 (xor_definition) }
% 175.75/27.68 or(and(a14, not(carryin)), and(carryin, not(a14)))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 or(and(not(carryin), a14), and(carryin, not(a14)))
% 175.75/27.68 = { by axiom 2 (not_involution) R->L }
% 175.75/27.68 or(and(not(carryin), not(not(a14))), and(carryin, not(a14)))
% 175.75/27.68 = { by lemma 48 R->L }
% 175.75/27.68 or(and(not(not(a14)), or(not(a14), not(carryin))), and(carryin, not(a14)))
% 175.75/27.68 = { by lemma 64 }
% 175.75/27.68 or(and(not(not(a14)), a15), and(carryin, not(a14)))
% 175.75/27.68 = { by axiom 2 (not_involution) }
% 175.75/27.68 or(and(a14, a15), and(carryin, not(a14)))
% 175.75/27.68 = { by lemma 63 }
% 175.75/27.68 or(not(a16), and(carryin, not(a14)))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 or(not(a16), and(not(a14), carryin))
% 175.75/27.68 = { by axiom 2 (not_involution) R->L }
% 175.75/27.68 or(not(a16), and(not(a14), not(not(carryin))))
% 175.75/27.68 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.68 or(not(a16), not(or(a14, not(carryin))))
% 175.75/27.68 = { by lemma 50 R->L }
% 175.75/27.68 or(not(a16), not(or(not(carryin), and(a14, carryin))))
% 175.75/27.68 = { by lemma 65 }
% 175.75/27.68 or(not(a16), not(or(not(carryin), not(a15))))
% 175.75/27.68 = { by axiom 4 (or_symmetry) }
% 175.75/27.68 or(not(a16), not(or(not(a15), not(carryin))))
% 175.75/27.68 = { by lemma 110 }
% 175.75/27.68 or(not(a16), not(a17))
% 175.75/27.68 = { by lemma 111 }
% 175.75/27.68 s1
% 175.75/27.68
% 175.75/27.68 Lemma 113: and(Y, and(X, Z)) = and(X, and(Y, Z)).
% 175.75/27.68 Proof:
% 175.75/27.68 and(Y, and(X, Z))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 and(Y, and(Z, X))
% 175.75/27.68 = { by lemma 57 }
% 175.75/27.68 and(X, and(Y, Z))
% 175.75/27.68
% 175.75/27.68 Lemma 114: and(a12, and(X, a14)) = and(X, not(a13)).
% 175.75/27.68 Proof:
% 175.75/27.68 and(a12, and(X, a14))
% 175.75/27.68 = { by lemma 113 }
% 175.75/27.68 and(X, and(a12, a14))
% 175.75/27.68 = { by lemma 56 }
% 175.75/27.68 and(X, not(a13))
% 175.75/27.68
% 175.75/27.68 Lemma 115: and(a14, and(X, carryin)) = and(X, not(a15)).
% 175.75/27.68 Proof:
% 175.75/27.68 and(a14, and(X, carryin))
% 175.75/27.68 = { by lemma 58 R->L }
% 175.75/27.68 and(and(a14, X), carryin)
% 175.75/27.68 = { by axiom 31 (and_commutativity) R->L }
% 175.75/27.68 and(and(a14, carryin), X)
% 175.75/27.68 = { by lemma 65 }
% 175.75/27.68 and(not(a15), X)
% 175.75/27.68 = { by axiom 9 (and_symmetry) }
% 175.75/27.68 and(X, not(a15))
% 175.75/27.68
% 175.75/27.68 Lemma 116: or(Y, or(X, Z)) = or(X, or(Y, Z)).
% 175.75/27.68 Proof:
% 175.75/27.68 or(Y, or(X, Z))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 or(Y, or(Z, X))
% 175.75/27.68 = { by lemma 69 }
% 175.75/27.68 or(X, or(Y, Z))
% 175.75/27.68
% 175.75/27.68 Lemma 117: and(not(a13), or(X, a)) = and(X, not(a13)).
% 175.75/27.68 Proof:
% 175.75/27.68 and(not(a13), or(X, a))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 and(or(X, a), not(a13))
% 175.75/27.68 = { by lemma 41 R->L }
% 175.75/27.68 and(or(X, a), and(a11, b))
% 175.75/27.68 = { by lemma 57 }
% 175.75/27.68 and(b, and(or(X, a), a11))
% 175.75/27.68 = { by lemma 57 }
% 175.75/27.68 and(a11, and(b, or(X, a)))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 and(a11, and(b, or(a, X)))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 and(a11, and(or(a, X), b))
% 175.75/27.68 = { by axiom 33 (and_or_simplification) }
% 175.75/27.68 and(a11, or(and(a, b), and(X, b)))
% 175.75/27.68 = { by lemma 45 }
% 175.75/27.68 and(a11, or(not(a11), and(X, b)))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 and(a11, or(and(X, b), not(a11)))
% 175.75/27.68 = { by lemma 75 }
% 175.75/27.68 and(a11, and(X, b))
% 175.75/27.68 = { by lemma 59 }
% 175.75/27.68 and(X, not(a13))
% 175.75/27.68
% 175.75/27.68 Lemma 118: or(not(X), and(X, Y)) = or(Y, not(X)).
% 175.75/27.68 Proof:
% 175.75/27.68 or(not(X), and(X, Y))
% 175.75/27.68 = { by axiom 2 (not_involution) R->L }
% 175.75/27.68 or(not(X), and(not(not(X)), Y))
% 175.75/27.68 = { by lemma 92 }
% 175.75/27.68 or(not(X), Y)
% 175.75/27.68 = { by axiom 4 (or_symmetry) }
% 175.75/27.68 or(Y, not(X))
% 175.75/27.68
% 175.75/27.68 Lemma 119: or(not(X), carryout(X, Y, Z)) = or(Y, or(Z, not(X))).
% 175.75/27.68 Proof:
% 175.75/27.68 or(not(X), carryout(X, Y, Z))
% 175.75/27.68 = { by axiom 37 (carryout_definition) }
% 175.75/27.68 or(not(X), or(and(X, or(Y, Z)), and(not(X), and(Y, Z))))
% 175.75/27.68 = { by lemma 100 }
% 175.75/27.68 or(not(X), and(X, or(Y, Z)))
% 175.75/27.68 = { by lemma 118 }
% 175.75/27.68 or(or(Y, Z), not(X))
% 175.75/27.68 = { by lemma 79 }
% 175.75/27.68 or(Y, or(Z, not(X)))
% 175.75/27.68
% 175.75/27.68 Lemma 120: or(b, or(X, not(a))) = or(X, a12).
% 175.75/27.68 Proof:
% 175.75/27.68 or(b, or(X, not(a)))
% 175.75/27.68 = { by lemma 116 }
% 175.75/27.68 or(X, or(b, not(a)))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 or(X, or(not(a), b))
% 175.75/27.68 = { by axiom 2 (not_involution) R->L }
% 175.75/27.68 or(X, or(not(a), not(not(b))))
% 175.75/27.68 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.68 or(X, not(and(a, not(b))))
% 175.75/27.68 = { by lemma 94 }
% 175.75/27.68 or(X, not(not(a12)))
% 175.75/27.68 = { by axiom 2 (not_involution) }
% 175.75/27.68 or(X, a12)
% 175.75/27.68
% 175.75/27.68 Lemma 121: or(carryout(a, b, carryin), not(a)) = or(a12, a16).
% 175.75/27.68 Proof:
% 175.75/27.68 or(carryout(a, b, carryin), not(a))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 or(not(a), carryout(a, b, carryin))
% 175.75/27.68 = { by lemma 119 }
% 175.75/27.68 or(b, or(carryin, not(a)))
% 175.75/27.68 = { by lemma 120 }
% 175.75/27.68 or(carryin, a12)
% 175.75/27.68 = { by axiom 4 (or_symmetry) }
% 175.75/27.68 or(a12, carryin)
% 175.75/27.68 = { by lemma 101 }
% 175.75/27.68 or(a12, a16)
% 175.75/27.68
% 175.75/27.68 Lemma 122: and(carryout(a, b, carryin), a) = and(a16, a).
% 175.75/27.68 Proof:
% 175.75/27.68 and(carryout(a, b, carryin), a)
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 and(a, carryout(a, b, carryin))
% 175.75/27.68 = { by lemma 75 R->L }
% 175.75/27.68 and(a, or(carryout(a, b, carryin), not(a)))
% 175.75/27.68 = { by lemma 121 }
% 175.75/27.68 and(a, or(a12, a16))
% 175.75/27.68 = { by lemma 86 R->L }
% 175.75/27.68 and(a, or(a12, c1))
% 175.75/27.68 = { by lemma 82 R->L }
% 175.75/27.68 and(a, or(c1, not(a)))
% 175.75/27.68 = { by lemma 75 }
% 175.75/27.68 and(a, c1)
% 175.75/27.68 = { by axiom 9 (and_symmetry) }
% 175.75/27.68 and(c1, a)
% 175.75/27.68 = { by lemma 93 }
% 175.75/27.68 and(a16, a)
% 175.75/27.68
% 175.75/27.68 Lemma 123: or(and(X, Y), and(Z, X)) = and(X, or(Y, Z)).
% 175.75/27.68 Proof:
% 175.75/27.68 or(and(X, Y), and(Z, X))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 or(and(Y, X), and(Z, X))
% 175.75/27.68 = { by axiom 33 (and_or_simplification) R->L }
% 175.75/27.68 and(or(Y, Z), X)
% 175.75/27.68 = { by axiom 9 (and_symmetry) }
% 175.75/27.68 and(X, or(Y, Z))
% 175.75/27.68
% 175.75/27.68 Lemma 124: or(not(a12), and(a13, c1)) = a.
% 175.75/27.68 Proof:
% 175.75/27.68 or(not(a12), and(a13, c1))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 or(not(a12), and(c1, a13))
% 175.75/27.68 = { by lemma 61 R->L }
% 175.75/27.68 or(and(a13, a14), and(c1, a13))
% 175.75/27.68 = { by lemma 123 }
% 175.75/27.68 and(a13, or(a14, c1))
% 175.75/27.68 = { by axiom 4 (or_symmetry) }
% 175.75/27.68 and(a13, or(c1, a14))
% 175.75/27.68 = { by lemma 106 }
% 175.75/27.68 and(a13, xor(c1, not(a16)))
% 175.75/27.68 = { by lemma 109 R->L }
% 175.75/27.68 and(a13, xor(a, not(a13)))
% 175.75/27.68 = { by lemma 108 R->L }
% 175.75/27.68 and(a13, xor(b, not(a12)))
% 175.75/27.68 = { by lemma 98 R->L }
% 175.75/27.68 and(a13, or(a, b))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 and(a13, or(b, a))
% 175.75/27.68 = { by lemma 49 R->L }
% 175.75/27.68 and(a13, or(a, and(b, not(a))))
% 175.75/27.68 = { by lemma 51 }
% 175.75/27.68 and(a13, or(a, not(a13)))
% 175.75/27.68 = { by lemma 75 }
% 175.75/27.68 and(a13, a)
% 175.75/27.68 = { by lemma 60 }
% 175.75/27.68 a
% 175.75/27.68
% 175.75/27.68 Lemma 125: or(X, or(and(Y, X), Z)) = or(Z, X).
% 175.75/27.68 Proof:
% 175.75/27.68 or(X, or(and(Y, X), Z))
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 or(or(and(Y, X), Z), X)
% 175.75/27.68 = { by axiom 36 (and_or_subsumption3) }
% 175.75/27.68 or(Z, X)
% 175.75/27.68
% 175.75/27.68 Lemma 126: or(carryout(X, Y, Z), X) = or(X, and(Y, Z)).
% 175.75/27.68 Proof:
% 175.75/27.68 or(carryout(X, Y, Z), X)
% 175.75/27.68 = { by axiom 4 (or_symmetry) R->L }
% 175.75/27.68 or(X, carryout(X, Y, Z))
% 175.75/27.68 = { by axiom 37 (carryout_definition) }
% 175.75/27.68 or(X, or(and(X, or(Y, Z)), and(not(X), and(Y, Z))))
% 175.75/27.68 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.68 or(X, or(and(or(Y, Z), X), and(not(X), and(Y, Z))))
% 175.75/27.68 = { by lemma 125 }
% 175.75/27.68 or(and(not(X), and(Y, Z)), X)
% 175.75/27.69 = { by axiom 4 (or_symmetry) }
% 175.75/27.69 or(X, and(not(X), and(Y, Z)))
% 175.75/27.69 = { by lemma 92 }
% 175.75/27.69 or(X, and(Y, Z))
% 175.75/27.69
% 175.75/27.69 Lemma 127: and(sum(a, b, carryin), not(a13)) = and(a12, not(a16)).
% 175.75/27.69 Proof:
% 175.75/27.69 and(sum(a, b, carryin), not(a13))
% 175.75/27.69 = { by lemma 114 R->L }
% 175.75/27.69 and(a12, and(sum(a, b, carryin), a14))
% 175.75/27.69 = { by lemma 112 }
% 175.75/27.69 and(a12, and(s1, a14))
% 175.75/27.69 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.69 and(a12, and(a14, s1))
% 175.75/27.69 = { by lemma 54 R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, or(s1, a15))))
% 175.75/27.69 = { by axiom 2 (not_involution) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, or(s1, not(not(a15))))))
% 175.75/27.69 = { by axiom 2 (not_involution) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, or(not(not(s1)), not(not(a15))))))
% 175.75/27.69 = { by axiom 13 (demorgan1) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(s1), not(a15))))))
% 175.75/27.69 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), not(s1))))))
% 175.75/27.69 = { by lemma 111 R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), not(or(not(a16), not(a17))))))))
% 175.75/27.69 = { by axiom 12 (demorgan2) }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), and(not(not(a16)), not(not(a17))))))))
% 175.75/27.69 = { by axiom 2 (not_involution) }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), and(a16, not(not(a17))))))))
% 175.75/27.69 = { by axiom 2 (not_involution) }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), and(a16, a17))))))
% 175.75/27.69 = { by lemma 57 }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(a17, and(not(a15), a16))))))
% 175.75/27.69 = { by lemma 57 }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(a16, and(a17, not(a15)))))))
% 175.75/27.69 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(a16, and(not(a15), a17))))))
% 175.75/27.69 = { by lemma 110 R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(a16, and(not(a15), or(not(a15), not(carryin))))))))
% 175.75/27.69 = { by lemma 54 }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(a16, not(a15))))))
% 175.75/27.69 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), a16)))))
% 175.75/27.69 = { by axiom 2 (not_involution) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(and(not(a15), not(not(a16)))))))
% 175.75/27.69 = { by axiom 12 (demorgan2) R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(not(or(a15, not(a16)))))))
% 175.75/27.69 = { by lemma 63 R->L }
% 175.75/27.69 and(a12, and(a14, and(s1, not(not(or(a15, and(a14, a15)))))))
% 175.75/27.69 = { by lemma 53 }
% 175.75/27.69 and(a12, and(a14, and(s1, not(not(a15)))))
% 175.75/27.69 = { by axiom 2 (not_involution) }
% 175.75/27.69 and(a12, and(a14, and(s1, a15)))
% 175.75/27.69 = { by lemma 87 }
% 175.75/27.69 and(a12, and(s1, not(a16)))
% 175.75/27.69 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.69 and(a12, and(not(a16), s1))
% 175.75/27.69 = { by lemma 111 R->L }
% 175.75/27.69 and(a12, and(not(a16), or(not(a16), not(a17))))
% 175.75/27.69 = { by lemma 54 }
% 175.75/27.69 and(a12, not(a16))
% 175.75/27.69
% 175.75/27.69 Lemma 128: or(X, and(Y, or(X, Z))) = or(X, and(Y, Z)).
% 175.75/27.69 Proof:
% 175.75/27.69 or(X, and(Y, or(X, Z)))
% 175.75/27.69 = { by lemma 123 R->L }
% 175.75/27.69 or(X, or(and(Y, X), and(Z, Y)))
% 175.75/27.69 = { by lemma 125 }
% 175.75/27.69 or(and(Z, Y), X)
% 175.75/27.69 = { by axiom 4 (or_symmetry) }
% 175.75/27.69 or(X, and(Z, Y))
% 175.75/27.69 = { by axiom 9 (and_symmetry) }
% 175.75/27.69 or(X, and(Y, Z))
% 175.75/27.69
% 175.75/27.69 Lemma 129: or(carryout(a, b, carryin), not(a)) = or(carryout(a, b, carryin), a12).
% 175.75/27.69 Proof:
% 175.75/27.69 or(carryout(a, b, carryin), not(a))
% 175.75/27.69 = { by lemma 121 }
% 175.75/27.69 or(a12, a16)
% 175.75/27.69 = { by lemma 78 R->L }
% 175.75/27.69 or(a12, or(a12, a16))
% 175.75/27.69 = { by lemma 121 R->L }
% 175.75/27.69 or(a12, or(carryout(a, b, carryin), not(a)))
% 175.75/27.69 = { by lemma 80 }
% 175.75/27.69 or(carryout(a, b, carryin), a12)
% 175.75/27.69
% 175.75/27.69 Goal 1 (prove_circuit): circuit(sum(a, b, carryin), carryout(a, b, carryin)) = true.
% 175.75/27.69 Proof:
% 175.75/27.69 circuit(sum(a, b, carryin), carryout(a, b, carryin))
% 175.75/27.69 = { by axiom 10 (and_definition2) R->L }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), n1))
% 175.75/27.69 = { by axiom 1 (not_definition1) R->L }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(n0)))
% 175.75/27.69 = { by axiom 32 (and_not_evaluation3) R->L }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(and(not(c1), b), not(not(c1))))))
% 175.75/27.69 = { by axiom 9 (and_symmetry) }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(not(not(c1)), and(not(c1), b)))))
% 175.75/27.69 = { by axiom 2 (not_involution) }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(c1, and(not(c1), b)))))
% 175.75/27.69 = { by axiom 9 (and_symmetry) }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(c1, and(b, not(c1))))))
% 175.75/27.69 = { by lemma 76 R->L }
% 175.75/27.69 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(c1, and(a11, and(a15, b))))))
% 175.75/27.70 = { by lemma 59 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(c1, and(a15, not(a13))))))
% 175.75/27.70 = { by lemma 85 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(c1, and(a12, not(a16))))))
% 175.75/27.70 = { by lemma 127 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(c1, and(sum(a, b, carryin), not(a13))))))
% 175.75/27.70 = { by lemma 113 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(c1, not(a13))))))
% 175.75/27.70 = { by lemma 41 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(c1, and(a11, b))))))
% 175.75/27.70 = { by lemma 58 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(and(c1, a11), b)))))
% 175.75/27.70 = { by lemma 74 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(not(a15), b)))))
% 175.75/27.70 = { by lemma 67 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(and(a16, a14), b)))))
% 175.75/27.70 = { by lemma 58 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a16, and(a14, b))))))
% 175.75/27.70 = { by axiom 9 (and_symmetry) R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a16, and(b, a14))))))
% 175.75/27.70 = { by lemma 75 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a16, and(b, or(a14, not(b))))))))
% 175.75/27.70 = { by lemma 72 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a16, and(b, a11))))))
% 175.75/27.70 = { by axiom 9 (and_symmetry) }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a16, and(a11, b))))))
% 175.75/27.70 = { by lemma 41 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a16, not(a13))))))
% 175.75/27.70 = { by lemma 114 R->L }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a12, and(a16, a14))))))
% 175.75/27.70 = { by lemma 67 }
% 175.75/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a12, not(a15))))))
% 176.54/27.70 = { by lemma 65 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(a12, and(a14, carryin))))))
% 176.54/27.70 = { by lemma 84 }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(carryin, not(a13))))))
% 176.54/27.70 = { by lemma 41 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(carryin, and(a11, b))))))
% 176.54/27.70 = { by lemma 66 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(carryin, and(b, and(a11, b)))))))
% 176.54/27.70 = { by lemma 41 }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(carryin, and(b, not(a13)))))))
% 176.54/27.70 = { by lemma 113 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(b, and(carryin, not(a13)))))))
% 176.54/27.70 = { by lemma 58 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(and(b, carryin), not(a13))))))
% 176.54/27.70 = { by lemma 117 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(not(a13), or(and(b, carryin), a))))))
% 176.54/27.70 = { by axiom 4 (or_symmetry) }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(not(a13), or(a, and(b, carryin)))))))
% 176.54/27.70 = { by lemma 126 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(not(a13), or(carryout(a, b, carryin), a))))))
% 176.54/27.70 = { by lemma 117 }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(sum(a, b, carryin), and(carryout(a, b, carryin), not(a13))))))
% 176.54/27.70 = { by lemma 113 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(sum(a, b, carryin), not(a13))))))
% 176.54/27.70 = { by lemma 127 }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(a12, not(a16))))))
% 176.54/27.70 = { by lemma 48 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(a16, a12))))))
% 176.54/27.70 = { by axiom 4 (or_symmetry) }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(a12, a16))))))
% 176.54/27.70 = { by lemma 101 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(a12, carryin))))))
% 176.54/27.70 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(carryin, a12))))))
% 176.54/27.70 = { by lemma 120 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(b, or(carryin, not(a))))))))
% 176.54/27.70 = { by lemma 119 R->L }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(not(a), carryout(a, b, carryin)))))))
% 176.54/27.70 = { by axiom 4 (or_symmetry) }
% 176.54/27.70 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(carryout(a, b, carryin), not(a)))))))
% 176.54/27.71 = { by lemma 129 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(carryout(a, b, carryin), a12))))))
% 176.54/27.71 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(not(a16), or(a12, carryout(a, b, carryin)))))))
% 176.54/27.71 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), and(or(a12, carryout(a, b, carryin)), not(a16))))))
% 176.54/27.71 = { by lemma 58 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(and(carryout(a, b, carryin), or(a12, carryout(a, b, carryin))), not(a16)))))
% 176.54/27.71 = { by lemma 55 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), not(and(carryout(a, b, carryin), not(a16)))))
% 176.54/27.71 = { by axiom 13 (demorgan1) }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), or(not(carryout(a, b, carryin)), not(not(a16)))))
% 176.54/27.71 = { by axiom 2 (not_involution) }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), or(not(carryout(a, b, carryin)), a16)))
% 176.54/27.71 = { by axiom 4 (or_symmetry) }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), or(a16, not(carryout(a, b, carryin)))))
% 176.54/27.71 = { by lemma 75 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(carryout(a, b, carryin), a16))
% 176.54/27.71 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, carryout(a, b, carryin)))
% 176.54/27.71 = { by lemma 75 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), not(a16))))
% 176.54/27.71 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), carryout(a, b, carryin))))
% 176.54/27.71 = { by lemma 99 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(carryout(a, b, carryin), a)))))
% 176.54/27.71 = { by lemma 122 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(a16, a)))))
% 176.54/27.71 = { by lemma 93 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, a)))))
% 176.54/27.71 = { by lemma 128 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), a))))))
% 176.54/27.71 = { by lemma 53 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(not(a15), or(carryout(a, b, carryin), a))))))))
% 176.54/27.71 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(or(carryout(a, b, carryin), a), not(a15))))))))
% 176.54/27.71 = { by lemma 65 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(or(carryout(a, b, carryin), a), and(a14, carryin))))))))
% 176.54/27.71 = { by lemma 57 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(carryin, and(or(carryout(a, b, carryin), a), a14))))))))
% 176.54/27.71 = { by lemma 57 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(carryout(a, b, carryin), a)))))))))
% 176.54/27.71 = { by lemma 126 }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(a, and(b, carryin))))))))))
% 176.54/27.71 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(and(b, carryin), a)))))))))
% 176.54/27.71 = { by lemma 123 R->L }
% 176.54/27.71 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(carryin, and(b, carryin)), and(a, carryin)))))))))
% 176.54/27.71 = { by lemma 66 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(b, carryin), and(a, carryin)))))))))
% 176.54/27.72 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(carryin, b), and(a, carryin)))))))))
% 176.54/27.72 = { by lemma 123 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(b, a)))))))))
% 176.54/27.72 = { by axiom 4 (or_symmetry) }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(a, b)))))))))
% 176.54/27.72 = { by lemma 95 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(b, not(a12))))))))))
% 176.54/27.72 = { by lemma 49 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(not(a12), and(b, not(not(a12))))))))))))
% 176.54/27.72 = { by lemma 96 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(and(not(a12), not(b)), and(b, not(not(a12))))))))))))
% 176.54/27.72 = { by axiom 34 (xor_definition) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, xor(not(a12), b)))))))))
% 176.54/27.72 = { by lemma 97 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, xor(b, not(a12))))))))))
% 176.54/27.72 = { by lemma 108 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, xor(a, not(a13))))))))))
% 176.54/27.72 = { by lemma 109 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, xor(c1, not(a16))))))))))
% 176.54/27.72 = { by lemma 106 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(c1, a14)))))))))
% 176.54/27.72 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(a14, c1)))))))))
% 176.54/27.72 = { by lemma 49 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(c1, and(a14, not(c1)))))))))))
% 176.54/27.72 = { by lemma 104 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(c1, and(not(a16), not(c1)))))))))))
% 176.54/27.72 = { by lemma 49 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(carryin, or(not(a16), c1)))))))))
% 176.54/27.72 = { by lemma 123 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(carryin, not(a16)), and(c1, carryin)))))))))
% 176.54/27.72 = { by lemma 102 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(a14, and(a15, carryin)), and(c1, carryin)))))))))
% 176.54/27.72 = { by lemma 115 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(a15, not(a15)), and(c1, carryin)))))))))
% 176.54/27.72 = { by axiom 11 (and_not_evaluation1) }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(n0, and(c1, carryin)))))))))
% 176.54/27.72 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, or(and(c1, carryin), n0))))))))
% 176.54/27.72 = { by axiom 6 (or_definition1) }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(a14, and(c1, carryin))))))))
% 176.54/27.72 = { by lemma 115 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(c1, not(a15))))))))
% 176.54/27.72 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(not(a15), c1)))))))
% 176.54/27.72 = { by axiom 2 (not_involution) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), and(not(a15), not(not(c1)))))))))
% 176.54/27.72 = { by axiom 12 (demorgan2) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), not(or(a15, not(c1)))))))))
% 176.54/27.72 = { by lemma 43 R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), not(or(a15, and(a11, a15)))))))))
% 176.54/27.72 = { by lemma 53 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(carryout(a, b, carryin), a), not(a15)))))))
% 176.54/27.72 = { by lemma 79 }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(a, not(a15))))))))
% 176.54/27.72 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.72 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(not(a15), a)))))))
% 176.54/27.73 = { by axiom 2 (not_involution) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(not(a15), not(not(a)))))))))
% 176.54/27.73 = { by axiom 13 (demorgan1) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), not(and(a15, not(a)))))))))
% 176.54/27.73 = { by lemma 91 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), not(and(a12, and(a11, a15)))))))))
% 176.54/27.73 = { by lemma 43 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), not(and(a12, not(c1)))))))))
% 176.54/27.73 = { by axiom 13 (demorgan1) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(not(a12), not(not(c1)))))))))
% 176.54/27.73 = { by axiom 2 (not_involution) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(not(a12), c1)))))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, not(a12))))))))
% 176.54/27.73 = { by lemma 100 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, or(not(a12), and(c1, a)))))))))
% 176.54/27.73 = { by lemma 39 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, or(and(a11, a), and(c1, a)))))))))
% 176.54/27.73 = { by axiom 33 (and_or_simplification) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, and(or(a11, c1), a))))))))
% 176.54/27.73 = { by axiom 9 (and_symmetry) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, and(a, or(a11, c1)))))))))
% 176.54/27.73 = { by axiom 2 (not_involution) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, and(a, or(not(not(a11)), c1)))))))))
% 176.54/27.73 = { by lemma 42 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, and(a, or(not(not(a11)), or(not(a11), not(a15)))))))))))
% 176.54/27.73 = { by lemma 88 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, and(a, n1))))))))
% 176.54/27.73 = { by axiom 10 (and_definition2) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(c1, a)))))))
% 176.54/27.73 = { by lemma 69 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(c1, or(a, carryout(a, b, carryin))))))))
% 176.54/27.73 = { by lemma 54 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), c1))))
% 176.54/27.73 = { by axiom 10 (and_definition2) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, n1)))))
% 176.54/27.73 = { by axiom 5 (or_definition2) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), n1))))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(n1, carryout(a, b, carryin)))))))
% 176.54/27.73 = { by lemma 88 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(not(not(a11)), or(not(a11), not(a))), carryout(a, b, carryin)))))))
% 176.54/27.73 = { by lemma 38 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(not(not(a11)), a12), carryout(a, b, carryin)))))))
% 176.54/27.73 = { by axiom 2 (not_involution) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(a11, a12), carryout(a, b, carryin)))))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(a12, a11), carryout(a, b, carryin)))))))
% 176.54/27.73 = { by axiom 25 (or_commutativity) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(or(a12, carryout(a, b, carryin)), a11))))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(a11, or(a12, carryout(a, b, carryin))))))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(a11, or(carryout(a, b, carryin), a12)))))))
% 176.54/27.73 = { by lemma 129 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(a11, or(carryout(a, b, carryin), not(a))))))))
% 176.54/27.73 = { by lemma 116 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(a11, not(a))))))))
% 176.54/27.73 = { by lemma 90 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), or(a11, and(a11, not(a)))))))))
% 176.54/27.73 = { by lemma 99 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, or(carryout(a, b, carryin), a11))))))
% 176.54/27.73 = { by lemma 128 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), and(c1, a11)))))
% 176.54/27.73 = { by lemma 74 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(not(a16), or(carryout(a, b, carryin), not(a15)))))
% 176.54/27.73 = { by lemma 116 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(not(a16), not(a15)))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(not(a15), not(a16)))))
% 176.54/27.73 = { by lemma 63 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(not(a15), and(a14, a15)))))
% 176.54/27.73 = { by lemma 50 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a14, not(a15)))))
% 176.54/27.73 = { by lemma 65 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a14, and(a14, carryin)))))
% 176.54/27.73 = { by lemma 99 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), a14)))
% 176.54/27.73 = { by lemma 100 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a14, and(carryout(a, b, carryin), a)))))
% 176.54/27.73 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(carryout(a, b, carryin), a), a14))))
% 176.54/27.73 = { by lemma 122 }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(a16, a), a14))))
% 176.54/27.73 = { by lemma 93 R->L }
% 176.54/27.73 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(c1, a), a14))))
% 176.54/27.74 = { by lemma 60 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(c1, and(a13, a)), a14))))
% 176.54/27.74 = { by lemma 113 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(a13, and(c1, a)), a14))))
% 176.54/27.74 = { by lemma 58 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(and(a13, c1), a), a14))))
% 176.54/27.74 = { by lemma 124 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(and(a13, c1), or(not(a12), and(a13, c1))), a14))))
% 176.54/27.74 = { by lemma 55 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(and(a13, c1), a14))))
% 176.54/27.74 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a14, and(a13, c1)))))
% 176.54/27.74 = { by lemma 99 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(or(a14, and(a14, not(a12))), and(a13, c1)))))
% 176.54/27.74 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(or(a14, and(not(a12), a14)), and(a13, c1)))))
% 176.54/27.74 = { by lemma 46 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(or(a14, and(not(a12), or(not(a12), not(a13)))), and(a13, c1)))))
% 176.54/27.74 = { by lemma 54 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(or(a14, not(a12)), and(a13, c1)))))
% 176.54/27.74 = { by lemma 79 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a14, or(not(a12), and(a13, c1))))))
% 176.54/27.74 = { by lemma 124 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a14, a))))
% 176.54/27.74 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a, a14))))
% 176.54/27.74 = { by lemma 107 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a, xor(a, b)))))
% 176.54/27.74 = { by lemma 97 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a, xor(b, a)))))
% 176.54/27.74 = { by axiom 34 (xor_definition) }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a, or(and(b, not(a)), and(a, not(b)))))))
% 176.54/27.74 = { by lemma 100 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(a, and(b, not(a))))))
% 176.54/27.74 = { by lemma 49 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(carryout(a, b, carryin), or(b, a))))
% 176.54/27.74 = { by lemma 116 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(b, or(carryout(a, b, carryin), a))))
% 176.54/27.74 = { by lemma 126 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(b, or(a, and(b, carryin)))))
% 176.54/27.74 = { by lemma 100 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(b, a)))
% 176.54/27.74 = { by axiom 4 (or_symmetry) }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(a, b)))
% 176.54/27.74 = { by lemma 98 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, xor(b, not(a12))))
% 176.54/27.74 = { by lemma 108 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, xor(a, not(a13))))
% 176.54/27.74 = { by lemma 109 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, xor(c1, not(a16))))
% 176.54/27.74 = { by lemma 106 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(c1, a14)))
% 176.54/27.74 = { by lemma 105 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, or(c1, not(a16))))
% 176.54/27.74 = { by lemma 75 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(a16, c1))
% 176.54/27.74 = { by axiom 9 (and_symmetry) R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, a16))
% 176.54/27.74 = { by lemma 75 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(a16, not(c1))))
% 176.54/27.74 = { by axiom 4 (or_symmetry) R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(not(c1), a16)))
% 176.54/27.74 = { by axiom 2 (not_involution) R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(not(c1), not(not(a16)))))
% 176.54/27.74 = { by lemma 118 R->L }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(not(not(a16)), and(not(a16), not(c1)))))
% 176.54/27.74 = { by lemma 104 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(not(not(a16)), and(a14, not(c1)))))
% 176.54/27.74 = { by axiom 2 (not_involution) }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(a16, and(a14, not(c1)))))
% 176.54/27.74 = { by lemma 89 }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, or(a16, not(a16))))
% 176.54/27.74 = { by axiom 7 (or_not_evaluation1) }
% 176.54/27.74 circuit(sum(a, b, carryin), and(c1, n1))
% 176.54/27.74 = { by axiom 10 (and_definition2) }
% 176.54/27.74 circuit(sum(a, b, carryin), c1)
% 176.54/27.74 = { by lemma 112 }
% 176.54/27.74 circuit(s1, c1)
% 176.54/27.74 = { by axiom 3 (the_output_circuit) }
% 176.54/27.74 true
% 176.54/27.74 % SZS output end Proof
% 176.54/27.74
% 176.54/27.74 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------