gand1(G,A),gand2(G,B),gand3(G,C),and1(A,"true"),and2(B,"true") :> and3(C,"true"). gand1(G,A),gand2(G,B),gand3(G,C),and1(A,"true"),and2(B,"false") :> and3(C,"false"). gand1(G,A),gand2(G,B),gand3(G,C),and1(A,"false"),and2(B,"true") :> and3(C,"false"). gand1(G,A),gand2(G,B),gand3(G,C),and1(A,"false"),and2(B,"false") :> and3(C,"false"). gnot1(G,A),gnot2(G,A1),not1(A,"true") :> not2(A1,"false"). gnot1(G,A),gnot2(G,A1),not1(A,"false") :> not2(A1,"true"). gnand1(G,A),gnand2(G,B),gnand3(G,C),nand1(A,"true"),nand2(B,"true") :> nand3(C,"false"). gnand1(G,A),gnand2(G,B),gnand3(G,C),nand1(A,"true"),nand2(B,"false") :> nand3(C,"true"). gnand1(G,A),gnand2(G,B),gnand3(G,C),nand1(A,"false"),nand2(B,"true") :> nand3(C,"true"). gnand1(G,A),gnand2(G,B),gnand3(G,C),nand1(A,"false"),nand2(B,"false") :> nand3(C,"true"). nandnand2(G1,G2),gnand3(G1,X),gnand2(G2,X),nand3(X,V) :> nand2(X,V). nandnand1(G1,G2),gnand3(G1,X),gnand1(G2,X),nand3(X,V) :> nand1(X,V). gnand1(g1,a). gnand2(g1,b). gnand3(g1,a11). nand1(a,"true"). nand2(b,"false"). nandnand1(g1,g3). nandnand2(g1,g2). nandnand2(g1,g9). gnand1(g2,a). gnand2(g2,a11). gnand3(g2,a12). nandnand1(g2,g4). gnand1(g3,a11). gnand2(g3,b). gnand3(g3,a13). nandnand2(g3,g4). gnand1(g4,a12). gnand2(g4,a13). gnand3(g4,a14). nandnand1(g4,g6). nandnand1(g4,g5). gnand1(g5,a14). gnand2(g5,cin). gnand3(g5,a15). nand2(cin,"true"). nandnand1(g5,g8). nandnand1(g5,g9). nandnand2(g5,g6). gnand1(g6,a14). gnand2(g6,a15). gnand3(g6,a16). nandnand1(g6,g7). gnand1(g7,a16). gnand2(g7,a17). gnand3(g7,sum). gnand1(g8,a15). gnand2(g8,cin). gnand3(g8,a17). nandnand2(g8,g7). gnand1(g9,a15). gnand2(g9,a11). gnand3(g9,cout).