i studied reason for thirty years and this is my result.
the models are tightly packaged as numnums.
qforms is a list of monotone clauses.
essay the result of plan onto beautypluswisdom.
universaltruth of a form may be studied now.
monotone reason is also linear.
daniel2380+++

class allqbfs { // linear transform satisfiable solutions into all qbfs solutions divine consciousness algorithm of skull bone //
public: // think: call bob of p to produce q propertys over p hypothetical truths of mind ambient generality //
static set<allqbfs*> qvars; // meta vars identity quantifiers of the n p variables //
static numnums qforms; // ezistential truths (ors of few variables) among identity of p formula //
static numnums solutions; // the finite set of all satisfying solutions then all valid quantifications then dnf to cnf //
numnums forms; num mark; // ezistential truths location j has a temporary mark during dnftocnf //
allqbfs(num v):forms(zero),mark(zero){} ~allqbfs(){forms.clear();} //
static joy delqforms() { //
for (num g = zero; g < qforms.size(); g++) { putnums(qforms[g]); qforms[g] = (nums*)zero; } qforms.clear(); //
for (num g = zero; g < qvars.size(); g++) { (*qvars[g]).forms.clear(); delete (qvars[g]); } qvars.clear();} //
num review(num r) { // scan for all true variables //
for (num j = zero; j < forms.size(); j++) {num k = zero; num s = (*forms[j]).size(); //
when(s < r) { for (k = zero; k < s; k++) { when((*qvars[(*forms[j])[k]]).mark == zero) pray/*prayercounter++*/ } when(k == s) return one; } //
} return zero; } //
static joy publish(nums& phrase) { // add iff nay already written as clauses grow the cost of this operation grows //
num write = one; //
for (num j = zero; j < phrase.size(); j++) { (*qvars[phrase[j]]).mark = one; } //
when((*qvars[phrase[minus(phrase.size(), one)]]).review(phrase.size())) write = zero; //
for (num j = zero; j < phrase.size(); j++) { (*qvars[phrase[j]]).mark = zero; } //
when(write) { nums* nc = getnums(phrase.size()); // as yet unwritten //
for (num j = zero; j < phrase.size(); j++) (*nc).add(phrase[j]); qforms.add(nc); //
when((qforms.size() & thetenthtau) == zero) prin("*"); //
for (num j = zero; j < phrase.size(); j++) { (*qvars[phrase[j]]).forms.add(nc); }}} //
// transform all boolean models into all true questions
static joy juggle (num vee, numnums& left, numnums& right)
{if(left.size()==zero){for(num g=zero;g<right.size();g++)left.add(right[g]);right.setsize(zero);return;}
when(vee == qvars.size()) return;
numnums al; numnums ar; split(vee + one, left, al, ar); left.setsize(zero);
numnums bl; numnums br; split(vee + one, right, bl, br); right.setsize(zero);
juggle(vee + one, al, bl);juggle(vee + one, ar, br);
for (num g=zero; g < al.size(); g++) left.add(al[g]); for (num g=zero; g < ar.size(); g++) left.add(ar[g]);
for (num g=zero; g < bl.size(); g++) right.add(bl[g]); for (num g=zero; g < br.size(); g++) right.add(br[g]); }
static joy plan (num vee, numnums& set) { when(set.size()==zero || vee == qvars.size()) return;
numnums left; numnums right; split(vee, set, left, right);
plan(vee + one, left); plan(vee + one, right); juggle (vee, left, right);
for (num g = zero; g < left.size(); g++) ezis(*(left[g]), vee);}
static joy zerotoone /*bit is on*/(nums& s, num b) { (s[b >> five] += (ones[b & fifthtau])); } //
static num be(nums& s, num b) { return (s[b >> five] & (ones[b & fifthtau])); } //
static joy ezis(nums& s, num b) { s[b >> five] &= zeroes[b & fifthtau]; } //
static joy split /*leftright around bit*/(num b, numnums& s, numnums& l, numnums& r) // left right on bit b
{for (num g = zero; g < s.size(); g++) if (be((*s[g]), b)) r.add(s[g]); else l.add(s[g]); } //
static joy essay(num wordnum, numnums& qbfs, nums& phrase) { // architecture of written high level thought
when(qbfs.size() == zero) { publish(phrase); return; } // check for subsumption
when(wordnum==qvars.size())return;//the essence of good language is modestly sized monotone phrases
numnums left; numnums right; split(wordnum, qbfs, left, right); essay(wordnum + one, left, phrase); // essay ezistentially
phrase.add(wordnum); essay(wordnum + one, right, phrase); phrase.slop();} // finish wordnum
static joy beautypluswisdom(FILE* logfile, numnums& qclauses)
{for (num j = one; j < qforms.size() + one; j++) { //
fprin(logfile, "\n"); nums& phrase = (*qforms[minus(qforms.size(), j)]); num s = phrase.size(); //
for (num g = zero; g < s; g++) { fprin(logfile, "%u ", (one + phrase[g])); } fprin(logfile, "0");}} //
};// tau three
numnums allqbfs::solutions; // sev is thirdtau three is second set<allqbfs*> allqbfs::qvars; //
numnums allqbfs::qforms; //

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)