%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO076-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 12:59:45 PM UTC 2026
% Result : Unsatisfiable 103.95s 28.64s
% Output : CNFRefutation 103.95s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
nand(nand(X1,nand(nand(X2,X1),X1)),nand(X2,nand(X3,X1))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
nand(nand(X1,nand(nand(X2,X1),X1)),nand(X2,nand(X3,X1))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t4,plain,
X1 = nand(nand(nand(X2,nand(X3,Y3)),nand(nand(X1,nand(X2,nand(X3,Y3))),nand(X2,nand(X3,Y3)))),nand(X1,X2)),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t5,plain,
nand(nand(nand(X1,nand(X2,X3)),nand(nand(Y3,nand(X1,nand(X2,X3))),nand(X1,nand(X2,X3)))),nand(Y3,X1)) = Y3,
inference(orient,[status(thm)],[t4]) ).
cnf(t7,plain,
X1 = nand(nand(nand(X2,X3),nand(nand(X1,nand(X2,nand(nand(Y3,nand(nand(X3,Y3),Y3)),nand(X3,nand(Y4,Y3))))),nand(X2,nand(nand(Y3,nand(nand(X3,Y3),Y3)),nand(X3,nand(Y4,Y3)))))),nand(X1,X2)),
inference(cp,[status(thm)],[t5,t1]) ).
cnf(t135509,plain,
X1 = nand(nand(nand(X2,X3),nand(nand(X1,nand(X2,X3)),nand(X2,nand(nand(Y3,nand(nand(X3,Y3),Y3)),nand(X3,nand(Y4,Y3)))))),nand(X1,X2)),
inference(step,[status(thm)],[t7,t1]) ).
cnf(t135510,plain,
X1 = nand(nand(nand(X2,X3),nand(nand(X1,nand(X2,X3)),nand(X2,X3))),nand(X1,X2)),
inference(step,[status(thm)],[t135509,t1]) ).
cnf(t44,plain,
nand(nand(nand(X1,X2),nand(nand(X3,nand(X1,X2)),nand(X1,X2))),nand(X3,X1)) = X3,
inference(orient,[status(thm)],[t135510]) ).
cnf(t6,plain,
X1 = nand(nand(X2,nand(nand(X1,nand(nand(X3,nand(nand(X2,X3),X3)),nand(X2,nand(Y3,X3)))),nand(nand(X3,nand(nand(X2,X3),X3)),nand(X2,nand(Y3,X3))))),nand(X1,nand(X3,nand(nand(X2,X3),X3)))),
inference(cp,[status(thm)],[t5,t1]) ).
cnf(t135507,plain,
X1 = nand(nand(X2,nand(nand(X1,X2),nand(nand(X3,nand(nand(X2,X3),X3)),nand(X2,nand(Y3,X3))))),nand(X1,nand(X3,nand(nand(X2,X3),X3)))),
inference(step,[status(thm)],[t6,t1]) ).
cnf(t135508,plain,
X1 = nand(nand(X2,nand(nand(X1,X2),X2)),nand(X1,nand(X3,nand(nand(X2,X3),X3)))),
inference(step,[status(thm)],[t135507,t1]) ).
cnf(t25,plain,
nand(nand(X1,nand(nand(X2,X1),X1)),nand(X2,nand(X3,nand(nand(X1,X3),X3)))) = X2,
inference(orient,[status(thm)],[t135508]) ).
cnf(t28,plain,
nand(X1,nand(nand(X1,X1),X1)) = nand(nand(X2,nand(nand(nand(X1,nand(nand(X1,X1),X1)),X2),X2)),X1),
inference(cp,[status(thm)],[t25,t1]) ).
cnf(t62,plain,
nand(nand(X1,nand(nand(nand(X2,nand(nand(X2,X2),X2)),X1),X1)),X2) = nand(X2,nand(nand(X2,X2),X2)),
inference(orient,[status(thm)],[t28]) ).
cnf(t63,plain,
nand(X1,nand(nand(X1,X1),X1)) = nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),X1),
inference(cp,[status(thm)],[t62,t1]) ).
cnf(t78,plain,
nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),X1) = nand(X1,nand(nand(X1,X1),X1)),
inference(orient,[status(thm)],[t63]) ).
cnf(t79,plain,
nand(X1,nand(nand(X1,X1),X1)) = nand(X1,X1),
inference(cp,[status(thm)],[t78,t25]) ).
cnf(t102,plain,
nand(X1,nand(nand(X1,X1),X1)) = nand(X1,X1),
inference(orient,[status(thm)],[t79]) ).
cnf(t135513,plain,
nand(nand(X1,nand(nand(nand(X2,X2),X1),X1)),X2) = nand(X2,nand(nand(X2,X2),X2)),
inference(step,[status(thm)],[t62,t102]) ).
cnf(t135514,plain,
nand(nand(X1,nand(nand(nand(X2,X2),X1),X1)),X2) = nand(X2,X2),
inference(step,[status(thm)],[t135513,t102]) ).
cnf(t117,plain,
nand(nand(X1,nand(nand(nand(X2,X2),X1),X1)),X2) = nand(X2,X2),
inference(rw,[status(thm)],[t135514]) ).
cnf(t145,plain,
nand(nand(X1,nand(nand(nand(X2,X2),X1),X1)),X2) = nand(X2,X2),
inference(orient,[status(thm)],[t117]) ).
cnf(t107,plain,
X1 = nand(nand(X1,nand(nand(X1,X1),X1)),nand(X1,X1)),
inference(cp,[status(thm)],[t1,t102]) ).
cnf(t135515,plain,
X1 = nand(nand(X1,X1),nand(X1,X1)),
inference(step,[status(thm)],[t107,t102]) ).
cnf(t118,plain,
nand(nand(X1,X1),nand(X1,X1)) = X1,
inference(orient,[status(thm)],[t135515]) ).
cnf(t146,plain,
nand(nand(X1,X1),nand(X1,X1)) = nand(nand(X2,nand(nand(X1,X2),X2)),nand(X1,X1)),
inference(cp,[status(thm)],[t145,t118]) ).
cnf(t135516,plain,
X1 = nand(nand(X2,nand(nand(X1,X2),X2)),nand(X1,X1)),
inference(step,[status(thm)],[t146,t118]) ).
cnf(t155,plain,
nand(nand(X1,nand(nand(X2,X1),X1)),nand(X2,X2)) = X2,
inference(orient,[status(thm)],[t135516]) ).
cnf(t169,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(nand(nand(X2,X2),nand(X2,nand(X2,X2))),nand(nand(X1,nand(nand(X2,X1),X1)),X2)),
inference(cp,[status(thm)],[t44,t155]) ).
cnf(t105,plain,
X1 = nand(nand(X1,X1),nand(X1,nand(X2,X1))),
inference(cp,[status(thm)],[t1,t102]) ).
cnf(t128,plain,
nand(nand(X1,X1),nand(X1,nand(X2,X1))) = X1,
inference(orient,[status(thm)],[t105]) ).
cnf(t135517,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(X2,nand(nand(X1,nand(nand(X2,X1),X1)),X2)),
inference(step,[status(thm)],[t169,t128]) ).
cnf(t201,plain,
nand(X1,nand(nand(X2,nand(nand(X1,X2),X2)),X1)) = nand(X2,nand(nand(X1,X2),X2)),
inference(orient,[status(thm)],[t135517]) ).
cnf(t162,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(nand(nand(X2,X2),nand(X2,nand(X2,X2))),nand(nand(X1,nand(nand(X2,X1),X1)),nand(X3,nand(X2,X2)))),
inference(cp,[status(thm)],[t1,t155]) ).
cnf(t135522,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(X2,nand(nand(X1,nand(nand(X2,X1),X1)),nand(X3,nand(X2,X2)))),
inference(step,[status(thm)],[t162,t128]) ).
cnf(t511,plain,
nand(X1,nand(nand(X2,nand(nand(X1,X2),X2)),nand(X3,nand(X1,X1)))) = nand(X2,nand(nand(X1,X2),X2)),
inference(orient,[status(thm)],[t135522]) ).
cnf(t143,plain,
nand(X1,X1) = nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),nand(nand(X1,X1),X1)),
inference(cp,[status(thm)],[t44,t128]) ).
cnf(t887,plain,
nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),nand(nand(X1,X1),X1)) = nand(X1,X1),
inference(orient,[status(thm)],[t143]) ).
cnf(t950,plain,
nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))) = nand(nand(X1,nand(nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),X1),X1)),nand(X1,X1)),
inference(cp,[status(thm)],[t1,t887]) ).
cnf(t135511,plain,
nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),X1) = nand(X1,X1),
inference(step,[status(thm)],[t78,t102]) ).
cnf(t103,plain,
nand(nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))),X1) = nand(X1,X1),
inference(orient,[status(thm)],[t135511]) ).
cnf(t135529,plain,
nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))) = nand(nand(X1,nand(nand(X1,X1),X1)),nand(X1,X1)),
inference(step,[status(thm)],[t950,t103]) ).
cnf(t135530,plain,
nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))) = nand(nand(X1,X1),nand(X1,X1)),
inference(step,[status(thm)],[t135529,t102]) ).
cnf(t135531,plain,
nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))) = X1,
inference(step,[status(thm)],[t135530,t118]) ).
cnf(t976,plain,
nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))) = X1,
inference(orient,[status(thm)],[t135531]) ).
cnf(t1050,plain,
X1 = nand(nand(X2,nand(nand(X1,nand(nand(X2,nand(X3,X2)),nand(X2,nand(X2,nand(X3,X2))))),nand(nand(X2,nand(X3,X2)),nand(X2,nand(X2,nand(X3,X2)))))),nand(X1,nand(X2,nand(X3,X2)))),
inference(cp,[status(thm)],[t44,t976]) ).
cnf(t135551,plain,
X1 = nand(nand(X2,nand(nand(X1,X2),nand(nand(X2,nand(X3,X2)),nand(X2,nand(X2,nand(X3,X2)))))),nand(X1,nand(X2,nand(X3,X2)))),
inference(step,[status(thm)],[t1050,t976]) ).
cnf(t135552,plain,
X1 = nand(nand(X2,nand(nand(X1,X2),X2)),nand(X1,nand(X2,nand(X3,X2)))),
inference(step,[status(thm)],[t135551,t976]) ).
cnf(t1802,plain,
nand(nand(X1,nand(nand(X2,X1),X1)),nand(X2,nand(X1,nand(X3,X1)))) = X2,
inference(orient,[status(thm)],[t135552]) ).
cnf(t2,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(nand(nand(X2,nand(X3,X1)),nand(X2,nand(X2,nand(X3,X1)))),nand(nand(X1,nand(nand(X2,X1),X1)),nand(Y3,nand(X2,nand(X3,X1))))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t2166,plain,
nand(nand(nand(X1,nand(X2,X3)),nand(X1,nand(X1,nand(X2,X3)))),nand(nand(X3,nand(nand(X1,X3),X3)),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X3,nand(nand(X1,X3),X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t212,plain,
X1 = nand(nand(X1,X1),nand(X2,nand(nand(X1,X2),X2))),
inference(cp,[status(thm)],[t128,t201]) ).
cnf(t232,plain,
nand(nand(X1,X1),nand(X2,nand(nand(X1,X2),X2))) = X1,
inference(orient,[status(thm)],[t212]) ).
cnf(t2375,plain,
nand(X1,nand(nand(X1,X1),X1)) = nand(nand(nand(X1,nand(nand(X2,X1),X1)),nand(X1,nand(X1,nand(nand(X2,X1),X1)))),nand(nand(X1,nand(nand(X1,X1),X1)),X2)),
inference(cp,[status(thm)],[t2166,t232]) ).
cnf(t135554,plain,
nand(X1,X1) = nand(nand(nand(X1,nand(nand(X2,X1),X1)),nand(X1,nand(X1,nand(nand(X2,X1),X1)))),nand(nand(X1,nand(nand(X1,X1),X1)),X2)),
inference(step,[status(thm)],[t2375,t102]) ).
cnf(t135555,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,nand(nand(X1,X1),X1)),X2)),
inference(step,[status(thm)],[t135554,t976]) ).
cnf(t135556,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,X1),X2)),
inference(step,[status(thm)],[t135555,t102]) ).
cnf(t2546,plain,
nand(X1,nand(nand(X1,X1),X2)) = nand(X1,X1),
inference(orient,[status(thm)],[t135556]) ).
cnf(t2547,plain,
nand(nand(X1,X1),nand(X1,X1)) = nand(nand(X1,X1),nand(X1,X2)),
inference(cp,[status(thm)],[t2546,t118]) ).
cnf(t135557,plain,
X1 = nand(nand(X1,X1),nand(X1,X2)),
inference(step,[status(thm)],[t2547,t118]) ).
cnf(t2584,plain,
nand(nand(X1,X1),nand(X1,X2)) = X1,
inference(orient,[status(thm)],[t135557]) ).
cnf(t2619,plain,
nand(X1,X1) = nand(nand(nand(X1,X2),nand(X1,nand(X1,X2))),nand(nand(X1,X1),X1)),
inference(cp,[status(thm)],[t44,t2584]) ).
cnf(t1033,plain,
nand(X1,nand(X2,X1)) = nand(X1,nand(nand(X1,nand(X2,X1)),nand(nand(X1,nand(X2,X1)),nand(X1,nand(X1,nand(X2,X1)))))),
inference(cp,[status(thm)],[t976,t976]) ).
cnf(t135532,plain,
nand(X1,nand(X2,X1)) = nand(X1,nand(nand(X1,nand(X2,X1)),X1)),
inference(step,[status(thm)],[t1033,t976]) ).
cnf(t1056,plain,
nand(X1,nand(nand(X1,nand(X2,X1)),X1)) = nand(X1,nand(X2,X1)),
inference(orient,[status(thm)],[t135532]) ).
cnf(t1057,plain,
nand(X1,nand(nand(nand(X1,X1),X1),X1)) = nand(X1,nand(X1,X1)),
inference(cp,[status(thm)],[t1056,t145]) ).
cnf(t1109,plain,
nand(X1,nand(nand(nand(X1,X1),X1),X1)) = nand(X1,nand(X1,X1)),
inference(orient,[status(thm)],[t1057]) ).
cnf(t1119,plain,
X1 = nand(nand(X1,nand(X1,X1)),nand(X1,nand(X1,nand(nand(nand(X1,X1),X1),X1)))),
inference(cp,[status(thm)],[t976,t1109]) ).
cnf(t129,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,X1),nand(X2,nand(X1,X1)))),
inference(cp,[status(thm)],[t128,t118]) ).
cnf(t171,plain,
nand(X1,nand(nand(X1,X1),nand(X2,nand(X1,X1)))) = nand(X1,X1),
inference(orient,[status(thm)],[t129]) ).
cnf(t216,plain,
nand(X1,X1) = nand(X1,nand(X2,nand(nand(nand(X1,X1),X2),X2))),
inference(cp,[status(thm)],[t171,t201]) ).
cnf(t260,plain,
nand(X1,nand(X2,nand(nand(nand(X1,X1),X2),X2))) = nand(X1,X1),
inference(orient,[status(thm)],[t216]) ).
cnf(t135537,plain,
X1 = nand(nand(X1,nand(X1,X1)),nand(X1,X1)),
inference(step,[status(thm)],[t1119,t260]) ).
cnf(t1201,plain,
nand(nand(X1,nand(X1,X1)),nand(X1,X1)) = X1,
inference(orient,[status(thm)],[t135537]) ).
cnf(t1208,plain,
nand(X1,nand(X1,X1)) = nand(nand(X1,nand(nand(nand(X1,nand(X1,X1)),X1),X1)),X1),
inference(cp,[status(thm)],[t1,t1201]) ).
cnf(t1124,plain,
nand(X1,X1) = nand(nand(X1,nand(X1,X1)),nand(nand(X1,X1),nand(X1,X1))),
inference(cp,[status(thm)],[t155,t1109]) ).
cnf(t135536,plain,
nand(X1,X1) = nand(nand(X1,nand(X1,X1)),X1),
inference(step,[status(thm)],[t1124,t118]) ).
cnf(t1183,plain,
nand(nand(X1,nand(X1,X1)),X1) = nand(X1,X1),
inference(orient,[status(thm)],[t135536]) ).
cnf(t135540,plain,
nand(X1,nand(X1,X1)) = nand(nand(X1,nand(nand(X1,X1),X1)),X1),
inference(step,[status(thm)],[t1208,t1183]) ).
cnf(t135541,plain,
nand(X1,nand(X1,X1)) = nand(nand(X1,X1),X1),
inference(step,[status(thm)],[t135540,t102]) ).
cnf(t1240,plain,
nand(nand(X1,X1),X1) = nand(X1,nand(X1,X1)),
inference(orient,[status(thm)],[t135541]) ).
cnf(t135564,plain,
nand(X1,X1) = nand(nand(nand(X1,X2),nand(X1,nand(X1,X2))),nand(X1,nand(X1,X1))),
inference(step,[status(thm)],[t2619,t1240]) ).
cnf(t2720,plain,
nand(nand(nand(X1,X2),nand(X1,nand(X1,X2))),nand(X1,nand(X1,X1))) = nand(X1,X1),
inference(orient,[status(thm)],[t135564]) ).
cnf(t2771,plain,
nand(nand(X1,X2),nand(X1,nand(X1,X2))) = nand(nand(X1,nand(nand(nand(nand(X1,X2),nand(X1,nand(X1,X2))),X1),X1)),nand(X1,X1)),
inference(cp,[status(thm)],[t1802,t2720]) ).
cnf(t2579,plain,
nand(X1,X1) = nand(nand(nand(nand(nand(X1,X1),nand(X1,X1)),X2),nand(nand(nand(X1,X1),nand(X1,X1)),nand(nand(nand(X1,X1),nand(X1,X1)),X2))),X1),
inference(cp,[status(thm)],[t145,t2546]) ).
cnf(t135561,plain,
nand(X1,X1) = nand(nand(nand(X1,X2),nand(nand(nand(X1,X1),nand(X1,X1)),nand(nand(nand(X1,X1),nand(X1,X1)),X2))),X1),
inference(step,[status(thm)],[t2579,t2584]) ).
cnf(t135562,plain,
nand(X1,X1) = nand(nand(nand(X1,X2),nand(X1,nand(nand(nand(X1,X1),nand(X1,X1)),X2))),X1),
inference(step,[status(thm)],[t135561,t2584]) ).
cnf(t135563,plain,
nand(X1,X1) = nand(nand(nand(X1,X2),nand(X1,nand(X1,X2))),X1),
inference(step,[status(thm)],[t135562,t2584]) ).
cnf(t2670,plain,
nand(nand(nand(X1,X2),nand(X1,nand(X1,X2))),X1) = nand(X1,X1),
inference(orient,[status(thm)],[t135563]) ).
cnf(t135565,plain,
nand(nand(X1,X2),nand(X1,nand(X1,X2))) = nand(nand(X1,nand(nand(X1,X1),X1)),nand(X1,X1)),
inference(step,[status(thm)],[t2771,t2670]) ).
cnf(t135566,plain,
nand(nand(X1,X2),nand(X1,nand(X1,X2))) = nand(nand(X1,nand(X1,nand(X1,X1))),nand(X1,X1)),
inference(step,[status(thm)],[t135565,t1240]) ).
cnf(t1122,plain,
nand(X1,X1) = nand(nand(nand(X1,X1),nand(X1,X1)),nand(X1,nand(X1,X1))),
inference(cp,[status(thm)],[t232,t1109]) ).
cnf(t135535,plain,
nand(X1,X1) = nand(X1,nand(X1,nand(X1,X1))),
inference(step,[status(thm)],[t1122,t118]) ).
cnf(t1158,plain,
nand(X1,nand(X1,nand(X1,X1))) = nand(X1,X1),
inference(orient,[status(thm)],[t135535]) ).
cnf(t135567,plain,
nand(nand(X1,X2),nand(X1,nand(X1,X2))) = nand(nand(X1,X1),nand(X1,X1)),
inference(step,[status(thm)],[t135566,t1158]) ).
cnf(t135568,plain,
nand(nand(X1,X2),nand(X1,nand(X1,X2))) = X1,
inference(step,[status(thm)],[t135567,t2584]) ).
cnf(t2808,plain,
nand(nand(X1,X2),nand(X1,nand(X1,X2))) = X1,
inference(orient,[status(thm)],[t135568]) ).
cnf(t2814,plain,
nand(X1,X2) = nand(X1,nand(nand(X1,X2),nand(nand(X1,X2),nand(X1,nand(X1,X2))))),
inference(cp,[status(thm)],[t2808,t2808]) ).
cnf(t135570,plain,
nand(X1,X2) = nand(X1,nand(nand(X1,X2),X1)),
inference(step,[status(thm)],[t2814,t2808]) ).
cnf(t2843,plain,
nand(X1,nand(nand(X1,X2),X1)) = nand(X1,X2),
inference(orient,[status(thm)],[t135570]) ).
cnf(t2864,plain,
nand(nand(nand(X1,X2),X1),nand(nand(X1,nand(nand(X1,X2),X1)),nand(nand(X1,X2),X1))) = nand(X1,nand(nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),X1))),nand(X3,nand(X1,X1)))),
inference(cp,[status(thm)],[t511,t2843]) ).
cnf(t135574,plain,
nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),X1))) = nand(X1,nand(nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),X1))),nand(X3,nand(X1,X1)))),
inference(step,[status(thm)],[t2864,t2843]) ).
cnf(t994,plain,
nand(X1,X2) = nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),nand(nand(nand(X2,X3),nand(nand(X1,nand(X2,X3)),nand(X2,X3))),nand(X1,X2))))),
inference(cp,[status(thm)],[t976,t44]) ).
cnf(t135553,plain,
nand(X1,X2) = nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),X1))),
inference(step,[status(thm)],[t994,t44]) ).
cnf(t2046,plain,
nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),X1))) = nand(X1,X2),
inference(orient,[status(thm)],[t135553]) ).
cnf(t135575,plain,
nand(X1,X2) = nand(X1,nand(nand(nand(nand(X1,X2),X1),nand(nand(X1,X2),nand(nand(X1,X2),X1))),nand(X3,nand(X1,X1)))),
inference(step,[status(thm)],[t135574,t2046]) ).
cnf(t135576,plain,
nand(X1,X2) = nand(X1,nand(nand(X1,X2),nand(X3,nand(X1,X1)))),
inference(step,[status(thm)],[t135575,t2046]) ).
cnf(t2959,plain,
nand(X1,nand(nand(X1,X2),nand(X3,nand(X1,X1)))) = nand(X1,X2),
inference(orient,[status(thm)],[t135576]) ).
cnf(t2961,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(X1,X2),
inference(cp,[status(thm)],[t2959,t1]) ).
cnf(t2998,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(X1,X2),
inference(orient,[status(thm)],[t2961]) ).
cnf(t135592,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(X2,nand(nand(X1,X2),X2)),
inference(step,[status(thm)],[t201,t2998]) ).
cnf(t135593,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X2),X2)),
inference(step,[status(thm)],[t135592,t2998]) ).
cnf(t135594,plain,
nand(X1,X2) = nand(X2,X1),
inference(step,[status(thm)],[t135593,t2998]) ).
cnf(t3017,plain,
nand(X1,X2) = nand(X2,X1),
inference(rw,[status(thm)],[t135594]) ).
cnf(t3021,plain,
nand(X1,X2) = nand(X2,X1),
inference(orient,[status(thm)],[t3017]) ).
cnf(t135577,plain,
nand(nand(X1,X2),nand(X2,nand(X3,X1))) = X2,
inference(step,[status(thm)],[t1,t2998]) ).
cnf(t3008,plain,
nand(nand(X1,X2),nand(X2,nand(X3,X1))) = X2,
inference(rw,[status(thm)],[t135577]) ).
cnf(t135605,plain,
nand(nand(X1,X2),nand(X2,nand(X1,X3))) = X2,
inference(step,[status(thm)],[t3008,t3021]) ).
cnf(t3094,plain,
nand(nand(X1,X2),nand(X2,nand(X1,X3))) = X2,
inference(orient,[status(thm)],[t135605]) ).
cnf(t135580,plain,
nand(nand(X1,X2),nand(X2,X2)) = X2,
inference(step,[status(thm)],[t155,t2998]) ).
cnf(t3011,plain,
nand(nand(X1,X2),nand(X2,X2)) = X2,
inference(rw,[status(thm)],[t135580]) ).
cnf(t3042,plain,
nand(nand(X1,X2),nand(X2,X2)) = X2,
inference(orient,[status(thm)],[t3011]) ).
cnf(t3113,plain,
X1 = nand(nand(nand(X2,X3),X1),nand(X1,X3)),
inference(cp,[status(thm)],[t3094,t3042]) ).
cnf(t135606,plain,
X1 = nand(nand(X1,X3),nand(nand(X2,X3),X1)),
inference(step,[status(thm)],[t3113,t3021]) ).
cnf(t135607,plain,
X1 = nand(nand(X1,X3),nand(X1,nand(X2,X3))),
inference(step,[status(thm)],[t135606,t3021]) ).
cnf(t3167,plain,
nand(nand(X1,X2),nand(X1,nand(X3,X2))) = X1,
inference(orient,[status(thm)],[t135607]) ).
cnf(t3182,plain,
nand(X1,X2) = nand(nand(nand(X1,X2),nand(X1,X3)),X2),
inference(cp,[status(thm)],[t3167,t3094]) ).
cnf(t135609,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X2),nand(X1,X3))),
inference(step,[status(thm)],[t3182,t3021]) ).
cnf(t3239,plain,
nand(X1,nand(nand(X2,X1),nand(X2,X3))) = nand(X2,X1),
inference(orient,[status(thm)],[t135609]) ).
cnf(t3103,plain,
X1 = nand(nand(X1,X2),nand(X1,nand(X2,X3))),
inference(cp,[status(thm)],[t3094,t3021]) ).
cnf(t3127,plain,
nand(nand(X1,X2),nand(X1,nand(X2,X3))) = X1,
inference(orient,[status(thm)],[t3103]) ).
cnf(t3251,plain,
nand(nand(X1,X2),X3) = nand(X3,nand(nand(nand(X1,X2),X3),X1)),
inference(cp,[status(thm)],[t3239,t3127]) ).
cnf(t135611,plain,
nand(X3,nand(X1,X2)) = nand(X3,nand(nand(nand(X1,X2),X3),X1)),
inference(step,[status(thm)],[t3251,t3021]) ).
cnf(t135612,plain,
nand(X3,nand(X1,X2)) = nand(X3,nand(X1,nand(nand(X1,X2),X3))),
inference(step,[status(thm)],[t135611,t3021]) ).
cnf(t135613,plain,
nand(X3,nand(X1,X2)) = nand(X3,nand(X1,nand(X3,nand(X1,X2)))),
inference(step,[status(thm)],[t135612,t3021]) ).
cnf(t3306,plain,
nand(X1,nand(X2,nand(X1,nand(X2,X3)))) = nand(X1,nand(X2,X3)),
inference(orient,[status(thm)],[t135613]) ).
cnf(t3311,plain,
nand(X1,nand(nand(X1,X2),X2)) = nand(X1,X1),
inference(cp,[status(thm)],[t3306,t3167]) ).
cnf(t135614,plain,
nand(X1,nand(X2,nand(X1,X2))) = nand(X1,X1),
inference(step,[status(thm)],[t3311,t3021]) ).
cnf(t3332,plain,
nand(X1,nand(X2,nand(X1,X2))) = nand(X1,X1),
inference(orient,[status(thm)],[t135614]) ).
cnf(t3354,plain,
nand(X1,nand(X2,X1)) = nand(X1,nand(X2,X2)),
inference(cp,[status(thm)],[t3306,t3332]) ).
cnf(t135615,plain,
nand(X1,nand(X1,X2)) = nand(X1,nand(X2,X2)),
inference(step,[status(thm)],[t3354,t3021]) ).
cnf(t3355,plain,
nand(X1,nand(X1,X2)) = nand(X1,nand(X2,X2)),
inference(orient,[status(thm)],[t135615]) ).
cnf(t3376,plain,
nand(X1,X1) = nand(X1,nand(nand(X2,X2),nand(X1,nand(X1,X2)))),
inference(cp,[status(thm)],[t3332,t3355]) ).
cnf(t3547,plain,
nand(X1,nand(nand(X2,X2),nand(X1,nand(X1,X2)))) = nand(X1,X1),
inference(orient,[status(thm)],[t3376]) ).
cnf(t3588,plain,
nand(nand(X1,X1),nand(X2,nand(X2,X1))) = nand(nand(X1,X1),nand(X2,X2)),
inference(cp,[status(thm)],[t3306,t3547]) ).
cnf(t135622,plain,
nand(nand(X1,X1),nand(X2,nand(X1,X1))) = nand(nand(X1,X1),nand(X2,X2)),
inference(step,[status(thm)],[t3588,t3355]) ).
cnf(t3589,plain,
nand(nand(X1,X1),nand(X2,nand(X1,X1))) = nand(nand(X1,X1),nand(X2,X2)),
inference(orient,[status(thm)],[t135622]) ).
cnf(t3628,plain,
nand(nand(X1,X1),nand(nand(X2,X2),nand(X1,X1))) = nand(nand(X1,X1),X2),
inference(cp,[status(thm)],[t3589,t3042]) ).
cnf(t135626,plain,
nand(nand(X1,X1),nand(nand(X1,X1),nand(X2,X2))) = nand(nand(X1,X1),X2),
inference(step,[status(thm)],[t3628,t3021]) ).
cnf(t135627,plain,
nand(nand(X1,X1),nand(nand(X1,X1),nand(X2,X2))) = nand(X2,nand(X1,X1)),
inference(step,[status(thm)],[t135626,t3021]) ).
cnf(t3689,plain,
nand(nand(X1,X1),nand(nand(X1,X1),nand(X2,X2))) = nand(X2,nand(X1,X1)),
inference(orient,[status(thm)],[t135627]) ).
cnf(t3691,plain,
nand(X1,nand(nand(X2,X2),nand(X2,X2))) = nand(X2,nand(nand(nand(X2,X2),nand(X2,X2)),nand(X1,X1))),
inference(cp,[status(thm)],[t3689,t3042]) ).
cnf(t135628,plain,
nand(X1,nand(X1,nand(X2,X2))) = nand(X2,nand(nand(nand(X2,X2),nand(X2,X2)),nand(X1,X1))),
inference(step,[status(thm)],[t3691,t3355]) ).
cnf(t135629,plain,
nand(X1,nand(X1,nand(X1,X2))) = nand(X2,nand(nand(nand(X2,X2),nand(X2,X2)),nand(X1,X1))),
inference(step,[status(thm)],[t135628,t3355]) ).
cnf(t163,plain,
nand(X1,nand(nand(X2,X1),X1)) = nand(nand(X2,nand(nand(nand(X1,nand(nand(X2,X1),X1)),X2),X2)),X2),
inference(cp,[status(thm)],[t1,t155]) ).
cnf(t562,plain,
nand(nand(X1,nand(nand(nand(X2,nand(nand(X1,X2),X2)),X1),X1)),X1) = nand(X2,nand(nand(X1,X2),X2)),
inference(orient,[status(thm)],[t163]) ).
cnf(t135597,plain,
nand(nand(X1,nand(X2,nand(nand(X1,X2),X2))),X1) = nand(X2,nand(nand(X1,X2),X2)),
inference(step,[status(thm)],[t562,t2998]) ).
cnf(t135598,plain,
nand(nand(X1,nand(X2,X1)),X1) = nand(X2,nand(nand(X1,X2),X2)),
inference(step,[status(thm)],[t135597,t2998]) ).
cnf(t135599,plain,
nand(nand(X1,nand(X2,X1)),X1) = nand(X2,X1),
inference(step,[status(thm)],[t135598,t2998]) ).
cnf(t3020,plain,
nand(nand(X1,nand(X2,X1)),X1) = nand(X2,X1),
inference(rw,[status(thm)],[t135599]) ).
cnf(t135600,plain,
nand(X1,nand(X1,nand(X2,X1))) = nand(X2,X1),
inference(step,[status(thm)],[t3020,t3021]) ).
cnf(t135601,plain,
nand(X1,nand(X1,nand(X1,X2))) = nand(X2,X1),
inference(step,[status(thm)],[t135600,t3021]) ).
cnf(t135602,plain,
nand(X1,nand(X1,nand(X1,X2))) = nand(X1,X2),
inference(step,[status(thm)],[t135601,t3021]) ).
cnf(t3067,plain,
nand(X1,nand(X1,nand(X1,X2))) = nand(X1,X2),
inference(orient,[status(thm)],[t135602]) ).
cnf(t135630,plain,
nand(X1,X2) = nand(X2,nand(nand(nand(X2,X2),nand(X2,X2)),nand(X1,X1))),
inference(step,[status(thm)],[t135629,t3067]) ).
cnf(t135631,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X1),nand(nand(X2,X2),nand(X2,X2)))),
inference(step,[status(thm)],[t135630,t3021]) ).
cnf(t135632,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X1),nand(nand(X2,X2),nand(X1,X1)))),
inference(step,[status(thm)],[t135631,t3589]) ).
cnf(t135633,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X1),nand(nand(X1,X1),nand(X2,X2)))),
inference(step,[status(thm)],[t135632,t3021]) ).
cnf(t135634,plain,
nand(X1,X2) = nand(X2,nand(X2,nand(X1,X1))),
inference(step,[status(thm)],[t135633,t3689]) ).
cnf(t3723,plain,
nand(X1,nand(X1,nand(X2,X2))) = nand(X2,X1),
inference(orient,[status(thm)],[t135634]) ).
cnf(t3744,plain,
nand(X1,nand(X1,nand(X2,X2))) = nand(nand(X1,nand(X2,X2)),nand(nand(X2,X1),nand(X1,X3))),
inference(cp,[status(thm)],[t3239,t3723]) ).
cnf(t135657,plain,
nand(X2,X1) = nand(nand(X1,nand(X2,X2)),nand(nand(X2,X1),nand(X1,X3))),
inference(step,[status(thm)],[t3744,t3723]) ).
cnf(t5922,plain,
nand(nand(X1,nand(X2,X2)),nand(nand(X2,X1),nand(X1,X3))) = nand(X2,X1),
inference(orient,[status(thm)],[t135657]) ).
cnf(t3245,plain,
nand(nand(X1,X2),nand(X1,nand(X2,X3))) = nand(nand(X1,nand(X2,X3)),nand(X1,nand(nand(X1,X2),Y3))),
inference(cp,[status(thm)],[t3239,t3127]) ).
cnf(t135636,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(nand(X1,X2),Y3))),
inference(step,[status(thm)],[t3245,t3127]) ).
cnf(t135637,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X1,X2)))),
inference(step,[status(thm)],[t135636,t3021]) ).
cnf(t3840,plain,
nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X1,X2)))) = X1,
inference(orient,[status(thm)],[t135637]) ).
cnf(t5930,plain,
nand(nand(X1,nand(X2,nand(X1,X2))),X3) = nand(nand(X3,X1),nand(nand(nand(X1,nand(X2,nand(X1,X2))),X3),nand(X3,Y3))),
inference(cp,[status(thm)],[t5922,t3840]) ).
cnf(t135701,plain,
nand(X3,nand(X1,nand(X2,nand(X1,X2)))) = nand(nand(X3,X1),nand(nand(nand(X1,nand(X2,nand(X1,X2))),X3),nand(X3,Y3))),
inference(step,[status(thm)],[t5930,t3021]) ).
cnf(t135702,plain,
nand(X3,nand(X1,X1)) = nand(nand(X3,X1),nand(nand(nand(X1,nand(X2,nand(X1,X2))),X3),nand(X3,Y3))),
inference(step,[status(thm)],[t135701,t3332]) ).
cnf(t135703,plain,
nand(X3,nand(X1,X1)) = nand(nand(X1,X3),nand(nand(nand(X1,nand(X2,nand(X1,X2))),X3),nand(X3,Y3))),
inference(step,[status(thm)],[t135702,t3021]) ).
cnf(t135704,plain,
nand(X3,nand(X1,X1)) = nand(nand(X1,X3),nand(nand(X3,Y3),nand(nand(X1,nand(X2,nand(X1,X2))),X3))),
inference(step,[status(thm)],[t135703,t3021]) ).
cnf(t135705,plain,
nand(X3,nand(X1,X1)) = nand(nand(X1,X3),nand(nand(X3,Y3),nand(X3,nand(X1,nand(X2,nand(X1,X2)))))),
inference(step,[status(thm)],[t135704,t3021]) ).
cnf(t135706,plain,
nand(X3,nand(X1,X1)) = nand(nand(X1,X3),nand(nand(X3,Y3),nand(X3,nand(X1,X1)))),
inference(step,[status(thm)],[t135705,t3332]) ).
cnf(t9687,plain,
nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,nand(X1,X1)))) = nand(X2,nand(X1,X1)),
inference(orient,[status(thm)],[t135706]) ).
cnf(t3350,plain,
X1 = nand(nand(X1,nand(X2,nand(X3,X2))),nand(X1,nand(X3,X3))),
inference(cp,[status(thm)],[t3167,t3332]) ).
cnf(t135641,plain,
X1 = nand(nand(X1,nand(X3,X3)),nand(X1,nand(X2,nand(X3,X2)))),
inference(step,[status(thm)],[t3350,t3021]) ).
cnf(t135642,plain,
X1 = nand(nand(X1,nand(X1,X3)),nand(X1,nand(X2,nand(X3,X2)))),
inference(step,[status(thm)],[t135641,t3355]) ).
cnf(t135643,plain,
X1 = nand(nand(X1,nand(X1,X3)),nand(X1,nand(X2,nand(X2,X3)))),
inference(step,[status(thm)],[t135642,t3021]) ).
cnf(t4267,plain,
nand(nand(X1,nand(X1,X2)),nand(X1,nand(X3,nand(X3,X2)))) = X1,
inference(orient,[status(thm)],[t135643]) ).
cnf(t4273,plain,
X1 = nand(nand(X1,X2),nand(X1,nand(X3,nand(X3,nand(X1,X2))))),
inference(cp,[status(thm)],[t4267,t3067]) ).
cnf(t4525,plain,
nand(nand(X1,X2),nand(X1,nand(X3,nand(X3,nand(X1,X2))))) = X1,
inference(orient,[status(thm)],[t4273]) ).
cnf(t4598,plain,
nand(X1,X2) = nand(nand(nand(X1,X2),nand(X3,nand(X3,nand(X1,X2)))),X1),
inference(cp,[status(thm)],[t3167,t4525]) ).
cnf(t135658,plain,
nand(X1,X2) = nand(X1,nand(nand(X1,X2),nand(X3,nand(X3,nand(X1,X2))))),
inference(step,[status(thm)],[t4598,t3021]) ).
cnf(t6078,plain,
nand(X1,nand(nand(X1,X2),nand(X3,nand(X3,nand(X1,X2))))) = nand(X1,X2),
inference(orient,[status(thm)],[t135658]) ).
cnf(t6140,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(nand(X1,nand(X2,X3)),nand(nand(X2,X1),X1))),
inference(cp,[status(thm)],[t6078,t3094]) ).
cnf(t135707,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(nand(X1,nand(X2,X3)),nand(X1,nand(X2,X1)))),
inference(step,[status(thm)],[t6140,t3021]) ).
cnf(t135708,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(nand(X1,nand(X2,X1)),nand(X1,nand(X2,X3)))),
inference(step,[status(thm)],[t135707,t3021]) ).
cnf(t135709,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(nand(X1,nand(X1,X2)),nand(X1,nand(X2,X3)))),
inference(step,[status(thm)],[t135708,t3021]) ).
cnf(t10234,plain,
nand(X1,nand(nand(X1,nand(X1,X2)),nand(X1,nand(X2,X3)))) = nand(X1,nand(X2,X3)),
inference(orient,[status(thm)],[t135709]) ).
cnf(t3183,plain,
nand(X1,X2) = nand(nand(nand(X1,X2),nand(X2,X3)),X1),
inference(cp,[status(thm)],[t3167,t3127]) ).
cnf(t135610,plain,
nand(X1,X2) = nand(X1,nand(nand(X1,X2),nand(X2,X3))),
inference(step,[status(thm)],[t3183,t3021]) ).
cnf(t3272,plain,
nand(X1,nand(nand(X1,X2),nand(X2,X3))) = nand(X1,X2),
inference(orient,[status(thm)],[t135610]) ).
cnf(t3280,plain,
nand(nand(X1,X2),nand(X1,nand(X2,X3))) = nand(nand(X1,X2),nand(X1,nand(nand(X1,nand(X2,X3)),Y3))),
inference(cp,[status(thm)],[t3272,t3127]) ).
cnf(t135639,plain,
X1 = nand(nand(X1,X2),nand(X1,nand(nand(X1,nand(X2,X3)),Y3))),
inference(step,[status(thm)],[t3280,t3127]) ).
cnf(t135640,plain,
X1 = nand(nand(X1,X2),nand(X1,nand(Y3,nand(X1,nand(X2,X3))))),
inference(step,[status(thm)],[t135639,t3021]) ).
cnf(t4170,plain,
nand(nand(X1,X2),nand(X1,nand(X3,nand(X1,nand(X2,Y3))))) = X1,
inference(orient,[status(thm)],[t135640]) ).
cnf(t10243,plain,
nand(X1,nand(X2,nand(X1,nand(nand(X1,X2),X3)))) = nand(X1,X1),
inference(cp,[status(thm)],[t10234,t4170]) ).
cnf(t135710,plain,
nand(X1,nand(X2,nand(X1,nand(X3,nand(X1,X2))))) = nand(X1,X1),
inference(step,[status(thm)],[t10243,t3021]) ).
cnf(t10901,plain,
nand(X1,nand(X2,nand(X1,nand(X3,nand(X1,X2))))) = nand(X1,X1),
inference(orient,[status(thm)],[t135710]) ).
cnf(t11032,plain,
nand(X1,nand(X2,nand(X3,nand(X2,X1)))) = nand(X1,nand(X2,X2)),
inference(cp,[status(thm)],[t3306,t10901]) ).
cnf(t135711,plain,
nand(X1,nand(X2,nand(X3,nand(X1,X2)))) = nand(X1,nand(X2,X2)),
inference(step,[status(thm)],[t11032,t3021]) ).
cnf(t135712,plain,
nand(X1,nand(X2,nand(X3,nand(X1,X2)))) = nand(X1,nand(X1,X2)),
inference(step,[status(thm)],[t135711,t3355]) ).
cnf(t11049,plain,
nand(X1,nand(X2,nand(X3,nand(X1,X2)))) = nand(X1,nand(X1,X2)),
inference(orient,[status(thm)],[t135712]) ).
cnf(t11167,plain,
nand(nand(X1,X2),nand(nand(X1,X2),nand(X2,nand(X1,X3)))) = nand(nand(X1,X2),nand(nand(X2,nand(X1,X3)),nand(Y3,X2))),
inference(cp,[status(thm)],[t11049,t3094]) ).
cnf(t135792,plain,
nand(nand(X1,X2),X2) = nand(nand(X1,X2),nand(nand(X2,nand(X1,X3)),nand(Y3,X2))),
inference(step,[status(thm)],[t11167,t3094]) ).
cnf(t135793,plain,
nand(X2,nand(X1,X2)) = nand(nand(X1,X2),nand(nand(X2,nand(X1,X3)),nand(Y3,X2))),
inference(step,[status(thm)],[t135792,t3021]) ).
cnf(t135794,plain,
nand(X2,nand(X1,X2)) = nand(nand(X1,X2),nand(nand(Y3,X2),nand(X2,nand(X1,X3)))),
inference(step,[status(thm)],[t135793,t3021]) ).
cnf(t135795,plain,
nand(X2,nand(X1,X2)) = nand(nand(X1,X2),nand(nand(X2,Y3),nand(X2,nand(X1,X3)))),
inference(step,[status(thm)],[t135794,t3021]) ).
cnf(t23119,plain,
nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,nand(X1,Y3)))) = nand(X2,nand(X1,X2)),
inference(orient,[status(thm)],[t135795]) ).
cnf(t135796,plain,
nand(X2,nand(X1,X2)) = nand(X2,nand(X1,X1)),
inference(step,[status(thm)],[t9687,t23119]) ).
cnf(t23604,plain,
nand(X2,nand(X1,X2)) = nand(X2,nand(X1,X1)),
inference(rw,[status(thm)],[t135796]) ).
cnf(t23605,plain,
nand(X1,nand(X2,X1)) = nand(X1,nand(X2,X2)),
inference(orient,[status(thm)],[t23604]) ).
cnf(t3274,plain,
nand(X1,nand(nand(X2,X1),nand(X2,X3))) = nand(X1,nand(nand(X2,X1),nand(nand(nand(X2,X1),nand(X2,X3)),Y3))),
inference(cp,[status(thm)],[t3272,t3239]) ).
cnf(t45849,plain,
nand(X1,nand(nand(X2,X1),nand(X3,nand(nand(X2,X1),nand(X2,Y3))))) = nand(X2,X1),
inference(orient,[status(thm)],[t3274]) ).
cnf(t11170,plain,
nand(nand(X1,X1),nand(nand(X1,X1),nand(X1,X2))) = nand(nand(X1,X1),nand(nand(X1,X2),nand(X3,X1))),
inference(cp,[status(thm)],[t11049,t2584]) ).
cnf(t135713,plain,
nand(nand(X1,X1),X1) = nand(nand(X1,X1),nand(nand(X1,X2),nand(X3,X1))),
inference(step,[status(thm)],[t11170,t2584]) ).
cnf(t135714,plain,
nand(X1,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X1,X2),nand(X3,X1))),
inference(step,[status(thm)],[t135713,t3021]) ).
cnf(t135715,plain,
nand(X1,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X1,X2),nand(X1,X3))),
inference(step,[status(thm)],[t135714,t3021]) ).
cnf(t11286,plain,
nand(nand(X1,X1),nand(nand(X1,X2),nand(X1,X3))) = nand(X1,nand(X1,X1)),
inference(orient,[status(thm)],[t135715]) ).
cnf(t11396,plain,
nand(nand(X1,X1),nand(nand(nand(X1,X2),nand(X1,X3)),Y3)) = nand(nand(X1,X1),nand(nand(nand(X1,X1),nand(X1,nand(X1,X1))),nand(nand(X1,X1),nand(nand(nand(X1,X2),nand(X1,X3)),Y3)))),
inference(cp,[status(thm)],[t10234,t11286]) ).
cnf(t135716,plain,
nand(nand(X1,X1),nand(Y3,nand(nand(X1,X2),nand(X1,X3)))) = nand(nand(X1,X1),nand(nand(nand(X1,X1),nand(X1,nand(X1,X1))),nand(nand(X1,X1),nand(nand(nand(X1,X2),nand(X1,X3)),Y3)))),
inference(step,[status(thm)],[t11396,t3021]) ).
cnf(t135717,plain,
nand(nand(X1,X1),nand(Y3,nand(nand(X1,X2),nand(X1,X3)))) = nand(nand(X1,X1),nand(X1,nand(nand(X1,X1),nand(nand(nand(X1,X2),nand(X1,X3)),Y3)))),
inference(step,[status(thm)],[t135716,t3094]) ).
cnf(t3883,plain,
nand(X1,X1) = nand(nand(nand(X1,X1),nand(X2,X3)),X1),
inference(cp,[status(thm)],[t3840,t2584]) ).
cnf(t135638,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,X1),nand(X2,X3))),
inference(step,[status(thm)],[t3883,t3021]) ).
cnf(t3987,plain,
nand(X1,nand(nand(X1,X1),nand(X2,X3))) = nand(X1,X1),
inference(orient,[status(thm)],[t135638]) ).
cnf(t135718,plain,
nand(nand(X1,X1),nand(Y3,nand(nand(X1,X2),nand(X1,X3)))) = nand(nand(X1,X1),nand(X1,X1)),
inference(step,[status(thm)],[t135717,t3987]) ).
cnf(t135719,plain,
nand(nand(X1,X1),nand(Y3,nand(nand(X1,X2),nand(X1,X3)))) = X1,
inference(step,[status(thm)],[t135718,t3042]) ).
cnf(t11503,plain,
nand(nand(X1,X1),nand(X2,nand(nand(X1,X3),nand(X1,Y3)))) = X1,
inference(orient,[status(thm)],[t135719]) ).
cnf(t11516,plain,
X1 = nand(nand(X1,X1),nand(X2,nand(X2,nand(X1,X3)))),
inference(cp,[status(thm)],[t11503,t11049]) ).
cnf(t11743,plain,
nand(nand(X1,X1),nand(X2,nand(X2,nand(X1,X3)))) = X1,
inference(orient,[status(thm)],[t11516]) ).
cnf(t11854,plain,
X1 = nand(nand(X1,nand(X2,nand(X2,nand(X3,Y3)))),nand(X1,X3)),
inference(cp,[status(thm)],[t3167,t11743]) ).
cnf(t135723,plain,
X1 = nand(nand(X1,X3),nand(X1,nand(X2,nand(X2,nand(X3,Y3))))),
inference(step,[status(thm)],[t11854,t3021]) ).
cnf(t12117,plain,
nand(nand(X1,X2),nand(X1,nand(X3,nand(X3,nand(X2,Y3))))) = X1,
inference(orient,[status(thm)],[t135723]) ).
cnf(t12246,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(Y3,X2)))),
inference(cp,[status(thm)],[t12117,t4525]) ).
cnf(t135730,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X2,X2)))),
inference(step,[status(thm)],[t12246,t3355]) ).
cnf(t12898,plain,
nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X2,X2)))) = X1,
inference(orient,[status(thm)],[t135730]) ).
cnf(t3378,plain,
nand(X1,nand(X2,X2)) = nand(nand(X2,X2),nand(nand(X1,nand(X1,X2)),nand(X1,X3))),
inference(cp,[status(thm)],[t3239,t3355]) ).
cnf(t135675,plain,
nand(X1,nand(X1,X2)) = nand(nand(X2,X2),nand(nand(X1,nand(X1,X2)),nand(X1,X3))),
inference(step,[status(thm)],[t3378,t3355]) ).
cnf(t135676,plain,
nand(X1,nand(X1,X2)) = nand(nand(X2,X2),nand(nand(X1,X3),nand(X1,nand(X1,X2)))),
inference(step,[status(thm)],[t135675,t3021]) ).
cnf(t7630,plain,
nand(nand(X1,X1),nand(nand(X2,X3),nand(X2,nand(X2,X1)))) = nand(X2,nand(X2,X1)),
inference(orient,[status(thm)],[t135676]) ).
cnf(t12962,plain,
X1 = nand(nand(X1,nand(X2,nand(X2,X3))),nand(X1,nand(Y3,nand(nand(X3,X3),nand(X3,X3))))),
inference(cp,[status(thm)],[t12898,t7630]) ).
cnf(t135733,plain,
X1 = nand(nand(X1,nand(X2,nand(X2,X3))),nand(X1,nand(Y3,nand(Y3,nand(X3,X3))))),
inference(step,[status(thm)],[t12962,t3355]) ).
cnf(t135734,plain,
X1 = nand(nand(X1,nand(X2,nand(X2,X3))),nand(X1,nand(X3,Y3))),
inference(step,[status(thm)],[t135733,t3723]) ).
cnf(t135735,plain,
X1 = nand(nand(X1,nand(X3,Y3)),nand(X1,nand(X2,nand(X2,X3)))),
inference(step,[status(thm)],[t135734,t3021]) ).
cnf(t13869,plain,
nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(Y3,X2)))) = X1,
inference(orient,[status(thm)],[t135735]) ).
cnf(t46004,plain,
nand(X1,nand(X2,X3)) = nand(nand(X2,X3),nand(nand(X1,nand(X2,X3)),nand(Y3,X1))),
inference(cp,[status(thm)],[t45849,t13869]) ).
cnf(t135923,plain,
nand(X1,nand(X2,X3)) = nand(nand(X2,X3),nand(nand(Y3,X1),nand(X1,nand(X2,X3)))),
inference(step,[status(thm)],[t46004,t3021]) ).
cnf(t135924,plain,
nand(X1,nand(X2,X3)) = nand(nand(X2,X3),nand(nand(X1,Y3),nand(X1,nand(X2,X3)))),
inference(step,[status(thm)],[t135923,t3021]) ).
cnf(t46427,plain,
nand(nand(X1,X2),nand(nand(X3,Y3),nand(X3,nand(X1,X2)))) = nand(X3,nand(X1,X2)),
inference(orient,[status(thm)],[t135924]) ).
cnf(t3260,plain,
X1 = nand(nand(X2,X1),nand(X1,nand(X3,nand(nand(X2,X1),nand(X2,Y3))))),
inference(cp,[status(thm)],[t3167,t3239]) ).
cnf(t135845,plain,
X1 = nand(nand(X1,X2),nand(X1,nand(X3,nand(nand(X2,X1),nand(X2,Y3))))),
inference(step,[status(thm)],[t3260,t3021]) ).
cnf(t135846,plain,
X1 = nand(nand(X1,X2),nand(X1,nand(X3,nand(nand(X1,X2),nand(X2,Y3))))),
inference(step,[status(thm)],[t135845,t3021]) ).
cnf(t30546,plain,
nand(nand(X1,X2),nand(X1,nand(X3,nand(nand(X1,X2),nand(X2,Y3))))) = X1,
inference(orient,[status(thm)],[t135846]) ).
cnf(t46558,plain,
nand(nand(X1,X2),nand(X3,Y3)) = nand(nand(X3,Y3),nand(X1,nand(nand(X1,X2),nand(X3,Y3)))),
inference(cp,[status(thm)],[t46427,t30546]) ).
cnf(t46996,plain,
nand(nand(X1,X2),nand(X3,nand(nand(X3,Y3),nand(X1,X2)))) = nand(nand(X3,Y3),nand(X1,X2)),
inference(orient,[status(thm)],[t46558]) ).
cnf(t135797,plain,
nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,nand(X1,Y3)))) = nand(X2,nand(X1,X1)),
inference(step,[status(thm)],[t23119,t23605]) ).
cnf(t23606,plain,
nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,nand(X1,Y3)))) = nand(X2,nand(X1,X1)),
inference(orient,[status(thm)],[t135797]) ).
cnf(t47119,plain,
nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,nand(X1,Y3)))) = nand(nand(nand(X2,X3),nand(X2,nand(X1,Y3))),nand(X1,nand(X2,nand(X1,X1)))),
inference(cp,[status(thm)],[t46996,t23606]) ).
cnf(t47538,plain,
nand(nand(X1,X1),nand(nand(X2,X3),nand(X2,nand(X1,Y3)))) = nand(X2,nand(X2,X1)),
inference(orient,[status(thm)],[t47119]) ).
cnf(t47580,plain,
nand(X1,nand(X1,nand(X2,X2))) = nand(X2,nand(nand(X1,X3),nand(X1,nand(nand(X2,X2),Y3)))),
inference(cp,[status(thm)],[t47538,t3042]) ).
cnf(t48187,plain,
nand(X1,nand(nand(X2,X3),nand(X2,nand(Y3,nand(X1,X1))))) = nand(X1,X2),
inference(orient,[status(thm)],[t47580]) ).
cnf(t48255,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(X2,nand(nand(X2,X3),nand(Y3,nand(X1,X1))))),
inference(cp,[status(thm)],[t48187,t30546]) ).
cnf(t49279,plain,
nand(X1,nand(X2,nand(nand(X2,X3),nand(Y3,nand(X1,X1))))) = nand(X1,nand(X2,X3)),
inference(orient,[status(thm)],[t48255]) ).
cnf(t12251,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(Y3,X3)))),
inference(cp,[status(thm)],[t12117,t3042]) ).
cnf(t135731,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X3,X3)))),
inference(step,[status(thm)],[t12251,t3355]) ).
cnf(t13258,plain,
nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X3,X3)))) = X1,
inference(orient,[status(thm)],[t135731]) ).
cnf(t13492,plain,
nand(X1,nand(X2,X3)) = nand(nand(nand(X1,nand(X2,X3)),nand(Y3,nand(X3,X3))),X1),
inference(cp,[status(thm)],[t3167,t13258]) ).
cnf(t135812,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(nand(X1,nand(X2,X3)),nand(Y3,nand(X3,X3)))),
inference(step,[status(thm)],[t13492,t3021]) ).
cnf(t26553,plain,
nand(X1,nand(nand(X1,nand(X2,X3)),nand(Y3,nand(X3,X3)))) = nand(X1,nand(X2,X3)),
inference(orient,[status(thm)],[t135812]) ).
cnf(t49347,plain,
nand(nand(X1,X1),nand(X2,X3)) = nand(nand(X1,X1),nand(X2,nand(nand(X2,X3),nand(Y3,X1)))),
inference(cp,[status(thm)],[t49279,t26553]) ).
cnf(t135947,plain,
nand(nand(X1,X1),nand(X2,X3)) = nand(nand(X1,X1),nand(X2,nand(nand(X2,X3),nand(X1,Y3)))),
inference(step,[status(thm)],[t49347,t3021]) ).
cnf(t135948,plain,
nand(nand(X1,X1),nand(X2,X3)) = nand(nand(X1,X1),nand(X2,nand(nand(X1,Y3),nand(X2,X3)))),
inference(step,[status(thm)],[t135947,t3021]) ).
cnf(t53927,plain,
nand(nand(X1,X1),nand(X2,nand(nand(X1,X3),nand(X2,Y3)))) = nand(nand(X1,X1),nand(X2,Y3)),
inference(orient,[status(thm)],[t135948]) ).
cnf(t13086,plain,
nand(X1,nand(X2,X3)) = nand(nand(nand(X1,nand(X2,X3)),nand(Y3,nand(X2,X2))),X1),
inference(cp,[status(thm)],[t3167,t12898]) ).
cnf(t135811,plain,
nand(X1,nand(X2,X3)) = nand(X1,nand(nand(X1,nand(X2,X3)),nand(Y3,nand(X2,X2)))),
inference(step,[status(thm)],[t13086,t3021]) ).
cnf(t26264,plain,
nand(X1,nand(nand(X1,nand(X2,X3)),nand(Y3,nand(X2,X2)))) = nand(X1,nand(X2,X3)),
inference(orient,[status(thm)],[t135811]) ).
cnf(t135569,plain,
nand(X1,nand(nand(X3,nand(nand(X1,X3),X3)),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X3,nand(nand(X1,X3),X3)),
inference(step,[status(thm)],[t2166,t2808]) ).
cnf(t2842,plain,
nand(X1,nand(nand(X3,nand(nand(X1,X3),X3)),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X3,nand(nand(X1,X3),X3)),
inference(rw,[status(thm)],[t135569]) ).
cnf(t135650,plain,
nand(X1,nand(nand(X3,nand(X3,nand(X1,X3))),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X3,nand(nand(X1,X3),X3)),
inference(step,[status(thm)],[t2842,t3021]) ).
cnf(t3050,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X2),nand(nand(X1,X2),nand(X2,X2)))),
inference(cp,[status(thm)],[t2808,t3042]) ).
cnf(t135603,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X2),X2)),
inference(step,[status(thm)],[t3050,t3042]) ).
cnf(t135604,plain,
nand(X1,X2) = nand(X2,nand(X2,nand(X1,X2))),
inference(step,[status(thm)],[t135603,t3021]) ).
cnf(t3074,plain,
nand(X1,nand(X1,nand(X2,X1))) = nand(X2,X1),
inference(orient,[status(thm)],[t135604]) ).
cnf(t135651,plain,
nand(X1,nand(nand(X1,X3),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X3,nand(nand(X1,X3),X3)),
inference(step,[status(thm)],[t135650,t3074]) ).
cnf(t135652,plain,
nand(X1,nand(nand(X1,X3),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X3,nand(X3,nand(X1,X3))),
inference(step,[status(thm)],[t135651,t3021]) ).
cnf(t135653,plain,
nand(X1,nand(nand(X1,X3),nand(Y3,nand(X1,nand(X2,X3))))) = nand(X1,X3),
inference(step,[status(thm)],[t135652,t3074]) ).
cnf(t5361,plain,
nand(X1,nand(nand(X1,X2),nand(X3,nand(X1,nand(Y3,X2))))) = nand(X1,X2),
inference(orient,[status(thm)],[t135653]) ).
cnf(t11033,plain,
nand(X1,nand(X2,nand(X3,X1))) = nand(X1,nand(nand(X1,nand(X2,nand(X3,X1))),nand(X3,X3))),
inference(cp,[status(thm)],[t5361,t10901]) ).
cnf(t135895,plain,
nand(X1,nand(X2,nand(X1,X3))) = nand(X1,nand(nand(X1,nand(X2,nand(X3,X1))),nand(X3,X3))),
inference(step,[status(thm)],[t11033,t3021]) ).
cnf(t135896,plain,
nand(X1,nand(X2,nand(X1,X3))) = nand(X1,nand(nand(X3,X3),nand(X1,nand(X2,nand(X3,X1))))),
inference(step,[status(thm)],[t135895,t3021]) ).
cnf(t135897,plain,
nand(X1,nand(X2,nand(X1,X3))) = nand(X1,nand(nand(X3,X3),nand(X1,nand(X2,nand(X1,X3))))),
inference(step,[status(thm)],[t135896,t3021]) ).
cnf(t39876,plain,
nand(X1,nand(nand(X2,X2),nand(X1,nand(X3,nand(X1,X2))))) = nand(X1,nand(X3,nand(X1,X2))),
inference(orient,[status(thm)],[t135897]) ).
cnf(t40167,plain,
nand(X1,nand(nand(X2,X2),nand(X1,nand(X3,nand(X1,X2))))) = nand(X1,nand(nand(X1,nand(X3,nand(X1,X2))),nand(Y3,nand(nand(X2,X2),nand(X2,X2))))),
inference(cp,[status(thm)],[t26264,t39876]) ).
cnf(t135915,plain,
nand(X1,nand(X3,nand(X1,X2))) = nand(X1,nand(nand(X1,nand(X3,nand(X1,X2))),nand(Y3,nand(nand(X2,X2),nand(X2,X2))))),
inference(step,[status(thm)],[t40167,t39876]) ).
cnf(t135916,plain,
nand(X1,nand(X3,nand(X1,X2))) = nand(X1,nand(nand(X1,nand(X3,nand(X1,X2))),nand(Y3,nand(nand(X2,X2),Y3)))),
inference(step,[status(thm)],[t135915,t23605]) ).
cnf(t135917,plain,
nand(X1,nand(X3,nand(X1,X2))) = nand(X1,nand(nand(X1,nand(X3,nand(X1,X2))),nand(Y3,nand(Y3,nand(X2,X2))))),
inference(step,[status(thm)],[t135916,t3021]) ).
cnf(t23680,plain,
nand(X1,X2) = nand(X2,nand(X2,nand(X1,X1))),
inference(cp,[status(thm)],[t3074,t23605]) ).
cnf(t23956,plain,
nand(X1,nand(X1,nand(X2,X2))) = nand(X2,X1),
inference(orient,[status(thm)],[t23680]) ).
cnf(t135918,plain,
nand(X1,nand(X3,nand(X1,X2))) = nand(X1,nand(nand(X1,nand(X3,nand(X1,X2))),nand(X2,Y3))),
inference(step,[status(thm)],[t135917,t23956]) ).
cnf(t135919,plain,
nand(X1,nand(X3,nand(X1,X2))) = nand(X1,nand(nand(X2,Y3),nand(X1,nand(X3,nand(X1,X2))))),
inference(step,[status(thm)],[t135918,t3021]) ).
cnf(t44549,plain,
nand(X1,nand(nand(X2,X3),nand(X1,nand(Y3,nand(X1,X2))))) = nand(X1,nand(Y3,nand(X1,X2))),
inference(orient,[status(thm)],[t135919]) ).
cnf(t11833,plain,
nand(X1,X2) = nand(nand(nand(X1,X2),nand(X1,X2)),nand(X3,nand(X3,X2))),
inference(cp,[status(thm)],[t11743,t3042]) ).
cnf(t135750,plain,
nand(X1,X2) = nand(nand(X3,nand(X3,X2)),nand(nand(X1,X2),nand(X1,X2))),
inference(step,[status(thm)],[t11833,t3021]) ).
cnf(t135751,plain,
nand(X1,X2) = nand(nand(X3,nand(X2,X2)),nand(nand(X1,X2),nand(X1,X2))),
inference(step,[status(thm)],[t135750,t3355]) ).
cnf(t17272,plain,
nand(nand(X1,nand(X2,X2)),nand(nand(X3,X2),nand(X3,X2))) = nand(X3,X2),
inference(orient,[status(thm)],[t135751]) ).
cnf(t23944,plain,
nand(nand(X1,nand(X2,X2)),nand(nand(X3,X2),nand(X3,X2))) = nand(X3,X2),
inference(rw,[status(thm)],[t17272]) ).
cnf(t135806,plain,
nand(nand(X1,nand(X2,X1)),nand(nand(X3,X2),nand(X3,X2))) = nand(X3,X2),
inference(step,[status(thm)],[t23944,t23605]) ).
cnf(t135807,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X3,X2),nand(X3,X2))) = nand(X3,X2),
inference(step,[status(thm)],[t135806,t3021]) ).
cnf(t135808,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X2,X3),nand(X3,X2))) = nand(X3,X2),
inference(step,[status(thm)],[t135807,t3021]) ).
cnf(t135809,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X2,X3),nand(X2,X3))) = nand(X3,X2),
inference(step,[status(thm)],[t135808,t3021]) ).
cnf(t135810,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X2,X3),nand(X2,X3))) = nand(X2,X3),
inference(step,[status(thm)],[t135809,t3021]) ).
cnf(t25148,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X2,X3),nand(X2,X3))) = nand(X2,X3),
inference(orient,[status(thm)],[t135810]) ).
cnf(t25396,plain,
nand(X1,nand(X1,X2)) = nand(nand(X2,X3),nand(nand(X1,nand(X1,X2)),nand(Y3,nand(nand(X2,X3),nand(X2,X3))))),
inference(cp,[status(thm)],[t3167,t25148]) ).
cnf(t12301,plain,
nand(X1,nand(X2,nand(X2,nand(nand(X1,X2),X3)))) = nand(X1,X1),
inference(cp,[status(thm)],[t10234,t12117]) ).
cnf(t135724,plain,
nand(X1,nand(X2,nand(X2,nand(X3,nand(X1,X2))))) = nand(X1,X1),
inference(step,[status(thm)],[t12301,t3021]) ).
cnf(t12417,plain,
nand(X1,nand(X2,nand(X2,nand(X3,nand(X1,X2))))) = nand(X1,X1),
inference(orient,[status(thm)],[t135724]) ).
cnf(t11749,plain,
nand(X1,nand(X2,nand(X1,X2))) = nand(X1,nand(X3,nand(X3,nand(nand(X1,nand(X2,nand(X1,X2))),Y3)))),
inference(cp,[status(thm)],[t11743,t3840]) ).
cnf(t135720,plain,
nand(X1,X1) = nand(X1,nand(X3,nand(X3,nand(nand(X1,nand(X2,nand(X1,X2))),Y3)))),
inference(step,[status(thm)],[t11749,t3332]) ).
cnf(t135721,plain,
nand(X1,X1) = nand(X1,nand(X3,nand(X3,nand(Y3,nand(X1,nand(X2,nand(X1,X2))))))),
inference(step,[status(thm)],[t135720,t3021]) ).
cnf(t135722,plain,
nand(X1,X1) = nand(X1,nand(X3,nand(X3,nand(Y3,nand(X1,X1))))),
inference(step,[status(thm)],[t135721,t3332]) ).
cnf(t11971,plain,
nand(X1,nand(X2,nand(X2,nand(X3,nand(X1,X1))))) = nand(X1,X1),
inference(orient,[status(thm)],[t135722]) ).
cnf(t12437,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,nand(X2,nand(X3,X3))),nand(nand(X1,nand(X2,nand(X3,X3))),nand(X3,X3)))),
inference(cp,[status(thm)],[t12417,t11971]) ).
cnf(t135725,plain,
nand(X1,X1) = nand(X1,nand(X3,nand(X1,nand(X2,nand(X3,X3))))),
inference(step,[status(thm)],[t12437,t3723]) ).
cnf(t12626,plain,
nand(X1,nand(X2,nand(X1,nand(X3,nand(X2,X2))))) = nand(X1,X1),
inference(orient,[status(thm)],[t135725]) ).
cnf(t12721,plain,
nand(X1,nand(X2,nand(X3,nand(X1,X1)))) = nand(X1,nand(X2,X2)),
inference(cp,[status(thm)],[t3306,t12626]) ).
cnf(t135736,plain,
nand(X1,nand(X2,nand(X3,nand(X1,X1)))) = nand(X1,nand(X1,X2)),
inference(step,[status(thm)],[t12721,t3355]) ).
cnf(t15634,plain,
nand(X1,nand(X2,nand(X3,nand(X1,X1)))) = nand(X1,nand(X1,X2)),
inference(orient,[status(thm)],[t135736]) ).
cnf(t135825,plain,
nand(X1,nand(X1,X2)) = nand(nand(X2,X3),nand(nand(X2,X3),nand(X1,nand(X1,X2)))),
inference(step,[status(thm)],[t25396,t15634]) ).
cnf(t28533,plain,
nand(nand(X1,X2),nand(nand(X1,X2),nand(X3,nand(X3,X1)))) = nand(X3,nand(X3,X1)),
inference(orient,[status(thm)],[t135825]) ).
cnf(t28559,plain,
nand(X1,nand(X1,nand(X2,X3))) = nand(X2,nand(nand(nand(X2,X3),nand(X2,nand(Y3,nand(Y3,nand(X2,X3))))),nand(X1,nand(X1,nand(X2,X3))))),
inference(cp,[status(thm)],[t28533,t4525]) ).
cnf(t135826,plain,
nand(X1,nand(X1,nand(X2,X3))) = nand(X2,nand(nand(X1,nand(X1,nand(X2,X3))),nand(nand(X2,X3),nand(X2,nand(Y3,nand(Y3,nand(X2,X3))))))),
inference(step,[status(thm)],[t28559,t3021]) ).
cnf(t135827,plain,
nand(X1,nand(X1,nand(X2,X3))) = nand(X2,nand(nand(X1,nand(X1,nand(X2,X3))),X2)),
inference(step,[status(thm)],[t135826,t4525]) ).
cnf(t135828,plain,
nand(X1,nand(X1,nand(X2,X3))) = nand(X2,nand(X2,nand(X1,nand(X1,nand(X2,X3))))),
inference(step,[status(thm)],[t135827,t3021]) ).
cnf(t28936,plain,
nand(X1,nand(X1,nand(X2,nand(X2,nand(X1,X3))))) = nand(X2,nand(X2,nand(X1,X3))),
inference(orient,[status(thm)],[t135828]) ).
cnf(t12663,plain,
nand(X1,X1) = nand(X1,nand(nand(X2,nand(X3,nand(X2,X3))),nand(X1,nand(Y3,X2)))),
inference(cp,[status(thm)],[t12626,t3840]) ).
cnf(t135726,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,nand(Y3,X2)),nand(X2,nand(X3,nand(X2,X3))))),
inference(step,[status(thm)],[t12663,t3021]) ).
cnf(t135727,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,nand(X2,Y3)),nand(X2,nand(X3,nand(X2,X3))))),
inference(step,[status(thm)],[t135726,t3021]) ).
cnf(t135728,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,nand(X2,Y3)),nand(X2,X2))),
inference(step,[status(thm)],[t135727,t3332]) ).
cnf(t135729,plain,
nand(X1,X1) = nand(X1,nand(nand(X2,X2),nand(X1,nand(X2,Y3)))),
inference(step,[status(thm)],[t135728,t3021]) ).
cnf(t12737,plain,
nand(X1,nand(nand(X2,X2),nand(X1,nand(X2,X3)))) = nand(X1,X1),
inference(orient,[status(thm)],[t135729]) ).
cnf(t12827,plain,
nand(X1,X1) = nand(X1,nand(nand(nand(X2,X3),nand(X2,X3)),nand(X1,X3))),
inference(cp,[status(thm)],[t12737,t3042]) ).
cnf(t135754,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,X3),nand(nand(X2,X3),nand(X2,X3)))),
inference(step,[status(thm)],[t12827,t3021]) ).
cnf(t135755,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,X3),nand(nand(X1,X3),nand(X2,X3)))),
inference(step,[status(thm)],[t135754,t3355]) ).
cnf(t17887,plain,
nand(X1,nand(nand(X1,X2),nand(nand(X1,X2),nand(X3,X2)))) = nand(X1,X1),
inference(orient,[status(thm)],[t135755]) ).
cnf(t18028,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,nand(X2,nand(X2,nand(X3,nand(Y3,X2))))),nand(nand(X1,nand(X2,nand(X2,nand(X3,nand(Y3,X2))))),nand(Y3,Y3)))),
inference(cp,[status(thm)],[t17887,t12417]) ).
cnf(t135986,plain,
nand(X1,X1) = nand(X1,nand(Y3,nand(X1,nand(X2,nand(X2,nand(X3,nand(Y3,X2))))))),
inference(step,[status(thm)],[t18028,t23956]) ).
cnf(t62410,plain,
nand(X1,nand(X2,nand(X1,nand(X3,nand(X3,nand(Y3,nand(X2,X3))))))) = nand(X1,X1),
inference(orient,[status(thm)],[t135986]) ).
cnf(t62723,plain,
nand(X1,nand(X2,nand(X3,nand(X3,nand(Y3,nand(X1,X3)))))) = nand(nand(X2,X2),nand(nand(X1,nand(X2,nand(X3,nand(X3,nand(Y3,nand(X1,X3)))))),nand(X1,nand(X2,nand(X3,nand(X3,nand(Y3,nand(X1,X3)))))))),
inference(cp,[status(thm)],[t3042,t62410]) ).
cnf(t135987,plain,
nand(X1,nand(X2,nand(X3,nand(X3,nand(Y3,nand(X1,X3)))))) = nand(X1,nand(X1,X2)),
inference(step,[status(thm)],[t62723,t47538]) ).
cnf(t62919,plain,
nand(X1,nand(X2,nand(X3,nand(X3,nand(Y3,nand(X1,X3)))))) = nand(X1,nand(X1,X2)),
inference(orient,[status(thm)],[t135987]) ).
cnf(t10381,plain,
nand(X1,nand(nand(X2,X2),nand(nand(X3,Y3),nand(X3,nand(X3,X2))))) = nand(X1,nand(nand(X1,nand(X1,nand(X2,X2))),nand(X1,nand(X3,nand(X3,X2))))),
inference(cp,[status(thm)],[t10234,t7630]) ).
cnf(t39339,plain,
nand(X1,nand(nand(X1,X2),nand(X1,nand(X3,nand(X3,X2))))) = nand(X1,nand(X3,nand(X3,X2))),
inference(orient,[status(thm)],[t10381]) ).
cnf(t11717,plain,
nand(X1,X1) = nand(X1,nand(nand(nand(X2,X3),nand(X2,Y3)),nand(X1,X2))),
inference(cp,[status(thm)],[t10901,t11503]) ).
cnf(t135739,plain,
nand(X1,X1) = nand(X1,nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,Y3)))),
inference(step,[status(thm)],[t11717,t3021]) ).
cnf(t16074,plain,
nand(X1,nand(nand(X1,X2),nand(nand(X2,X3),nand(X2,Y3)))) = nand(X1,X1),
inference(orient,[status(thm)],[t135739]) ).
cnf(t3340,plain,
nand(nand(X1,X2),nand(X1,X2)) = nand(nand(X1,X2),nand(nand(X1,nand(X2,X3)),X1)),
inference(cp,[status(thm)],[t3332,t3127]) ).
cnf(t135644,plain,
nand(nand(X1,X2),nand(X1,X2)) = nand(nand(X1,X2),nand(X1,nand(X1,nand(X2,X3)))),
inference(step,[status(thm)],[t3340,t3021]) ).
cnf(t4786,plain,
nand(nand(X1,X2),nand(X1,nand(X1,nand(X2,X3)))) = nand(nand(X1,X2),nand(X1,X2)),
inference(orient,[status(thm)],[t135644]) ).
cnf(t14066,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X2,Y3)))),
inference(cp,[status(thm)],[t13869,t3021]) ).
cnf(t14271,plain,
nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X2,Y3)))) = X1,
inference(orient,[status(thm)],[t14066]) ).
cnf(t3253,plain,
nand(nand(X1,X2),X3) = nand(X3,nand(nand(nand(X1,X2),X3),X2)),
inference(cp,[status(thm)],[t3239,t3042]) ).
cnf(t135616,plain,
nand(X3,nand(X1,X2)) = nand(X3,nand(nand(nand(X1,X2),X3),X2)),
inference(step,[status(thm)],[t3253,t3021]) ).
cnf(t135617,plain,
nand(X3,nand(X1,X2)) = nand(X3,nand(X2,nand(nand(X1,X2),X3))),
inference(step,[status(thm)],[t135616,t3021]) ).
cnf(t135618,plain,
nand(X3,nand(X1,X2)) = nand(X3,nand(X2,nand(X3,nand(X1,X2)))),
inference(step,[status(thm)],[t135617,t3021]) ).
cnf(t3392,plain,
nand(X1,nand(X2,nand(X1,nand(X3,X2)))) = nand(X1,nand(X3,X2)),
inference(orient,[status(thm)],[t135618]) ).
cnf(t14274,plain,
X1 = nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X3,Y3)))),
inference(cp,[status(thm)],[t14271,t3392]) ).
cnf(t15200,plain,
nand(nand(X1,nand(X2,X3)),nand(X1,nand(Y3,nand(X3,Y3)))) = X1,
inference(orient,[status(thm)],[t14274]) ).
cnf(t15360,plain,
nand(X1,X1) = nand(nand(nand(X1,X1),nand(X2,X3)),nand(X3,nand(X3,X1))),
inference(cp,[status(thm)],[t15200,t7630]) ).
cnf(t135764,plain,
nand(X1,X1) = nand(nand(X3,nand(X3,X1)),nand(nand(X1,X1),nand(X2,X3))),
inference(step,[status(thm)],[t15360,t3021]) ).
cnf(t135765,plain,
nand(X1,X1) = nand(nand(X3,nand(X1,X1)),nand(nand(X1,X1),nand(X2,X3))),
inference(step,[status(thm)],[t135764,t3355]) ).
cnf(t19364,plain,
nand(nand(X1,nand(X2,X2)),nand(nand(X2,X2),nand(X3,X1))) = nand(X2,X2),
inference(orient,[status(thm)],[t135765]) ).
cnf(t23943,plain,
nand(nand(X1,nand(X2,X2)),nand(nand(X2,X2),nand(X3,X1))) = nand(X2,X2),
inference(rw,[status(thm)],[t19364]) ).
cnf(t135802,plain,
nand(nand(X1,nand(X2,X1)),nand(nand(X2,X2),nand(X3,X1))) = nand(X2,X2),
inference(step,[status(thm)],[t23943,t23605]) ).
cnf(t135803,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X2,X2),nand(X3,X1))) = nand(X2,X2),
inference(step,[status(thm)],[t135802,t3021]) ).
cnf(t135804,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X2,X2),nand(X1,X3))) = nand(X2,X2),
inference(step,[status(thm)],[t135803,t3021]) ).
cnf(t135805,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X1,X3),nand(X2,X2))) = nand(X2,X2),
inference(step,[status(thm)],[t135804,t3021]) ).
cnf(t24806,plain,
nand(nand(X1,nand(X1,X2)),nand(nand(X1,X3),nand(X2,X2))) = nand(X2,X2),
inference(orient,[status(thm)],[t135805]) ).
cnf(t25099,plain,
nand(nand(nand(X1,nand(X1,X2)),X2),nand(nand(X1,nand(X1,X2)),X2)) = nand(nand(nand(X1,nand(X1,X2)),X2),nand(X2,X2)),
inference(cp,[status(thm)],[t4786,t24806]) ).
cnf(t10239,plain,
nand(X1,nand(X2,nand(X2,X2))) = nand(X1,X1),
inference(cp,[status(thm)],[t10234,t4267]) ).
cnf(t10471,plain,
nand(X1,nand(X2,nand(X2,X2))) = nand(X1,X1),
inference(orient,[status(thm)],[t10239]) ).
cnf(t135850,plain,
nand(nand(nand(X1,nand(X1,X2)),X2),nand(c,nand(c,c))) = nand(nand(nand(X1,nand(X1,X2)),X2),nand(X2,X2)),
inference(step,[status(thm)],[t25099,t10471]) ).
cnf(t135851,plain,
nand(nand(c,nand(c,c)),nand(nand(X1,nand(X1,X2)),X2)) = nand(nand(nand(X1,nand(X1,X2)),X2),nand(X2,X2)),
inference(step,[status(thm)],[t135850,t3021]) ).
cnf(t135852,plain,
nand(nand(c,nand(c,c)),nand(X2,nand(X1,nand(X1,X2)))) = nand(nand(nand(X1,nand(X1,X2)),X2),nand(X2,X2)),
inference(step,[status(thm)],[t135851,t3021]) ).
cnf(t135853,plain,
nand(nand(c,nand(c,c)),nand(X2,nand(X1,nand(X1,X2)))) = X2,
inference(step,[status(thm)],[t135852,t3042]) ).
cnf(t31893,plain,
nand(nand(c,nand(c,c)),nand(X1,nand(X2,nand(X2,X1)))) = X1,
inference(orient,[status(thm)],[t135853]) ).
cnf(t32107,plain,
nand(c,c) = nand(c,nand(nand(c,c),X1)),
inference(cp,[status(thm)],[t16074,t31893]) ).
cnf(t135854,plain,
nand(c,c) = nand(c,nand(X1,nand(c,c))),
inference(step,[status(thm)],[t32107,t3021]) ).
cnf(t135855,plain,
nand(c,c) = nand(c,nand(X1,nand(c,X1))),
inference(step,[status(thm)],[t135854,t23605]) ).
cnf(t135856,plain,
nand(c,c) = nand(c,nand(X1,nand(X1,c))),
inference(step,[status(thm)],[t135855,t3021]) ).
cnf(t32258,plain,
nand(c,nand(X1,nand(X1,c))) = nand(c,c),
inference(orient,[status(thm)],[t135856]) ).
cnf(t39398,plain,
nand(c,nand(X1,nand(X1,nand(X2,nand(X2,c))))) = nand(c,nand(nand(c,c),nand(c,nand(X1,nand(X1,nand(X2,nand(X2,c))))))),
inference(cp,[status(thm)],[t39339,t32258]) ).
cnf(t135894,plain,
nand(c,nand(X1,nand(X1,nand(X2,nand(X2,c))))) = nand(c,c),
inference(step,[status(thm)],[t39398,t3239]) ).
cnf(t39744,plain,
nand(c,nand(X1,nand(X1,nand(X2,nand(X2,c))))) = nand(c,c),
inference(orient,[status(thm)],[t135894]) ).
cnf(t63119,plain,
nand(X1,nand(X1,X2)) = nand(X1,nand(X2,nand(nand(X1,nand(X3,nand(X3,c))),nand(nand(X1,nand(X3,nand(X3,c))),nand(c,c))))),
inference(cp,[status(thm)],[t62919,t39744]) ).
cnf(t135988,plain,
nand(X1,nand(X1,X2)) = nand(X1,nand(X2,nand(c,nand(X1,nand(X3,nand(X3,c)))))),
inference(step,[status(thm)],[t63119,t23956]) ).
cnf(t64112,plain,
nand(X1,nand(X2,nand(c,nand(X1,nand(X3,nand(X3,c)))))) = nand(X1,nand(X1,X2)),
inference(orient,[status(thm)],[t135988]) ).
cnf(t64421,plain,
nand(c,nand(c,nand(X1,nand(X2,nand(X2,c))))) = nand(X1,nand(X1,nand(X1,c))),
inference(cp,[status(thm)],[t28936,t64112]) ).
cnf(t135989,plain,
nand(c,nand(c,nand(X1,nand(X2,nand(X2,c))))) = nand(X1,c),
inference(step,[status(thm)],[t64421,t3067]) ).
cnf(t64468,plain,
nand(c,nand(c,nand(X1,nand(X2,nand(X2,c))))) = nand(X1,c),
inference(orient,[status(thm)],[t135989]) ).
cnf(t64544,plain,
nand(X1,c) = nand(X1,nand(nand(X1,c),nand(X2,c))),
inference(cp,[status(thm)],[t3272,t64468]) ).
cnf(t64786,plain,
nand(X1,nand(nand(X1,c),nand(X2,c))) = nand(X1,c),
inference(orient,[status(thm)],[t64544]) ).
cnf(t64971,plain,
nand(c,X1) = nand(c,nand(nand(X1,X2),nand(X1,c))),
inference(cp,[status(thm)],[t48187,t64786]) ).
cnf(t135990,plain,
nand(X1,c) = nand(c,nand(nand(X1,X2),nand(X1,c))),
inference(step,[status(thm)],[t64971,t3021]) ).
cnf(t65027,plain,
nand(c,nand(nand(X1,X2),nand(X1,c))) = nand(X1,c),
inference(orient,[status(thm)],[t135990]) ).
cnf(t65172,plain,
nand(X1,nand(X1,c)) = nand(nand(c,c),nand(nand(X1,X2),nand(X1,nand(X3,c)))),
inference(cp,[status(thm)],[t47538,t65027]) ).
cnf(t78329,plain,
nand(nand(c,c),nand(nand(X1,X2),nand(X1,nand(X3,c)))) = nand(X1,nand(X1,c)),
inference(orient,[status(thm)],[t65172]) ).
cnf(t78752,plain,
nand(nand(X1,X2),nand(X1,nand(nand(X1,X2),c))) = nand(nand(X1,X2),nand(X1,nand(X1,c))),
inference(cp,[status(thm)],[t44549,t78329]) ).
cnf(t136036,plain,
nand(nand(X1,X2),nand(X1,nand(c,nand(X1,X2)))) = nand(nand(X1,X2),nand(X1,nand(X1,c))),
inference(step,[status(thm)],[t78752,t3021]) ).
cnf(t78834,plain,
nand(nand(X1,X2),nand(X1,nand(c,nand(X1,X2)))) = nand(nand(X1,X2),nand(X1,nand(X1,c))),
inference(orient,[status(thm)],[t136036]) ).
cnf(t78840,plain,
nand(nand(X1,nand(nand(X2,X1),nand(X3,nand(nand(X2,X1),nand(X2,Y3))))),nand(X1,nand(X1,c))) = nand(nand(X2,X1),nand(X1,nand(c,nand(X1,nand(nand(X2,X1),nand(X3,nand(nand(X2,X1),nand(X2,Y3)))))))),
inference(cp,[status(thm)],[t78834,t45849]) ).
cnf(t136039,plain,
nand(nand(X2,X1),nand(X1,nand(X1,c))) = nand(nand(X2,X1),nand(X1,nand(c,nand(X1,nand(nand(X2,X1),nand(X3,nand(nand(X2,X1),nand(X2,Y3)))))))),
inference(step,[status(thm)],[t78840,t45849]) ).
cnf(t136040,plain,
nand(nand(X2,X1),nand(X1,nand(X1,c))) = nand(nand(X2,X1),nand(X1,nand(c,nand(X2,X1)))),
inference(step,[status(thm)],[t136039,t45849]) ).
cnf(t79642,plain,
nand(nand(X1,X2),nand(X2,nand(c,nand(X1,X2)))) = nand(nand(X1,X2),nand(X2,nand(X2,c))),
inference(orient,[status(thm)],[t136040]) ).
cnf(t80143,plain,
nand(nand(X1,X1),nand(X2,nand(c,nand(X1,X2)))) = nand(nand(X1,X1),nand(X2,nand(nand(X1,X2),nand(X2,nand(X2,c))))),
inference(cp,[status(thm)],[t53927,t79642]) ).
cnf(t136043,plain,
nand(nand(X1,X1),nand(X2,nand(c,nand(X1,X2)))) = nand(nand(X1,X1),nand(X2,nand(X2,c))),
inference(step,[status(thm)],[t80143,t53927]) ).
cnf(t81687,plain,
nand(nand(X1,X1),nand(X2,nand(c,nand(X1,X2)))) = nand(nand(X1,X1),nand(X2,nand(X2,c))),
inference(orient,[status(thm)],[t136043]) ).
cnf(t5484,plain,
X1 = nand(nand(X1,nand(X2,nand(X1,nand(X3,Y3)))),nand(X1,Y3)),
inference(cp,[status(thm)],[t3167,t5361]) ).
cnf(t135654,plain,
X1 = nand(nand(X1,Y3),nand(X1,nand(X2,nand(X1,nand(X3,Y3))))),
inference(step,[status(thm)],[t5484,t3021]) ).
cnf(t5530,plain,
nand(nand(X1,X2),nand(X1,nand(X3,nand(X1,nand(Y3,X2))))) = X1,
inference(orient,[status(thm)],[t135654]) ).
cnf(t49655,plain,
X1 = nand(nand(X1,nand(X2,nand(X3,X3))),nand(X1,nand(X3,nand(X1,Y3)))),
inference(cp,[status(thm)],[t5530,t49279]) ).
cnf(t135930,plain,
X1 = nand(nand(X1,nand(X2,nand(X3,X2))),nand(X1,nand(X3,nand(X1,Y3)))),
inference(step,[status(thm)],[t49655,t23605]) ).
cnf(t135931,plain,
X1 = nand(nand(X1,nand(X2,nand(X2,X3))),nand(X1,nand(X3,nand(X1,Y3)))),
inference(step,[status(thm)],[t135930,t3021]) ).
cnf(t50100,plain,
nand(nand(X1,nand(X2,nand(X2,X3))),nand(X1,nand(X3,nand(X1,Y3)))) = X1,
inference(orient,[status(thm)],[t135931]) ).
cnf(t81704,plain,
nand(nand(nand(X1,nand(X1,nand(X1,X1))),nand(X1,nand(X1,nand(X1,X1)))),nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(cp,[status(thm)],[t81687,t50100]) ).
cnf(t136044,plain,
nand(nand(X2,nand(X2,c)),nand(nand(X1,nand(X1,nand(X1,X1))),nand(X1,nand(X1,nand(X1,X1))))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t81704,t3021]) ).
cnf(t136045,plain,
nand(nand(X2,nand(X2,c)),nand(nand(X1,nand(X1,nand(X1,X1))),nand(X2,nand(X2,c)))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136044,t23605]) ).
cnf(t136046,plain,
nand(nand(X2,nand(X2,c)),nand(nand(X2,nand(X2,c)),nand(X1,nand(X1,nand(X1,X1))))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136045,t3021]) ).
cnf(t48285,plain,
nand(nand(X1,nand(X2,X2)),X2) = nand(nand(X1,nand(X2,X2)),nand(nand(X2,X3),nand(X2,X2))),
inference(cp,[status(thm)],[t48187,t11971]) ).
cnf(t135938,plain,
nand(X2,nand(X1,nand(X2,X2))) = nand(nand(X1,nand(X2,X2)),nand(nand(X2,X3),nand(X2,X2))),
inference(step,[status(thm)],[t48285,t3021]) ).
cnf(t135591,plain,
nand(X1,nand(X2,nand(X1,X1))) = nand(X1,X1),
inference(step,[status(thm)],[t260,t2998]) ).
cnf(t3016,plain,
nand(X1,nand(X2,nand(X1,X1))) = nand(X1,X1),
inference(rw,[status(thm)],[t135591]) ).
cnf(t3059,plain,
nand(X1,nand(X2,nand(X1,X1))) = nand(X1,X1),
inference(orient,[status(thm)],[t3016]) ).
cnf(t135939,plain,
nand(X2,X2) = nand(nand(X1,nand(X2,X2)),nand(nand(X2,X3),nand(X2,X2))),
inference(step,[status(thm)],[t135938,t3059]) ).
cnf(t135940,plain,
nand(X2,X2) = nand(nand(X1,nand(X2,X1)),nand(nand(X2,X3),nand(X2,X2))),
inference(step,[status(thm)],[t135939,t23605]) ).
cnf(t135941,plain,
nand(X2,X2) = nand(nand(X1,nand(X1,X2)),nand(nand(X2,X3),nand(X2,X2))),
inference(step,[status(thm)],[t135940,t3021]) ).
cnf(t135942,plain,
nand(X2,X2) = nand(nand(X1,nand(X1,X2)),nand(nand(X2,X2),nand(X2,X3))),
inference(step,[status(thm)],[t135941,t3021]) ).
cnf(t135943,plain,
nand(X2,X2) = nand(nand(X1,nand(X1,X2)),X2),
inference(step,[status(thm)],[t135942,t2584]) ).
cnf(t135944,plain,
nand(X2,X2) = nand(X2,nand(X1,nand(X1,X2))),
inference(step,[status(thm)],[t135943,t3021]) ).
cnf(t53659,plain,
nand(X1,nand(X2,nand(X2,X1))) = nand(X1,X1),
inference(orient,[status(thm)],[t135944]) ).
cnf(t136047,plain,
nand(nand(X2,nand(X2,c)),nand(nand(X2,nand(X2,c)),nand(X1,X1))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136046,t53659]) ).
cnf(t136048,plain,
nand(nand(X2,nand(X2,c)),nand(nand(X1,X1),nand(X2,nand(X2,c)))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136047,t3021]) ).
cnf(t136049,plain,
nand(nand(X2,nand(X2,c)),nand(nand(X1,X1),nand(X1,X1))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136048,t23605]) ).
cnf(t136050,plain,
nand(nand(X2,nand(X2,c)),X1) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136049,t3042]) ).
cnf(t136051,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(c,nand(nand(X1,nand(X1,nand(X1,X1))),X2)))),
inference(step,[status(thm)],[t136050,t3021]) ).
cnf(t136052,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(c,nand(X2,nand(X1,nand(X1,nand(X1,X1))))))),
inference(step,[status(thm)],[t136051,t3021]) ).
cnf(t136053,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(c,nand(X2,nand(X1,X1))))),
inference(step,[status(thm)],[t136052,t53659]) ).
cnf(t82217,plain,
nand(X1,nand(X2,nand(c,nand(X2,nand(X1,X1))))) = nand(X1,nand(X2,nand(X2,c))),
inference(orient,[status(thm)],[t136053]) ).
cnf(t12884,plain,
nand(nand(X1,X1),nand(X2,nand(X1,X3))) = nand(nand(X1,X1),nand(X2,X2)),
inference(cp,[status(thm)],[t3306,t12737]) ).
cnf(t34882,plain,
nand(nand(X1,X1),nand(X2,nand(X1,X3))) = nand(nand(X1,X1),nand(X2,X2)),
inference(orient,[status(thm)],[t12884]) ).
cnf(t35254,plain,
nand(nand(X1,nand(X2,X3)),nand(nand(X2,X2),nand(X2,X2))) = nand(nand(X1,nand(X2,X3)),nand(nand(X2,X2),nand(X1,X1))),
inference(cp,[status(thm)],[t23605,t34882]) ).
cnf(t135912,plain,
nand(nand(X1,nand(X2,X3)),X2) = nand(nand(X1,nand(X2,X3)),nand(nand(X2,X2),nand(X1,X1))),
inference(step,[status(thm)],[t35254,t3042]) ).
cnf(t135913,plain,
nand(X2,nand(X1,nand(X2,X3))) = nand(nand(X1,nand(X2,X3)),nand(nand(X2,X2),nand(X1,X1))),
inference(step,[status(thm)],[t135912,t3021]) ).
cnf(t135914,plain,
nand(X2,nand(X1,nand(X2,X3))) = nand(nand(X1,nand(X2,X3)),nand(nand(X1,X1),nand(X2,X2))),
inference(step,[status(thm)],[t135913,t3021]) ).
cnf(t44103,plain,
nand(nand(X1,nand(X2,X3)),nand(nand(X1,X1),nand(X2,X2))) = nand(X2,nand(X1,nand(X2,X3))),
inference(orient,[status(thm)],[t135914]) ).
cnf(t44281,plain,
nand(X1,nand(X2,nand(X1,X3))) = nand(nand(X2,nand(X1,X3)),nand(nand(X1,X1),nand(X2,X2))),
inference(cp,[status(thm)],[t44103,t3021]) ).
cnf(t45404,plain,
nand(nand(X1,nand(X2,X3)),nand(nand(X2,X2),nand(X1,X1))) = nand(X2,nand(X1,nand(X2,X3))),
inference(orient,[status(thm)],[t44281]) ).
cnf(t3134,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X2),nand(nand(X2,nand(X1,X3)),Y3))),
inference(cp,[status(thm)],[t3127,t3094]) ).
cnf(t135646,plain,
nand(X1,X2) = nand(X2,nand(nand(X1,X2),nand(Y3,nand(X2,nand(X1,X3))))),
inference(step,[status(thm)],[t3134,t3021]) ).
cnf(t4961,plain,
nand(X1,nand(nand(X2,X1),nand(X3,nand(X1,nand(X2,Y3))))) = nand(X2,X1),
inference(orient,[status(thm)],[t135646]) ).
cnf(t11616,plain,
X1 = nand(nand(X1,nand(X2,nand(nand(X3,Y3),nand(X3,Y4)))),nand(X1,X3)),
inference(cp,[status(thm)],[t3167,t11503]) ).
cnf(t135849,plain,
X1 = nand(nand(X1,X3),nand(X1,nand(X2,nand(nand(X3,Y3),nand(X3,Y4))))),
inference(step,[status(thm)],[t11616,t3021]) ).
cnf(t31417,plain,
nand(nand(X1,X2),nand(X1,nand(X3,nand(nand(X2,Y3),nand(X2,Y4))))) = X1,
inference(orient,[status(thm)],[t135849]) ).
cnf(t31781,plain,
nand(X1,nand(X2,nand(nand(nand(X1,X2),X3),nand(nand(X1,X2),Y3)))) = nand(X1,X1),
inference(cp,[status(thm)],[t10234,t31417]) ).
cnf(t136189,plain,
nand(X1,nand(X2,nand(nand(X3,nand(X1,X2)),nand(nand(X1,X2),Y3)))) = nand(X1,X1),
inference(step,[status(thm)],[t31781,t3021]) ).
cnf(t136190,plain,
nand(X1,nand(X2,nand(nand(X3,nand(X1,X2)),nand(Y3,nand(X1,X2))))) = nand(X1,X1),
inference(step,[status(thm)],[t136189,t3021]) ).
cnf(t120768,plain,
nand(X1,nand(X2,nand(nand(X3,nand(X1,X2)),nand(Y3,nand(X1,X2))))) = nand(X1,X1),
inference(orient,[status(thm)],[t136190]) ).
cnf(t121803,plain,
nand(nand(X1,nand(X2,X3)),X3) = nand(X3,nand(nand(nand(X1,nand(X2,X3)),X3),nand(X2,X2))),
inference(cp,[status(thm)],[t4961,t120768]) ).
cnf(t136191,plain,
nand(X3,nand(X1,nand(X2,X3))) = nand(X3,nand(nand(nand(X1,nand(X2,X3)),X3),nand(X2,X2))),
inference(step,[status(thm)],[t121803,t3021]) ).
cnf(t136192,plain,
nand(X3,nand(X1,nand(X2,X3))) = nand(X3,nand(nand(X2,X2),nand(nand(X1,nand(X2,X3)),X3))),
inference(step,[status(thm)],[t136191,t3021]) ).
cnf(t136193,plain,
nand(X3,nand(X1,nand(X2,X3))) = nand(X3,nand(nand(X2,X2),nand(X3,nand(X1,nand(X2,X3))))),
inference(step,[status(thm)],[t136192,t3021]) ).
cnf(t121834,plain,
nand(X1,nand(nand(X2,X2),nand(X1,nand(X3,nand(X2,X1))))) = nand(X1,nand(X3,nand(X2,X1))),
inference(orient,[status(thm)],[t136193]) ).
cnf(t48208,plain,
nand(nand(X1,X1),X2) = nand(nand(X1,X1),nand(nand(X2,nand(X3,nand(nand(X1,X1),nand(X1,X1)))),nand(X1,Y3))),
inference(cp,[status(thm)],[t48187,t34882]) ).
cnf(t135925,plain,
nand(X2,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X2,nand(X3,nand(nand(X1,X1),nand(X1,X1)))),nand(X1,Y3))),
inference(step,[status(thm)],[t48208,t3021]) ).
cnf(t135926,plain,
nand(X2,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X1,Y3),nand(X2,nand(X3,nand(nand(X1,X1),nand(X1,X1)))))),
inference(step,[status(thm)],[t135925,t3021]) ).
cnf(t135927,plain,
nand(X2,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X1,Y3),nand(X2,nand(X3,nand(nand(X1,X1),X3))))),
inference(step,[status(thm)],[t135926,t23605]) ).
cnf(t135928,plain,
nand(X2,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X1,Y3),nand(X2,nand(X3,nand(X3,nand(X1,X1)))))),
inference(step,[status(thm)],[t135927,t3021]) ).
cnf(t135929,plain,
nand(X2,nand(X1,X1)) = nand(nand(X1,X1),nand(nand(X1,Y3),nand(X2,nand(X1,X3)))),
inference(step,[status(thm)],[t135928,t23956]) ).
cnf(t48675,plain,
nand(nand(X1,X1),nand(nand(X1,X2),nand(X3,nand(X1,Y3)))) = nand(X3,nand(X1,X1)),
inference(orient,[status(thm)],[t135929]) ).
cnf(t121849,plain,
nand(nand(X1,X2),nand(X3,nand(X1,nand(X1,X2)))) = nand(nand(X1,X2),nand(X3,nand(X1,X1))),
inference(cp,[status(thm)],[t121834,t48675]) ).
cnf(t127349,plain,
nand(nand(X1,X2),nand(X3,nand(X1,nand(X1,X2)))) = nand(nand(X1,X2),nand(X3,nand(X1,X1))),
inference(orient,[status(thm)],[t121849]) ).
cnf(t127826,plain,
nand(X1,nand(nand(X2,X3),nand(X1,nand(X2,nand(X2,X3))))) = nand(nand(nand(X2,X3),nand(X1,nand(X2,X2))),nand(nand(X1,X1),nand(nand(X2,X3),nand(X2,X3)))),
inference(cp,[status(thm)],[t45404,t127349]) ).
cnf(t136206,plain,
nand(X1,nand(X2,nand(X2,X3))) = nand(nand(nand(X2,X3),nand(X1,nand(X2,X2))),nand(nand(X1,X1),nand(nand(X2,X3),nand(X2,X3)))),
inference(step,[status(thm)],[t127826,t3392]) ).
cnf(t136207,plain,
nand(X1,nand(X2,nand(X2,X3))) = nand(X1,nand(nand(X2,X3),nand(X1,nand(X2,X2)))),
inference(step,[status(thm)],[t136206,t45404]) ).
cnf(t136208,plain,
nand(X1,nand(X2,nand(X2,X3))) = nand(X1,nand(nand(X2,X3),nand(X1,nand(X2,X1)))),
inference(step,[status(thm)],[t136207,t23605]) ).
cnf(t136209,plain,
nand(X1,nand(X2,nand(X2,X3))) = nand(X1,nand(nand(X2,X3),nand(X1,nand(X1,X2)))),
inference(step,[status(thm)],[t136208,t3021]) ).
cnf(t128101,plain,
nand(X1,nand(nand(X2,X3),nand(X1,nand(X1,X2)))) = nand(X1,nand(X2,nand(X2,X3))),
inference(orient,[status(thm)],[t136209]) ).
cnf(t128201,plain,
nand(X1,nand(c,nand(c,nand(nand(X2,X3),nand(X2,c))))) = nand(X1,nand(nand(X2,c),nand(X1,nand(X1,c)))),
inference(cp,[status(thm)],[t128101,t65027]) ).
cnf(t136215,plain,
nand(X1,nand(c,nand(X2,c))) = nand(X1,nand(nand(X2,c),nand(X1,nand(X1,c)))),
inference(step,[status(thm)],[t128201,t65027]) ).
cnf(t136216,plain,
nand(X1,nand(c,nand(X2,X2))) = nand(X1,nand(nand(X2,c),nand(X1,nand(X1,c)))),
inference(step,[status(thm)],[t136215,t23605]) ).
cnf(t130150,plain,
nand(X1,nand(c,nand(X2,X2))) = nand(X1,nand(nand(X2,c),nand(X1,nand(X1,c)))),
inference(orient,[status(thm)],[t136216]) ).
cnf(t130483,plain,
nand(X1,nand(c,nand(X2,X2))) = nand(X1,nand(nand(X2,X2),nand(X1,nand(nand(X2,c),nand(X1,nand(X1,c)))))),
inference(cp,[status(thm)],[t3392,t130150]) ).
cnf(t136217,plain,
nand(X1,nand(c,nand(X2,X2))) = nand(X1,nand(nand(X2,X2),nand(X1,nand(X1,c)))),
inference(step,[status(thm)],[t130483,t53927]) ).
cnf(t121844,plain,
nand(X1,nand(c,nand(X2,X1))) = nand(X1,nand(nand(X2,X2),nand(X1,nand(X1,c)))),
inference(cp,[status(thm)],[t121834,t81687]) ).
cnf(t136194,plain,
nand(X1,nand(c,nand(X1,X2))) = nand(X1,nand(nand(X2,X2),nand(X1,nand(X1,c)))),
inference(step,[status(thm)],[t121844,t3021]) ).
cnf(t122643,plain,
nand(X1,nand(nand(X2,X2),nand(X1,nand(X1,c)))) = nand(X1,nand(c,nand(X1,X2))),
inference(orient,[status(thm)],[t136194]) ).
cnf(t136218,plain,
nand(X1,nand(c,nand(X2,X2))) = nand(X1,nand(c,nand(X1,X2))),
inference(step,[status(thm)],[t136217,t122643]) ).
cnf(t131105,plain,
nand(X1,nand(c,nand(X2,X2))) = nand(X1,nand(c,nand(X1,X2))),
inference(orient,[status(thm)],[t136218]) ).
cnf(t131903,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(c,nand(nand(X1,X1),nand(X1,X1))))),
inference(cp,[status(thm)],[t82217,t131105]) ).
cnf(t136228,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(c,X1))),
inference(step,[status(thm)],[t131903,t3042]) ).
cnf(t136229,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(X1,c))),
inference(step,[status(thm)],[t136228,t3021]) ).
cnf(t134825,plain,
nand(X1,nand(X2,nand(X2,c))) = nand(X1,nand(X2,nand(X1,c))),
inference(orient,[status(thm)],[t136229]) ).
cnf(goal_0,negated_conjecture,
nand(nand(nand(c,b),b),a) != nand(a,nand(b,nand(a,c))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
nand(a,nand(nand(c,b),b)) != nand(a,nand(b,nand(a,c))),
inference(rw,[status(thm)],[goal_0,t3021]) ).
cnf(g0_1,plain,
nand(a,nand(b,nand(c,b))) != nand(a,nand(b,nand(a,c))),
inference(rw,[status(thm)],[g0_0,t3021]) ).
cnf(g0_2,plain,
nand(a,nand(b,nand(c,c))) != nand(a,nand(b,nand(a,c))),
inference(rw,[status(thm)],[g0_1,t23605]) ).
cnf(g0_3,plain,
nand(a,nand(b,nand(c,c))) != nand(a,nand(b,nand(b,c))),
inference(rw,[status(thm)],[g0_2,t134825]) ).
cnf(g0_4,plain,
nand(a,nand(b,nand(c,c))) != nand(a,nand(b,nand(c,c))),
inference(rw,[status(thm)],[g0_3,t3355]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO076-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.20/15.47 % Computer : n009.cluster.edu
% 0.20/15.47 % Model : x86_64 x86_64
% 0.20/15.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/15.47 % Memory : 8046.5625MB
% 0.20/15.47 % OS : Linux 6.8.0-71-generic
% 0.20/15.47 % CPULimit : 300
% 0.20/15.47 % WCLimit : 300
% 0.20/15.47 % DateTime : Fri Sep 25 06:44:14 UTC 2026
% 0.20/15.47 % CPUTime :
% 0.20/15.47 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 103.95/28.64 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 103.95/28.64 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------