%% Copyright (C) 2005 Igor Stéphan
%% 
%% This program is free software; you can redistribute it and/or
%% modify it under the terms of the GNU General Public License
%% as published by the Free Software Foundation; either version 2
%% of the License, or (at your option) any later version.
%% 
%% This program is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%% 
%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
%% http:%%www.gnu.org/copyleft/gpl.html
%%
%% igor.stephan@univ-angers.fr
%% 
'qbf_and'(LX, LY, LZ) <=>LX=0, LY=0, LZ=1 | fail. %[2]
'qbf_and'(LX, LY, LZ) <=>universal(LZ), LX=0, LY=0 | fail. %[4]
'qbf_and'(LX, LY, LZ) <=>LX=0, LY=1, LZ=1 | fail. %[6]
'qbf_and'(LX, LY, LZ) <=>universal(LZ), LX=0, LY=1 | fail. %[8]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=0, LZ=1 | fail. %[11]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=0, LZ=1 | fail. %[12]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=0, LY=LZ | fail. %[14]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=0, litteraux_opposes(LY,LZ) | fail. %[16]
'qbf_and'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=0,leq(LY,LZ) | fail. %[18]
'qbf_and'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=0,leq(LY,LZ) | fail. %[20]
'qbf_and'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=0,leq(LZ,LY) | fail. %[23]
'qbf_and'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=0,leq(LZ,LY) | fail. %[24]
'qbf_and'(LX, LY, LZ) <=>LX=1, LY=0, LZ=1 | fail. %[26]
'qbf_and'(LX, LY, LZ) <=>universal(LZ), LX=1, LY=0 | fail. %[28]
'qbf_and'(LX, LY, LZ) <=>LX=1, LY=1, LZ=0 | fail. %[29]
'qbf_and'(LX, LY, LZ) <=>universal(LZ), LX=1, LY=1 | fail. %[32]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=1, LZ=0 | fail. %[34]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=1, LZ=1 | fail. %[36]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=1, litteraux_opposes(LY,LZ) | fail. %[39]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=1, litteraux_opposes(LY,LZ) | fail. %[40]
'qbf_and'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=1,leq(LY,LZ) | fail. %[42]
'qbf_and'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=1,leq(LY,LZ) | fail. %[44]
'qbf_and'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=1,leq(LZ,LY) | fail. %[46]
'qbf_and'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=1,leq(LZ,LY) | fail. %[48]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=0, LZ=1 | fail. %[51]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=0, LZ=1 | fail. %[52]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=0, LX=LZ | fail. %[54]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=0, litteraux_opposes(LX,LZ) | fail. %[56]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=0,leq(LX,LZ) | fail. %[58]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=0,leq(LX,LZ) | fail. %[60]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=0,leq(LZ,LX) | fail. %[63]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=0,leq(LZ,LX) | fail. %[64]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=1, LZ=0 | fail. %[66]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=1, LZ=1 | fail. %[68]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=1, litteraux_opposes(LX,LZ) | fail. %[71]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=1, litteraux_opposes(LX,LZ) | fail. %[72]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=1,leq(LX,LZ) | fail. %[74]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=1,leq(LX,LZ) | fail. %[76]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=1,leq(LZ,LX) | fail. %[78]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=1,leq(LZ,LX) | fail. %[80]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LZ=0, LX=LY | fail. %[82]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LZ=1, LX=LY | fail. %[84]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LX=LY, litteraux_opposes(LX,LZ) | fail. %[87]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LX=LY, litteraux_opposes(LX,LZ) | fail. %[88]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), LX=LY,leq(LX,LZ) | fail. %[90]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), LX=LY,leq(LX,LZ) | fail. %[92]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), LX=LY,leq(LZ,LX) | fail. %[94]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), LX=LY,leq(LZ,LX) | fail. %[96]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LZ=1, litteraux_opposes(LX,LY) | fail. %[99]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LZ=1, litteraux_opposes(LX,LY) | fail. %[100]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LX=LZ, litteraux_opposes(LX,LY) | fail. %[102]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=LZ, litteraux_opposes(LX,LY) | fail. %[104]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | fail. %[106]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | fail. %[108]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | fail. %[111]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | fail. %[112]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=0,leq(LX,LY) | fail. %[116]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=0,leq(LY,LX) | fail. %[120]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=1,leq(LX,LY) | fail. %[122]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=1,leq(LX,LY) | fail. %[123]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=1,leq(LX,LY) | fail. %[124]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=1,leq(LY,LX) | fail. %[126]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=1,leq(LY,LX) | fail. %[127]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=1,leq(LY,LX) | fail. %[128]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LX=LZ,leq(LX,LY) | fail. %[132]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LX=LZ,leq(LY,LX) | fail. %[136]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | fail. %[138]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | fail. %[139]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | fail. %[140]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | fail. %[142]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | fail. %[143]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | fail. %[144]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LY=LZ,leq(LX,LY) | fail. %[148]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), LY=LZ,leq(LY,LX) | fail. %[152]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | fail. %[154]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | fail. %[155]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | fail. %[156]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | fail. %[158]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | fail. %[159]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | fail. %[160]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[162]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[164]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[166]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[168]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[172]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[174]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[175]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[176]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[178]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[180]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[182]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[184]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[188]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[190]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[191]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[192]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[196]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[198]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[199]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[200]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[204]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[206]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[207]
'qbf_and'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[208]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | LY <- 0,LZ <- 0. %[186]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | LZ <- 0,LY <- 0. %[202]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | LX <- 0,LZ <- 0. %[170]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | LZ <- 0,LX <- 0. %[194]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | LY <- 1,LX <- LZ. %[187]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | LX <- 1,LY <- LZ. %[171]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | LX <- 0,LY <- 1. %[153]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | LY <- 1,LX <- 0. %[157]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=0, LY=LZ | LY <- 0. %[13]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=1, LZ=0 | LY <- 0. %[33]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=0,leq(LY,LX) | LY <- 0. %[118]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), LY=LZ,leq(LY,LX) | LY <- 0. %[150]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=0, litteraux_opposes(LX,LZ) | LX <- 1. %[55]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=1, LZ=1 | LX <- 1. %[67]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LZ=1, LX=LY | LX <- 1. %[83]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=LZ, litteraux_opposes(LX,LY) | LX <- 1. %[103]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), LY=LZ,leq(LX,LY) | LX <- 1. %[146]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | LX <- 1,LY <- 0. %[137]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | LY <- 0,LX <- 1. %[141]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=0, litteraux_opposes(LY,LZ) | LY <- 1. %[15]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=1, LZ=1 | LY <- 1. %[35]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LY), LX=LZ,leq(LY,LX) | LY <- 1. %[134]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=0, LX=LZ | LX <- 0. %[53]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=1, LZ=0 | LX <- 0. %[65]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LZ=0, LX=LY | LX <- 0. %[81]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LX=LZ, litteraux_opposes(LX,LY) | LX <- 0. %[101]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=0,leq(LX,LY) | LX <- 0. %[114]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LY), LX=LZ,leq(LX,LY) | LX <- 0. %[130]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), LZ=1,leq(LX,LY) | LX <- 1,LY <- 1. %[121]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LY), LZ=1,leq(LY,LX) | LY <- 1,LX <- 1. %[125]
'qbf_and'(LX, LY, LZ) <=>existential(LZ), LX=0, LY=0 | LZ <- 0. %[3]
'qbf_and'(LX, LY, LZ) <=>existential(LZ), LX=0, LY=1 | LZ <- 0. %[7]
'qbf_and'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=0,leq(LY,LZ) | LZ <- 0. %[17]
'qbf_and'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=0,leq(LY,LZ) | LZ <- 0. %[19]
'qbf_and'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=0,leq(LZ,LY) | LZ <- 0. %[21]
'qbf_and'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=0,leq(LZ,LY) | LZ <- 0. %[22]
'qbf_and'(LX, LY, LZ) <=>existential(LZ), LX=1, LY=0 | LZ <- 0. %[27]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=0,leq(LX,LZ) | LZ <- 0. %[57]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=0,leq(LX,LZ) | LZ <- 0. %[59]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=0,leq(LZ,LX) | LZ <- 0. %[61]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=0,leq(LZ,LX) | LZ <- 0. %[62]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | LZ <- 0. %[105]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | LZ <- 0. %[107]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | LZ <- 0. %[109]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | LZ <- 0. %[110]
'qbf_and'(LX, LY, LZ) <=>LX=0, LY=0, LZ=0 | true. %[1]
'qbf_and'(LX, LY, LZ) <=>LX=0, LY=1, LZ=0 | true. %[5]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=0, LZ=0 | true. %[9]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=0, LZ=0 | true. %[10]
'qbf_and'(LX, LY, LZ) <=>LX=1, LY=0, LZ=0 | true. %[25]
'qbf_and'(LX, LY, LZ) <=>LX=1, LY=1, LZ=1 | true. %[30]
'qbf_and'(LX, LY, LZ) <=>existential(LY), LX=1, LY=LZ | true. %[37]
'qbf_and'(LX, LY, LZ) <=>universal(LY), LX=1, LY=LZ | true. %[38]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=0, LZ=0 | true. %[49]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=0, LZ=0 | true. %[50]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LY=1, LX=LZ | true. %[69]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LY=1, LX=LZ | true. %[70]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LX=LY, LX=LZ | true. %[85]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LX=LY, LX=LZ | true. %[86]
'qbf_and'(LX, LY, LZ) <=>existential(LX), LZ=0, litteraux_opposes(LX,LY) | true. %[97]
'qbf_and'(LX, LY, LZ) <=>universal(LX), LZ=0, litteraux_opposes(LX,LY) | true. %[98]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=1,leq(LZ,LX) | LX <- LZ. %[77]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=1,leq(LZ,LX) | LX <- LZ. %[79]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), LX=LY,leq(LZ,LX) | LX <- LZ. %[93]
'qbf_and'(LX, LY, LZ) <=>existential(LX), universal(LZ), LX=LY,leq(LZ,LX) | LX <- LZ. %[95]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=1,leq(LX,LZ) | LZ <- LX. %[73]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=1,leq(LX,LZ) | LZ <- LX. %[75]
'qbf_and'(LX, LY, LZ) <=>existential(LX), existential(LZ), LX=LY,leq(LX,LZ) | LZ <- LX. %[89]
'qbf_and'(LX, LY, LZ) <=>universal(LX), existential(LZ), LX=LY,leq(LX,LZ) | LZ <- LX. %[91]
'qbf_and'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=1,leq(LZ,LY) | LY <- LZ. %[45]
'qbf_and'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=1,leq(LZ,LY) | LY <- LZ. %[47]
'qbf_and'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=1,leq(LY,LZ) | LZ <- LY. %[41]
'qbf_and'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=1,leq(LY,LZ) | LZ <- LY. %[43]
'qbf_and'(LX, LY, LZ) <=>existential(LZ), LX=1, LY=1 | LZ <- 1. %[31]
'qbf_and'(LX, LY, LZ) ==>universal(LX), existential(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | LZ <- 0. %[195]
'qbf_and'(LX, LY, LZ) ==>existential(LX), universal(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | LZ <- 0. %[203]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), LZ=0,leq(LX,LY) [113]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), LZ=0,leq(LX,LY) [115]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), LZ=0,leq(LY,LX) [117]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), LZ=0,leq(LY,LX) [119]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), LX=LZ,leq(LX,LY) [129]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), LX=LZ,leq(LX,LY) [131]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), LX=LZ,leq(LY,LX) [133]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), LX=LZ,leq(LY,LX) [135]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), LY=LZ,leq(LX,LY) [145]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), LY=LZ,leq(LX,LY) [147]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), LY=LZ,leq(LY,LX) [149]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), LY=LZ,leq(LY,LX) [151]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [161]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [163]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [165]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), universal(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [167]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) [169]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) [173]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [177]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [179]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [181]
%'qbf_and'(LX, LY, LZ) est contingent pour universal(LX), universal(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [183]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) [185]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) [189]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) [193]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) [197]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) [201]
%'qbf_and'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) [205]