/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : z3_randomTest_80_100_0.cl
* Type       : Knowledge Base
* Domain     : Randomly Generated
* Date       : 2023-12-19
* Version    : v1.0
* 
* Details    : Signature size        : 80
*              #Conditionals per KB  : 100
* 
* Refs       : 
*
* Comments   : generated for benchmarking a reasoning implementation using the z3 SMT-solver
*
****************************************************************/

signature
fjcv,vjkg,wsbr,dhlb,yxiz,mzyb,grte,vzmc,link,ummr,yghi,xdyp,qnnl,hxjn,kujf,dvbn,sseb,nyzu,niky,mjnj,mgzh,wpkn,skqv,ebut,vuol,oggb,obri,fwpe,covh,juhi,ptms,wfxd,mzjt,wgya,cped,wwdr,ruir,ygjx,xspx,mtnd,uwxe,ymhx,sfdn,pjix,iplk,ogyp,suhr,kylu,icqb,nxvd,hlod,rhni,hiad,cpie,rueg,rrjm,kpno,xhch,jirr,pljq,oase,ywsp,jfzy,vpmh,bgxy,abhj,fard,njay,bxme,uhvy,nwbk,gprh,qlaq,vmwh,wjdv,oqin,fvfa,mbny,ildy,mkhs
conditionals
randomTest_80_100_0 {
(((wwdr;ogyp),(oqin;fwpe)) | (vjkg;(wjdv,((!abhj),grte)))),
((((!(!wpkn));(!vzmc)),((!ygjx);(!ruir))) | vuol),
(((!(kujf;(!(!rueg))));((!(ptms,vzmc)),kylu)) | (mkhs;((!((icqb;mzyb),uwxe)),ywsp))),
(ruir | ((!((!uhvy),(covh,wpkn))),(!((qnnl;fwpe),yghi)))),
(((bgxy,(mgzh;covh));qnnl) | (uwxe;(!ogyp))),
(((((!oggb),(!pjix)),((!fwpe),nyzu));((!(!vjkg));sfdn)) | yxiz),
(((!xspx);(fjcv;(fard,suhr))) | mzjt),
(dhlb | ((!(oase;fjcv));(!covh))),
((pljq,skqv) | ((!(!(ywsp;(fvfa,mzyb)))),(!abhj))),
((((nxvd;(!ptms)),mzyb),((vpmh;wjdv),(ygjx,wgya))) | cped),
(ruir | (gprh,((!oggb),uhvy))),
((ummr;(!vzmc)) | ((ygjx,mkhs),(vjkg,ywsp))),
((kylu,xspx) | (oase;((((!dhlb);(!covh)),skqv),(!((!grte),gprh))))),
(((mkhs;fjcv);mgzh) | (hlod,((((oggb;wgya),(!pljq)),(!ruir)),(!ywsp)))),
((((mjnj;ildy);(suhr,(!ptms))),((!(wwdr,mzjt));kujf)) | (oase,(!(!(!(rhni;nwbk)))))),
((dhlb;(!(ygjx,uwxe))) | ((!mzjt);(!(!((ymhx;wfxd),(covh,mgzh)))))),
((hiad;mtnd) | ((((jfzy;xspx),mjnj);dhlb),(!(!nwbk)))),
(((!(skqv,(vmwh;(!grte))));((!covh);(!ummr))) | ((njay;ywsp);dvbn)),
((((vjkg;ptms);(yghi,rrjm));(!(!(!oase)))) | ((!gprh);(rhni;obri))),
(((!(((!(mzjt;mtnd)),yghi);ummr)),(!iplk)) | (ildy,cpie)),
((((!hxjn),xhch);(xdyp;uhvy)) | (kylu,(!(dvbn;(hlod;niky))))),
((skqv;(!(yxiz,(!cped)))) | ((!((uwxe;vmwh);(!yghi)));(xspx;jfzy))),
(((!fwpe);(oase,cpie)) | mkhs),
(((!(!sseb)),(((!(!wsbr)),((!ymhx),njay)),((!mgzh);(jirr,vpmh)))) | kylu),
(((!(abhj;ymhx)),(!hxjn)) | ((!(!(!mjnj))),(dhlb;((!((!xspx);fjcv)),((!(qlaq,ptms));(!rueg)))))),
(((!((!wfxd),(mjnj,yxiz))),((!((!(iplk;mtnd)),(!(!rrjm)))),(!(!fard)))) | bxme),
(((hlod,njay);nwbk) | ((!pjix);((!sfdn);link))),
((qnnl;cped) | (((!(!((suhr,uwxe);(!vjkg))));hxjn),(!(ygjx;sfdn)))),
((juhi,ruir) | (vpmh,ebut)),
(((!(ywsp;(vpmh;yxiz)));(!(!gprh))) | ((link,oggb),(!(!(ummr;kylu))))),
(((icqb;kylu),((!fjcv);(!pjix))) | (qnnl,(!wsbr))),
((ymhx,sfdn) | ((((!(!(!gprh))),pjix);(vmwh,(mjnj,mbny)));((wwdr,niky);(!yxiz)))),
((((!gprh),(!((oqin,kylu);((xhch,mkhs),wfxd)))),wwdr) | (qlaq;abhj)),
(((!(!ogyp)),(!((!rhni);(!dvbn)))) | ((!(hxjn;icqb)),(!(!((cped,covh);niky))))),
(((mzyb;hxjn),(ywsp;obri)) | ((mzjt;((bgxy,rrjm),covh));fard)),
((oase,(xdyp,(mtnd;vmwh))) | vjkg),
(ogyp | (wgya;(ummr;vmwh))),
((ptms,mzyb) | (((vjkg;abhj),ebut),(!obri))),
((((ebut;wsbr);(!(!link)));vuol) | ((!cped);pljq)),
(ymhx | ((!oggb),((vpmh;uwxe);wwdr))),
(((!(((!icqb);(!hlod));((!bxme);sfdn))),(!(!(!ruir)))) | bgxy),
(wsbr | ((hiad,kujf),vmwh)),
(ildy | (((fard,wjdv);hiad),ywsp)),
(((nyzu,ildy);(!rrjm)) | wwdr),
(((!(!fvfa)),(mzjt,kpno)) | rhni),
((bxme,rueg) | ((!(dhlb,(hlod;iplk)));((ogyp,ildy);((!vuol),fvfa)))),
((sseb;mjnj) | ((ildy;(gprh;link));(((!cpie);ygjx),juhi))),
((oqin;(ummr,hxjn)) | ((!(bxme;niky)),(fjcv,qlaq))),
(((skqv,ymhx);qlaq) | ((ptms,kylu),((kpno;juhi);covh))),
((((!(icqb;ptms));(mzjt,kylu)),((link,(bgxy,(jfzy;ogyp))),covh)) | suhr),
(nyzu | ((!(!kpno));((fvfa;mkhs),((!fjcv);(!ummr))))),
(((!((fwpe,(nxvd;(rrjm;ruir)));vuol));(!oqin)) | (((yghi;rueg);(!rhni)),(!(!mjnj)))),
(((!oggb),iplk) | (hiad;gprh)),
((vjkg;abhj) | (kpno;(((dvbn,mgzh);vpmh);(!pljq)))),
(wjdv | ((!(!(!(!((!(!fwpe));((vmwh,hlod);rrjm)))))),(!(!vzmc)))),
(((wgya,xhch),grte) | ygjx),
(((xspx,nwbk),(!kujf)) | mjnj),
(((fjcv,wsbr),(!(mjnj,((ebut,wwdr);(!uwxe))))) | ((!(!(icqb,dhlb))),(!link))),
(((!uhvy),((!obri),(!nxvd))) | (((icqb,covh),yxiz);vuol)),
((rrjm,(!(wpkn;(!dhlb)))) | (gprh,xspx)),
(((!((!(!(bgxy,fwpe))),(uwxe,jfzy))),(!(oqin,(bxme;(dvbn,vzmc))))) | (qnnl;niky)),
(nxvd | ((dhlb;fard);(!((wsbr,njay);mtnd)))),
(qlaq | ((!(!(link;(xspx;(fwpe,icqb))))),(((!skqv);(fjcv,(hiad,ummr)));yxiz))),
((((!jirr),qnnl),((wgya;(!ogyp));((dvbn;jfzy),suhr))) | ((!grte);(ruir;(!ymhx)))),
(vpmh | ((!(vuol,(vjkg;wwdr))),(((!(sfdn,vzmc)),((!nyzu),(!uwxe))),oqin))),
((((!(!((uwxe;xdyp),fwpe))),(!(!mkhs)));((rhni,sfdn);(wpkn,ygjx))) | (jirr;dvbn)),
(((mgzh;iplk);(hxjn,(pjix;skqv))) | ((!((mzyb;nyzu),(rrjm;uhvy))),njay)),
(((!(link,((!pljq);ywsp))),(mkhs;niky)) | ((!(dhlb;vzmc));(!((!jfzy);vmwh)))),
(qnnl | (obri;(xdyp;ogyp))),
((hiad,(!ymhx)) | ((wjdv,(!oase)),mgzh)),
((((!vuol),(!vjkg));oase) | ((rhni;(gprh,kpno));(!(!ebut)))),
((rrjm;uhvy) | ((!oase),(skqv;(mbny,(nwbk;obri))))),
(mjnj | ((!((ygjx,mtnd);rhni));qnnl)),
((wgya,((ymhx,vpmh);oqin)) | (qlaq;(!cped))),
(((!(((!(mtnd;vzmc)),(wjdv;uhvy));ymhx));ygjx) | (((cped;(!ruir)),sfdn),hxjn)),
(((!((oqin,jfzy),(!ygjx))),((!(!wgya));(oase,cpie))) | (((ymhx,(!sseb)),juhi),oggb)),
((hlod,(wgya;fjcv)) | covh),
(((dvbn;(!kylu)),((!(!icqb));(!fard))) | (kujf,uhvy)),
(((!(!(!qlaq))),(!(nxvd,((!(oggb;fard)),(vjkg,fwpe))))) | ((!nwbk);(wsbr;vzmc))),
(wsbr | (((!(link;(kpno;(!vuol))));(!(yghi;mbny)));nwbk)),
(qnnl | ((bgxy;wwdr),(mkhs;mzjt))),
(((!(!fwpe)),(!ildy)) | ((((oggb,obri),(!(ogyp,xhch))),fjcv),uwxe)),
((xspx;(!(!(kylu,wpkn)))) | fwpe),
((bxme,((rhni,wsbr),vmwh)) | (nxvd,(wgya,mtnd))),
((hiad,grte) | ((((!nwbk),(!(ygjx;bxme))),(!((!pjix),mtnd)));(wwdr,juhi))),
(((dvbn,(cped,(qlaq;wwdr))),dhlb) | ((!(fard;mgzh));oggb)),
(rueg | ((!(xspx,(!wfxd)));((!vpmh);mzyb))),
(((((ygjx,link),wgya);bgxy),(oqin,pljq)) | (oase;(cpie;jirr))),
(((yxiz,rhni);(!vpmh)) | (mzjt;(sseb,(oqin;(wjdv;mgzh))))),
(((!(mjnj;((!ywsp);ptms))),((!fard);(!icqb))) | suhr),
(((oqin;((skqv,covh),oggb));(!xhch)) | (((!mkhs);(!rrjm)),jfzy)),
((mjnj,(xhch,(!mgzh))) | ((!(ruir,xspx)),((!(!oase));((!(mzjt;rueg)),cped)))),
(kujf | (((juhi,jirr),((mbny;njay),rrjm)),(!((jfzy;ummr);ruir)))),
((wpkn,((!(!(!(!((!(!uwxe));dhlb))))),pjix)) | kylu),
(((kylu;(hiad,(!xdyp)));(!(((ywsp,ptms);(!njay)),vzmc))) | (((!ymhx),(!(!wpkn)));(!vjkg))),
(sseb | ((ywsp,cpie),(!dhlb))),
(((!(dhlb;grte)),(dvbn,kpno)) | (((!kylu),yghi);ywsp)),
(((qnnl;(vuol;mkhs));((!wgya);(oase,(mzyb;icqb)))) | covh),
(((jfzy,(gprh,rhni)),cped) | covh),
((((!(!dhlb)),(!(!wsbr))),(!(!vjkg))) | (fjcv,(!yxiz)))
}