% File generated by sugar.Output [int,x,[[2,9]]]. [int,y,[[2,3],[5,5],[8,9]]]. [int,z,[[1,3],[5,5],[7,9]]]. [int,w,[[-927,1000]]]. % $I1 : (abs w) [int,'$I1',[[0,1000]]]. % $I2 : $I1+y+0 [int,'$I2',[[2,1009]]]. % $I3 : w+z+0 [int,'$I3',[[-918,1009]]]. [bool,p]. [bool,q]. [bool,r]. [bool,'$B1']. [bool,'$B2']. [bool,'$B3']. [bool,'$B4']. [bool,'$B5']. [bool,'$B6']. [bool,'$B7']. [bool,'$B8']. [bool,'$B9']. [bool,'$B10']. [bool,'$B11']. [bool,'$B12']. [bool,'$B13']. [bool,'$B14']. [bool,'$B15']. [relation,r,2,[conflicts,[1,2],[3,4]]]. % (imp p (imp q r)) [or,[not,p],[not,q],r]. [or,[not,'$B2'],[not,[r,x,y]]]. [or,[not,'$B3'],[r,y,x]]. [or,'$B2','$B3']. [or,[not,'$B4'],[r,x,y]]. [or,[not,'$B5'],[not,[r,y,x]]]. [or,'$B4','$B5']. % (gt (add x y) 10) [wsum,[[1,x],[1,y]],ge,11]. % (imp (eq x 9) (and p q (eq z 1))) [or,[wsum,[[1,x]],le,8],'$B1']. [or,p,[not,'$B1']]. [or,q,[not,'$B1']]. [or,[wsum,[[1,z]],le,1],[not,'$B1']]. [or,[not,'$B6'],[wsum,[[1,x],[1,y]],ge,10]]. [or,[not,'$B7'],[wsum,[[1,y],[1,z]],ge,10]]. [or,'$B6','$B7']. % $I1 == (abs w) [wsum,[[1,'$I1'],[-1,w]],ge,0]. [wsum,[[1,'$I1'],[1,w]],ge,0]. [or,[not,'$B8'],[wsum,[[1,'$I1'],[-1,w]],le,0]]. [or,[not,'$B9'],[wsum,[[1,'$I1'],[1,w]],le,0]]. [or,'$B8','$B9']. % $I2 == (add 0 (mul 1 $I1) (mul 1 y)) [wsum,[[-1,'$I1'],[1,'$I2'],[-1,y]],le,0]. [wsum,[[-1,'$I1'],[1,'$I2'],[-1,y]],ge,0]. % $I3 == (add 0 (mul 1 w) (mul 1 z)) [wsum,[[1,'$I3'],[-1,w],[-1,z]],le,0]. [wsum,[[1,'$I3'],[-1,w],[-1,z]],ge,0]. % (ge (add w (abs w) x y z) 100) [wsum,[[1,'$I2'],[1,'$I3'],[1,x]],ge,100]. [or,[not,'$B10'],[wsum,[[1,x],[-1,y]],le,-1]]. [or,[not,'$B11'],[wsum,[[1,x],[-1,y]],ge,1]]. [or,'$B10','$B11']. [or,[not,'$B12'],[wsum,[[1,x],[-1,z]],le,-1]]. [or,[not,'$B13'],[wsum,[[1,x],[-1,z]],ge,1]]. [or,'$B12','$B13']. [or,[not,'$B14'],[wsum,[[1,y],[-1,z]],le,-1]]. [or,[not,'$B15'],[wsum,[[1,y],[-1,z]],ge,1]]. [or,'$B14','$B15']. [or,[wsum,[[1,x]],ge,3],[wsum,[[1,y]],ge,3],[wsum,[[1,z]],ge,3]]. [or,[wsum,[[1,x]],le,7],[wsum,[[1,y]],le,7],[wsum,[[1,z]],le,7]].