%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : HWV004-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 60.74s 8.08s
% Output : Proof 61.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV004-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 10:54:23 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 60.74/8.08 Command-line arguments: --flatten --complete-subsets
% 60.74/8.08
% 60.74/8.08 % SZS status Unsatisfiable
% 60.74/8.08
% 61.85/8.20 % SZS output start Proof
% 61.85/8.20 Axiom 1 (not_definition2): not(n1) = n0.
% 61.85/8.20 Axiom 2 (not_definition1): not(n0) = n1.
% 61.85/8.20 Axiom 3 (not_involution): not(not(X)) = X.
% 61.85/8.20 Axiom 4 (or_symmetry): or(X, Y) = or(Y, X).
% 61.85/8.20 Axiom 5 (or_definition1): or(X, n0) = X.
% 61.85/8.20 Axiom 6 (or_not_evaluation1): or(X, not(X)) = n1.
% 61.85/8.20 Axiom 7 (and_idempotency): and(X, X) = X.
% 61.85/8.20 Axiom 8 (and_symmetry): and(X, Y) = and(Y, X).
% 61.85/8.20 Axiom 9 (and_definition2): and(X, n1) = X.
% 61.85/8.21 Axiom 10 (and_definition1): and(X, n0) = n0.
% 61.85/8.21 Axiom 11 (and_not_evaluation1): and(X, not(X)) = n0.
% 61.85/8.21 Axiom 12 (demorgan2): not(or(X, Y)) = and(not(X), not(Y)).
% 61.85/8.21 Axiom 13 (demorgan1): not(and(X, Y)) = or(not(X), not(Y)).
% 61.85/8.21 Axiom 14 (the_output_circuit): circuit(s0, s1, overflow) = true.
% 61.85/8.21 Axiom 15 (s0_definition): s0 = sum(a0, b0, n0).
% 61.85/8.21 Axiom 16 (sum_definition): sum(X, Y, Z) = xor(xor(X, Y), Z).
% 61.85/8.21 Axiom 17 (or_evaluation1): or(or(X, Y), Y) = or(X, Y).
% 61.85/8.21 Axiom 18 (or_commutativity): or(or(X, Y), Z) = or(or(X, Z), Y).
% 61.85/8.21 Axiom 19 (or_not_evaluation2): or(or(X, Y), not(Y)) = n1.
% 61.85/8.21 Axiom 20 (and_or_subsumption2): or(and(X, Y), X) = X.
% 61.85/8.21 Axiom 21 (and_or_subsumption1): or(and(X, Y), Y) = Y.
% 61.85/8.21 Axiom 22 (karnaugh1): or(and(X, not(Y)), Y) = or(X, Y).
% 61.85/8.21 Axiom 23 (and_evaluation1): and(and(X, Y), Y) = and(X, Y).
% 61.85/8.21 Axiom 24 (and_commutativity): and(and(X, Y), Z) = and(and(X, Z), Y).
% 61.85/8.21 Axiom 25 (and_not_evaluation3): and(and(X, Y), not(X)) = n0.
% 61.85/8.21 Axiom 26 (s1_definition): s1 = sum(a1, b1, carryout(a0, b0, n0)).
% 61.85/8.21 Axiom 27 (overflow_definition): overflow = carryout(a1, b1, carryout(a0, b0, n0)).
% 61.85/8.21 Axiom 28 (and_or_simplification): and(or(X, Y), Z) = or(and(X, Z), and(Y, Z)).
% 61.85/8.21 Axiom 29 (xor_definition): xor(X, Y) = or(and(X, not(Y)), and(Y, not(X))).
% 61.85/8.21 Axiom 30 (and_or_subsumption4): or(or(X, and(Y, Z)), Z) = or(X, Z).
% 61.85/8.21 Axiom 31 (and_or_subsumption3): or(or(and(X, Y), Z), Y) = or(Z, Y).
% 61.85/8.21 Axiom 32 (carryout_definition): carryout(X, Y, Z) = or(and(X, or(Y, Z)), and(not(X), and(Y, Z))).
% 61.85/8.21
% 61.85/8.21 Lemma 33: xor(Y, X) = xor(X, Y).
% 61.85/8.21 Proof:
% 61.85/8.21 xor(Y, X)
% 61.85/8.21 = { by axiom 29 (xor_definition) }
% 61.85/8.21 or(and(Y, not(X)), and(X, not(Y)))
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(and(X, not(Y)), and(Y, not(X)))
% 61.85/8.21 = { by axiom 29 (xor_definition) R->L }
% 61.85/8.21 xor(X, Y)
% 61.85/8.21
% 61.85/8.21 Lemma 34: and(X, not(n0)) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 and(X, not(n0))
% 61.85/8.21 = { by axiom 2 (not_definition1) }
% 61.85/8.21 and(X, n1)
% 61.85/8.21 = { by axiom 9 (and_definition2) }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 35: and(X, not(n1)) = not(n1).
% 61.85/8.21 Proof:
% 61.85/8.21 and(X, not(n1))
% 61.85/8.21 = { by axiom 1 (not_definition2) }
% 61.85/8.21 and(X, n0)
% 61.85/8.21 = { by axiom 10 (and_definition1) }
% 61.85/8.21 n0
% 61.85/8.21 = { by axiom 1 (not_definition2) R->L }
% 61.85/8.21 not(n1)
% 61.85/8.21
% 61.85/8.21 Lemma 36: and(not(n0), X) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 and(not(n0), X)
% 61.85/8.21 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.21 and(X, not(n0))
% 61.85/8.21 = { by lemma 34 }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 37: or(X, not(n1)) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 or(X, not(n1))
% 61.85/8.21 = { by axiom 1 (not_definition2) }
% 61.85/8.21 or(X, n0)
% 61.85/8.21 = { by axiom 5 (or_definition1) }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 38: or(not(n1), X) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 or(not(n1), X)
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(X, not(n1))
% 61.85/8.21 = { by lemma 37 }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 39: carryout(X, Y, n0) = and(X, Y).
% 61.85/8.21 Proof:
% 61.85/8.21 carryout(X, Y, n0)
% 61.85/8.21 = { by axiom 1 (not_definition2) R->L }
% 61.85/8.21 carryout(X, Y, not(n1))
% 61.85/8.21 = { by axiom 32 (carryout_definition) }
% 61.85/8.21 or(and(X, or(Y, not(n1))), and(not(X), and(Y, not(n1))))
% 61.85/8.21 = { by lemma 37 }
% 61.85/8.21 or(and(X, Y), and(not(X), and(Y, not(n1))))
% 61.85/8.21 = { by lemma 35 }
% 61.85/8.21 or(and(X, Y), and(not(X), not(n1)))
% 61.85/8.21 = { by lemma 35 }
% 61.85/8.21 or(and(X, Y), not(n1))
% 61.85/8.21 = { by lemma 37 }
% 61.85/8.21 and(X, Y)
% 61.85/8.21
% 61.85/8.21 Lemma 40: and(X, and(Y, X)) = and(Y, X).
% 61.85/8.21 Proof:
% 61.85/8.21 and(X, and(Y, X))
% 61.85/8.21 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.21 and(and(Y, X), X)
% 61.85/8.21 = { by axiom 23 (and_evaluation1) }
% 61.85/8.21 and(Y, X)
% 61.85/8.21
% 61.85/8.21 Lemma 41: and(X, and(Y, Z)) = and(Z, and(X, Y)).
% 61.85/8.21 Proof:
% 61.85/8.21 and(X, and(Y, Z))
% 61.85/8.21 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.21 and(and(Y, Z), X)
% 61.85/8.21 = { by axiom 24 (and_commutativity) }
% 61.85/8.21 and(and(Y, X), Z)
% 61.85/8.21 = { by axiom 8 (and_symmetry) }
% 61.85/8.21 and(Z, and(Y, X))
% 61.85/8.21 = { by axiom 8 (and_symmetry) }
% 61.85/8.21 and(Z, and(X, Y))
% 61.85/8.21
% 61.85/8.21 Lemma 42: or(X, and(Y, X)) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 or(X, and(Y, X))
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(and(Y, X), X)
% 61.85/8.21 = { by axiom 21 (and_or_subsumption1) }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 43: and(X, or(X, Y)) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 and(X, or(X, Y))
% 61.85/8.21 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.21 and(or(X, Y), X)
% 61.85/8.21 = { by axiom 28 (and_or_simplification) }
% 61.85/8.21 or(and(X, X), and(Y, X))
% 61.85/8.21 = { by axiom 7 (and_idempotency) }
% 61.85/8.21 or(X, and(Y, X))
% 61.85/8.21 = { by lemma 42 }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 44: and(X, or(Y, X)) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 and(X, or(Y, X))
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 and(X, or(X, Y))
% 61.85/8.21 = { by lemma 43 }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 45: or(X, and(X, Y)) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 or(X, and(X, Y))
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(and(X, Y), X)
% 61.85/8.21 = { by axiom 20 (and_or_subsumption2) }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 46: or(Y, or(Z, X)) = or(X, or(Y, Z)).
% 61.85/8.21 Proof:
% 61.85/8.21 or(Y, or(Z, X))
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(or(Z, X), Y)
% 61.85/8.21 = { by axiom 18 (or_commutativity) }
% 61.85/8.21 or(or(Z, Y), X)
% 61.85/8.21 = { by axiom 4 (or_symmetry) }
% 61.85/8.21 or(X, or(Z, Y))
% 61.85/8.21 = { by axiom 4 (or_symmetry) }
% 61.85/8.21 or(X, or(Y, Z))
% 61.85/8.21
% 61.85/8.21 Lemma 47: or(X, or(Y, Z)) = or(Z, or(Y, X)).
% 61.85/8.21 Proof:
% 61.85/8.21 or(X, or(Y, Z))
% 61.85/8.21 = { by lemma 46 }
% 61.85/8.21 or(Z, or(X, Y))
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(Z, or(Y, X))
% 61.85/8.21
% 61.85/8.21 Lemma 48: or(and(X, Y), X) = X.
% 61.85/8.21 Proof:
% 61.85/8.21 or(and(X, Y), X)
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(X, and(X, Y))
% 61.85/8.21 = { by lemma 45 }
% 61.85/8.21 X
% 61.85/8.21
% 61.85/8.21 Lemma 49: or(or(X, Y), Z) = or(X, or(Y, Z)).
% 61.85/8.21 Proof:
% 61.85/8.21 or(or(X, Y), Z)
% 61.85/8.21 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.21 or(or(Y, X), Z)
% 61.85/8.21 = { by axiom 18 (or_commutativity) }
% 61.85/8.21 or(or(Y, Z), X)
% 61.85/8.21 = { by axiom 4 (or_symmetry) }
% 61.85/8.21 or(X, or(Y, Z))
% 61.85/8.21
% 61.85/8.21 Lemma 50: sum(X, Y, not(n0)) = not(xor(X, Y)).
% 61.85/8.21 Proof:
% 61.85/8.21 sum(X, Y, not(n0))
% 61.85/8.21 = { by axiom 16 (sum_definition) }
% 61.85/8.21 xor(xor(X, Y), not(n0))
% 61.85/8.21 = { by lemma 33 }
% 61.85/8.21 xor(xor(Y, X), not(n0))
% 61.85/8.21 = { by lemma 33 }
% 61.85/8.21 xor(not(n0), xor(Y, X))
% 61.85/8.21 = { by axiom 29 (xor_definition) }
% 61.85/8.21 or(and(not(n0), not(xor(Y, X))), and(xor(Y, X), not(not(n0))))
% 61.85/8.21 = { by lemma 36 }
% 61.85/8.21 or(not(xor(Y, X)), and(xor(Y, X), not(not(n0))))
% 61.85/8.21 = { by axiom 2 (not_definition1) }
% 61.85/8.21 or(not(xor(Y, X)), and(xor(Y, X), not(n1)))
% 61.85/8.21 = { by lemma 35 }
% 61.85/8.21 or(not(xor(Y, X)), not(n1))
% 61.85/8.21 = { by lemma 37 }
% 61.85/8.21 not(xor(Y, X))
% 61.85/8.21 = { by lemma 33 R->L }
% 61.85/8.22 not(xor(X, Y))
% 61.85/8.22
% 61.85/8.22 Lemma 51: and(not(X), or(X, Y)) = and(Y, not(X)).
% 61.85/8.22 Proof:
% 61.85/8.22 and(not(X), or(X, Y))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 and(not(X), or(Y, X))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 and(or(Y, X), not(X))
% 61.85/8.22 = { by axiom 28 (and_or_simplification) }
% 61.85/8.22 or(and(Y, not(X)), and(X, not(X)))
% 61.85/8.22 = { by axiom 11 (and_not_evaluation1) }
% 61.85/8.22 or(and(Y, not(X)), n0)
% 61.85/8.22 = { by axiom 1 (not_definition2) R->L }
% 61.85/8.22 or(and(Y, not(X)), not(n1))
% 61.85/8.22 = { by lemma 37 }
% 61.85/8.22 and(Y, not(X))
% 61.85/8.22
% 61.85/8.22 Lemma 52: and(X, or(Y, not(X))) = and(X, Y).
% 61.85/8.22 Proof:
% 61.85/8.22 and(X, or(Y, not(X)))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 and(X, or(not(X), Y))
% 61.85/8.22 = { by axiom 3 (not_involution) R->L }
% 61.85/8.22 and(not(not(X)), or(not(X), Y))
% 61.85/8.22 = { by lemma 51 }
% 61.85/8.22 and(Y, not(not(X)))
% 61.85/8.22 = { by axiom 3 (not_involution) }
% 61.85/8.22 and(Y, X)
% 61.85/8.22 = { by axiom 8 (and_symmetry) }
% 61.85/8.22 and(X, Y)
% 61.85/8.22
% 61.85/8.22 Lemma 53: and(and(X, Y), not(X)) = not(n1).
% 61.85/8.22 Proof:
% 61.85/8.22 and(and(X, Y), not(X))
% 61.85/8.22 = { by axiom 25 (and_not_evaluation3) }
% 61.85/8.22 n0
% 61.85/8.22 = { by axiom 1 (not_definition2) R->L }
% 61.85/8.22 not(n1)
% 61.85/8.22
% 61.85/8.22 Lemma 54: and(X, not(and(X, Y))) = xor(and(X, Y), X).
% 61.85/8.22 Proof:
% 61.85/8.22 and(X, not(and(X, Y)))
% 61.85/8.22 = { by lemma 38 R->L }
% 61.85/8.22 or(not(n1), and(X, not(and(X, Y))))
% 61.85/8.22 = { by lemma 53 R->L }
% 61.85/8.22 or(and(and(X, Y), not(X)), and(X, not(and(X, Y))))
% 61.85/8.22 = { by axiom 29 (xor_definition) R->L }
% 61.85/8.22 xor(and(X, Y), X)
% 61.85/8.22
% 61.85/8.22 Lemma 55: and(or(X, Y), not(Y)) = xor(or(X, Y), Y).
% 61.85/8.22 Proof:
% 61.85/8.22 and(or(X, Y), not(Y))
% 61.85/8.22 = { by lemma 38 R->L }
% 61.85/8.22 or(not(n1), and(or(X, Y), not(Y)))
% 61.85/8.22 = { by axiom 19 (or_not_evaluation2) R->L }
% 61.85/8.22 or(not(or(or(X, Y), not(Y))), and(or(X, Y), not(Y)))
% 61.85/8.22 = { by axiom 12 (demorgan2) }
% 61.85/8.22 or(and(not(or(X, Y)), not(not(Y))), and(or(X, Y), not(Y)))
% 61.85/8.22 = { by axiom 3 (not_involution) }
% 61.85/8.22 or(and(not(or(X, Y)), Y), and(or(X, Y), not(Y)))
% 61.85/8.22 = { by axiom 8 (and_symmetry) }
% 61.85/8.22 or(and(Y, not(or(X, Y))), and(or(X, Y), not(Y)))
% 61.85/8.22 = { by axiom 29 (xor_definition) R->L }
% 61.85/8.22 xor(Y, or(X, Y))
% 61.85/8.22 = { by lemma 33 R->L }
% 61.85/8.22 xor(or(X, Y), Y)
% 61.85/8.22
% 61.85/8.22 Lemma 56: or(X, and(Y, not(X))) = or(Y, X).
% 61.85/8.22 Proof:
% 61.85/8.22 or(X, and(Y, not(X)))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 or(and(Y, not(X)), X)
% 61.85/8.22 = { by axiom 22 (karnaugh1) }
% 61.85/8.22 or(Y, X)
% 61.85/8.22
% 61.85/8.22 Lemma 57: or(X, and(not(X), Y)) = or(X, Y).
% 61.85/8.22 Proof:
% 61.85/8.22 or(X, and(not(X), Y))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 or(X, and(Y, not(X)))
% 61.85/8.22 = { by lemma 56 }
% 61.85/8.22 or(Y, X)
% 61.85/8.22 = { by axiom 4 (or_symmetry) }
% 61.85/8.22 or(X, Y)
% 61.85/8.22
% 61.85/8.22 Lemma 58: or(X, not(or(Y, X))) = xor(X, not(or(Y, X))).
% 61.85/8.22 Proof:
% 61.85/8.22 or(X, not(or(Y, X)))
% 61.85/8.22 = { by lemma 56 R->L }
% 61.85/8.22 or(not(or(Y, X)), and(X, not(not(or(Y, X)))))
% 61.85/8.22 = { by axiom 17 (or_evaluation1) R->L }
% 61.85/8.22 or(not(or(or(Y, X), X)), and(X, not(not(or(Y, X)))))
% 61.85/8.22 = { by axiom 12 (demorgan2) }
% 61.85/8.22 or(and(not(or(Y, X)), not(X)), and(X, not(not(or(Y, X)))))
% 61.85/8.22 = { by axiom 29 (xor_definition) R->L }
% 61.85/8.22 xor(not(or(Y, X)), X)
% 61.85/8.22 = { by lemma 33 R->L }
% 61.85/8.22 xor(X, not(or(Y, X)))
% 61.85/8.22
% 61.85/8.22 Lemma 59: or(not(X), and(X, Y)) = or(Y, not(X)).
% 61.85/8.22 Proof:
% 61.85/8.22 or(not(X), and(X, Y))
% 61.85/8.22 = { by axiom 3 (not_involution) R->L }
% 61.85/8.22 or(not(X), and(not(not(X)), Y))
% 61.85/8.22 = { by lemma 57 }
% 61.85/8.22 or(not(X), Y)
% 61.85/8.22 = { by axiom 4 (or_symmetry) }
% 61.85/8.22 or(Y, not(X))
% 61.85/8.22
% 61.85/8.22 Lemma 60: or(not(X), and(Y, X)) = or(Y, not(X)).
% 61.85/8.22 Proof:
% 61.85/8.22 or(not(X), and(Y, X))
% 61.85/8.22 = { by axiom 3 (not_involution) R->L }
% 61.85/8.22 or(not(X), and(Y, not(not(X))))
% 61.85/8.22 = { by lemma 56 }
% 61.85/8.22 or(Y, not(X))
% 61.85/8.22
% 61.85/8.22 Lemma 61: or(and(X, Y), not(X)) = xor(Y, not(or(X, Y))).
% 61.85/8.22 Proof:
% 61.85/8.22 or(and(X, Y), not(X))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 or(not(X), and(X, Y))
% 61.85/8.22 = { by axiom 3 (not_involution) R->L }
% 61.85/8.22 or(not(X), not(not(and(X, Y))))
% 61.85/8.22 = { by axiom 13 (demorgan1) R->L }
% 61.85/8.22 not(and(X, not(and(X, Y))))
% 61.85/8.22 = { by lemma 54 }
% 61.85/8.22 not(xor(and(X, Y), X))
% 61.85/8.22 = { by lemma 50 R->L }
% 61.85/8.22 sum(and(X, Y), X, not(n0))
% 61.85/8.22 = { by axiom 16 (sum_definition) }
% 61.85/8.22 xor(xor(and(X, Y), X), not(n0))
% 61.85/8.22 = { by lemma 54 R->L }
% 61.85/8.22 xor(and(X, not(and(X, Y))), not(n0))
% 61.85/8.22 = { by axiom 3 (not_involution) R->L }
% 61.85/8.22 xor(and(not(not(X)), not(and(X, Y))), not(n0))
% 61.85/8.22 = { by axiom 13 (demorgan1) }
% 61.85/8.22 xor(and(not(not(X)), or(not(X), not(Y))), not(n0))
% 61.85/8.22 = { by lemma 51 }
% 61.85/8.22 xor(and(not(Y), not(not(X))), not(n0))
% 61.85/8.22 = { by axiom 12 (demorgan2) R->L }
% 61.85/8.22 xor(not(or(Y, not(X))), not(n0))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 xor(not(or(not(X), Y)), not(n0))
% 61.85/8.22 = { by lemma 56 R->L }
% 61.85/8.22 xor(not(or(Y, and(not(X), not(Y)))), not(n0))
% 61.85/8.22 = { by axiom 12 (demorgan2) R->L }
% 61.85/8.22 xor(not(or(Y, not(or(X, Y)))), not(n0))
% 61.85/8.22 = { by axiom 12 (demorgan2) }
% 61.85/8.22 xor(and(not(Y), not(not(or(X, Y)))), not(n0))
% 61.85/8.22 = { by axiom 3 (not_involution) }
% 61.85/8.22 xor(and(not(Y), or(X, Y)), not(n0))
% 61.85/8.22 = { by axiom 8 (and_symmetry) }
% 61.85/8.22 xor(and(or(X, Y), not(Y)), not(n0))
% 61.85/8.22 = { by lemma 55 }
% 61.85/8.22 xor(xor(or(X, Y), Y), not(n0))
% 61.85/8.22 = { by axiom 16 (sum_definition) R->L }
% 61.85/8.22 sum(or(X, Y), Y, not(n0))
% 61.85/8.22 = { by lemma 50 }
% 61.85/8.22 not(xor(or(X, Y), Y))
% 61.85/8.22 = { by lemma 55 R->L }
% 61.85/8.22 not(and(or(X, Y), not(Y)))
% 61.85/8.22 = { by axiom 13 (demorgan1) }
% 61.85/8.22 or(not(or(X, Y)), not(not(Y)))
% 61.85/8.22 = { by axiom 3 (not_involution) }
% 61.85/8.22 or(not(or(X, Y)), Y)
% 61.85/8.22 = { by axiom 4 (or_symmetry) }
% 61.85/8.22 or(Y, not(or(X, Y)))
% 61.85/8.22 = { by lemma 58 }
% 61.85/8.22 xor(Y, not(or(X, Y)))
% 61.85/8.22
% 61.85/8.22 Lemma 62: xor(X, not(or(Y, X))) = xor(Y, not(and(Y, X))).
% 61.85/8.22 Proof:
% 61.85/8.22 xor(X, not(or(Y, X)))
% 61.85/8.22 = { by lemma 61 R->L }
% 61.85/8.22 or(and(Y, X), not(Y))
% 61.85/8.22 = { by axiom 3 (not_involution) R->L }
% 61.85/8.22 or(not(not(and(Y, X))), not(Y))
% 61.85/8.22 = { by lemma 59 R->L }
% 61.85/8.22 or(not(Y), and(Y, not(not(and(Y, X)))))
% 61.85/8.22 = { by lemma 48 R->L }
% 61.85/8.22 or(not(or(and(Y, X), Y)), and(Y, not(not(and(Y, X)))))
% 61.85/8.22 = { by axiom 12 (demorgan2) }
% 61.85/8.22 or(and(not(and(Y, X)), not(Y)), and(Y, not(not(and(Y, X)))))
% 61.85/8.22 = { by axiom 29 (xor_definition) R->L }
% 61.85/8.22 xor(not(and(Y, X)), Y)
% 61.85/8.22 = { by lemma 33 R->L }
% 61.85/8.22 xor(Y, not(and(Y, X)))
% 61.85/8.22
% 61.85/8.22 Lemma 63: or(and(X, Y), and(Z, X)) = and(X, or(Y, Z)).
% 61.85/8.22 Proof:
% 61.85/8.22 or(and(X, Y), and(Z, X))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 or(and(Y, X), and(Z, X))
% 61.85/8.22 = { by axiom 28 (and_or_simplification) R->L }
% 61.85/8.22 and(or(Y, Z), X)
% 61.85/8.22 = { by axiom 8 (and_symmetry) }
% 61.85/8.22 and(X, or(Y, Z))
% 61.85/8.22
% 61.85/8.22 Lemma 64: and(X, or(Y, and(X, Z))) = and(X, or(Z, Y)).
% 61.85/8.22 Proof:
% 61.85/8.22 and(X, or(Y, and(X, Z)))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 and(X, or(Y, and(Z, X)))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 and(X, or(and(Z, X), Y))
% 61.85/8.22 = { by lemma 63 R->L }
% 61.85/8.22 or(and(X, and(Z, X)), and(Y, X))
% 61.85/8.22 = { by lemma 40 }
% 61.85/8.22 or(and(Z, X), and(Y, X))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 or(and(X, Z), and(Y, X))
% 61.85/8.22 = { by lemma 63 }
% 61.85/8.22 and(X, or(Z, Y))
% 61.85/8.22
% 61.85/8.22 Lemma 65: or(X, or(Y, and(X, Z))) = or(X, Y).
% 61.85/8.22 Proof:
% 61.85/8.22 or(X, or(Y, and(X, Z)))
% 61.85/8.22 = { by lemma 49 R->L }
% 61.85/8.22 or(or(X, Y), and(X, Z))
% 61.85/8.22 = { by axiom 18 (or_commutativity) R->L }
% 61.85/8.22 or(or(X, and(X, Z)), Y)
% 61.85/8.22 = { by lemma 45 }
% 61.85/8.22 or(X, Y)
% 61.85/8.22
% 61.85/8.22 Lemma 66: or(X, or(and(Y, X), Z)) = or(Z, X).
% 61.85/8.22 Proof:
% 61.85/8.22 or(X, or(and(Y, X), Z))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 or(or(and(Y, X), Z), X)
% 61.85/8.22 = { by axiom 31 (and_or_subsumption3) }
% 61.85/8.22 or(Z, X)
% 61.85/8.22
% 61.85/8.22 Lemma 67: and(or(and(X, Y), Z), or(Z, X)) = or(and(X, Y), Z).
% 61.85/8.22 Proof:
% 61.85/8.22 and(or(and(X, Y), Z), or(Z, X))
% 61.85/8.22 = { by lemma 48 R->L }
% 61.85/8.22 and(or(and(X, Y), Z), or(Z, or(and(X, Y), X)))
% 61.85/8.22 = { by lemma 47 }
% 61.85/8.22 and(or(and(X, Y), Z), or(X, or(and(X, Y), Z)))
% 61.85/8.22 = { by axiom 4 (or_symmetry) }
% 61.85/8.22 and(or(and(X, Y), Z), or(or(and(X, Y), Z), X))
% 61.85/8.22 = { by lemma 43 }
% 61.85/8.22 or(and(X, Y), Z)
% 61.85/8.22
% 61.85/8.22 Lemma 68: or(X, and(and(and(Y, Z), or(W, V)), V)) = or(carryout(X, V, carryout(Y, Z, n0)), X).
% 61.85/8.22 Proof:
% 61.85/8.22 or(X, and(and(and(Y, Z), or(W, V)), V))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 or(X, and(V, and(and(Y, Z), or(W, V))))
% 61.85/8.22 = { by lemma 41 R->L }
% 61.85/8.22 or(X, and(and(Y, Z), and(or(W, V), V)))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 or(X, and(and(Y, Z), and(V, or(W, V))))
% 61.85/8.22 = { by lemma 44 }
% 61.85/8.22 or(X, and(and(Y, Z), V))
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 or(X, and(V, and(Y, Z)))
% 61.85/8.22 = { by lemma 39 R->L }
% 61.85/8.22 or(X, and(V, carryout(Y, Z, n0)))
% 61.85/8.22 = { by lemma 57 R->L }
% 61.85/8.22 or(X, and(not(X), and(V, carryout(Y, Z, n0))))
% 61.85/8.22 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.22 or(and(not(X), and(V, carryout(Y, Z, n0))), X)
% 61.85/8.22 = { by lemma 66 R->L }
% 61.85/8.22 or(X, or(and(or(V, carryout(Y, Z, n0)), X), and(not(X), and(V, carryout(Y, Z, n0)))))
% 61.85/8.22 = { by axiom 8 (and_symmetry) }
% 61.85/8.22 or(X, or(and(X, or(V, carryout(Y, Z, n0))), and(not(X), and(V, carryout(Y, Z, n0)))))
% 61.85/8.22 = { by axiom 32 (carryout_definition) R->L }
% 61.85/8.22 or(X, carryout(X, V, carryout(Y, Z, n0)))
% 61.85/8.22 = { by axiom 4 (or_symmetry) }
% 61.85/8.22 or(carryout(X, V, carryout(Y, Z, n0)), X)
% 61.85/8.22
% 61.85/8.22 Lemma 69: and(or(and(X, Y), and(and(Z, W), or(X, V))), X) = and(carryout(X, Y, carryout(Z, W, n0)), X).
% 61.85/8.22 Proof:
% 61.85/8.22 and(or(and(X, Y), and(and(Z, W), or(X, V))), X)
% 61.85/8.22 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.22 and(X, or(and(X, Y), and(and(Z, W), or(X, V))))
% 61.85/8.23 = { by lemma 52 R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), not(X)))
% 61.85/8.23 = { by lemma 36 R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), and(not(n0), not(X))))
% 61.85/8.23 = { by axiom 2 (not_definition1) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), and(n1, not(X))))
% 61.85/8.23 = { by axiom 6 (or_not_evaluation1) R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), and(or(not(and(X, Y)), not(not(and(X, Y)))), not(X))))
% 61.85/8.23 = { by axiom 28 (and_or_simplification) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), not(X)), and(not(not(and(X, Y))), not(X)))))
% 61.85/8.23 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), not(X)), and(not(X), not(not(and(X, Y)))))))
% 61.85/8.23 = { by lemma 40 R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), not(X)), and(not(not(and(X, Y))), and(not(X), not(not(and(X, Y))))))))
% 61.85/8.23 = { by axiom 8 (and_symmetry) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), not(X)), and(not(not(and(X, Y))), and(not(not(and(X, Y))), not(X))))))
% 61.85/8.23 = { by lemma 52 R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), or(not(X), not(not(and(X, Y))))), and(not(not(and(X, Y))), and(not(not(and(X, Y))), not(X))))))
% 61.85/8.23 = { by axiom 4 (or_symmetry) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), or(not(not(and(X, Y))), not(X))), and(not(not(and(X, Y))), and(not(not(and(X, Y))), not(X))))))
% 61.85/8.23 = { by axiom 32 (carryout_definition) R->L }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), carryout(not(and(X, Y)), not(not(and(X, Y))), not(X))))
% 61.85/8.23 = { by axiom 3 (not_involution) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), carryout(not(and(X, Y)), and(X, Y), not(X))))
% 61.85/8.23 = { by axiom 32 (carryout_definition) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), or(and(X, Y), not(X))), and(not(not(and(X, Y))), and(and(X, Y), not(X))))))
% 61.85/8.23 = { by lemma 53 }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), or(and(X, Y), not(X))), and(not(not(and(X, Y))), not(n1)))))
% 61.85/8.23 = { by lemma 61 }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), xor(Y, not(or(X, Y)))), and(not(not(and(X, Y))), not(n1)))))
% 61.85/8.23 = { by lemma 35 }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(and(not(and(X, Y)), xor(Y, not(or(X, Y)))), not(n1))))
% 61.85/8.23 = { by lemma 37 }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), and(not(and(X, Y)), xor(Y, not(or(X, Y))))))
% 61.85/8.23 = { by lemma 62 }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), and(not(and(X, Y)), xor(X, not(and(X, Y))))))
% 61.85/8.23 = { by axiom 8 (and_symmetry) }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), and(xor(X, not(and(X, Y))), not(and(X, Y)))))
% 61.85/8.23 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.23 and(X, or(and(xor(X, not(and(X, Y))), not(and(X, Y))), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by lemma 47 R->L }
% 61.85/8.23 and(X, or(and(and(Z, W), or(X, V)), or(and(X, Y), and(xor(X, not(and(X, Y))), not(and(X, Y))))))
% 61.85/8.23 = { by lemma 56 }
% 61.85/8.23 and(X, or(and(and(Z, W), or(X, V)), or(xor(X, not(and(X, Y))), and(X, Y))))
% 61.85/8.23 = { by lemma 46 R->L }
% 61.85/8.23 and(X, or(xor(X, not(and(X, Y))), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by lemma 62 R->L }
% 61.85/8.23 and(X, or(xor(Y, not(or(X, Y))), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by lemma 58 R->L }
% 61.85/8.23 and(X, or(or(Y, not(or(X, Y))), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by axiom 12 (demorgan2) }
% 61.85/8.23 and(X, or(or(Y, and(not(X), not(Y))), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by lemma 56 }
% 61.85/8.23 and(X, or(or(not(X), Y), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by axiom 4 (or_symmetry) }
% 61.85/8.23 and(X, or(or(Y, not(X)), or(and(X, Y), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by lemma 49 }
% 61.85/8.23 and(X, or(Y, or(not(X), or(and(X, Y), and(and(Z, W), or(X, V))))))
% 61.85/8.23 = { by lemma 46 }
% 61.85/8.23 and(X, or(or(and(X, Y), and(and(Z, W), or(X, V))), or(Y, not(X))))
% 61.85/8.23 = { by lemma 49 R->L }
% 61.85/8.23 and(X, or(or(or(and(X, Y), and(and(Z, W), or(X, V))), Y), not(X)))
% 61.85/8.23 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.23 and(X, or(or(Y, or(and(X, Y), and(and(Z, W), or(X, V)))), not(X)))
% 61.85/8.23 = { by axiom 4 (or_symmetry) }
% 61.85/8.23 and(X, or(or(Y, or(and(and(Z, W), or(X, V)), and(X, Y))), not(X)))
% 61.85/8.23 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.23 and(X, or(or(or(and(and(Z, W), or(X, V)), and(X, Y)), Y), not(X)))
% 61.85/8.23 = { by axiom 30 (and_or_subsumption4) }
% 61.85/8.23 and(X, or(or(and(and(Z, W), or(X, V)), Y), not(X)))
% 61.85/8.23 = { by lemma 49 }
% 61.85/8.23 and(X, or(and(and(Z, W), or(X, V)), or(Y, not(X))))
% 61.85/8.23 = { by lemma 46 R->L }
% 61.85/8.23 and(X, or(Y, or(not(X), and(and(Z, W), or(X, V)))))
% 61.85/8.23 = { by axiom 4 (or_symmetry) }
% 61.85/8.24 and(X, or(Y, or(and(and(Z, W), or(X, V)), not(X))))
% 61.85/8.24 = { by lemma 60 R->L }
% 61.85/8.24 and(X, or(Y, or(not(X), and(and(and(Z, W), or(X, V)), X))))
% 61.85/8.24 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.24 and(X, or(Y, or(not(X), and(X, and(and(Z, W), or(X, V))))))
% 61.85/8.24 = { by lemma 41 R->L }
% 61.85/8.24 and(X, or(Y, or(not(X), and(and(Z, W), and(or(X, V), X)))))
% 61.85/8.24 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.24 and(X, or(Y, or(not(X), and(and(Z, W), and(X, or(X, V))))))
% 61.85/8.24 = { by lemma 43 }
% 61.85/8.24 and(X, or(Y, or(not(X), and(and(Z, W), X))))
% 61.85/8.24 = { by lemma 60 }
% 61.85/8.24 and(X, or(Y, or(and(Z, W), not(X))))
% 61.85/8.24 = { by lemma 49 R->L }
% 61.85/8.24 and(X, or(or(Y, and(Z, W)), not(X)))
% 61.85/8.24 = { by lemma 59 R->L }
% 61.85/8.24 and(X, or(not(X), and(X, or(Y, and(Z, W)))))
% 61.85/8.24 = { by lemma 65 R->L }
% 61.85/8.24 and(X, or(not(X), or(and(X, or(Y, and(Z, W))), and(not(X), and(Y, and(Z, W))))))
% 61.85/8.24 = { by axiom 32 (carryout_definition) R->L }
% 61.85/8.24 and(X, or(not(X), carryout(X, Y, and(Z, W))))
% 61.85/8.24 = { by lemma 39 R->L }
% 61.85/8.24 and(X, or(not(X), carryout(X, Y, carryout(Z, W, n0))))
% 61.85/8.24 = { by axiom 4 (or_symmetry) }
% 61.85/8.24 and(X, or(carryout(X, Y, carryout(Z, W, n0)), not(X)))
% 61.85/8.24 = { by lemma 52 }
% 61.85/8.24 and(X, carryout(X, Y, carryout(Z, W, n0)))
% 61.85/8.24 = { by axiom 8 (and_symmetry) }
% 61.85/8.24 and(carryout(X, Y, carryout(Z, W, n0)), X)
% 61.85/8.24
% 61.85/8.24 Lemma 70: or(and(and(X, Y), or(Z, W)), or(carryout(V, W, carryout(X, Y, n0)), V)) = or(and(and(X, Y), or(Z, W)), V).
% 61.85/8.24 Proof:
% 61.85/8.24 or(and(and(X, Y), or(Z, W)), or(carryout(V, W, carryout(X, Y, n0)), V))
% 61.85/8.24 = { by lemma 68 R->L }
% 61.85/8.24 or(and(and(X, Y), or(Z, W)), or(V, and(and(and(X, Y), or(Z, W)), W)))
% 61.85/8.24 = { by lemma 65 }
% 61.85/8.24 or(and(and(X, Y), or(Z, W)), V)
% 61.85/8.24
% 61.85/8.24 Goal 1 (prove_circuit): circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), or(and(a1, b1), and(and(a0, b0), or(a1, b1)))) = true.
% 61.85/8.24 Proof:
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), or(and(a1, b1), and(and(a0, b0), or(a1, b1))))
% 61.85/8.24 = { by lemma 67 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(and(and(a0, b0), or(a1, b1)), a1)))
% 61.85/8.24 = { by lemma 70 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(and(and(a0, b0), or(a1, b1)), or(carryout(a1, b1, carryout(a0, b0, n0)), a1))))
% 61.85/8.24 = { by lemma 46 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(carryout(a1, b1, carryout(a0, b0, n0)), or(a1, and(and(a0, b0), or(a1, b1))))))
% 61.85/8.24 = { by lemma 49 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(or(carryout(a1, b1, carryout(a0, b0, n0)), a1), and(and(a0, b0), or(a1, b1)))))
% 61.85/8.24 = { by lemma 40 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(or(carryout(a1, b1, carryout(a0, b0, n0)), a1), and(or(a1, b1), and(and(a0, b0), or(a1, b1))))))
% 61.85/8.24 = { by axiom 8 (and_symmetry) }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(or(carryout(a1, b1, carryout(a0, b0, n0)), a1), and(and(and(a0, b0), or(a1, b1)), or(a1, b1)))))
% 61.85/8.24 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(or(carryout(a1, b1, carryout(a0, b0, n0)), a1), and(and(and(a0, b0), or(a1, b1)), or(b1, a1)))))
% 61.85/8.24 = { by lemma 64 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(or(carryout(a1, b1, carryout(a0, b0, n0)), a1), and(and(and(a0, b0), or(a1, b1)), or(a1, and(and(and(a0, b0), or(a1, b1)), b1))))))
% 61.85/8.24 = { by lemma 68 }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(or(carryout(a1, b1, carryout(a0, b0, n0)), a1), and(and(and(a0, b0), or(a1, b1)), or(carryout(a1, b1, carryout(a0, b0, n0)), a1)))))
% 61.85/8.24 = { by lemma 42 }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(carryout(a1, b1, carryout(a0, b0, n0)), a1)))
% 61.85/8.24 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(a1, carryout(a1, b1, carryout(a0, b0, n0)))))
% 61.85/8.24 = { by lemma 64 R->L }
% 61.85/8.24 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(carryout(a1, b1, carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), a1))))
% 61.85/8.24 = { by lemma 69 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(carryout(a1, b1, carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), a1))))
% 61.85/8.25 = { by lemma 45 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), carryout(a1, b1, carryout(a0, b0, n0))))
% 61.85/8.25 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(a1, b1), and(and(a0, b0), or(a1, b1)))))
% 61.85/8.25 = { by lemma 67 R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), or(and(and(a0, b0), or(a1, b1)), a1))))
% 61.85/8.25 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), and(or(and(and(a0, b0), or(a1, b1)), a1), or(and(a1, b1), and(and(a0, b0), or(a1, b1))))))
% 61.85/8.25 = { by axiom 28 (and_or_simplification) }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(and(a0, b0), or(a1, b1)), or(and(a1, b1), and(and(a0, b0), or(a1, b1)))), and(a1, or(and(a1, b1), and(and(a0, b0), or(a1, b1)))))))
% 61.85/8.25 = { by lemma 44 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(a1, or(and(a1, b1), and(and(a0, b0), or(a1, b1)))))))
% 61.85/8.25 = { by axiom 8 (and_symmetry) }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(or(and(a1, b1), and(and(a0, b0), or(a1, b1))), a1))))
% 61.85/8.25 = { by lemma 69 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(carryout(a1, b1, carryout(a0, b0, n0)), a1))))
% 61.85/8.25 = { by axiom 8 (and_symmetry) R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(a1, carryout(a1, b1, carryout(a0, b0, n0))))))
% 61.85/8.25 = { by axiom 4 (or_symmetry) R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(a1, carryout(a1, b1, carryout(a0, b0, n0))), and(and(a0, b0), or(a1, b1)))))
% 61.85/8.25 = { by lemma 66 R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), or(and(carryout(a1, b1, carryout(a0, b0, n0)), and(and(a0, b0), or(a1, b1))), and(a1, carryout(a1, b1, carryout(a0, b0, n0)))))))
% 61.85/8.25 = { by lemma 63 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), a1)))))
% 61.85/8.25 = { by lemma 70 R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), or(carryout(a1, b1, carryout(a0, b0, n0)), a1))))))
% 61.85/8.25 = { by lemma 46 R->L }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(carryout(a1, b1, carryout(a0, b0, n0)), or(a1, and(and(a0, b0), or(a1, b1))))))))
% 61.85/8.25 = { by lemma 43 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), and(carryout(a1, b1, carryout(a0, b0, n0)), or(and(and(a0, b0), or(a1, b1)), carryout(a1, b1, carryout(a0, b0, n0)))))
% 61.85/8.25 = { by lemma 44 }
% 61.85/8.25 circuit(xor(a0, b0), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by lemma 38 R->L }
% 61.85/8.25 circuit(or(not(n1), xor(a0, b0)), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by lemma 56 R->L }
% 61.85/8.25 circuit(or(xor(a0, b0), and(not(n1), not(xor(a0, b0)))), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by lemma 34 R->L }
% 61.85/8.25 circuit(or(and(xor(a0, b0), not(n0)), and(not(n1), not(xor(a0, b0)))), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by axiom 1 (not_definition2) R->L }
% 61.85/8.25 circuit(or(and(xor(a0, b0), not(not(n1))), and(not(n1), not(xor(a0, b0)))), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by axiom 29 (xor_definition) R->L }
% 61.85/8.25 circuit(xor(xor(a0, b0), not(n1)), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by axiom 16 (sum_definition) R->L }
% 61.85/8.25 circuit(sum(a0, b0, not(n1)), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by axiom 1 (not_definition2) }
% 61.85/8.25 circuit(sum(a0, b0, n0), xor(xor(a1, b1), carryout(a0, b0, n0)), carryout(a1, b1, carryout(a0, b0, n0)))
% 61.85/8.25 = { by axiom 27 (overflow_definition) R->L }
% 61.85/8.25 circuit(sum(a0, b0, n0), xor(xor(a1, b1), carryout(a0, b0, n0)), overflow)
% 61.85/8.25 = { by axiom 16 (sum_definition) R->L }
% 61.85/8.25 circuit(sum(a0, b0, n0), sum(a1, b1, carryout(a0, b0, n0)), overflow)
% 61.85/8.25 = { by axiom 26 (s1_definition) R->L }
% 61.85/8.25 circuit(sum(a0, b0, n0), s1, overflow)
% 61.85/8.25 = { by axiom 15 (s0_definition) R->L }
% 61.85/8.25 circuit(s0, s1, overflow)
% 61.85/8.25 = { by axiom 14 (the_output_circuit) }
% 61.85/8.25 true
% 61.85/8.25 % SZS output end Proof
% 61.85/8.25
% 61.85/8.25 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------