/****************************************************************
* This file is part of CLKR - www.fernuni-hagen.de/wbs/clkr/
* 
* File       : z3_randomTest_80_100_2.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
zman,yaeg,hhlm,prfu,cpep,yeyy,bbxi,xipg,afhc,qqfx,nxrw,fqas,rxwh,zjqs,hgfu,fsxv,keae,otsu,ppfv,kaii,caxt,sweb,jaii,hzpn,rpzv,ogfy,fyok,wgjd,jdsn,fwce,zwyy,nprg,ofxg,udkx,spcu,qvqm,stao,hhdx,cvzo,ujgn,hipb,ocjs,gvfp,rxtg,pyzv,uqmg,zafu,dpsk,zddz,jwsp,tgky,lwho,jwfj,zgtb,wqib,kapu,aihz,tmjc,lwzb,ppjy,huur,oojo,vsyd,syjg,cnxk,vdun,mkdm,cbvu,hyqj,mlnd,idxh,lpuq,auko,fytg,buoo,ewmy,oykr,ynrz,aeah,edml
conditionals
randomTest_80_100_2 {
(((uqmg;(prfu;aeah)),(jwfj,ogfy)) | cbvu),
(ynrz | ((((!fsxv),jaii);((!rxwh);((!(!lwho));ewmy))),aihz)),
((jwfj;(((ppfv;jwsp);uqmg),((edml,ewmy);(!(!fytg))))) | (yaeg,syjg)),
((((uqmg;cvzo),(!(!(!(!tmjc)))));(!cbvu)) | ((hzpn;idxh),(lwho;(edml;auko)))),
(((!aeah),(((fytg;(pyzv;edml));mlnd),(!(huur,yeyy)))) | ujgn),
((wgjd,(!hipb)) | (((tgky;(!zgtb)),idxh);bbxi)),
(xipg | ((!(!tmjc));((hzpn,((((prfu,lwzb);nxrw);syjg);(!hyqj)));wgjd))),
(caxt | (ogfy;(kaii,(!gvfp)))),
(((!ocjs);ppfv) | ((!(!(!(dpsk;cnxk))));(!((!lwho),((fwce;keae),fsxv))))),
((((oojo;zwyy),(bbxi,zgtb));((tmjc;nxrw),xipg)) | jwsp),
((((spcu,fytg);(!(nprg;sweb))),(!(!((!(lwho;keae));cpep)))) | tgky),
(((pyzv;jwfj);(!(lpuq,otsu))) | kaii),
((((vdun;(!hgfu)),(fytg,ppjy));(ogfy,(!kapu))) | zjqs),
((hzpn;wqib) | (((!((udkx;vdun),oojo));((!(!cpep));aeah)),(!(!(spcu,(hipb,cbvu)))))),
((((hhdx;(!lwho));(!(!(afhc,(ppjy,prfu))))),(udkx,yeyy)) | sweb),
(ynrz | (sweb;(tgky,((!(!zddz)),(nprg,ogfy))))),
(spcu | ((huur;prfu),(!((rxtg;stao),(fsxv,(ujgn,(sweb;auko))))))),
(afhc | ((rpzv,sweb),stao)),
(((!mlnd);((ewmy;fyok),(!ogfy))) | ((sweb,tgky);udkx)),
(((!(!ujgn));cpep) | ((!kaii),(((!pyzv);huur),(stao,lwho)))),
(((afhc;(hhdx;zgtb));jdsn) | ((!(mkdm;((!sweb),yeyy)));(!(prfu,rpzv)))),
(cpep | (((qvqm,(idxh;buoo)),(!ynrz)),(!aeah))),
(((cbvu,qqfx),((!(oykr;((!nxrw),jwsp))),caxt)) | (zgtb,kapu)),
(udkx | ((!(!(!vsyd)));((((oykr,uqmg);(!fqas)),(!lpuq)),(((!ewmy),(!buoo));(qqfx;cnxk))))),
(((zjqs;(!ynrz));(!zgtb)) | (bbxi;(!(otsu;auko)))),
(((tmjc,((cvzo;zddz);kapu)),(lwzb;(!sweb))) | (hyqj;stao)),
(((!(ujgn;cvzo)),lwho) | cpep),
(zddz | (((!lwho),(!wqib)),(!(!(udkx,fwce))))),
(((tgky;spcu);yaeg) | ((kaii,aeah);(cbvu,(hipb,cpep)))),
(((cnxk;nxrw);aeah) | (hgfu;(tgky;zddz))),
((syjg,udkx) | (((wgjd,hgfu),mkdm),((ewmy;rxtg),((fwce,buoo);ynrz)))),
(rxwh | ((zafu;(!otsu)),(!((zman;(oojo;hyqj));fsxv)))),
(((ynrz,(((gvfp;zjqs);(!otsu));hzpn)),(!(((xipg;prfu);lwzb);rxwh))) | zman),
(hhdx | ((!((!(aeah,caxt));(((!idxh),oojo);bbxi)));(!(!(huur;vdun))))),
(((!kaii);((jdsn,keae);(dpsk;xipg))) | ((hzpn,(!(lpuq,sweb))),(ppjy;bbxi))),
(((fsxv;mlnd),cnxk) | (((aeah,((!huur);(!otsu))),nprg);(((!jaii),(!idxh));cpep))),
(((mlnd,fyok),(rpzv,wgjd)) | tgky),
((udkx;(!(!mlnd))) | (lwzb,nprg)),
(((((jwsp,aeah),(!cpep));(ogfy,lpuq));(!otsu)) | fsxv),
((fqas;cpep) | ((!dpsk);(((ppjy,((hyqj,ofxg);hzpn));qvqm),keae))),
(((!(aeah;(buoo;(lpuq,qvqm))));((!nprg),(!yeyy))) | ((!(otsu;fyok)),(hhlm;fwce))),
((rpzv;hhlm) | ((hhdx,(cpep,udkx)),(!(!pyzv)))),
(((qqfx;vdun),(!((!(!hhdx)),(!keae)))) | ogfy),
(((aihz,lwzb);((!zddz),(hzpn;(!((xipg;qqfx);dpsk))))) | (afhc,fsxv)),
((((!(!(!zman))),auko),(!dpsk)) | (((!hipb);(((!oykr),lpuq),afhc)),(cnxk;fsxv))),
(((!(hhlm;(qvqm,kapu)));(!tgky)) | ((otsu,lpuq),(!cvzo))),
((fytg;(idxh,vdun)) | ((!(!(wqib;qqfx)));((ocjs,(aeah,wgjd));edml))),
(((syjg;ofxg),(!spcu)) | ((qqfx;fqas);(!nxrw))),
(((!(((!(!fwce));ujgn),wgjd)),fsxv) | ((spcu,(cbvu;(!(stao;hhdx)))),vsyd)),
(lwho | (((!(jwfj,caxt)),(!hyqj));(buoo,(yeyy,ofxg)))),
((rpzv,(yeyy;zafu)) | ((!(!(qqfx;gvfp)));mkdm)),
(((ppjy,buoo),caxt) | (afhc;mkdm)),
((oykr,kapu) | (jdsn,ewmy)),
((aeah,(ewmy;(((!nxrw);aihz);spcu))) | (jdsn,((rxtg,gvfp),lpuq))),
(((lpuq,hyqj);huur) | qqfx),
(((lpuq;(fytg,lwzb));(!sweb)) | hyqj),
((fsxv;(ofxg;vsyd)) | vdun),
(((oykr,(!spcu)),(cpep;lwzb)) | (aeah,((!((ppjy,(!cvzo)),(lwho,afhc))),hipb))),
((((!((!qvqm),kapu));hipb),(!mkdm)) | (cbvu;fwce)),
(((ujgn;(!cvzo));(!rxtg)) | cnxk),
(((keae,(!auko)),((zman;bbxi),gvfp)) | (spcu,((!(!(!cvzo))),ynrz))),
((buoo;cpep) | ((fqas;((xipg,hhdx);(!rxtg)));((cnxk,tgky),wgjd))),
(((((lwzb;prfu);uqmg),(!((!ppfv);((oykr;jwfj),ujgn))));zafu) | (udkx;huur)),
(((!(bbxi;mkdm)),wgjd) | (jdsn,otsu)),
(((udkx;(aihz,(!prfu))),(vdun;zafu)) | ((!rxwh);((!(!(kapu,vsyd))),(!dpsk)))),
((jwsp;(udkx;huur)) | ((dpsk;(!((bbxi;nxrw);ewmy)));ujgn)),
(((!(ogfy;ofxg)),(!(!(!(((!(oojo;(rpzv;(fwce,hhdx)))),cnxk),mlnd))))) | rxwh),
(dpsk | ((!vsyd),((uqmg,kapu);ofxg))),
(zddz | ((!(zwyy;ofxg)),((wgjd,rpzv),afhc))),
((lwho,(hyqj;(!oojo))) | ((!(!wqib)),(((!aeah);(!kapu));(ujgn;((!tgky),zgtb))))),
(pyzv | (((!zddz);dpsk);idxh)),
(dpsk | ((stao,xipg),sweb)),
(((wgjd,(!(keae;edml)));((jdsn;(!lwho));zgtb)) | (kaii;oojo)),
((((ynrz,fytg);(!otsu)),mlnd) | zman),
(((!zddz);(((!lwho);oojo),pyzv)) | ((rxtg;tgky);(!(nxrw,(fsxv;jwsp))))),
((jwfj,(lwho;fqas)) | vdun),
((ynrz;vsyd) | ((zgtb;rxwh);oojo)),
((((vdun;ujgn);((jaii,ppjy),(!cpep)));(!fyok)) | lpuq),
((((!(!rxwh)),(!(!afhc)));(!tmjc)) | (xipg,(!fyok))),
((qvqm;(ppjy;fytg)) | cvzo),
((idxh;(!spcu)) | ((!(!sweb)),((rxwh,kapu);hipb))),
(edml | ((nxrw,rpzv),(zafu,huur))),
(idxh | ((!zman),((!(buoo;jwsp));(!lwho)))),
(((!((ogfy;(ppfv;hzpn)),(!(wqib;syjg))));(!((!zgtb);((!ppjy);rpzv)))) | (nprg;zwyy)),
((nxrw;(ocjs;caxt)) | (prfu;(!(ofxg,((qqfx;fqas);kapu))))),
(zddz | ((stao;yeyy),(!(!(!auko))))),
(jwsp | ((keae,(!(!hhlm)));ynrz)),
((jaii;oykr) | ((!(!((ogfy,buoo);sweb)));((!(ewmy;(!((hhdx;bbxi),hgfu))));(!stao)))),
(udkx | (qvqm;(mlnd,aeah))),
(((auko,((qqfx;vdun),((!mkdm),(!ogfy)))),(jwsp;stao)) | ((keae,wqib),hhlm)),
((pyzv,(hipb;cpep)) | (((ynrz,udkx),(cvzo;buoo)),(zafu,yaeg))),
((rxwh;(aeah,((huur,cvzo);vdun))) | hhdx),
(rxtg | ((hhdx,(!zafu)),jdsn)),
(hyqj | ((ofxg;cvzo),otsu)),
(((!(!zgtb));(!(!(!spcu)))) | ((!rxwh),(bbxi,(auko;cnxk)))),
(((rpzv;lpuq),(!auko)) | (keae,((((afhc;(mlnd,hyqj)),(!zgtb)),aihz);hipb))),
(ynrz | (ocjs,(yaeg;fqas))),
((((auko;mlnd);vsyd),(!(!hyqj))) | (((!((!qqfx),(!(!(!zjqs)))));(!((!tmjc);bbxi)));(!(!(!(wqib,yeyy)))))),
((((!(zafu,ppfv));(((lwho;hyqj),(vdun,rpzv)),caxt));(!ewmy)) | zman),
(((!(!hhlm));(yaeg,prfu)) | zman)
}