/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : z3_randomTest_80_100_1.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
rtot,hyty,ymwh,nbeu,kjpl,tlsk,gplx,uurn,qpuy,pyqn,ejrc,uigo,rgqn,yhgh,zpno,hido,yctp,bfsy,fsjs,zpfc,nwbu,ondx,potn,clrq,uhrs,iidm,vniv,mmbp,sjvg,iwvi,lvrf,tisw,ktuf,gqbu,kbvx,javp,mais,lwng,akwc,godx,fsxg,nutn,ippw,xepw,wsok,yaoa,ihuh,cuvx,ufde,xqgf,nxhd,zxbj,jsft,gtyo,blfn,zmay,rjxr,jjvj,wbee,ttgg,leuj,owfi,jxrd,jzuq,lodu,txrr,vlte,dwzu,vbwy,yknt,kvyk,cjeb,nmll,mbln,nhyp,thdt,kgne,jtjq,cwwj,iqor
conditionals
randomTest_80_100_1 {
((((!iidm),((lodu,vniv),rgqn)),(!(yhgh,(clrq;ejrc)))) | leuj),
((((!jxrd),yctp);((ihuh,kjpl),((!nwbu),(!yhgh)))) | ((!(!ttgg)),(nmll,((!nbeu);hyty)))),
(((!(!((qpuy;hyty);kvyk)));(!owfi)) | (ippw;sjvg)),
((vlte,thdt) | ((nbeu,((nwbu,((hido,cuvx);rjxr));(!zpfc)));(!(!ippw)))),
(((leuj;(!lodu));(!yaoa)) | ufde),
(((!(zmay;(hido;qpuy)));(lwng,(kgne,nbeu))) | (wsok;gqbu)),
(bfsy | (akwc;(jxrd,tlsk))),
((rjxr;ippw) | (jzuq;cjeb)),
((((!(!vlte)),zpfc);(!(qpuy;ondx))) | (iqor,(!(kgne;uigo)))),
((qpuy;(jsft,(!(nbeu;godx)))) | nwbu),
((((!uhrs),thdt),((!(zpno,akwc));fsjs)) | ((!ondx);dwzu)),
((((zpfc;(wbee;ttgg)),(!(nhyp,zxbj))),(((!thdt),nxhd),rtot)) | mmbp),
((hyty,zpfc) | (lwng,cjeb)),
(tisw | (ttgg;(nxhd;(!(ejrc,pyqn))))),
(gqbu | ((!qpuy),((tlsk,kjpl);(!nmll)))),
((javp;(cuvx,(clrq;ymwh))) | ((!(!zpfc)),(!(!(nutn,(yaoa,zxbj)))))),
(((!nmll);kjpl) | (gplx,(!(!((!kbvx),blfn))))),
((((iqor,yctp);(!thdt));(!(!(!cuvx)))) | (fsxg;(!(txrr,nutn)))),
((bfsy;(jzuq,ippw)) | ((nutn,(vlte;ttgg)),hyty)),
(((!(!(!jsft)));((sjvg;ymwh);((kvyk;(ttgg;cwwj)),leuj))) | (rtot,jxrd)),
(((!vniv);ondx) | ((yctp,clrq);vbwy)),
(lodu | (((!(!(!((wsok,jjvj),(ihuh;uhrs)))));((jzuq,owfi);(!(!javp)))),(!ktuf))),
((((!fsxg),(!hyty)),((!(akwc,(!cwwj))),nwbu)) | (wbee,lodu)),
(jsft | ((nhyp,lodu),(!(!iidm)))),
((((!(!(!(!(!(kvyk,rjxr))))));vlte),(!((blfn;(ttgg;yhgh));(!godx)))) | (nxhd;(gqbu,nhyp))),
((((!(!kjpl));(((vlte;yknt);(!(!ymwh)));clrq)),jxrd) | uurn),
((cuvx;(((wsok;(clrq;hyty));rgqn);(!sjvg))) | (xepw,ejrc)),
(((!zmay);(!(thdt,hyty))) | (iidm;vlte)),
(((ippw,akwc);gtyo) | ((!(!gqbu)),(ihuh;dwzu))),
(((ktuf,kgne),(kvyk;(!gtyo))) | vlte),
((ihuh,(nwbu,tlsk)) | (((!iwvi);((lvrf,clrq);nmll)),((!kjpl);uhrs))),
(nbeu | ((!((ondx;tlsk);mmbp));(!(nutn,tisw)))),
(((iidm,nutn);(yknt;qpuy)) | (gqbu,(!jsft))),
(((uurn,(yaoa,owfi));(gqbu;jxrd)) | (((mbln,cuvx),(lvrf;rtot));(!sjvg))),
(((hido;(potn,(cuvx,rjxr))),(!(!ejrc))) | ((lvrf,yknt);(!thdt))),
((((qpuy,zmay),((!kgne);(!(nhyp,cjeb)))),gqbu) | xqgf),
((((!mais),(lvrf;(yaoa,jsft)));(iidm,(!zxbj))) | potn),
(((tlsk;(thdt,qpuy)),akwc) | uigo),
((fsjs,(!thdt)) | (((!(ufde;ttgg)),(!(sjvg;nhyp)));jtjq)),
(((!((!sjvg);jzuq)),gplx) | (nutn,((akwc,(!(!((yhgh;(!javp)),mbln))));nhyp))),
((lwng,((!(lodu;uhrs)),(!(!(!nbeu))))) | (owfi;mais)),
((gqbu,(!jzuq)) | ((!cwwj);((jjvj;lvrf);((!(qpuy;jtjq));potn)))),
(nmll | ((rjxr;thdt);mais)),
(((jtjq,uigo),((!gqbu);mbln)) | ((cwwj,vbwy),fsxg)),
(txrr | ((!((iqor,cjeb);leuj));(((!jjvj);ejrc),jzuq))),
(((owfi;(!(!leuj)));(!((!ejrc),((!yknt);(!vbwy))))) | ((zpfc,tisw),((!nmll),(!kjpl)))),
(((!yctp),(((!gtyo),qpuy);(!cjeb))) | ((rjxr;blfn),(!((!(nbeu,bfsy));(godx,kvyk))))),
(((uhrs,(gqbu,nxhd));hido) | (((!nutn),((iqor;ufde),uurn)),(kvyk;wbee))),
(((wsok,(((!iidm);(((!lvrf);nwbu),tlsk)),(!(cwwj,yctp)))),((!nhyp);mais)) | thdt),
(((((uurn;nhyp);tlsk);((godx;lvrf),yhgh)),(sjvg;cuvx)) | jsft),
(((jjvj;cjeb);hyty) | ((kbvx;wsok),xqgf)),
(((!((uurn;gtyo),fsxg)),(!iwvi)) | ((ttgg,leuj),yctp)),
((((ktuf,(!kbvx));((!iqor);rgqn));(!rjxr)) | ((uigo,thdt),(bfsy;lwng))),
((clrq;((!(!qpuy)),nbeu)) | (((vniv;ejrc),(!(!uigo)));jjvj)),
((kbvx;(iqor,zpfc)) | ((!((!(!gtyo)),(gqbu;mais)));iwvi)),
(((!hyty),(ufde;javp)) | ((hido,(jjvj;clrq)),wbee)),
(txrr | ((!rjxr);((!(wbee;godx)),(!(!jjvj))))),
((((yctp;iqor),leuj);jsft) | (rgqn;vbwy)),
((((!(mmbp,iwvi)),(!(!akwc)));(javp;(kbvx,kvyk))) | ((!(!ttgg)),(!(!(ejrc;(!rgqn)))))),
(((!(kbvx,gplx));(kjpl,(!owfi))) | ((!(xepw,(!(jzuq,leuj))));((!((!ttgg);(!ihuh)));zmay))),
((jzuq,(nmll,(dwzu;akwc))) | (leuj,((zxbj;(kbvx,fsjs)),(!tisw)))),
((kgne;((yknt,akwc),nhyp)) | ((kbvx,((!owfi),(!(!((dwzu,ktuf);(!(!uhrs)))))));nbeu)),
(((!iwvi);nmll) | (((!(!gplx));thdt),(((!lwng),uigo);(gqbu;cwwj)))),
(((!(!zpno)),((tisw,iidm),(!(!iqor)))) | (((mbln,(wbee;(!ondx)));(!owfi));(gplx;gtyo))),
(((!jxrd);(((!mmbp);uurn);clrq)) | ((!rtot),ufde)),
(((!ufde);yctp) | (gplx,mmbp)),
((lodu,godx) | ((!((jxrd;kgne);ihuh));(!((!zxbj),fsjs)))),
((((!kvyk);mais),((vlte;ttgg),uigo)) | ((clrq;(!zxbj)),ippw)),
(((!zxbj),((vlte,(!(nwbu;gplx)));yctp)) | (zpno,(!lodu))),
(mais | (lwng,(!(ufde;ymwh)))),
((dwzu;(!(godx;(!sjvg)))) | (uigo,(!(!(!wsok))))),
((qpuy,leuj) | ((!iwvi),((pyqn;bfsy),gqbu))),
(((ihuh;(gqbu,hyty));(!yknt)) | (lwng;wsok)),
((wsok;pyqn) | ((!ejrc);vniv)),
(((!xqgf);(ufde;ejrc)) | ((!nutn),godx)),
(((xqgf,(!lodu));nhyp) | ((uurn,yctp);(!nwbu))),
(((ejrc;thdt),(jzuq,jjvj)) | zpfc),
((clrq,(!((!thdt),((!(ondx,kbvx));dwzu)))) | ((zxbj;lodu);rtot)),
(((!vlte),(!xqgf)) | ((vbwy;kgne);(rgqn,jzuq))),
((wsok,((!((!vniv);nmll)),(tlsk,jjvj))) | (rtot,(!kvyk))),
(rgqn | ((ymwh,wsok),(tlsk,javp))),
((cwwj;vlte) | (((!(!(!(iidm;(!sjvg)))));(!yctp));(!(!(((wsok;nhyp);zxbj),tlsk))))),
((((akwc;leuj);kvyk),((uurn;(cuvx,lwng));(!(!yaoa)))) | (vlte,yknt)),
(((jtjq;zxbj);(!mmbp)) | (ymwh,(zmay,ejrc))),
((rjxr;gtyo) | ((nbeu;ippw),jzuq)),
(vbwy | (((kjpl,(!(!yhgh)));((ippw,zmay);iwvi));mmbp)),
(((lodu;vbwy),ihuh) | ((iidm;(!akwc)),zpno)),
((owfi,((!yctp);tlsk)) | ((kvyk;kjpl);(!(ktuf,zpno)))),
((xepw;vbwy) | ((godx,mais);((!((owfi,ejrc);(thdt,uurn))),(nbeu,(!(!wbee)))))),
(((!(godx;bfsy));((!ejrc);(tisw,rgqn))) | ((!akwc);((kvyk,(!(!mbln)));(kbvx,ttgg)))),
(lvrf | (((!owfi);(((!(jtjq;nhyp)),hyty),mbln)),(!(!(cjeb;kjpl))))),
((xepw;vbwy) | (((jtjq;ufde);wbee),cjeb)),
(lodu | ((!rtot),(ktuf;(sjvg,((yhgh;leuj);(!kvyk)))))),
((((!((!gtyo),(!uurn)));(!txrr)),jtjq) | (potn,nxhd)),
((wbee;(iwvi;mbln)) | (iidm;lodu)),
((yknt,ufde) | ((!(iwvi;(ttgg;ymwh))),(uigo;(zpfc,ejrc)))),
((((yhgh,zxbj),(vlte;(!(!ihuh)))),(lodu;((rjxr;(!uhrs)),(!wsok)))) | vniv),
(((!(!sjvg)),(!(mmbp;rjxr))) | nutn),
((((!(nbeu,(zpfc,(jxrd,mbln))));(!uigo));(!(!mais))) | (godx,blfn)),
((((rtot;(!(tlsk,hyty)));ymwh);(!nbeu)) | kjpl)
}