/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : z3_randomTest_80_100_5.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
dber,mxvx,efta,pwxo,qmbs,gygc,sqol,cgzg,qpwx,ieqn,ylpx,qaef,jopo,hgqb,fquh,embi,ayei,tdcr,gjya,zvxx,cxhc,rxbb,thsg,ygux,wvnp,hllx,xlhw,hhcv,xmak,wawb,saph,etse,nmfs,fsin,ghxs,vpre,yxgz,htgn,jmsu,kaqt,ulvz,qxvq,azfk,lupn,adgq,xijl,zjlj,ozpb,wqin,nysa,vxsx,xizc,drti,edvh,mnuw,jnwp,bqmi,yqnx,jjcf,dusc,fdrp,dolh,amdi,gley,dswp,zcvp,uidy,kjjv,degi,iics,eubm,rvtd,lurw,ryoi,sxcs,lwby,nyyr,zmws,vkyp,iyll
conditionals
randomTest_80_100_5 {
((ayei;(nyyr,fsin)) | (tdcr,lupn)),
((wqin;(jopo,dswp)) | qaef),
(((xmak,ieqn);(!((ulvz,(!nysa)),(!(sxcs;jjcf))))) | ((fsin,nmfs),sqol)),
((((!nyyr),kjjv);(yqnx,(pwxo;iics))) | zvxx),
((mxvx;qpwx) | (qmbs,uidy)),
(((!lupn),(((uidy;pwxo),(!iyll)),jmsu)) | rxbb),
((xizc,(!embi)) | (pwxo,ulvz)),
(((hgqb;(!cgzg)),(!mnuw)) | ((!((uidy,wqin);(amdi;ozpb)));(!degi))),
(((mnuw,(qaef;(!jjcf)));((hgqb,(!ylpx)),(sxcs,iyll))) | ((lwby;(!ieqn));(!edvh))),
((((ayei;lwby),(thsg;vkyp));embi) | efta),
((pwxo;wvnp) | (eubm,vxsx)),
((etse,((!((ryoi;ghxs),((!nmfs);dber))),(!(!(dusc,zcvp))))) | (pwxo,htgn)),
((degi,(adgq,lupn)) | (((!(!hllx)),((ygux,ayei);(cxhc;ieqn)));(!(!(!jjcf))))),
(((!(drti,nyyr)),cxhc) | (((jmsu,cgzg),(!vxsx));((fquh,adgq),(!hllx)))),
((((ryoi,ygux);(dber,lurw));((!efta);(wqin;((!cxhc);hllx)))) | fquh),
((jopo,gjya) | (((!(!(jjcf;dswp))),(nyyr;(!fquh)));(xijl,cxhc))),
((hgqb,(!hllx)) | ((jjcf,saph),(!gley))),
((saph;rxbb) | (jjcf;(vkyp;(uidy,amdi)))),
(((ozpb,(!kaqt));(dusc,saph)) | ((efta;amdi),sxcs)),
(((gley,(!(!tdcr)));hgqb) | (cgzg,((etse,(zvxx;amdi)),(!(lurw,bqmi))))),
((((!(qxvq,htgn)),(cxhc;vkyp));(!(!bqmi))) | ((!(qpwx,(saph,vpre))),(!(kjjv,cgzg)))),
(((!(!(!(((qaef,vkyp);fdrp),uidy)))),(dolh;(azfk;wvnp))) | (((!yxgz),(!ryoi));(!fquh))),
(saph | ((!((!efta),dswp));((!((!(ieqn;qxvq));tdcr));((edvh;(xlhw;nysa));dber)))),
((pwxo,((htgn,bqmi),(!xijl))) | ((mxvx;dber);(jopo,iyll))),
(((!drti),((!dber),lupn)) | ((!(!xlhw)),ryoi)),
((gjya,(hllx,(!htgn))) | lurw),
(((!ieqn);((sqol,(!cgzg));wqin)) | ((!edvh);(((xlhw,iyll);nmfs),zmws))),
(((!(!jnwp)),(eubm,dusc)) | gjya),
(lwby | (((!(hgqb;qaef));((!(jopo;lurw));zjlj)),hllx)),
(((!(!wqin)),((zcvp,(xizc;qmbs));(!(((vxsx,rxbb),ygux),saph)))) | ozpb),
((((((!eubm);rvtd);(!thsg));(cxhc;(!vpre))),(hllx,zcvp)) | gygc),
(((((ryoi,dber);zvxx);iyll);(!zcvp)) | jopo),
(((!xijl);((!(dolh;((!iics);(!zmws))));(!vxsx))) | ((!(!(!jjcf))),(!(xizc,(!saph))))),
((nmfs,htgn) | ((((qpwx;((iyll;eubm),vxsx));(!dswp));lwby),jjcf)),
((qaef;zvxx) | ((wawb,(!kjjv));((!(bqmi;hgqb)),wvnp))),
(((lwby,(!gygc)),(!(!yqnx))) | (rxbb,saph)),
(((xlhw;(!dolh)),(!(!vpre))) | ((degi,(!dusc));(!(!(ryoi;hhcv))))),
((((zmws,(embi,fdrp)),(xizc,sxcs)),(thsg;uidy)) | htgn),
(qmbs | (((jnwp;qxvq);nyyr);dber)),
((dber;zcvp) | (fquh;(!gley))),
((((qmbs;ryoi),(!uidy));(jnwp,iyll)) | (vkyp;(nysa;etse))),
(((!(!(kaqt,ygux))),((!((((!ylpx);cxhc),pwxo),lupn));amdi)) | (dber;xijl)),
(((!vkyp),(!dusc)) | (((!(vxsx;ozpb)),(!(!ylpx)));(xijl;ayei))),
(thsg | (((!(mnuw;dswp)),(!((gjya;wqin);degi))),(!(jopo;rxbb)))),
((zjlj,(amdi,dolh)) | (ryoi,((!ieqn),(xizc;((xmak;eubm);(qpwx,bqmi)))))),
(embi | (((zmws;(ylpx,hllx));(kjjv,(!ghxs))),hgqb)),
(((!(((wvnp,ghxs);(!xijl)),(wqin;ozpb)));((!lurw);(qmbs;mxvx))) | bqmi),
(((qaef,adgq);bqmi) | pwxo),
(((!(etse;kjjv)),(!pwxo)) | ((!((drti;((mxvx;amdi),xmak));gygc)),(!(!(ulvz,ryoi))))),
((sqol,(eubm;yxgz)) | (lurw;(!(!(!(lwby;htgn)))))),
(((jopo;thsg),(!(eubm,dusc))) | zjlj),
((mnuw,bqmi) | (sqol;(xmak,ygux))),
(((gygc,(gley,fquh)),((!xijl);(!bqmi))) | ryoi),
(tdcr | ((zmws;(mxvx,dswp)),((!(!amdi));((!yxgz);qpwx)))),
((((vxsx;efta),dusc),(gjya,((nmfs;(!hllx)),(embi,zmws)))) | (azfk;sxcs)),
(((zcvp,(!(!(hgqb,bqmi))));azfk) | nyyr),
((sxcs;ulvz) | (lupn;kaqt)),
(((xlhw;(!xijl)),(!ylpx)) | jopo),
((gley;dber) | (fdrp;(qaef,qmbs))),
(((jopo;xijl),zmws) | lupn),
(lwby | ((qxvq,kaqt),(!ylpx))),
((kaqt;(pwxo,tdcr)) | ((!htgn),((!zmws);(!dber)))),
(((nyyr;iyll),(!efta)) | (fsin,gley)),
(((jopo,ayei);saph) | ((!xmak);((dusc,(xijl,mnuw)),ulvz))),
(((ayei,(!lupn)),(vkyp,thsg)) | ((!kjjv),((wqin;lurw),(!(xizc,gygc))))),
((kaqt;(!((((!(!(!nmfs))),(wqin,(!(zcvp;dber))));((!yqnx),xizc));(!(!fquh))))) | gjya),
(qpwx | ((!((!(rxbb,edvh));((ozpb;rvtd);(lwby;(!zmws))))),(!xlhw))),
(zjlj | (((sqol,(hllx,zvxx));lwby),((!jmsu),(((!gley),vxsx),(!jjcf))))),
(((!((qpwx,edvh);((wawb;xijl),(!xizc))));(!((!tdcr),amdi))) | (dswp;lwby)),
((gjya,qxvq) | (((xmak,sqol),(!(fquh,xizc)));(lupn;iics))),
((lwby,gjya) | (((!((wawb,gley);rvtd));hgqb);((!(!(!ghxs))),(!(!dolh))))),
(ryoi | (((jnwp;ozpb),(!(((nmfs,nysa),dolh);sqol))),(!kjjv))),
((adgq;nmfs) | ((!((ieqn,amdi);(etse,(lurw,htgn))));(!(!(!efta))))),
(((nmfs,((!nysa);ygux)),vxsx) | wvnp),
(((!(((!((embi;zcvp);yxgz));wqin),(!(!(lwby,fdrp)))));(!(!amdi))) | (jnwp;qxvq)),
((fdrp,(!(!qpwx))) | ((!lupn);(((!(zcvp;(!xijl))),((jnwp;gley);(nysa,jopo))),(!(!(!drti)))))),
((((embi,(((!zvxx);rvtd);(!(ayei,dusc)))),degi);(!(!(!(!wqin))))) | lurw),
((zcvp;(bqmi,(hhcv,zjlj))) | qmbs),
(((gygc,kaqt),((!lurw),jjcf)) | ((!((htgn,hllx),zmws)),(drti,(uidy,(!jopo))))),
((degi;qxvq) | ((!(iyll,nmfs));(!bqmi))),
(saph | ((!(cgzg;kaqt));((!dber),(!qaef)))),
(fdrp | (((zcvp,dolh),ulvz),vpre)),
(((!((!lupn),((!wqin);zmws)));(qaef,(((jjcf,jopo);kjjv),(!yxgz)))) | nmfs),
((ieqn;lwby) | ((((!fdrp),sxcs);(!(iics;bqmi)));mnuw)),
(((cgzg,(!zjlj)),qxvq) | ((mnuw;iyll);((!(!(ulvz;gjya)));((!zcvp);qaef)))),
(((!rxbb),(sxcs;(dolh;xizc))) | (((!mnuw),((lupn,eubm),iyll));((!mxvx),jnwp))),
((pwxo;((!dber);etse)) | (fsin,bqmi)),
((hhcv;(!(!(hgqb;wqin)))) | ((!kjjv);vkyp)),
((gjya;(xijl,(((!(gley;uidy)),(!(jjcf;lupn))),(!embi)))) | (lwby,fquh)),
((((vkyp;(!ryoi)),((!hgqb),(!nmfs))),fdrp) | (xizc,xijl)),
((((!((iyll;nysa);htgn));sqol);qmbs) | ((!(qaef,(gley,tdcr)));(!gygc))),
(jnwp | (jjcf;((htgn,(!nyyr)),(qaef;degi)))),
((mnuw;(qaef;((!ylpx);amdi))) | (hhcv,(rxbb;dolh))),
(ozpb | (((qpwx;gygc),drti);(jnwp,(iics;htgn)))),
(((yxgz;edvh),ieqn) | ((!qxvq);((!vpre),iyll))),
((xijl;((lupn;qmbs),ghxs)) | (qpwx;(!jopo))),
((((qpwx,(!ylpx));(!azfk));(!((xlhw,yqnx),lurw))) | ((!(wawb;efta)),qmbs)),
(((qmbs,sxcs);wqin) | (gley,((!(yxgz;(ylpx;cxhc)));(!rvtd)))),
((((!(!rvtd));(iics;((!cxhc),(!embi)))),(!hllx)) | ((rxbb,zmws),(!dolh))),
(((pwxo;(efta;mxvx)),(!gygc)) | (((!dber);qpwx),(!(!((sqol,cgzg),(!qmbs))))))
}