/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : z3_randomTest_80_100_4.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
ueln,stzt,vnto,bwqg,atax,zfxz,hzty,tapg,hiqr,dcks,qchi,dmeg,pqys,pwvj,beyg,xdrg,bvyn,panj,etva,atja,umdd,aaqm,lwgu,enfr,gaar,ktjr,qtpa,vbxh,egha,hpxj,fqer,arcn,wzgl,rhfo,xwec,tvzn,vook,ppwr,pgcc,hnmm,rklj,avcy,jguz,dhhm,nnqu,fsje,qnlg,bgps,oiwv,orhc,pnyu,nauk,tgfq,bwuf,jwds,mqjq,vjtn,akbp,xcln,zvws,edeo,raxm,tmaa,frsv,cths,jsbv,ayvj,cckl,dluy,ldsm,jrol,tpmm,tqzi,onqx,xllw,wbjp,zxie,gprk,rwxd,morb
conditionals
randomTest_80_100_4 {
((fsje,dmeg) | ((wbjp;enfr),(zxie;panj))),
((zfxz;(((pnyu;vjtn);vbxh),(!(lwgu;tvzn)))) | aaqm),
(((!rhfo);(!nnqu)) | ((!((!panj);(wzgl,(zfxz,hpxj))));lwgu)),
(hnmm | ((!((!(xcln;ktjr)),oiwv));(!((!(!qchi)),(rwxd,((!(gaar;egha));(nauk,(!jrol)))))))),
(edeo | ((xcln;jrol);(!(hpxj;qchi)))),
((((!(!(!(!vbxh))));((!(atax;vnto)),(dmeg,(!(!qnlg))))),((!(!((dcks;ktjr),(!(!orhc)))));hiqr)) | jsbv),
(orhc | ((!hpxj),(((cths;((!zfxz),(ayvj;edeo)));(!fqer));(!enfr)))),
(zxie | ((tapg;(pnyu,xwec)),(!nnqu))),
(((!ppwr);(!(hzty;tgfq))) | ldsm),
(atja | ((!etva),(!(gprk;mqjq)))),
(((!ktjr),(((!pqys);dluy),(qnlg,fqer))) | (((!akbp),(hiqr;hpxj));panj)),
(((!(!(!((!(umdd;fsje)),jguz)))),(!(!(!xwec)))) | (hzty;lwgu)),
(fsje | ((panj;(!(dluy,avcy)));(nnqu;((!(tvzn,frsv));((arcn,cths),dhhm))))),
((((!fsje),pqys),((tgfq,bvyn);cckl)) | ((jwds,raxm);enfr)),
(gprk | (((vnto;(dluy;(!zfxz))),(fqer;etva)),(!(jsbv,atax)))),
(((!(!aaqm)),(!(!(dmeg,(!etva))))) | (xdrg,(!(zfxz;frsv)))),
((ayvj;raxm) | (fsje,pgcc)),
(((!(raxm,bgps));(((!(!(!(dmeg,vjtn)))),((!pnyu),(tmaa;jsbv))),onqx)) | bvyn),
((xcln;(xwec;tgfq)) | ((tvzn;zvws);(ayvj;beyg))),
(hpxj | (((!((!tvzn);oiwv)),(enfr;(edeo,tqzi))),(!xllw))),
((vook,pnyu) | ((!(!frsv)),(!((!(bvyn,orhc));(!(egha;pqys)))))),
(wbjp | ((!(!(egha;((tmaa,gprk),morb))));hzty)),
((xllw,zxie) | ((!((!vnto);(panj;bgps))),(!((!(fsje,dcks));(!lwgu))))),
((atax;vbxh) | (nauk,rhfo)),
(((dhhm;(vjtn,wzgl));mqjq) | (jwds;(!(((!(!((!ayvj),tvzn)));tmaa);(!(orhc;(!fqer))))))),
((aaqm,nauk) | (((etva;tpmm),(jguz;oiwv)),(!wbjp))),
((pnyu,ppwr) | ((stzt,(ueln,etva)),(lwgu,oiwv))),
((((hiqr,orhc),panj);vnto) | tapg),
(((panj;(onqx;qchi)),((nauk,(!hiqr));bvyn)) | fsje),
(((oiwv,akbp);(!ayvj)) | (arcn;(tvzn;rklj))),
((((!((bwuf;(!nnqu)),ldsm)),(qchi;(!hzty)));(!(xcln,(!(bgps;gaar))))) | akbp),
((umdd;egha) | ((vbxh,(((aaqm,rwxd),avcy),(cths;(!pgcc)))),((!tvzn);(!orhc)))),
(((!((!(hnmm;rwxd));(ueln;((xllw,qchi);panj)))),((!(ldsm;arcn));(!hpxj))) | orhc),
(((atja,(!(!qchi))),((rwxd,panj);(hzty;zvws))) | ((pnyu;onqx);(edeo;vbxh))),
((arcn;(rwxd;jguz)) | ((!panj),((!(!fqer));(wbjp,(atja;(!(!gaar))))))),
((pgcc,qchi) | (((!fsje),oiwv),(!nauk))),
((egha;zvws) | (bwuf,(dluy;wbjp))),
((etva,(rklj,tgfq)) | ((!((!vook),nnqu));(!dcks))),
(((zfxz;(!aaqm));(gaar;akbp)) | beyg),
((xcln;(tqzi;dcks)) | tmaa),
(jwds | (((dhhm;(!vook)),frsv),jsbv)),
(((!(!gaar)),(tqzi,((((!fsje);(!zxie)),gprk);(wzgl;tvzn)))) | ((!(!(tmaa;ldsm))),(!(!vbxh)))),
((cckl;((stzt,(hzty,dcks)),(!((!atja),pgcc)))) | (enfr;(gaar,tmaa))),
((atax;((!(!rhfo));(!xdrg))) | jsbv),
(rwxd | ((etva,pqys);((vook,((aaqm;dluy);gaar)),((dcks,wzgl),jrol)))),
(((!(!nnqu)),pgcc) | ((tqzi,(wbjp;gprk));pnyu)),
(cths | ((!(xwec;(!(!akbp))));((!((tmaa;dhhm),(!onqx)));((!panj);stzt)))),
(atja | (aaqm,(rwxd;xdrg))),
((((((!tqzi);jwds),rhfo);hnmm),(cckl;(stzt;(tgfq;dcks)))) | avcy),
(((!(!(!(xdrg;(ayvj;xcln)))));((!(!dcks)),((bvyn,etva),(vbxh;fqer)))) | akbp),
((((!(!etva));((!ueln),(bwqg,(xdrg,raxm))));bgps) | (lwgu;(tgfq,ldsm))),
((wzgl,(!(zvws,xwec))) | umdd),
(((!(!(zvws;pwvj))),(!(!nnqu))) | dluy),
(((!((!((!(!aaqm)),(!bwuf))),(!(qnlg;((vnto;fsje);xwec)))));(!rklj)) | zfxz),
(((umdd,(!onqx)),((bgps,atax);(xllw,morb))) | ((!qnlg),(!(pqys;(xdrg,cths))))),
((((qchi,atja);jwds),(tqzi,(!gprk))) | (dmeg;((!(!hnmm)),(!mqjq)))),
(((!(!(ayvj;pgcc)));(((cths;hpxj);vbxh);tqzi)) | ((!zvws),(hnmm,(beyg,atax)))),
(((vnto;xllw),arcn) | ((!akbp);((hpxj;ueln),pwvj))),
(jsbv | ((!vbxh);(!((!((morb;xwec);(!jwds)));wzgl)))),
(((!pgcc);(((etva;(onqx,arcn)),(!pqys)),panj)) | ((edeo;dcks);egha)),
((((xwec,xllw);ueln),(lwgu;tmaa)) | (beyg,(!(morb;(qnlg;aaqm))))),
(((stzt,((((wzgl,akbp),morb);(!atax));bvyn)),wbjp) | ayvj),
(((!(dluy,bgps)),xwec) | ((!(!(hiqr;atja)));((beyg;bwqg),(!nauk)))),
((atax,jguz) | ((!tapg),(fqer,tqzi))),
(xllw | (((!(!panj));(!qchi)),(((atax,lwgu);(!bgps));(jrol;((!morb);gprk))))),
(((qchi;wbjp),qtpa) | ((!(!(!jwds)));(xcln;fsje))),
(lwgu | ((!xllw),((!morb),((!((!(!raxm));((!xwec);(beyg;edeo)))),(xcln,qtpa))))),
((mqjq,bwqg) | ((!(!rwxd)),(!(bgps;zvws)))),
(bvyn | (((!bwuf),fsje),frsv)),
((gprk;hiqr) | (tqzi,morb)),
(((ueln;pqys);(!(zfxz,gprk))) | (((!beyg),(zxie,(!mqjq)));(!tpmm))),
((((xdrg,zvws),umdd);(!rwxd)) | ((!(rhfo;atax));(frsv,((vjtn,(!xcln)),dcks)))),
((((tmaa;(!oiwv));(!orhc)),(!nnqu)) | (((gaar;atax);xwec);(!(hzty,(dmeg,atja))))),
(((pqys,(tpmm;(!(tgfq;ktjr))));(((jsbv,dmeg);dluy),(!cckl))) | vbxh),
((bgps;akbp) | ((!(beyg;(tqzi;(!hiqr)))),((avcy,vook);fsje))),
((((!zvws);stzt),(!(!(!avcy)))) | (ueln;rwxd)),
((vnto;hnmm) | (hzty,qtpa)),
(((etva,tapg),(nauk;ppwr)) | qnlg),
((pqys;tqzi) | (xdrg;(hnmm;(gprk;(atax;pgcc))))),
((edeo;((!(jrol,raxm));umdd)) | ((vnto;(!(!ldsm))),(((!dhhm),zvws);avcy))),
(hnmm | (((!(!(!tmaa))),(!(((oiwv,atax);rhfo),stzt)));atja)),
(((!((!rwxd);((!(ktjr,(hpxj,(!(!(!panj))))));(!fsje))));(!(((!etva);(!ldsm));(!tgfq)))) | ayvj),
(((!(!(!nnqu))),((!mqjq),((!gaar);tgfq))) | ((lwgu;qchi),((!jguz),(!(!pnyu))))),
(((!wbjp);xwec) | (rklj;((gprk,(!((!akbp),jsbv)));(!nnqu)))),
(oiwv | (vnto,(bvyn,pnyu))),
(fqer | ((((zfxz,rklj);(jsbv;qnlg)),(tmaa,(umdd,(jrol;avcy)))),ktjr)),
((zxie,((wzgl;rklj),edeo)) | dmeg),
(((!(!(!(beyg;(!((!xllw);(!hzty)))))));((qtpa,(morb,fsje));arcn)) | ((!dluy);(lwgu;stzt))),
(((zvws,qchi),(tmaa,nauk)) | ppwr),
(egha | (ktjr,(!(dcks;bgps)))),
((xdrg;dluy) | ((arcn,ayvj),(vnto;(!(zvws,tapg))))),
(((mqjq;(onqx;xllw)),(!(bgps;morb))) | oiwv),
(((!tapg),(atax;dhhm)) | ((!(!(!((!dcks),(!(!(zfxz;hiqr)))))));(((pgcc,(!etva)),wzgl);(!(!hnmm))))),
((((((!xdrg);gaar);(!umdd)),(tpmm;tmaa));(rhfo;(!(!qnlg)))) | ((arcn,dcks);orhc)),
(((!enfr);atja) | ((!fqer),(!(((pwvj;zvws);((!ueln),(dluy;jguz))),(zxie,hnmm))))),
(((!((!tqzi),(aaqm;hnmm))),(cckl;edeo)) | (atja;panj)),
(((pgcc,qchi);vnto) | xdrg),
(ppwr | ((((pgcc;hpxj),zvws);tpmm);(!((rhfo,vook),tgfq)))),
(((vbxh,dcks);hnmm) | ((!(!cckl)),(fqer;jguz))),
(tapg | ((!zfxz),(((!(!stzt));(!((!((!hzty),(vnto,hiqr))),(!dcks))));((bwqg;ueln),atax))))
}