%% 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_xor'(LX, LY, LZ) <=>LX=0, LY=0, LZ=1 | fail. %[2]
'qbf_xor'(LX, LY, LZ) <=>universal(LZ), LX=0, LY=0 | fail. %[4]
'qbf_xor'(LX, LY, LZ) <=>LX=0, LY=1, LZ=0 | fail. %[5]
'qbf_xor'(LX, LY, LZ) <=>universal(LZ), LX=0, LY=1 | fail. %[8]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=0, LZ=0 | fail. %[10]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=0, LZ=1 | fail. %[12]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=0, litteraux_opposes(LY,LZ) | fail. %[15]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=0, litteraux_opposes(LY,LZ) | fail. %[16]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=0,leq(LY,LZ) | fail. %[18]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=0,leq(LY,LZ) | fail. %[20]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=0,leq(LZ,LY) | fail. %[22]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=0,leq(LZ,LY) | fail. %[24]
'qbf_xor'(LX, LY, LZ) <=>LX=1, LY=0, LZ=0 | fail. %[25]
'qbf_xor'(LX, LY, LZ) <=>universal(LZ), LX=1, LY=0 | fail. %[28]
'qbf_xor'(LX, LY, LZ) <=>LX=1, LY=1, LZ=1 | fail. %[30]
'qbf_xor'(LX, LY, LZ) <=>universal(LZ), LX=1, LY=1 | fail. %[32]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=1, LZ=0 | fail. %[34]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=1, LZ=1 | fail. %[36]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=1, LY=LZ | fail. %[37]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=1, LY=LZ | fail. %[38]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=1,leq(LY,LZ) | fail. %[42]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=1,leq(LY,LZ) | fail. %[44]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=1,leq(LZ,LY) | fail. %[46]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), universal(LZ), LX=1,leq(LZ,LY) | fail. %[48]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=0, LZ=0 | fail. %[50]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=0, LZ=1 | fail. %[52]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=0, litteraux_opposes(LX,LZ) | fail. %[55]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=0, litteraux_opposes(LX,LZ) | fail. %[56]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=0,leq(LX,LZ) | fail. %[58]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=0,leq(LX,LZ) | fail. %[60]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=0,leq(LZ,LX) | fail. %[62]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=0,leq(LZ,LX) | fail. %[64]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=1, LZ=0 | fail. %[66]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=1, LZ=1 | fail. %[68]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=1, LX=LZ | fail. %[69]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=1, LX=LZ | fail. %[70]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=1,leq(LX,LZ) | fail. %[74]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=1,leq(LX,LZ) | fail. %[76]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=1,leq(LZ,LX) | fail. %[78]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), LY=1,leq(LZ,LX) | fail. %[80]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LZ=1, LX=LY | fail. %[83]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LZ=1, LX=LY | fail. %[84]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LX=LY, LX=LZ | fail. %[86]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LX=LY, litteraux_opposes(LX,LZ) | fail. %[88]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), LX=LY,leq(LX,LZ) | fail. %[90]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), LX=LY,leq(LX,LZ) | fail. %[92]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), LX=LY,leq(LZ,LX) | fail. %[95]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), LX=LY,leq(LZ,LX) | fail. %[96]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LZ=0, litteraux_opposes(LX,LY) | fail. %[97]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LZ=0, litteraux_opposes(LX,LY) | fail. %[98]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LX=LZ, litteraux_opposes(LX,LY) | fail. %[102]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=LZ, litteraux_opposes(LX,LY) | fail. %[104]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | fail. %[106]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | fail. %[108]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | fail. %[111]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | fail. %[112]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=0,leq(LX,LY) | fail. %[114]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=0,leq(LX,LY) | fail. %[116]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=0,leq(LY,LX) | fail. %[118]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=0,leq(LY,LX) | fail. %[120]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=1,leq(LX,LY) | fail. %[122]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=1,leq(LX,LY) | fail. %[124]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=1,leq(LY,LX) | fail. %[126]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LZ=1,leq(LY,LX) | fail. %[128]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LX=LZ,leq(LX,LY) | fail. %[130]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LX=LZ,leq(LX,LY) | fail. %[132]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LX=LZ,leq(LY,LX) | fail. %[135]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LX=LZ,leq(LY,LX) | fail. %[136]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | fail. %[138]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | fail. %[140]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | fail. %[143]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | fail. %[144]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LY=LZ,leq(LX,LY) | fail. %[147]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LY=LZ,leq(LX,LY) | fail. %[148]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LY=LZ,leq(LY,LX) | fail. %[150]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), LY=LZ,leq(LY,LX) | fail. %[152]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | fail. %[155]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | fail. %[156]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | fail. %[158]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | fail. %[160]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[162]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[164]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[166]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) | fail. %[168]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[170]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[172]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[174]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) | fail. %[176]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[178]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[180]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[182]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) | fail. %[184]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[186]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[188]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[190]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) | fail. %[192]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[194]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[196]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[198]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) | fail. %[200]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[202]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[204]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[206]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), universal(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) | fail. %[208]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=0, LZ=1 | LX <- 1. %[51]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=1, LZ=0 | LX <- 1. %[65]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LX=LY, litteraux_opposes(LX,LZ) | LX <- 1. %[87]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LX=LZ, litteraux_opposes(LX,LY) | LX <- 1. %[101]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | LX <- 1. %[153]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LX,LY) | LX <- 1. %[154]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | LX <- 1. %[157]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), litteraux_opposes(LY,LZ),leq(LY,LX) | LX <- 1. %[159]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=0, LZ=0 | LX <- 0. %[49]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=1, LZ=1 | LX <- 0. %[67]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LX=LY, LX=LZ | LX <- 0. %[85]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=LZ, litteraux_opposes(LX,LY) | LX <- 0. %[103]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LY=LZ,leq(LX,LY) | LX <- 0. %[145]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LY=LZ,leq(LX,LY) | LX <- 0. %[146]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LY=LZ,leq(LY,LX) | LX <- 0. %[149]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LY=LZ,leq(LY,LX) | LX <- 0. %[151]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=0, LZ=1 | LY <- 1. %[11]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=1, LZ=0 | LY <- 1. %[33]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | LY <- 1. %[137]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LX,LY) | LY <- 1. %[139]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | LY <- 1. %[141]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), litteraux_opposes(LX,LZ),leq(LY,LX) | LY <- 1. %[142]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=0, LZ=0 | LY <- 0. %[9]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=1, LZ=1 | LY <- 0. %[35]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LX=LZ,leq(LX,LY) | LY <- 0. %[129]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LX=LZ,leq(LX,LY) | LY <- 0. %[131]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LX=LZ,leq(LY,LX) | LY <- 0. %[133]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LX=LZ,leq(LY,LX) | LY <- 0. %[134]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LZ=1,leq(LY,LX) | LX <- ~LY. %[125]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=1,leq(LY,LX) | LX <- ~LY. %[127]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LZ=1,leq(LX,LY) | LY <- ~LX. %[121]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=1,leq(LX,LY) | LY <- ~LX. %[123]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LZ=0,leq(LY,LX) | LX <- LY. %[117]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LY), LZ=0,leq(LY,LX) | LX <- LY. %[119]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LY), LZ=0,leq(LX,LY) | LY <- LX. %[113]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LY), LZ=0,leq(LX,LY) | LY <- LX. %[115]
'qbf_xor'(LX, LY, LZ) <=>existential(LZ), LX=0, LY=1 | LZ <- 1. %[7]
'qbf_xor'(LX, LY, LZ) <=>existential(LZ), LX=1, LY=0 | LZ <- 1. %[27]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | LZ <- 1. %[105]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LX,LZ) | LZ <- 1. %[107]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | LZ <- 1. %[109]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), litteraux_opposes(LX,LY),leq(LZ,LX) | LZ <- 1. %[110]
'qbf_xor'(LX, LY, LZ) <=>LX=0, LY=0, LZ=0 | true. %[1]
'qbf_xor'(LX, LY, LZ) <=>LX=0, LY=1, LZ=1 | true. %[6]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=0, LY=LZ | true. %[13]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=0, LY=LZ | true. %[14]
'qbf_xor'(LX, LY, LZ) <=>LX=1, LY=0, LZ=1 | true. %[26]
'qbf_xor'(LX, LY, LZ) <=>LX=1, LY=1, LZ=0 | true. %[29]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), LX=1, litteraux_opposes(LY,LZ) | true. %[39]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), LX=1, litteraux_opposes(LY,LZ) | true. %[40]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=0, LX=LZ | true. %[53]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=0, LX=LZ | true. %[54]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LY=1, litteraux_opposes(LX,LZ) | true. %[71]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LY=1, litteraux_opposes(LX,LZ) | true. %[72]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LZ=0, LX=LY | true. %[81]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LZ=0, LX=LY | true. %[82]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), LZ=1, litteraux_opposes(LX,LY) | true. %[99]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), LZ=1, litteraux_opposes(LX,LY) | true. %[100]
'qbf_xor'(LX, LY, LZ) <=>existential(LZ), LX=0, LY=0 | LZ <- 0. %[3]
'qbf_xor'(LX, LY, LZ) <=>existential(LZ), LX=1, LY=1 | LZ <- 0. %[31]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), LX=LY,leq(LX,LZ) | LZ <- 0. %[89]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), LX=LY,leq(LX,LZ) | LZ <- 0. %[91]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), LX=LY,leq(LZ,LX) | LZ <- 0. %[93]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), LX=LY,leq(LZ,LX) | LZ <- 0. %[94]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=1,leq(LZ,LX) | LX <- ~LZ. %[77]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=1,leq(LZ,LX) | LX <- ~LZ. %[79]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=1,leq(LX,LZ) | LZ <- ~LX. %[73]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=1,leq(LX,LZ) | LZ <- ~LX. %[75]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=0,leq(LZ,LX) | LX <- LZ. %[61]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), universal(LZ), LY=0,leq(LZ,LX) | LX <- LZ. %[63]
'qbf_xor'(LX, LY, LZ) <=>existential(LX), existential(LZ), LY=0,leq(LX,LZ) | LZ <- LX. %[57]
'qbf_xor'(LX, LY, LZ) <=>universal(LX), existential(LZ), LY=0,leq(LX,LZ) | LZ <- LX. %[59]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=1,leq(LZ,LY) | LY <- ~LZ. %[45]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=1,leq(LZ,LY) | LY <- ~LZ. %[47]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=1,leq(LY,LZ) | LZ <- ~LY. %[41]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=1,leq(LY,LZ) | LZ <- ~LY. %[43]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=0,leq(LZ,LY) | LY <- LZ. %[21]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), universal(LZ), LX=0,leq(LZ,LY) | LY <- LZ. %[23]
'qbf_xor'(LX, LY, LZ) <=>existential(LY), existential(LZ), LX=0,leq(LY,LZ) | LZ <- LY. %[17]
'qbf_xor'(LX, LY, LZ) <=>universal(LY), existential(LZ), LX=0,leq(LY,LZ) | LZ <- LY. %[19]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [161]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [163]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [165]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), universal(LY), existential(LZ),leq(LX,LY), leq(LY,LZ), leq(LX,LZ) [167]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) [169]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) [171]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) [173]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), universal(LZ),leq(LX,LZ), leq(LZ,LY), leq(LX,LY) [175]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [177]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [179]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [181]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), universal(LY), existential(LZ),leq(LY,LX), leq(LX,LZ), leq(LY,LZ) [183]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) [185]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) [187]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) [189]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), universal(LZ),leq(LY,LZ), leq(LZ,LX), leq(LY,LX) [191]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) [193]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), existential(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) [195]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) [197]
%'qbf_xor'(LX, LY, LZ) est contingent pour universal(LX), existential(LY), universal(LZ),leq(LZ,LX), leq(LX,LY), leq(LZ,LY) [199]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) [201]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), existential(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) [203]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), existential(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) [205]
%'qbf_xor'(LX, LY, LZ) est contingent pour existential(LX), universal(LY), universal(LZ),leq(LZ,LY), leq(LY,LX), leq(LZ,LX) [207]