isgcc([[1, 1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 0]], [[0, 0, 1], [0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]).

clause(1, and(0, 0, 0), true).
clause(2, and(0, 1, 0), true).
clause(3, and(1, 0, 0), true).
clause(4, and(1, 1, 1), true).
clause(5, or(0, 0, 0), true).
clause(6, or(0, 1, 1), true).
clause(7, or(1, 0, 1), true).
clause(9, inv(0, 1), true).
clause(10, inv(1, 0), true).
clause(12, dff(var('D'), 1, anonymous(1), var('D')), true).
clause(13,
       neta(var('A'), var('B'), var('Q')),
       (and(var('A'), var('B'), var('T1')),
        inv(var('A'), var('Na')),
        inv(var('B'), var('Nb')),
        and(var('Na'), var('Nb'), var('T2')),
        or(var('T1'), var('T2'), var('Q')))).
clause(14,
       netb(var('A'), var('B'), var('C'), var('Q1'), var('Q2')),
       (and(var('A'), var('C'), var('T1')),
        inv(var('C'), var('Nc')),
        and(var('B'), var('Nc'), var('T2')),
        inv(var('A'), var('Na')),
        and(var('Na'), var('C'), var('T3')),
        or(var('T1'), var('T2'), var('Q1')),
        or(var('T2'), var('T3'), var('Q2')))).
clause(15,
       gcc(var('C'), [var('Qa'), var('Qb'), var('Qc')], [var('Za'), var('Zb'), var('Zc')]),
       (netb(var('Qa'), var('Qb'), var('Qc'), var('D1'), var('D2')),
        neta(var('Qa'), var('Qb'), var('D3')),
        dff(var('D1'), var('C'), var('Qa'), var('Za')),
        dff(var('D2'), var('C'), var('Qb'), var('Zb')),
        dff(var('D3'), var('C'), var('Qc'), var('Zc')))).
clause(16, testgcc([], anonymous(1), []), true).
clause(17,
       testgcc([var('C') | var('Cs')], var('State'), [var('Next') | var('Rest')]),
       (gcc(var('C'), var('State'), var('Next')), testgcc(var('Cs'), var('Next'), var('Rest')))).
clause(18,
       isgcc([[1, 1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 0]], var('States')),
       testgcc([1, 1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 0], var('States'))).

step(isgcc([[1, 1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 0]], [[0, 0, 1], [0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(18),
     ['States' = [[0, 0, 1], [0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [testgcc([1, 1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 0], [[0, 0, 1], [0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(testgcc([1, 1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 0], [[0, 0, 1], [0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1, 1, 1, 1, 1, 1, 1],
      'State' = [0, 0, 0],
      'Next' = [0, 0, 1],
      'Rest' = [[0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [gcc(1, [0, 0, 0], [0, 0, 1]),
      testgcc([1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 1], [[0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [0, 0, 0], [0, 0, 1]),
     rule(15),
     ['C' = 1,
      'Qa' = 0,
      'Qb' = 0,
      'Qc' = 0,
      'Za' = 0,
      'Zb' = 0,
      'Zc' = 1,
      'D1' = 0,
      'D2' = 0,
      'D3' = 1],
     [netb(0, 0, 0, 0, 0), neta(0, 0, 1), dff(0, 1, 0, 0), dff(0, 1, 0, 0), dff(1, 1, 0, 1)]).
step(netb(0, 0, 0, 0, 0),
     rule(14),
     ['A' = 0,
      'B' = 0,
      'C' = 0,
      'Q1' = 0,
      'Q2' = 0,
      'T1' = 0,
      'Nc' = 1,
      'T2' = 0,
      'Na' = 1,
      'T3' = 0],
     [and(0, 0, 0), inv(0, 1), and(0, 1, 0), inv(0, 1), and(1, 0, 0), or(0, 0, 0), or(0, 0, 0)]).
step(and(0, 0, 0), fact(1), [], []).
step(inv(0, 1), fact(9), [], []).
step(and(0, 1, 0), fact(2), [], []).
step(and(1, 0, 0), fact(3), [], []).
step(or(0, 0, 0), fact(5), [], []).
step(neta(0, 0, 1),
     rule(13),
     ['A' = 0, 'B' = 0, 'Q' = 1, 'T1' = 0, 'Na' = 1, 'Nb' = 1, 'T2' = 1],
     [and(0, 0, 0), inv(0, 1), inv(0, 1), and(1, 1, 1), or(0, 1, 1)]).
step(and(1, 1, 1), fact(4), [], []).
step(or(0, 1, 1), fact(6), [], []).
step(dff(0, 1, 0, 0), fact(12), ['D' = 0], []).
step(dff(1, 1, 0, 1), fact(12), ['D' = 1], []).
step(testgcc([1, 1, 1, 1, 1, 1, 1, 1], [0, 0, 1], [[0, 1, 1], [0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1, 1, 1, 1, 1, 1],
      'State' = [0, 0, 1],
      'Next' = [0, 1, 1],
      'Rest' = [[0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [gcc(1, [0, 0, 1], [0, 1, 1]),
      testgcc([1, 1, 1, 1, 1, 1, 1], [0, 1, 1], [[0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [0, 0, 1], [0, 1, 1]),
     rule(15),
     ['C' = 1,
      'Qa' = 0,
      'Qb' = 0,
      'Qc' = 1,
      'Za' = 0,
      'Zb' = 1,
      'Zc' = 1,
      'D1' = 0,
      'D2' = 1,
      'D3' = 1],
     [netb(0, 0, 1, 0, 1), neta(0, 0, 1), dff(0, 1, 0, 0), dff(1, 1, 0, 1), dff(1, 1, 1, 1)]).
step(netb(0, 0, 1, 0, 1),
     rule(14),
     ['A' = 0,
      'B' = 0,
      'C' = 1,
      'Q1' = 0,
      'Q2' = 1,
      'T1' = 0,
      'Nc' = 0,
      'T2' = 0,
      'Na' = 1,
      'T3' = 1],
     [and(0, 1, 0), inv(1, 0), and(0, 0, 0), inv(0, 1), and(1, 1, 1), or(0, 0, 0), or(0, 1, 1)]).
step(inv(1, 0), fact(10), [], []).
step(dff(1, 1, 1, 1), fact(12), ['D' = 1], []).
step(testgcc([1, 1, 1, 1, 1, 1, 1], [0, 1, 1], [[0, 1, 0], [1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1, 1, 1, 1, 1],
      'State' = [0, 1, 1],
      'Next' = [0, 1, 0],
      'Rest' = [[1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [gcc(1, [0, 1, 1], [0, 1, 0]),
      testgcc([1, 1, 1, 1, 1, 1], [0, 1, 0], [[1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [0, 1, 1], [0, 1, 0]),
     rule(15),
     ['C' = 1,
      'Qa' = 0,
      'Qb' = 1,
      'Qc' = 1,
      'Za' = 0,
      'Zb' = 1,
      'Zc' = 0,
      'D1' = 0,
      'D2' = 1,
      'D3' = 0],
     [netb(0, 1, 1, 0, 1), neta(0, 1, 0), dff(0, 1, 0, 0), dff(1, 1, 1, 1), dff(0, 1, 1, 0)]).
step(netb(0, 1, 1, 0, 1),
     rule(14),
     ['A' = 0,
      'B' = 1,
      'C' = 1,
      'Q1' = 0,
      'Q2' = 1,
      'T1' = 0,
      'Nc' = 0,
      'T2' = 0,
      'Na' = 1,
      'T3' = 1],
     [and(0, 1, 0), inv(1, 0), and(1, 0, 0), inv(0, 1), and(1, 1, 1), or(0, 0, 0), or(0, 1, 1)]).
step(neta(0, 1, 0),
     rule(13),
     ['A' = 0, 'B' = 1, 'Q' = 0, 'T1' = 0, 'Na' = 1, 'Nb' = 0, 'T2' = 0],
     [and(0, 1, 0), inv(0, 1), inv(1, 0), and(1, 0, 0), or(0, 0, 0)]).
step(dff(0, 1, 1, 0), fact(12), ['D' = 0], []).
step(testgcc([1, 1, 1, 1, 1, 1], [0, 1, 0], [[1, 1, 0], [1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1, 1, 1, 1],
      'State' = [0, 1, 0],
      'Next' = [1, 1, 0],
      'Rest' = [[1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [gcc(1, [0, 1, 0], [1, 1, 0]),
      testgcc([1, 1, 1, 1, 1], [1, 1, 0], [[1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [0, 1, 0], [1, 1, 0]),
     rule(15),
     ['C' = 1,
      'Qa' = 0,
      'Qb' = 1,
      'Qc' = 0,
      'Za' = 1,
      'Zb' = 1,
      'Zc' = 0,
      'D1' = 1,
      'D2' = 1,
      'D3' = 0],
     [netb(0, 1, 0, 1, 1), neta(0, 1, 0), dff(1, 1, 0, 1), dff(1, 1, 1, 1), dff(0, 1, 0, 0)]).
step(netb(0, 1, 0, 1, 1),
     rule(14),
     ['A' = 0,
      'B' = 1,
      'C' = 0,
      'Q1' = 1,
      'Q2' = 1,
      'T1' = 0,
      'Nc' = 1,
      'T2' = 1,
      'Na' = 1,
      'T3' = 0],
     [and(0, 0, 0), inv(0, 1), and(1, 1, 1), inv(0, 1), and(1, 0, 0), or(0, 1, 1), or(1, 0, 1)]).
step(or(1, 0, 1), fact(7), [], []).
step(testgcc([1, 1, 1, 1, 1], [1, 1, 0], [[1, 1, 1], [1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1, 1, 1],
      'State' = [1, 1, 0],
      'Next' = [1, 1, 1],
      'Rest' = [[1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [gcc(1, [1, 1, 0], [1, 1, 1]),
      testgcc([1, 1, 1, 1], [1, 1, 1], [[1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [1, 1, 0], [1, 1, 1]),
     rule(15),
     ['C' = 1,
      'Qa' = 1,
      'Qb' = 1,
      'Qc' = 0,
      'Za' = 1,
      'Zb' = 1,
      'Zc' = 1,
      'D1' = 1,
      'D2' = 1,
      'D3' = 1],
     [netb(1, 1, 0, 1, 1), neta(1, 1, 1), dff(1, 1, 1, 1), dff(1, 1, 1, 1), dff(1, 1, 0, 1)]).
step(netb(1, 1, 0, 1, 1),
     rule(14),
     ['A' = 1,
      'B' = 1,
      'C' = 0,
      'Q1' = 1,
      'Q2' = 1,
      'T1' = 0,
      'Nc' = 1,
      'T2' = 1,
      'Na' = 0,
      'T3' = 0],
     [and(1, 0, 0), inv(0, 1), and(1, 1, 1), inv(1, 0), and(0, 0, 0), or(0, 1, 1), or(1, 0, 1)]).
step(neta(1, 1, 1),
     rule(13),
     ['A' = 1, 'B' = 1, 'Q' = 1, 'T1' = 1, 'Na' = 0, 'Nb' = 0, 'T2' = 0],
     [and(1, 1, 1), inv(1, 0), inv(1, 0), and(0, 0, 0), or(1, 0, 1)]).
step(testgcc([1, 1, 1, 1], [1, 1, 1], [[1, 0, 1], [1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1, 1],
      'State' = [1, 1, 1],
      'Next' = [1, 0, 1],
      'Rest' = [[1, 0, 0], [0, 0, 0], [0, 0, 1]]],
     [gcc(1, [1, 1, 1], [1, 0, 1]),
      testgcc([1, 1, 1], [1, 0, 1], [[1, 0, 0], [0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [1, 1, 1], [1, 0, 1]),
     rule(15),
     ['C' = 1,
      'Qa' = 1,
      'Qb' = 1,
      'Qc' = 1,
      'Za' = 1,
      'Zb' = 0,
      'Zc' = 1,
      'D1' = 1,
      'D2' = 0,
      'D3' = 1],
     [netb(1, 1, 1, 1, 0), neta(1, 1, 1), dff(1, 1, 1, 1), dff(0, 1, 1, 0), dff(1, 1, 1, 1)]).
step(netb(1, 1, 1, 1, 0),
     rule(14),
     ['A' = 1,
      'B' = 1,
      'C' = 1,
      'Q1' = 1,
      'Q2' = 0,
      'T1' = 1,
      'Nc' = 0,
      'T2' = 0,
      'Na' = 0,
      'T3' = 0],
     [and(1, 1, 1), inv(1, 0), and(1, 0, 0), inv(1, 0), and(0, 1, 0), or(1, 0, 1), or(0, 0, 0)]).
step(testgcc([1, 1, 1], [1, 0, 1], [[1, 0, 0], [0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1,
      'Cs' = [1, 1],
      'State' = [1, 0, 1],
      'Next' = [1, 0, 0],
      'Rest' = [[0, 0, 0], [0, 0, 1]]],
     [gcc(1, [1, 0, 1], [1, 0, 0]), testgcc([1, 1], [1, 0, 0], [[0, 0, 0], [0, 0, 1]])]).
step(gcc(1, [1, 0, 1], [1, 0, 0]),
     rule(15),
     ['C' = 1,
      'Qa' = 1,
      'Qb' = 0,
      'Qc' = 1,
      'Za' = 1,
      'Zb' = 0,
      'Zc' = 0,
      'D1' = 1,
      'D2' = 0,
      'D3' = 0],
     [netb(1, 0, 1, 1, 0), neta(1, 0, 0), dff(1, 1, 1, 1), dff(0, 1, 0, 0), dff(0, 1, 1, 0)]).
step(netb(1, 0, 1, 1, 0),
     rule(14),
     ['A' = 1,
      'B' = 0,
      'C' = 1,
      'Q1' = 1,
      'Q2' = 0,
      'T1' = 1,
      'Nc' = 0,
      'T2' = 0,
      'Na' = 0,
      'T3' = 0],
     [and(1, 1, 1), inv(1, 0), and(0, 0, 0), inv(1, 0), and(0, 1, 0), or(1, 0, 1), or(0, 0, 0)]).
step(neta(1, 0, 0),
     rule(13),
     ['A' = 1, 'B' = 0, 'Q' = 0, 'T1' = 0, 'Na' = 0, 'Nb' = 1, 'T2' = 0],
     [and(1, 0, 0), inv(1, 0), inv(0, 1), and(0, 1, 0), or(0, 0, 0)]).
step(testgcc([1, 1], [1, 0, 0], [[0, 0, 0], [0, 0, 1]]),
     rule(17),
     ['C' = 1, 'Cs' = [1], 'State' = [1, 0, 0], 'Next' = [0, 0, 0], 'Rest' = [[0, 0, 1]]],
     [gcc(1, [1, 0, 0], [0, 0, 0]), testgcc([1], [0, 0, 0], [[0, 0, 1]])]).
step(gcc(1, [1, 0, 0], [0, 0, 0]),
     rule(15),
     ['C' = 1,
      'Qa' = 1,
      'Qb' = 0,
      'Qc' = 0,
      'Za' = 0,
      'Zb' = 0,
      'Zc' = 0,
      'D1' = 0,
      'D2' = 0,
      'D3' = 0],
     [netb(1, 0, 0, 0, 0), neta(1, 0, 0), dff(0, 1, 1, 0), dff(0, 1, 0, 0), dff(0, 1, 0, 0)]).
step(netb(1, 0, 0, 0, 0),
     rule(14),
     ['A' = 1,
      'B' = 0,
      'C' = 0,
      'Q1' = 0,
      'Q2' = 0,
      'T1' = 0,
      'Nc' = 1,
      'T2' = 0,
      'Na' = 0,
      'T3' = 0],
     [and(1, 0, 0), inv(0, 1), and(0, 1, 0), inv(1, 0), and(0, 0, 0), or(0, 0, 0), or(0, 0, 0)]).
step(testgcc([1], [0, 0, 0], [[0, 0, 1]]),
     rule(17),
     ['C' = 1, 'Cs' = [], 'State' = [0, 0, 0], 'Next' = [0, 0, 1], 'Rest' = []],
     [gcc(1, [0, 0, 0], [0, 0, 1]), testgcc([], [0, 0, 1], [])]).
step(testgcc([], [0, 0, 1], []), fact(16), [], []).