%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : BOO039-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 09:35:39 AM UTC 2026
% Result : Unsatisfiable 173.79s 22.18s
% Output : Proof 176.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO039-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.16 % Computer : n009.cluster.edu
% 0.11/0.16 % Model : x86_64 x86_64
% 0.11/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.16 % Memory : 8046.5625MB
% 0.11/0.16 % OS : Linux 6.8.0-71-generic
% 0.11/0.16 % CPULimit : 300
% 0.11/0.16 % WCLimit : 300
% 0.11/0.16 % DateTime : Mon Sep 28 21:05:14 UTC 2026
% 0.11/0.17 % CPUTime :
% 0.11/0.17 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 173.79/22.18 Command-line arguments: --no-flatten-goal
% 173.79/22.18
% 173.79/22.18 % SZS status Unsatisfiable
% 173.79/22.18
% 175.93/22.43 % SZS output start Proof
% 175.93/22.43 Axiom 1 (sh_1): nand(nand(X, nand(nand(Y, X), X)), nand(Y, nand(Z, X))) = Y.
% 175.93/22.43
% 175.93/22.43 Lemma 2: nand(nand(nand(X, nand(Y, Z)), nand(nand(W, nand(X, nand(Y, Z))), nand(X, nand(Y, Z)))), nand(W, X)) = W.
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(nand(X, nand(Y, Z)), nand(nand(W, nand(X, nand(Y, Z))), nand(X, nand(Y, Z)))), nand(W, X))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(nand(X, nand(Y, Z)), nand(nand(W, nand(X, nand(Y, Z))), nand(X, nand(Y, Z)))), nand(W, nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(Y, Z)))))
% 175.93/22.43 = { by axiom 1 (sh_1) }
% 175.93/22.43 W
% 175.93/22.43
% 175.93/22.43 Lemma 3: nand(nand(X, nand(nand(Y, X), X)), nand(Y, nand(Z, nand(nand(X, Z), Z)))) = Y.
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(X, nand(nand(Y, X), X)), nand(Y, nand(Z, nand(nand(X, Z), Z))))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(X, nand(nand(Y, nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(W, Z)))), X)), nand(Y, nand(Z, nand(nand(X, Z), Z))))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(X, nand(nand(Y, nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(W, Z)))), nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(W, Z))))), nand(Y, nand(Z, nand(nand(X, Z), Z))))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(W, Z))), nand(nand(Y, nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(W, Z)))), nand(nand(Z, nand(nand(X, Z), Z)), nand(X, nand(W, Z))))), nand(Y, nand(Z, nand(nand(X, Z), Z))))
% 175.93/22.43 = { by lemma 2 }
% 175.93/22.43 Y
% 175.93/22.43
% 175.93/22.43 Lemma 4: nand(nand(X, nand(nand(nand(Y, nand(nand(Y, Y), Y)), X), X)), Y) = nand(Y, nand(nand(Y, Y), Y)).
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(X, nand(nand(nand(Y, nand(nand(Y, Y), Y)), X), X)), Y)
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(X, nand(nand(nand(Y, nand(nand(Y, Y), Y)), X), X)), nand(nand(Y, nand(nand(Y, Y), Y)), nand(Y, nand(nand(X, Y), Y))))
% 175.93/22.43 = { by lemma 3 }
% 175.93/22.43 nand(Y, nand(nand(Y, Y), Y))
% 175.93/22.43
% 175.93/22.43 Lemma 5: nand(X, nand(nand(X, X), X)) = nand(X, X).
% 175.93/22.43 Proof:
% 175.93/22.43 nand(X, nand(nand(X, X), X))
% 175.93/22.43 = { by lemma 4 R->L }
% 175.93/22.43 nand(nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(X, X), X))), nand(X, nand(nand(X, X), X)))), X)
% 175.93/22.43 = { by axiom 1 (sh_1) }
% 175.93/22.43 nand(nand(nand(X, nand(nand(X, X), X)), nand(X, nand(X, nand(nand(X, X), X)))), X)
% 175.93/22.43 = { by lemma 3 }
% 175.93/22.43 nand(X, X)
% 175.93/22.43
% 175.93/22.43 Lemma 6: nand(nand(X, X), nand(X, X)) = X.
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(X, X), nand(X, X))
% 175.93/22.43 = { by lemma 5 R->L }
% 175.93/22.43 nand(nand(X, nand(nand(X, X), X)), nand(X, X))
% 175.93/22.43 = { by lemma 5 R->L }
% 175.93/22.43 nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(X, X), X)))
% 175.93/22.43 = { by axiom 1 (sh_1) }
% 175.93/22.43 X
% 175.93/22.43
% 175.93/22.43 Lemma 7: nand(nand(X, X), nand(X, nand(X, X))) = X.
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(X, X), nand(X, nand(X, X)))
% 175.93/22.43 = { by lemma 6 R->L }
% 175.93/22.43 nand(nand(X, X), nand(nand(nand(X, X), nand(X, X)), nand(X, X)))
% 175.93/22.43 = { by lemma 5 }
% 175.93/22.43 nand(nand(X, X), nand(X, X))
% 175.93/22.43 = { by lemma 6 }
% 175.93/22.43 X
% 175.93/22.43
% 175.93/22.43 Lemma 8: nand(nand(X, nand(nand(Y, X), X)), nand(Y, Y)) = Y.
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(X, nand(nand(Y, X), X)), nand(Y, Y))
% 175.93/22.43 = { by lemma 5 R->L }
% 175.93/22.43 nand(nand(X, nand(nand(Y, X), X)), nand(Y, nand(nand(Y, Y), Y)))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(X, nand(nand(nand(nand(Y, nand(nand(Y, Y), Y)), nand(Y, nand(nand(Y, Y), Y))), X), X)), nand(Y, nand(nand(Y, Y), Y)))
% 175.93/22.43 = { by lemma 5 R->L }
% 175.93/22.43 nand(nand(X, nand(nand(nand(nand(Y, nand(nand(Y, Y), Y)), nand(nand(nand(Y, nand(nand(Y, Y), Y)), nand(Y, nand(nand(Y, Y), Y))), nand(Y, nand(nand(Y, Y), Y)))), X), X)), nand(Y, nand(nand(Y, Y), Y)))
% 175.93/22.43 = { by lemma 4 }
% 175.93/22.43 nand(nand(Y, nand(nand(Y, Y), Y)), nand(nand(nand(Y, nand(nand(Y, Y), Y)), nand(Y, nand(nand(Y, Y), Y))), nand(Y, nand(nand(Y, Y), Y))))
% 175.93/22.43 = { by lemma 5 }
% 175.93/22.43 nand(nand(Y, nand(nand(Y, Y), Y)), nand(Y, nand(nand(Y, Y), Y)))
% 175.93/22.43 = { by axiom 1 (sh_1) }
% 175.93/22.43 Y
% 175.93/22.43
% 175.93/22.43 Lemma 9: nand(nand(nand(X, Y), nand(nand(Z, nand(X, Y)), nand(X, Y))), nand(Z, X)) = Z.
% 175.93/22.43 Proof:
% 175.93/22.43 nand(nand(nand(X, Y), nand(nand(Z, nand(X, Y)), nand(X, Y))), nand(Z, X))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(nand(X, Y), nand(nand(Z, nand(X, nand(nand(W, nand(nand(Y, W), W)), nand(Y, nand(V, W))))), nand(X, Y))), nand(Z, X))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(nand(X, Y), nand(nand(Z, nand(X, nand(nand(W, nand(nand(Y, W), W)), nand(Y, nand(V, W))))), nand(X, nand(nand(W, nand(nand(Y, W), W)), nand(Y, nand(V, W)))))), nand(Z, X))
% 175.93/22.43 = { by axiom 1 (sh_1) R->L }
% 175.93/22.43 nand(nand(nand(X, nand(nand(W, nand(nand(Y, W), W)), nand(Y, nand(V, W)))), nand(nand(Z, nand(X, nand(nand(W, nand(nand(Y, W), W)), nand(Y, nand(V, W))))), nand(X, nand(nand(W, nand(nand(Y, W), W)), nand(Y, nand(V, W)))))), nand(Z, X))
% 175.93/22.43 = { by lemma 2 }
% 175.93/22.43 Z
% 175.93/22.43
% 175.93/22.43 Lemma 10: nand(X, nand(nand(Y, nand(nand(X, Y), Y)), X)) = nand(Y, nand(nand(X, Y), Y)).
% 175.93/22.43 Proof:
% 175.93/22.43 nand(X, nand(nand(Y, nand(nand(X, Y), Y)), X))
% 175.93/22.44 = { by lemma 7 R->L }
% 175.93/22.44 nand(nand(nand(X, X), nand(X, nand(X, X))), nand(nand(Y, nand(nand(X, Y), Y)), X))
% 175.93/22.44 = { by lemma 8 R->L }
% 175.93/22.44 nand(nand(nand(X, X), nand(nand(nand(Y, nand(nand(X, Y), Y)), nand(X, X)), nand(X, X))), nand(nand(Y, nand(nand(X, Y), Y)), X))
% 175.93/22.44 = { by lemma 9 }
% 175.93/22.44 nand(Y, nand(nand(X, Y), Y))
% 175.93/22.44
% 175.93/22.44 Lemma 11: nand(nand(X, X), nand(X, Y)) = X.
% 175.93/22.44 Proof:
% 175.93/22.44 nand(nand(X, X), nand(X, Y))
% 175.93/22.44 = { by lemma 7 R->L }
% 175.93/22.44 nand(nand(nand(nand(X, X), nand(X, X)), nand(nand(X, X), nand(nand(X, X), nand(X, X)))), nand(X, Y))
% 175.93/22.44 = { by lemma 8 R->L }
% 175.93/22.44 nand(nand(nand(nand(X, X), nand(X, X)), nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, X), nand(X, X))), nand(nand(X, X), nand(X, X)))), nand(X, Y))
% 175.93/22.44 = { by lemma 10 R->L }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(nand(nand(X, X), nand(X, X)), nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, X), nand(X, X))), nand(nand(X, X), nand(X, X)))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 8 }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(nand(nand(X, X), nand(X, X)), nand(nand(X, X), nand(nand(X, X), nand(X, X)))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 7 }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, X), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 5 R->L }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, nand(nand(X, X), X)), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by axiom 1 (sh_1) R->L }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(X, X), X))), nand(X, nand(nand(X, X), X)))), nand(nand(X, nand(nand(X, X), X)), nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(X, nand(nand(X, X), X))))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 5 }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(X, X), X))), nand(nand(X, nand(nand(X, X), X)), nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(X, nand(nand(X, X), X))))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by axiom 1 (sh_1) }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, nand(nand(X, nand(nand(X, X), X)), nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(X, nand(nand(X, X), X))))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 5 }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, nand(nand(X, nand(nand(X, X), X)), nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(X, X)))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 5 }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, nand(nand(X, X), nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(X, X)))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 10 }
% 175.93/22.44 nand(nand(nand(Y, nand(nand(nand(X, X), Y), Y)), nand(nand(X, nand(Y, nand(nand(nand(X, X), Y), Y))), nand(Y, nand(nand(nand(X, X), Y), Y)))), nand(X, Y))
% 175.93/22.44 = { by lemma 2 }
% 175.93/22.44 X
% 175.93/22.44
% 175.93/22.44 Lemma 12: nand(nand(nand(X, Y), nand(nand(nand(Y, nand(nand(Z, Y), Y)), nand(X, Y)), nand(X, Y))), Z) = nand(Y, nand(nand(Z, Y), Y)).
% 175.93/22.44 Proof:
% 175.93/22.44 nand(nand(nand(X, Y), nand(nand(nand(Y, nand(nand(Z, Y), Y)), nand(X, Y)), nand(X, Y))), Z)
% 175.93/22.44 = { by axiom 1 (sh_1) R->L }
% 175.93/22.44 nand(nand(nand(X, Y), nand(nand(nand(Y, nand(nand(Z, Y), Y)), nand(X, Y)), nand(X, Y))), nand(nand(Y, nand(nand(Z, Y), Y)), nand(Z, nand(X, Y))))
% 175.93/22.44 = { by axiom 1 (sh_1) }
% 175.93/22.44 nand(Y, nand(nand(Z, Y), Y))
% 175.93/22.44
% 175.93/22.44 Lemma 13: nand(X, nand(nand(nand(nand(Y, X), nand(Y, X)), X), X)) = nand(Y, X).
% 175.93/22.44 Proof:
% 175.93/22.44 nand(X, nand(nand(nand(nand(Y, X), nand(Y, X)), X), X))
% 175.93/22.44 = { by lemma 5 R->L }
% 175.93/22.44 nand(X, nand(nand(nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))), X), X))
% 175.93/22.44 = { by lemma 12 R->L }
% 175.93/22.44 nand(nand(nand(Y, X), nand(nand(nand(X, nand(nand(nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))), X), X)), nand(Y, X)), nand(Y, X))), nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))))
% 175.93/22.44 = { by lemma 4 }
% 175.93/22.44 nand(nand(nand(Y, X), nand(nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))), nand(Y, X))), nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))))
% 175.93/22.44 = { by lemma 10 }
% 175.93/22.44 nand(nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))), nand(nand(Y, X), nand(nand(nand(Y, X), nand(Y, X)), nand(Y, X))))
% 175.93/22.44 = { by axiom 1 (sh_1) }
% 175.93/22.44 nand(Y, X)
% 175.93/22.44
% 175.93/22.44 Lemma 14: nand(nand(X, Y), nand(X, nand(X, Y))) = X.
% 175.93/22.44 Proof:
% 175.93/22.44 nand(nand(X, Y), nand(X, nand(X, Y)))
% 175.93/22.44 = { by lemma 11 R->L }
% 175.93/22.44 nand(nand(X, Y), nand(nand(nand(X, X), nand(X, Y)), nand(X, Y)))
% 175.93/22.44 = { by lemma 2 R->L }
% 175.93/22.44 nand(nand(X, Y), nand(nand(nand(X, nand(nand(nand(Y, nand(Z, W)), nand(nand(X, nand(Y, nand(Z, W))), nand(Y, nand(Z, W)))), nand(X, Y))), nand(X, Y)), nand(X, Y)))
% 175.93/22.44 = { by lemma 2 R->L }
% 175.93/22.44 nand(nand(X, Y), nand(nand(nand(nand(nand(nand(Y, nand(Z, W)), nand(nand(X, nand(Y, nand(Z, W))), nand(Y, nand(Z, W)))), nand(X, Y)), nand(nand(nand(Y, nand(Z, W)), nand(nand(X, nand(Y, nand(Z, W))), nand(Y, nand(Z, W)))), nand(X, Y))), nand(X, Y)), nand(X, Y)))
% 175.93/22.44 = { by lemma 13 }
% 175.93/22.44 nand(nand(nand(Y, nand(Z, W)), nand(nand(X, nand(Y, nand(Z, W))), nand(Y, nand(Z, W)))), nand(X, Y))
% 175.93/22.45 = { by lemma 2 }
% 175.93/22.45 X
% 175.93/22.45
% 175.93/22.45 Lemma 15: nand(nand(X, X), nand(Y, X)) = X.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, X), nand(Y, X))
% 175.93/22.45 = { by lemma 5 R->L }
% 175.93/22.45 nand(nand(X, nand(nand(X, X), X)), nand(Y, X))
% 175.93/22.45 = { by lemma 13 R->L }
% 175.93/22.45 nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(nand(nand(Y, X), nand(Y, X)), X), X)))
% 175.93/22.45 = { by axiom 1 (sh_1) }
% 175.93/22.45 X
% 175.93/22.45
% 175.93/22.45 Lemma 16: nand(nand(X, Y), nand(Y, nand(X, Y))) = Y.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, Y), nand(Y, nand(X, Y)))
% 175.93/22.45 = { by lemma 15 R->L }
% 175.93/22.45 nand(nand(X, Y), nand(nand(nand(Y, Y), nand(X, Y)), nand(X, Y)))
% 175.93/22.45 = { by lemma 5 R->L }
% 175.93/22.45 nand(nand(X, Y), nand(nand(nand(Y, nand(nand(Y, Y), Y)), nand(X, Y)), nand(X, Y)))
% 175.93/22.45 = { by lemma 11 R->L }
% 175.93/22.45 nand(nand(X, Y), nand(nand(nand(nand(nand(Y, nand(nand(Y, Y), Y)), nand(Y, nand(nand(Y, Y), Y))), nand(nand(Y, nand(nand(Y, Y), Y)), nand(X, Y))), nand(X, Y)), nand(X, Y)))
% 175.93/22.45 = { by axiom 1 (sh_1) }
% 175.93/22.45 nand(nand(X, Y), nand(nand(nand(Y, nand(nand(Y, nand(nand(Y, Y), Y)), nand(X, Y))), nand(X, Y)), nand(X, Y)))
% 175.93/22.45 = { by lemma 5 }
% 175.93/22.45 nand(nand(X, Y), nand(nand(nand(Y, nand(nand(Y, Y), nand(X, Y))), nand(X, Y)), nand(X, Y)))
% 175.93/22.45 = { by lemma 15 R->L }
% 175.93/22.45 nand(nand(X, Y), nand(nand(nand(nand(nand(Y, Y), nand(X, Y)), nand(nand(Y, Y), nand(X, Y))), nand(X, Y)), nand(X, Y)))
% 175.93/22.45 = { by lemma 13 }
% 175.93/22.45 nand(nand(Y, Y), nand(X, Y))
% 175.93/22.45 = { by lemma 15 }
% 175.93/22.45 Y
% 175.93/22.45
% 175.93/22.45 Lemma 17: nand(X, nand(nand(Y, X), X)) = nand(Y, X).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, nand(nand(Y, X), X))
% 175.93/22.45 = { by lemma 14 R->L }
% 175.93/22.45 nand(nand(nand(X, nand(Y, X)), nand(X, nand(X, nand(Y, X)))), nand(nand(Y, X), X))
% 175.93/22.45 = { by lemma 16 R->L }
% 175.93/22.45 nand(nand(nand(X, nand(Y, X)), nand(nand(nand(Y, X), nand(X, nand(Y, X))), nand(X, nand(Y, X)))), nand(nand(Y, X), X))
% 175.93/22.45 = { by lemma 2 }
% 175.93/22.45 nand(Y, X)
% 175.93/22.45
% 175.93/22.45 Lemma 18: nand(X, nand(nand(X, Y), X)) = nand(X, Y).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, nand(nand(X, Y), X))
% 175.93/22.45 = { by lemma 14 R->L }
% 175.93/22.45 nand(nand(nand(X, nand(X, Y)), nand(X, nand(X, nand(X, Y)))), nand(nand(X, Y), X))
% 175.93/22.45 = { by lemma 14 R->L }
% 175.93/22.45 nand(nand(nand(X, nand(X, Y)), nand(nand(nand(X, Y), nand(X, nand(X, Y))), nand(X, nand(X, Y)))), nand(nand(X, Y), X))
% 175.93/22.45 = { by lemma 2 }
% 175.93/22.45 nand(X, Y)
% 175.93/22.45
% 175.93/22.45 Lemma 19: nand(nand(X, Y), nand(X, X)) = X.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, Y), nand(X, X))
% 175.93/22.45 = { by lemma 14 R->L }
% 175.93/22.45 nand(nand(nand(nand(X, Y), X), nand(nand(X, Y), nand(nand(X, Y), X))), nand(X, X))
% 175.93/22.45 = { by lemma 18 R->L }
% 175.93/22.45 nand(nand(nand(nand(X, Y), X), nand(nand(X, nand(nand(X, Y), X)), nand(nand(X, Y), X))), nand(X, X))
% 175.93/22.45 = { by lemma 8 }
% 175.93/22.45 X
% 175.93/22.45
% 175.93/22.45 Lemma 20: nand(X, Y) = nand(Y, X).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, Y)
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(Y, nand(nand(X, Y), Y))
% 175.93/22.45 = { by lemma 12 R->L }
% 175.93/22.45 nand(nand(nand(Y, Y), nand(nand(nand(Y, nand(nand(X, Y), Y)), nand(Y, Y)), nand(Y, Y))), X)
% 175.93/22.45 = { by lemma 19 }
% 175.93/22.45 nand(nand(nand(Y, Y), nand(Y, nand(Y, Y))), X)
% 175.93/22.45 = { by lemma 7 }
% 175.93/22.45 nand(Y, X)
% 175.93/22.45
% 175.93/22.45 Lemma 21: nand(nand(X, Y), nand(X, nand(Z, Y))) = X.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, Y), nand(X, nand(Z, Y)))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(X, nand(Z, Y)), nand(X, Y))
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, Y))
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(nand(nand(Z, Y), nand(nand(X, nand(Y, nand(nand(Z, Y), Y))), nand(Z, Y))), nand(X, Y))
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(nand(nand(Z, Y), nand(nand(X, nand(Y, nand(nand(Z, Y), Y))), nand(Y, nand(nand(Z, Y), Y)))), nand(X, Y))
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(nand(nand(Y, nand(nand(Z, Y), Y)), nand(nand(X, nand(Y, nand(nand(Z, Y), Y))), nand(Y, nand(nand(Z, Y), Y)))), nand(X, Y))
% 175.93/22.45 = { by lemma 2 }
% 175.93/22.45 X
% 175.93/22.45
% 175.93/22.45 Lemma 22: nand(X, nand(Y, nand(X, nand(Y, Z)))) = nand(X, nand(Y, Z)).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, nand(Y, nand(X, nand(Y, Z))))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(X, nand(nand(X, nand(Y, Z)), Y))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(nand(X, nand(Y, Z)), Y), X)
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(nand(nand(nand(Y, Z), nand(nand(X, nand(Y, Z)), nand(Y, Z))), Y), X)
% 175.93/22.45 = { by lemma 9 R->L }
% 175.93/22.45 nand(nand(nand(nand(Y, Z), nand(nand(X, nand(Y, Z)), nand(Y, Z))), Y), nand(nand(nand(Y, Z), nand(nand(X, nand(Y, Z)), nand(Y, Z))), nand(X, Y)))
% 175.93/22.45 = { by lemma 21 }
% 175.93/22.45 nand(nand(Y, Z), nand(nand(X, nand(Y, Z)), nand(Y, Z)))
% 175.93/22.45 = { by lemma 17 }
% 175.93/22.45 nand(X, nand(Y, Z))
% 175.93/22.45
% 175.93/22.45 Lemma 23: nand(X, nand(Y, nand(X, Y))) = nand(X, X).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, nand(Y, nand(X, Y)))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(X, nand(nand(X, Y), Y))
% 175.93/22.45 = { by lemma 16 R->L }
% 175.93/22.45 nand(X, nand(nand(Y, nand(nand(X, Y), Y)), nand(nand(nand(X, Y), Y), nand(Y, nand(nand(X, Y), Y)))))
% 175.93/22.45 = { by lemma 16 }
% 175.93/22.45 nand(X, nand(nand(Y, nand(nand(X, Y), Y)), Y))
% 175.93/22.45 = { by lemma 22 R->L }
% 175.93/22.45 nand(X, nand(nand(Y, nand(nand(X, Y), Y)), nand(X, nand(nand(Y, nand(nand(X, Y), Y)), Y))))
% 175.93/22.45 = { by axiom 1 (sh_1) }
% 175.93/22.45 nand(X, X)
% 175.93/22.45
% 175.93/22.45 Lemma 24: nand(X, nand(Y, Y)) = nand(X, nand(X, Y)).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, nand(Y, Y))
% 175.93/22.45 = { by lemma 23 R->L }
% 175.93/22.45 nand(X, nand(Y, nand(X, nand(Y, X))))
% 175.93/22.45 = { by lemma 22 }
% 175.93/22.45 nand(X, nand(Y, X))
% 175.93/22.45 = { by lemma 20 }
% 175.93/22.45 nand(X, nand(X, Y))
% 175.93/22.45
% 175.93/22.45 Lemma 25: nand(X, nand(Y, Y)) = nand(X, nand(Y, X)).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(X, nand(Y, Y))
% 175.93/22.45 = { by lemma 24 }
% 175.93/22.45 nand(X, nand(X, Y))
% 175.93/22.45 = { by lemma 20 }
% 175.93/22.45 nand(X, nand(Y, X))
% 175.93/22.45
% 175.93/22.45 Lemma 26: nand(nand(X, Y), nand(X, nand(Y, Z))) = X.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, Y), nand(X, nand(Y, Z)))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(X, Y), nand(X, nand(Z, Y)))
% 175.93/22.45 = { by lemma 17 R->L }
% 175.93/22.45 nand(nand(Y, nand(nand(X, Y), Y)), nand(X, nand(Z, Y)))
% 175.93/22.45 = { by axiom 1 (sh_1) }
% 175.93/22.45 X
% 175.93/22.45
% 175.93/22.45 Lemma 27: nand(nand(X, Y), nand(Y, nand(X, Z))) = Y.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, Y), nand(Y, nand(X, Z)))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(Y, X), nand(Y, nand(X, Z)))
% 175.93/22.45 = { by lemma 26 }
% 175.93/22.45 Y
% 175.93/22.45
% 175.93/22.45 Lemma 28: nand(nand(X, Y), nand(nand(X, Z), Y)) = Y.
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, Y), nand(nand(X, Z), Y))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(X, Y), nand(Y, nand(X, Z)))
% 175.93/22.45 = { by lemma 27 }
% 175.93/22.45 Y
% 175.93/22.45
% 175.93/22.45 Lemma 29: nand(nand(X, nand(X, X)), nand(nand(X, nand(X, X)), nand(X, nand(X, X)))) = nand(X, nand(X, X)).
% 175.93/22.45 Proof:
% 175.93/22.45 nand(nand(X, nand(X, X)), nand(nand(X, nand(X, X)), nand(X, nand(X, X))))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(nand(X, X), X), nand(nand(X, nand(X, X)), nand(X, nand(X, X))))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(nand(X, X), X), nand(nand(nand(X, X), X), nand(X, nand(X, X))))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(nand(X, X), X), nand(nand(nand(X, X), X), nand(nand(X, X), X)))
% 175.93/22.45 = { by lemma 20 R->L }
% 175.93/22.45 nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(X, X), X))
% 175.93/22.45 = { by axiom 1 (sh_1) R->L }
% 175.93/22.45 nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(nand(nand(X, X), X), nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(X, X), X))), nand(nand(nand(X, X), X), nand(nand(X, X), nand(nand(X, X), X)))))
% 175.93/22.46 = { by lemma 14 }
% 175.93/22.46 nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(nand(nand(X, X), X), nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(X, X), X))), nand(X, X)))
% 175.93/22.46 = { by lemma 5 }
% 175.93/22.46 nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(X, X)))
% 175.93/22.46 = { by lemma 24 R->L }
% 175.93/22.46 nand(nand(nand(nand(X, X), X), nand(nand(X, X), X)), nand(nand(X, X), nand(X, X)))
% 175.93/22.46 = { by lemma 20 }
% 175.93/22.46 nand(nand(nand(X, nand(X, X)), nand(nand(X, X), X)), nand(nand(X, X), nand(X, X)))
% 175.93/22.46 = { by lemma 20 }
% 175.93/22.46 nand(nand(nand(X, nand(X, X)), nand(X, nand(X, X))), nand(nand(X, X), nand(X, X)))
% 175.93/22.46 = { by lemma 6 }
% 175.93/22.46 nand(nand(nand(X, nand(X, X)), nand(X, nand(X, X))), X)
% 175.93/22.46 = { by lemma 5 R->L }
% 175.93/22.46 nand(nand(nand(X, nand(X, X)), nand(nand(nand(X, nand(X, X)), nand(X, nand(X, X))), nand(X, nand(X, X)))), X)
% 175.93/22.46 = { by lemma 14 R->L }
% 175.93/22.46 nand(nand(nand(X, nand(X, X)), nand(nand(nand(X, nand(X, X)), nand(X, nand(X, X))), nand(X, nand(X, X)))), nand(nand(X, nand(X, X)), nand(X, nand(X, nand(X, X)))))
% 175.93/22.46 = { by axiom 1 (sh_1) }
% 175.93/22.46 nand(X, nand(X, X))
% 175.93/22.46
% 175.93/22.46 Lemma 30: nand(X, nand(Z, nand(Z, Z))) = nand(X, nand(Y, nand(Y, Y))).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(Z, nand(Z, Z)))
% 175.93/22.46 = { by lemma 29 R->L }
% 175.93/22.46 nand(X, nand(nand(Z, nand(Z, Z)), nand(nand(Z, nand(Z, Z)), nand(Z, nand(Z, Z)))))
% 175.93/22.46 = { by lemma 22 R->L }
% 175.93/22.46 nand(X, nand(nand(Z, nand(Z, Z)), nand(X, nand(nand(Z, nand(Z, Z)), nand(nand(Z, nand(Z, Z)), nand(Z, nand(Z, Z)))))))
% 175.93/22.46 = { by lemma 29 }
% 175.93/22.46 nand(X, nand(nand(Z, nand(Z, Z)), nand(X, nand(Z, nand(Z, Z)))))
% 175.93/22.46 = { by lemma 23 }
% 175.93/22.46 nand(X, X)
% 175.93/22.46 = { by lemma 23 R->L }
% 175.93/22.46 nand(X, nand(nand(Y, nand(Y, Y)), nand(X, nand(Y, nand(Y, Y)))))
% 175.93/22.46 = { by lemma 29 R->L }
% 175.93/22.46 nand(X, nand(nand(Y, nand(Y, Y)), nand(X, nand(nand(Y, nand(Y, Y)), nand(nand(Y, nand(Y, Y)), nand(Y, nand(Y, Y)))))))
% 175.93/22.46 = { by lemma 22 }
% 175.93/22.46 nand(X, nand(nand(Y, nand(Y, Y)), nand(nand(Y, nand(Y, Y)), nand(Y, nand(Y, Y)))))
% 175.93/22.46 = { by lemma 29 }
% 175.93/22.46 nand(X, nand(Y, nand(Y, Y)))
% 175.93/22.46
% 175.93/22.46 Lemma 31: nand(Y, nand(Y, Y)) = nand(X, nand(X, X)).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(Y, nand(Y, Y))
% 175.93/22.46 = { by lemma 28 R->L }
% 175.93/22.46 nand(nand(Z, nand(Y, nand(Y, Y))), nand(nand(Z, W), nand(Y, nand(Y, Y))))
% 175.93/22.46 = { by lemma 30 }
% 175.93/22.46 nand(nand(Z, nand(Y, nand(Y, Y))), nand(nand(Z, W), nand(X, nand(X, X))))
% 175.93/22.46 = { by lemma 30 }
% 175.93/22.46 nand(nand(Z, nand(X, nand(X, X))), nand(nand(Z, W), nand(X, nand(X, X))))
% 175.93/22.46 = { by lemma 28 }
% 175.93/22.46 nand(X, nand(X, X))
% 175.93/22.46
% 175.93/22.46 Lemma 32: nand(X, nand(X, nand(X, Y))) = nand(X, Y).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(X, nand(X, Y)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(X, nand(Y, X)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(nand(Y, X), X))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(nand(X, Y), X))
% 175.93/22.46 = { by lemma 18 }
% 175.93/22.46 nand(X, Y)
% 175.93/22.46
% 175.93/22.46 Lemma 33: nand(X, nand(Y, nand(X, X))) = nand(X, X).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(Y, nand(X, X)))
% 175.93/22.46 = { by lemma 5 R->L }
% 175.93/22.46 nand(X, nand(Y, nand(X, nand(nand(X, X), X))))
% 175.93/22.46 = { by axiom 1 (sh_1) R->L }
% 175.93/22.46 nand(nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(X, X), X))), nand(Y, nand(X, nand(nand(X, X), X))))
% 175.93/22.46 = { by lemma 15 }
% 175.93/22.46 nand(X, nand(nand(X, X), X))
% 175.93/22.46 = { by lemma 5 }
% 175.93/22.46 nand(X, X)
% 175.93/22.46
% 175.93/22.46 Lemma 34: nand(X, nand(Y, nand(Y, Y))) = nand(X, X).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(Y, nand(Y, Y)))
% 175.93/22.46 = { by lemma 29 R->L }
% 175.93/22.46 nand(X, nand(nand(Y, nand(Y, Y)), nand(nand(Y, nand(Y, Y)), nand(Y, nand(Y, Y)))))
% 175.93/22.46 = { by lemma 22 R->L }
% 175.93/22.46 nand(X, nand(nand(Y, nand(Y, Y)), nand(X, nand(nand(Y, nand(Y, Y)), nand(nand(Y, nand(Y, Y)), nand(Y, nand(Y, Y)))))))
% 175.93/22.46 = { by lemma 29 }
% 175.93/22.46 nand(X, nand(nand(Y, nand(Y, Y)), nand(X, nand(Y, nand(Y, Y)))))
% 175.93/22.46 = { by lemma 23 }
% 175.93/22.46 nand(X, X)
% 175.93/22.46
% 175.93/22.46 Lemma 35: nand(nand(X, nand(Y, Z)), nand(nand(X, Y), nand(X, Y))) = nand(X, nand(X, nand(Y, Z))).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(nand(X, nand(Y, Z)), nand(nand(X, Y), nand(X, Y)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(nand(X, nand(Y, Z)), nand(nand(Y, X), nand(X, Y)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(nand(X, nand(Y, Z)), nand(nand(Y, X), nand(Y, X)))
% 175.93/22.46 = { by lemma 25 }
% 175.93/22.46 nand(nand(X, nand(Y, Z)), nand(nand(Y, X), nand(X, nand(Y, Z))))
% 175.93/22.46 = { by lemma 27 }
% 175.93/22.46 nand(nand(X, nand(Y, Z)), X)
% 175.93/22.46 = { by lemma 20 }
% 175.93/22.46 nand(X, nand(X, nand(Y, Z)))
% 175.93/22.46
% 175.93/22.46 Lemma 36: nand(nand(X, Y), nand(Y, Y)) = Y.
% 175.93/22.46 Proof:
% 175.93/22.46 nand(nand(X, Y), nand(Y, Y))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(nand(Y, Y), nand(X, Y))
% 175.93/22.46 = { by lemma 15 }
% 175.93/22.46 Y
% 175.93/22.46
% 175.93/22.46 Lemma 37: nand(X, nand(nand(X, Y), nand(Y, Z))) = nand(X, Y).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(nand(X, Y), nand(Y, Z)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(nand(nand(X, Y), nand(Y, Z)), X)
% 175.93/22.46 = { by lemma 17 R->L }
% 175.93/22.46 nand(nand(nand(Y, Z), nand(nand(nand(X, Y), nand(Y, Z)), nand(Y, Z))), X)
% 175.93/22.46 = { by lemma 26 R->L }
% 175.93/22.46 nand(nand(nand(Y, Z), nand(nand(nand(X, Y), nand(Y, Z)), nand(Y, Z))), nand(nand(X, Y), nand(X, nand(Y, Z))))
% 175.93/22.46 = { by axiom 1 (sh_1) }
% 175.93/22.46 nand(X, Y)
% 175.93/22.46
% 175.93/22.46 Lemma 38: nand(nand(X, Y), nand(Y, nand(Z, X))) = Y.
% 175.93/22.46 Proof:
% 175.93/22.46 nand(nand(X, Y), nand(Y, nand(Z, X)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(nand(Y, X), nand(Y, nand(Z, X)))
% 175.93/22.46 = { by lemma 21 }
% 175.93/22.46 Y
% 175.93/22.46
% 175.93/22.46 Lemma 39: nand(X, nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z)))) = nand(X, X).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))))
% 175.93/22.46 = { by lemma 22 R->L }
% 175.93/22.46 nand(X, nand(nand(X, Y), nand(X, nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))))))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(nand(X, Y), nand(nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))), X)))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(nand(nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))), X), nand(X, Y)))
% 175.93/22.46 = { by lemma 37 R->L }
% 175.93/22.46 nand(X, nand(nand(nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))), X), nand(X, nand(nand(X, Y), nand(Y, Z)))))
% 175.93/22.46 = { by lemma 37 R->L }
% 175.93/22.46 nand(X, nand(nand(nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))), X), nand(X, nand(nand(X, nand(nand(X, Y), nand(Y, Z))), nand(nand(nand(X, Y), nand(Y, Z)), nand(X, Y))))))
% 175.93/22.46 = { by lemma 37 }
% 175.93/22.46 nand(X, nand(nand(nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))), X), nand(X, nand(nand(X, Y), nand(nand(nand(X, Y), nand(Y, Z)), nand(X, Y))))))
% 175.93/22.46 = { by lemma 20 }
% 175.93/22.46 nand(X, nand(nand(nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z))), X), nand(X, nand(nand(X, Y), nand(nand(X, Y), nand(nand(X, Y), nand(Y, Z)))))))
% 175.93/22.46 = { by lemma 38 }
% 175.93/22.46 nand(X, X)
% 175.93/22.46
% 175.93/22.46 Lemma 40: nand(X, nand(nand(Y, Y), nand(X, nand(Y, Z)))) = nand(X, X).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(nand(Y, Y), nand(X, nand(Y, Z))))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(nand(X, nand(Y, Z)), nand(Y, Y)))
% 175.93/22.46 = { by lemma 34 R->L }
% 175.93/22.46 nand(X, nand(nand(X, nand(Y, Z)), nand(Y, nand(W, nand(W, W)))))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(nand(X, nand(Z, Y)), nand(Y, nand(W, nand(W, W)))))
% 175.93/22.46 = { by lemma 34 }
% 175.93/22.46 nand(X, nand(nand(X, nand(Z, Y)), nand(Y, Y)))
% 175.93/22.46 = { by lemma 25 }
% 175.93/22.46 nand(X, nand(nand(X, nand(Z, Y)), nand(Y, nand(X, nand(Z, Y)))))
% 175.93/22.46 = { by lemma 20 }
% 175.93/22.46 nand(X, nand(nand(X, nand(Z, Y)), nand(nand(X, nand(Z, Y)), Y)))
% 175.93/22.46 = { by lemma 36 R->L }
% 175.93/22.46 nand(X, nand(nand(X, nand(Z, Y)), nand(nand(X, nand(Z, Y)), nand(nand(Z, Y), nand(Y, Y)))))
% 175.93/22.46 = { by lemma 39 }
% 175.93/22.46 nand(X, X)
% 175.93/22.46
% 175.93/22.46 Lemma 41: nand(X, nand(Y, nand(Z, nand(X, X)))) = nand(X, nand(X, Y)).
% 175.93/22.46 Proof:
% 175.93/22.46 nand(X, nand(Y, nand(Z, nand(X, X))))
% 175.93/22.46 = { by lemma 22 R->L }
% 175.93/22.46 nand(X, nand(Y, nand(X, nand(Y, nand(Z, nand(X, X))))))
% 175.93/22.46 = { by lemma 20 R->L }
% 175.93/22.46 nand(X, nand(Y, nand(nand(Y, nand(Z, nand(X, X))), X)))
% 175.93/22.46 = { by axiom 1 (sh_1) R->L }
% 175.93/22.46 nand(X, nand(Y, nand(nand(Y, nand(Z, nand(X, X))), nand(nand(X, nand(nand(X, X), X)), nand(X, nand(nand(X, X), X))))))
% 175.93/22.46 = { by lemma 24 }
% 175.93/22.46 nand(X, nand(Y, nand(nand(Y, nand(Z, nand(X, X))), nand(nand(Y, nand(Z, nand(X, X))), nand(X, nand(nand(X, X), X))))))
% 175.93/22.46 = { by lemma 5 }
% 175.93/22.46 nand(X, nand(Y, nand(nand(Y, nand(Z, nand(X, X))), nand(nand(Y, nand(Z, nand(X, X))), nand(X, X)))))
% 175.93/22.47 = { by lemma 33 R->L }
% 175.93/22.47 nand(X, nand(Y, nand(nand(Y, nand(Z, nand(X, X))), nand(nand(Y, nand(Z, nand(X, X))), nand(X, nand(Z, nand(X, X)))))))
% 175.93/22.47 = { by lemma 20 R->L }
% 175.93/22.47 nand(X, nand(Y, nand(nand(Y, nand(Z, nand(X, X))), nand(nand(Y, nand(Z, nand(X, X))), nand(nand(Z, nand(X, X)), X)))))
% 175.93/22.47 = { by lemma 39 }
% 175.93/22.47 nand(X, nand(Y, Y))
% 175.93/22.47 = { by lemma 25 }
% 175.93/22.47 nand(X, nand(Y, X))
% 175.93/22.47 = { by lemma 20 }
% 175.93/22.47 nand(X, nand(X, Y))
% 175.93/22.47
% 175.93/22.47 Lemma 42: nand(X, nand(nand(X, Y), nand(Z, nand(X, nand(X, Y))))) = nand(X, Y).
% 175.93/22.47 Proof:
% 175.93/22.47 nand(X, nand(nand(X, Y), nand(Z, nand(X, nand(X, Y)))))
% 175.93/22.47 = { by lemma 14 R->L }
% 175.93/22.47 nand(nand(nand(X, nand(X, Y)), nand(X, nand(X, nand(X, Y)))), nand(nand(X, Y), nand(Z, nand(X, nand(X, Y)))))
% 175.93/22.47 = { by lemma 14 R->L }
% 175.93/22.47 nand(nand(nand(X, nand(X, Y)), nand(nand(nand(X, Y), nand(X, nand(X, Y))), nand(X, nand(X, Y)))), nand(nand(X, Y), nand(Z, nand(X, nand(X, Y)))))
% 175.93/22.47 = { by axiom 1 (sh_1) }
% 175.93/22.47 nand(X, Y)
% 175.93/22.47
% 175.93/22.47 Lemma 43: nand(nand(X, Y), nand(X, nand(Z, nand(X, nand(X, Y))))) = X.
% 175.93/22.47 Proof:
% 175.93/22.47 nand(nand(X, Y), nand(X, nand(Z, nand(X, nand(X, Y)))))
% 175.93/22.47 = { by lemma 20 R->L }
% 175.93/22.47 nand(nand(X, Y), nand(X, nand(Z, nand(nand(X, Y), X))))
% 175.93/22.47 = { by lemma 14 R->L }
% 175.93/22.47 nand(nand(nand(nand(X, Y), X), nand(nand(X, Y), nand(nand(X, Y), X))), nand(X, nand(Z, nand(nand(X, Y), X))))
% 175.93/22.47 = { by lemma 18 R->L }
% 175.93/22.47 nand(nand(nand(nand(X, Y), X), nand(nand(X, nand(nand(X, Y), X)), nand(nand(X, Y), X))), nand(X, nand(Z, nand(nand(X, Y), X))))
% 175.93/22.47 = { by axiom 1 (sh_1) }
% 175.93/22.47 X
% 175.93/22.47
% 175.93/22.47 Lemma 44: nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z)))) = nand(X, nand(Y, Z)).
% 175.93/22.47 Proof:
% 175.93/22.47 nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))))
% 175.93/22.47 = { by lemma 20 R->L }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), X)
% 175.93/22.47 = { by lemma 9 R->L }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, Z)))
% 175.93/22.47 = { by lemma 42 R->L }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, Z)), nand(nand(X, nand(Y, Z)), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 9 }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 17 }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(nand(X, nand(Z, Y)), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 17 }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(nand(Z, Y), nand(nand(X, nand(Z, Y)), nand(Z, Y))), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, nand(Z, Y)), nand(nand(X, nand(Z, Y)), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 17 }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(X, nand(Z, Y)), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, nand(Z, Y)), nand(nand(X, nand(Z, Y)), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 24 R->L }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(X, nand(Z, Y)), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, nand(Z, Y)), nand(nand(X, Z), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 20 }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(X, nand(Z, Y)), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 20 }
% 175.93/22.47 nand(nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z))), nand(nand(X, nand(Y, Z)), nand(X, nand(nand(X, nand(Y, Z)), nand(nand(X, nand(Y, Z)), nand(nand(X, Z), nand(X, Z)))))))
% 175.93/22.47 = { by lemma 43 }
% 175.93/22.47 nand(X, nand(Y, Z))
% 175.93/22.47
% 175.93/22.47 Lemma 45: nand(nand(X, X), nand(nand(X, Y), nand(X, Y))) = nand(Z, nand(Z, Z)).
% 175.93/22.47 Proof:
% 175.93/22.47 nand(nand(X, X), nand(nand(X, Y), nand(X, Y)))
% 175.93/22.47 = { by lemma 24 }
% 175.93/22.47 nand(nand(X, X), nand(nand(X, X), nand(X, Y)))
% 175.93/22.47 = { by lemma 11 }
% 175.93/22.47 nand(nand(X, X), X)
% 175.93/22.47 = { by lemma 20 }
% 175.93/22.47 nand(X, nand(X, X))
% 175.93/22.47 = { by lemma 31 R->L }
% 175.93/22.47 nand(Z, nand(Z, Z))
% 175.93/22.47
% 175.93/22.47 Lemma 46: nand(nand(X, X), nand(nand(X, Y), nand(Z, nand(X, X)))) = nand(Z, nand(X, X)).
% 175.93/22.47 Proof:
% 175.93/22.47 nand(nand(X, X), nand(nand(X, Y), nand(Z, nand(X, X))))
% 175.93/22.47 = { by lemma 20 R->L }
% 175.93/22.47 nand(nand(X, X), nand(nand(X, Y), nand(nand(X, X), Z)))
% 175.93/22.47 = { by lemma 20 R->L }
% 175.93/22.47 nand(nand(X, X), nand(nand(Y, X), nand(nand(X, X), Z)))
% 175.93/22.47 = { by lemma 20 R->L }
% 175.93/22.47 nand(nand(X, X), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by lemma 5 R->L }
% 175.93/22.47 nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by lemma 5 R->L }
% 175.93/22.47 nand(nand(X, nand(nand(X, nand(nand(X, X), X)), X)), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by lemma 4 R->L }
% 175.93/22.47 nand(nand(X, nand(nand(nand(nand(nand(nand(X, nand(nand(X, X), X)), Z), nand(X, nand(nand(X, X), X))), nand(nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, nand(nand(X, X), X)), Z), nand(X, nand(nand(X, X), X)))), nand(nand(nand(X, nand(nand(X, X), X)), Z), nand(X, nand(nand(X, X), X))))), X), X)), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by lemma 18 }
% 175.93/22.47 nand(nand(X, nand(nand(nand(nand(nand(nand(X, nand(nand(X, X), X)), Z), nand(X, nand(nand(X, X), X))), nand(nand(nand(X, nand(nand(X, X), X)), Z), nand(nand(nand(X, nand(nand(X, X), X)), Z), nand(X, nand(nand(X, X), X))))), X), X)), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by lemma 14 }
% 175.93/22.47 nand(nand(X, nand(nand(nand(nand(X, nand(nand(X, X), X)), Z), X), X)), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by lemma 5 }
% 175.93/22.47 nand(nand(X, nand(nand(nand(nand(X, X), Z), X), X)), nand(nand(nand(X, X), Z), nand(Y, X)))
% 175.93/22.47 = { by axiom 1 (sh_1) }
% 175.93/22.47 nand(nand(X, X), Z)
% 175.93/22.47 = { by lemma 20 }
% 175.93/22.47 nand(Z, nand(X, X))
% 175.93/22.47
% 175.93/22.47 Lemma 47: nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))) = X.
% 175.93/22.47 Proof:
% 175.93/22.47 nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z))))
% 175.93/22.47 = { by lemma 44 R->L }
% 175.93/22.47 nand(nand(X, X), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(X, X), nand(nand(X, Z), nand(X, Z))), nand(nand(X, X), nand(nand(X, Z), nand(X, Z))))))
% 175.93/22.47 = { by lemma 45 }
% 175.93/22.47 nand(nand(X, X), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(W, nand(W, W)), nand(nand(X, X), nand(nand(X, Z), nand(X, Z))))))
% 175.93/22.48 = { by lemma 45 }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))
% 175.93/22.48 = { by lemma 6 R->L }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))
% 175.93/22.48 = { by lemma 46 R->L }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(V, nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))))
% 175.93/22.48 = { by lemma 15 R->L }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(V, nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))))
% 175.93/22.48 = { by lemma 20 R->L }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(V, nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))))
% 175.93/22.48 = { by lemma 42 }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))))
% 175.93/22.48 = { by lemma 20 }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))))
% 175.93/22.48 = { by lemma 31 R->L }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(W, nand(W, W)), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))))
% 175.93/22.48 = { by lemma 6 }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W))))), nand(nand(W, nand(W, W)), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))
% 175.93/22.48 = { by lemma 6 }
% 175.93/22.48 nand(nand(X, X), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(nand(nand(X, X), nand(Y, nand(nand(X, Z), nand(X, Z)))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))))
% 175.93/22.49 = { by lemma 33 }
% 175.93/22.49 nand(nand(X, X), nand(nand(nand(W, nand(W, W)), nand(W, nand(W, W))), nand(nand(W, nand(W, W)), nand(W, nand(W, W)))))
% 175.93/22.49 = { by lemma 6 }
% 175.93/22.49 nand(nand(X, X), nand(W, nand(W, W)))
% 175.93/22.49 = { by lemma 34 }
% 175.93/22.49 nand(nand(X, X), nand(X, X))
% 175.93/22.49 = { by lemma 6 }
% 175.93/22.49 X
% 175.93/22.49
% 175.93/22.49 Lemma 48: nand(nand(nand(X, Y), nand(X, Y)), nand(nand(Z, nand(X, Y)), W)) = nand(nand(X, W), nand(nand(X, Y), nand(X, Y))).
% 175.93/22.49 Proof:
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(nand(Z, nand(X, Y)), W))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(nand(nand(X, Y), Z), W))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(X, Y), Z)))
% 175.93/22.49 = { by lemma 22 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(X, Y), Z)))))
% 175.93/22.49 = { by lemma 40 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, W))
% 175.93/22.49 = { by lemma 40 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(X, Y), nand(X, Y))))))
% 175.93/22.49 = { by lemma 22 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(X, Y), nand(X, Y))))
% 175.93/22.49 = { by lemma 20 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(nand(nand(X, Y), nand(X, Y)), W))
% 175.93/22.49 = { by lemma 41 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, nand(nand(X, X), nand(nand(nand(X, Y), nand(X, Y)), nand(nand(X, Y), nand(X, Y))))))
% 175.93/22.49 = { by lemma 47 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(X, Y)), nand(W, X))
% 175.93/22.49 = { by lemma 20 }
% 175.93/22.49 nand(nand(W, X), nand(nand(X, Y), nand(X, Y)))
% 175.93/22.49 = { by lemma 20 }
% 175.93/22.49 nand(nand(X, W), nand(nand(X, Y), nand(X, Y)))
% 175.93/22.49
% 175.93/22.49 Lemma 49: nand(nand(X, Y), nand(X, nand(nand(X, nand(X, Y)), Z))) = X.
% 175.93/22.49 Proof:
% 175.93/22.49 nand(nand(X, Y), nand(X, nand(nand(X, nand(X, Y)), Z)))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(X, Y), nand(X, nand(Z, nand(X, nand(X, Y)))))
% 175.93/22.49 = { by lemma 43 }
% 175.93/22.49 X
% 175.93/22.49
% 175.93/22.49 Lemma 50: nand(nand(X, Y), nand(nand(X, Y), nand(Z, nand(X, X)))) = nand(Z, nand(X, X)).
% 175.93/22.49 Proof:
% 175.93/22.49 nand(nand(X, Y), nand(nand(X, Y), nand(Z, nand(X, X))))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(X, Y))
% 175.93/22.49 = { by axiom 1 (sh_1) R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(X, X), nand(nand(nand(X, Y), nand(X, X)), nand(X, X))), nand(nand(X, Y), nand(Z, nand(X, X)))))
% 175.93/22.49 = { by lemma 19 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(X, X), nand(X, nand(X, X))), nand(nand(X, Y), nand(Z, nand(X, X)))))
% 175.93/22.49 = { by lemma 7 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(X, nand(nand(X, Y), nand(Z, nand(X, X)))))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))
% 175.93/22.49 = { by lemma 47 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(X, X)), nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(X, X))))))
% 175.93/22.49 = { by lemma 36 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(X, nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(X, X))))))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(X, nand(nand(X, X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))))))
% 175.93/22.49 = { by lemma 17 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(X, nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))))))
% 175.93/22.49 = { by lemma 17 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(X, nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)))))))
% 175.93/22.49 = { by lemma 20 R->L }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, nand(nand(X, X), X)), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))), X))))
% 175.93/22.49 = { by lemma 12 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(X, nand(nand(X, X), X)))))
% 175.93/22.49 = { by lemma 17 }
% 175.93/22.49 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X)), nand(Z, nand(X, X))))
% 175.93/22.50 = { by lemma 20 }
% 175.93/22.50 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(Z, nand(X, X)), nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))))
% 175.93/22.50 = { by lemma 46 R->L }
% 175.93/22.50 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(X, X), nand(nand(X, Y), nand(Z, nand(X, X)))), nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))))
% 175.93/22.50 = { by lemma 20 R->L }
% 175.93/22.50 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(X, X)), nand(nand(nand(nand(X, Y), nand(Z, nand(X, X))), X), nand(nand(nand(X, Y), nand(Z, nand(X, X))), X))))
% 175.93/22.50 = { by lemma 44 }
% 175.93/22.50 nand(nand(nand(X, Y), nand(Z, nand(X, X))), nand(X, X))
% 175.93/22.50 = { by lemma 20 }
% 175.93/22.50 nand(nand(X, X), nand(nand(X, Y), nand(Z, nand(X, X))))
% 175.93/22.50 = { by lemma 46 }
% 175.93/22.50 nand(Z, nand(X, X))
% 175.93/22.50
% 175.93/22.50 Lemma 51: nand(X, nand(X, nand(Y, nand(nand(X, Z), nand(X, Z))))) = nand(Y, nand(nand(X, Z), nand(X, Z))).
% 175.93/22.50 Proof:
% 175.93/22.50 nand(X, nand(X, nand(Y, nand(nand(X, Z), nand(X, Z)))))
% 175.93/22.50 = { by lemma 49 R->L }
% 175.93/22.50 nand(X, nand(nand(nand(X, Z), nand(X, nand(nand(X, nand(X, Z)), W))), nand(Y, nand(nand(X, Z), nand(X, Z)))))
% 175.93/22.50 = { by lemma 49 R->L }
% 175.93/22.50 nand(nand(nand(X, Z), nand(X, nand(nand(X, nand(X, Z)), W))), nand(nand(nand(X, Z), nand(X, nand(nand(X, nand(X, Z)), W))), nand(Y, nand(nand(X, Z), nand(X, Z)))))
% 175.93/22.50 = { by lemma 50 }
% 175.93/22.50 nand(Y, nand(nand(X, Z), nand(X, Z)))
% 175.93/22.50
% 175.93/22.50 Lemma 52: nand(Y, nand(Y, nand(X, nand(nand(Y, Z), X)))) = nand(X, nand(nand(Y, Z), nand(Y, Z))).
% 175.93/22.50 Proof:
% 175.93/22.50 nand(Y, nand(Y, nand(X, nand(nand(Y, Z), X))))
% 175.93/22.50 = { by lemma 25 R->L }
% 175.93/22.50 nand(Y, nand(Y, nand(X, nand(nand(Y, Z), nand(Y, Z)))))
% 175.93/22.50 = { by lemma 51 }
% 175.93/22.50 nand(X, nand(nand(Y, Z), nand(Y, Z)))
% 175.93/22.50
% 175.93/22.50 Lemma 53: nand(Y, nand(Y, nand(X, nand(nand(Z, Y), nand(Z, Y))))) = nand(X, nand(X, nand(Y, Z))).
% 175.93/22.50 Proof:
% 175.93/22.50 nand(Y, nand(Y, nand(X, nand(nand(Z, Y), nand(Z, Y)))))
% 175.93/22.50 = { by lemma 25 }
% 175.93/22.50 nand(Y, nand(Y, nand(X, nand(nand(Z, Y), X))))
% 175.93/22.50 = { by lemma 20 R->L }
% 175.93/22.50 nand(Y, nand(Y, nand(X, nand(nand(Y, Z), X))))
% 175.93/22.50 = { by lemma 52 }
% 175.93/22.50 nand(X, nand(nand(Y, Z), nand(Y, Z)))
% 176.68/22.50 = { by lemma 25 }
% 176.68/22.50 nand(X, nand(nand(Y, Z), X))
% 176.68/22.50 = { by lemma 20 }
% 176.68/22.50 nand(X, nand(X, nand(Y, Z)))
% 176.68/22.50
% 176.68/22.50 Lemma 54: nand(Y, nand(Y, nand(Z, X))) = nand(X, nand(X, nand(Y, Z))).
% 176.68/22.50 Proof:
% 176.68/22.50 nand(Y, nand(Y, nand(Z, X)))
% 176.68/22.50 = { by lemma 35 R->L }
% 176.68/22.50 nand(nand(Y, nand(Z, X)), nand(nand(Y, Z), nand(Y, Z)))
% 176.68/22.50 = { by lemma 48 R->L }
% 176.68/22.50 nand(nand(nand(Y, Z), nand(Y, Z)), nand(nand(nand(Y, Z), nand(Y, Z)), nand(Z, X)))
% 176.68/22.50 = { by lemma 53 R->L }
% 176.68/22.50 nand(Z, nand(Z, nand(nand(nand(Y, Z), nand(Y, Z)), nand(nand(X, Z), nand(X, Z)))))
% 176.68/22.50 = { by lemma 20 R->L }
% 176.68/22.50 nand(Z, nand(Z, nand(nand(nand(X, Z), nand(X, Z)), nand(nand(Y, Z), nand(Y, Z)))))
% 176.68/22.50 = { by lemma 53 }
% 176.68/22.50 nand(nand(nand(X, Z), nand(X, Z)), nand(nand(nand(X, Z), nand(X, Z)), nand(Z, Y)))
% 176.68/22.50 = { by lemma 48 }
% 176.68/22.50 nand(nand(X, nand(Z, Y)), nand(nand(X, Z), nand(X, Z)))
% 176.68/22.50 = { by lemma 35 }
% 176.68/22.50 nand(X, nand(X, nand(Z, Y)))
% 176.68/22.50 = { by lemma 20 }
% 176.68/22.50 nand(X, nand(X, nand(Y, Z)))
% 176.68/22.50
% 176.68/22.50 Goal 1 (prove_meredith_2_basis): tuple(nand(a, nand(b, nand(a, c))), nand(nand(a, a), nand(b, a))) = tuple(nand(nand(nand(c, b), b), a), a).
% 176.68/22.50 Proof:
% 176.68/22.50 tuple(nand(a, nand(b, nand(a, c))), nand(nand(a, a), nand(b, a)))
% 176.68/22.50 = { by lemma 15 }
% 176.68/22.50 tuple(nand(a, nand(b, nand(a, c))), a)
% 176.68/22.50 = { by lemma 32 R->L }
% 176.68/22.50 tuple(nand(a, nand(a, nand(a, nand(b, nand(a, c))))), a)
% 176.68/22.50 = { by lemma 20 R->L }
% 176.68/22.50 tuple(nand(a, nand(a, nand(a, nand(b, nand(c, a))))), a)
% 176.68/22.50 = { by lemma 54 }
% 176.68/22.50 tuple(nand(a, nand(nand(c, a), nand(nand(c, a), nand(a, b)))), a)
% 176.68/22.50 = { by lemma 20 R->L }
% 176.68/22.50 tuple(nand(a, nand(nand(c, a), nand(nand(a, b), nand(c, a)))), a)
% 176.68/22.50 = { by lemma 25 R->L }
% 176.68/22.50 tuple(nand(a, nand(nand(c, a), nand(nand(a, b), nand(a, b)))), a)
% 176.68/22.50 = { by lemma 20 R->L }
% 176.68/22.50 tuple(nand(a, nand(nand(nand(a, b), nand(a, b)), nand(c, a))), a)
% 176.68/22.50 = { by lemma 22 R->L }
% 176.68/22.50 tuple(nand(a, nand(nand(nand(a, b), nand(a, b)), nand(c, nand(nand(nand(a, b), nand(a, b)), nand(c, a))))), a)
% 176.68/22.50 = { by lemma 20 }
% 176.68/22.50 tuple(nand(a, nand(nand(nand(a, b), nand(a, b)), nand(c, nand(nand(c, a), nand(nand(a, b), nand(a, b)))))), a)
% 176.68/22.50 = { by lemma 25 }
% 176.68/22.50 tuple(nand(a, nand(nand(nand(a, b), nand(a, b)), nand(c, nand(nand(c, a), nand(nand(a, b), nand(c, a)))))), a)
% 176.68/22.50 = { by lemma 20 R->L }
% 176.68/22.50 tuple(nand(a, nand(nand(nand(a, b), nand(a, b)), nand(c, nand(nand(c, a), nand(nand(c, a), nand(a, b)))))), a)
% 176.68/22.50 = { by lemma 39 }
% 176.68/22.50 tuple(nand(a, nand(nand(nand(a, b), nand(a, b)), nand(c, c))), a)
% 176.68/22.50 = { by lemma 20 }
% 176.68/22.50 tuple(nand(a, nand(nand(c, c), nand(nand(a, b), nand(a, b)))), a)
% 176.68/22.50 = { by lemma 51 R->L }
% 176.68/22.50 tuple(nand(a, nand(a, nand(a, nand(nand(c, c), nand(nand(a, b), nand(a, b)))))), a)
% 176.68/22.50 = { by lemma 25 }
% 176.68/22.50 tuple(nand(a, nand(a, nand(a, nand(nand(c, c), nand(nand(a, b), nand(c, c)))))), a)
% 176.68/22.50 = { by lemma 20 R->L }
% 176.68/22.50 tuple(nand(a, nand(a, nand(a, nand(nand(c, c), nand(nand(c, c), nand(a, b)))))), a)
% 176.68/22.50 = { by lemma 22 R->L }
% 176.68/22.50 tuple(nand(a, nand(a, nand(a, nand(nand(c, c), nand(nand(c, c), nand(a, nand(nand(c, c), nand(a, b)))))))), a)
% 176.68/22.51 = { by lemma 20 R->L }
% 176.68/22.51 tuple(nand(a, nand(a, nand(a, nand(nand(c, c), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(c, c)))))), a)
% 176.68/22.51 = { by lemma 52 }
% 176.68/22.51 tuple(nand(a, nand(nand(c, c), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))))), a)
% 176.68/22.51 = { by lemma 50 R->L }
% 176.68/22.51 tuple(nand(a, nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(nand(nand(c, c), nand(a, b)), nand(nand(c, c), nand(a, b)))), nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(nand(nand(c, c), nand(a, b)), nand(nand(c, c), nand(a, b)))), nand(nand(c, c), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))))))), a)
% 176.68/22.51 = { by lemma 36 }
% 176.68/22.51 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(nand(nand(c, c), nand(a, b)), nand(nand(c, c), nand(a, b)))), nand(nand(c, c), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))))))), a)
% 176.68/22.51 = { by lemma 20 R->L }
% 176.68/22.51 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(c, c), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b))))), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(nand(nand(c, c), nand(a, b)), nand(nand(c, c), nand(a, b))))))), a)
% 176.68/22.51 = { by lemma 41 }
% 176.68/22.51 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(c, c), nand(a, b)), nand(nand(c, c), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))))))), a)
% 176.68/22.51 = { by lemma 20 R->L }
% 176.68/22.51 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))), nand(c, c))))), a)
% 176.68/22.51 = { by lemma 20 R->L }
% 176.68/22.51 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))), nand(c, c)), nand(nand(c, c), nand(a, b))))), a)
% 176.68/22.52 = { by lemma 22 R->L }
% 176.68/22.52 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))), nand(c, c)), nand(nand(c, c), nand(a, nand(nand(c, c), nand(a, b))))))), a)
% 176.68/22.52 = { by lemma 37 R->L }
% 176.68/22.52 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))), nand(c, c)), nand(nand(c, c), nand(nand(nand(c, c), nand(a, nand(nand(c, c), nand(a, b)))), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b))))))))), a)
% 176.68/22.52 = { by lemma 22 }
% 176.68/22.52 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(nand(nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b)))), nand(c, c)), nand(nand(c, c), nand(nand(nand(c, c), nand(a, b)), nand(nand(a, nand(nand(c, c), nand(a, b))), nand(a, nand(nand(c, c), nand(a, b))))))))), a)
% 176.68/22.52 = { by lemma 38 }
% 176.68/22.52 tuple(nand(a, nand(nand(nand(c, c), nand(a, b)), nand(c, c))), a)
% 176.68/22.52 = { by lemma 20 }
% 176.68/22.52 tuple(nand(a, nand(nand(c, c), nand(nand(c, c), nand(a, b)))), a)
% 176.68/22.52 = { by lemma 20 }
% 176.68/22.52 tuple(nand(a, nand(nand(c, c), nand(nand(c, c), nand(b, a)))), a)
% 176.68/22.52 = { by lemma 54 }
% 176.68/22.52 tuple(nand(a, nand(a, nand(a, nand(nand(c, c), b)))), a)
% 176.68/22.52 = { by lemma 20 }
% 176.68/22.52 tuple(nand(a, nand(a, nand(a, nand(b, nand(c, c))))), a)
% 176.68/22.52 = { by lemma 32 }
% 176.68/22.52 tuple(nand(a, nand(b, nand(c, c))), a)
% 176.68/22.52 = { by lemma 25 }
% 176.68/22.52 tuple(nand(a, nand(b, nand(c, b))), a)
% 176.68/22.52 = { by lemma 20 R->L }
% 176.68/22.52 tuple(nand(a, nand(nand(c, b), b)), a)
% 176.68/22.52 = { by lemma 20 R->L }
% 176.68/22.52 tuple(nand(nand(nand(c, b), b), a), a)
% 176.68/22.52 % SZS output end Proof
% 176.68/22.52
% 176.68/22.52 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------