/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : z3_randomTest_80_100_3.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
sqve,mdyt,wgli,syaw,nulm,mlgm,eaay,vrfv,lehi,toef,iigk,vgwy,cjiq,qewi,pphf,gxxn,fcrx,mrtp,wzkm,ujbb,nfsv,vajk,afsf,hpub,jnyg,qrpl,mxqo,avdn,sdli,obow,keoi,nxxn,rkxw,oxar,oafj,bhqm,qvlh,ghhy,wode,wqgx,bpkz,qumy,ywus,kowi,kipk,yeqd,eraj,fveq,aksz,vpuz,usgb,ysdg,mtji,shyc,mkue,dkpc,dqnz,qwou,ntxg,dtsw,zquq,yall,hxla,dodu,cgvz,sckp,fxcq,nyqy,tjdq,qovy,rrfy,kugl,gvzv,dzpr,naan,xyiz,flbd,zuwp,yfeo,dqjr
conditionals
randomTest_80_100_3 {
(((vpuz,(afsf;(!qewi)));kugl) | (wgli,eaay)),
((((nxxn;(wgli;rrfy));vajk);(mkue,shyc)) | kowi),
(wzkm | (((toef;mxqo),(!xyiz));(!(naan,yall)))),
(((!(!((qewi,nxxn);mrtp)));wgli) | (((pphf;qumy),dkpc),gxxn)),
((flbd,lehi) | (bpkz;(qovy;jnyg))),
(((!iigk);(((qumy;mtji),((!yfeo),kipk)),((mrtp,zquq);fxcq))) | vajk),
(((!(sqve;fcrx)),(((!(!(kowi,vpuz))),eaay),xyiz)) | (dqnz;(!((cgvz,obow);shyc)))),
(xyiz | ((!((!pphf);(zuwp,(!qumy)))),((!(!fcrx));(yall;(((toef,sqve),vgwy);keoi))))),
((rrfy,(qovy;vajk)) | (((pphf;ysdg),((!(!aksz)),hxla));(oafj;(!gxxn)))),
(hxla | (((!(((rrfy,oafj);(keoi;tjdq));dodu)),(!nyqy));((!dqjr);wode))),
(kipk | (((cgvz;(tjdq;(zuwp;aksz))),((mkue,ghhy),obow)),shyc)),
(((!(!gvzv));(!((rkxw;(bpkz,sqve));mxqo))) | (mdyt;(eaay;vgwy))),
((nyqy;wode) | (((mrtp;((yeqd;qumy),qrpl)),mlgm),(!qovy))),
(((!eraj);qwou) | ((!(avdn,dqjr)),(!(!nyqy)))),
((wode,yall) | ((zuwp,lehi),(!(!vpuz)))),
(usgb | (cgvz,(qewi;(!iigk)))),
((shyc,yfeo) | (nyqy;jnyg)),
(((!((naan,(!dqjr)),vajk)),(!(rkxw;(!cjiq)))) | bpkz),
((((!(gvzv;ghhy)),(!(kipk;(!mxqo))));(pphf;dodu)) | ((!(!(eaay,nxxn))),(!(tjdq;oxar)))),
(((naan,wqgx);(lehi,aksz)) | gvzv),
(((!(!(qumy,qovy))),(!((oxar;(flbd,zuwp)),(!yfeo)))) | ((eaay,hxla),vajk)),
(((!(!(!qwou)));(naan,(oafj;(wqgx;jnyg)))) | (((!pphf),(!cjiq));(!(!dtsw)))),
((((kipk,mdyt);(!wzkm));ywus) | ((!cgvz);(!(fxcq,((!vajk),(!(((!mlgm),qvlh),qewi))))))),
((((vpuz,eaay);(wode,(!rrfy)));nulm) | sdli),
((eraj;(flbd,(!dzpr))) | (dodu,ghhy)),
((sckp,kowi) | ((!vpuz),((toef,kugl);((!zuwp);gxxn)))),
(mlgm | ((sckp;(nulm,kowi));(fveq,cjiq))),
(oxar | ((!(!(!((iigk;tjdq),(((shyc;fcrx);kipk),dqjr))))),(!keoi))),
(((!qvlh);((ghhy,(toef;eaay));(dodu,jnyg))) | ((vajk,ysdg);nulm)),
(((!(flbd,(((!fveq);yeqd),(bpkz,(oafj;qovy)))));kipk) | yall),
(dkpc | (dtsw,((!(!gxxn));nxxn))),
(((dkpc,sdli),(!fxcq)) | ((!obow),(!(dtsw;(!bhqm))))),
((gvzv,oafj) | ((!(!(!qovy))),(afsf;lehi))),
((tjdq;(!qumy)) | (oxar;(!aksz))),
((afsf,nyqy) | (((!(!wqgx)),zuwp),(vgwy,yall))),
(wzkm | ((!(!(!((!((flbd,(pphf,toef));((!obow),(mdyt,qrpl))));(mlgm,eraj))))),usgb)),
((fveq,tjdq) | (((!sckp);(!mkue));(ntxg;((toef,eraj);vpuz)))),
((wzkm;(!((gvzv,qrpl),(!(((!sckp);syaw);(nxxn,avdn)))))) | (vrfv,(!vajk))),
(((!((((vrfv;wgli),(wzkm;eraj));nxxn),(!kugl)));(wqgx;qwou)) | (nyqy,toef)),
((((!syaw),dtsw);lehi) | (((toef;(!wode));(kugl;nulm)),(sdli,(!((!wqgx),(!bpkz)))))),
(mkue | ((!(!(dqnz;gvzv))),(cjiq;((!dkpc);((yall;pphf);fcrx))))),
(((!nfsv),(shyc,wode)) | tjdq),
((((!flbd);(!wgli)),(ujbb,(!(!dtsw)))) | (qumy,eaay)),
(((obow,fveq);rkxw) | (((!gvzv);ysdg);sckp)),
((dzpr,(!iigk)) | (ywus,((syaw,bpkz),sckp))),
(((qvlh,ujbb);(((!yall);(!(!qumy)));rkxw)) | (ywus;fxcq)),
(((!vajk);(yeqd,naan)) | ((lehi;(!ntxg)),(!wqgx))),
(cjiq | ((!gxxn);((!(zuwp;(!wgli)));(obow;(!(toef;nxxn)))))),
(((!vpuz),(wqgx;(ujbb,ysdg))) | nxxn),
(((!(dodu;mtji));((!(!((aksz;(!nfsv));yeqd))),((oafj,wqgx),syaw))) | hpub),
(qwou | ((iigk;sckp);(!qrpl))),
((nfsv,yall) | ((eraj;xyiz),((cjiq;ghhy),(!yfeo)))),
(((xyiz;mrtp);((ywus,(dtsw;hxla));(!eaay))) | (tjdq,naan)),
(((!(bhqm,mtji)),(!((mxqo;nfsv);wzkm))) | (toef,hxla)),
(lehi | ((vpuz;qewi);(flbd;(!(!(ujbb,jnyg)))))),
((mtji;(gvzv,vpuz)) | (((!(!(!fcrx)));(lehi,sdli)),(!((xyiz;wzkm),(!nfsv))))),
(eraj | (((!(vrfv,fxcq)),(!(((!qvlh);ywus),(mkue,(dqjr;(!zuwp))))));sckp)),
(((!(vgwy;yall)),(mlgm,ysdg)) | (fcrx,oafj)),
((fveq;dodu) | ((!kugl);qvlh)),
(zuwp | ((!((shyc,hxla),(((nulm,tjdq),kipk);nyqy)));(vpuz,wqgx))),
((yeqd;qewi) | (syaw;vajk)),
(((keoi;mlgm);(kugl;gxxn)) | fveq),
(((zquq;xyiz);(naan,nyqy)) | (mxqo;flbd)),
((kipk,xyiz) | (((rrfy,fveq);sckp);zuwp)),
(((shyc,vgwy);(afsf;mkue)) | sdli),
((((mdyt,gvzv),(yeqd;cjiq)),(zuwp;lehi)) | nfsv),
(hxla | ((!(!iigk));((shyc;(!(!dqjr)));(eaay,(sckp;zuwp))))),
(vgwy | ((!(!cgvz)),(!(!(((mdyt;(nulm;qvlh)),bhqm),ntxg))))),
((((wqgx,yfeo),((!iigk);ntxg));(!kugl)) | dzpr),
(((!vpuz);(cgvz;((obow,(wgli;eaay)),hpub))) | ((!rrfy);((dkpc,iigk);oafj))),
(((ywus,((eaay;xyiz);yall));(!(cgvz;iigk))) | zquq),
(((!mxqo),(!(!((!jnyg),((!dodu),cjiq))))) | (naan,(qovy;(tjdq,(dkpc,(!rrfy)))))),
(((obow;yfeo),mkue) | ((pphf,cgvz);(!(!((!ysdg);shyc))))),
((mrtp,(mxqo,(wqgx,dkpc))) | (hxla;(!(!qewi)))),
(mtji | ((qwou;hpub);dkpc)),
(((!(qovy;hpub));(!wqgx)) | ((mtji,(!avdn));((((!cjiq),fxcq);(nxxn;pphf));sckp))),
(fcrx | ((!(keoi,ghhy));(wgli;(!(!(shyc,vgwy)))))),
(((!(!qwou)),(sdli;((!dzpr);kugl))) | ((iigk;vrfv);(!fxcq))),
((zuwp;(!oafj)) | (hpub,cgvz)),
(mlgm | (qwou,((dqnz,vrfv),(!(zuwp,oxar))))),
(((!(!avdn));(gvzv,dodu)) | naan),
(((mdyt;mrtp);(!oxar)) | (((!qovy);(mtji,tjdq)),(!nxxn))),
(((wzkm,(!mrtp)),(!rkxw)) | eraj),
(((!obow);((!oafj);(fcrx;(!bhqm)))) | ((gxxn;jnyg),(aksz,fxcq))),
(rkxw | ((!bhqm);((!((wode,pphf),((ywus,zquq),afsf))),sckp))),
((((!(sdli;(!(qvlh;iigk)))),(!((!naan);vrfv)));dodu) | (((!mtji);ywus),sqve)),
((ntxg;(nyqy;vrfv)) | ((!(!(!(qrpl,eraj))));(!(!(oafj;hxla))))),
(gvzv | ((!(!(!((!kowi);(!rkxw)))));(!((fcrx;((!wgli),dqnz));lehi)))),
(((shyc,mxqo);naan) | hxla),
(naan | ((!(eaay,sqve)),(!((nulm;(!nxxn));oafj)))),
((rrfy,fcrx) | ((qovy,(!nxxn)),(!hxla))),
((sqve;(((!(avdn,mkue)),wzkm),((!nfsv);dqjr))) | aksz),
((vpuz;mlgm) | ((pphf,zuwp),(!rrfy))),
(dkpc | (lehi,(jnyg;(mtji;((!rkxw),ghhy))))),
(((qewi;kipk),(zquq,((dtsw,(kugl,yall)),oxar))) | vgwy),
(((toef;nulm);ysdg) | afsf),
((kipk;((!obow),(!((mtji;usgb),(nulm,dtsw))))) | vpuz),
(((!((!gvzv);ujbb));(!qovy)) | (((qumy,(!yeqd));(yfeo,yall)),(!(!((!(oafj;(!flbd)));dqnz))))),
(((yeqd,gvzv);(sqve;wzkm)) | dzpr),
(((wgli,sqve);((nulm;(!syaw)),(!(!mdyt)))) | mlgm)
}