ZenonModulo---0.5.0.UNK-Non.f

%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : SYN425+1 : TPTP v8.2.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n012.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Jun 25 02:18:35 EDT 2024

% Result   : Unknown 2.20s 2.44s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SYN425+1 : TPTP v8.2.0. Released v2.1.0.
% 0.00/0.12  % Command  : run_zenon_modulo %d %s
% 0.11/0.33  % Computer : n012.cluster.edu
% 0.11/0.33  % Model    : x86_64 x86_64
% 0.11/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33  % Memory   : 8042.1875MB
% 0.11/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33  % CPULimit : 300
% 0.11/0.33  % WCLimit  : 300
% 0.11/0.33  % DateTime : Mon Jun 24 02:00:09 EDT 2024
% 0.11/0.33  % CPUTime  : 
% 2.20/2.43  Zenon error: exhausted search space without finding a proof
% 2.20/2.43  (* Current branch:
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X52))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X31)
% 2.20/2.43  ((a1300) != (a1326))
% 2.20/2.43  (c7_2 (a1346) zenon_X65)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X32))
% 2.20/2.43  ((a1282) != zenon_X101)
% 2.20/2.43  (c10_2 zenon_X25 (a1351))
% 2.20/2.43  ((a1223) != zenon_X39)
% 2.20/2.43  (c9_2 (a1293) zenon_X71)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X41))
% 2.20/2.43  (c3_2 (a1363) (a1294))
% 2.20/2.43  (c9_1 (a1255))
% 2.20/2.43  (zenon_X27 != (a1307))
% 2.20/2.43  (zenon_X17 != (a1354))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X59))
% 2.20/2.43  ((a1347) != zenon_X42)
% 2.20/2.43  (zenon_X59 != (a1271))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X73))
% 2.20/2.43  ((a1282) != zenon_X50)
% 2.20/2.43  (zenon_X73 != zenon_X82)
% 2.20/2.43  (c9_2 (a1281) (a1347))
% 2.20/2.43  ((a1364) != zenon_X54)
% 2.20/2.43  (c9_2 zenon_X35 (a1300))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X57)
% 2.20/2.43  ((a1282) != (a1256))
% 2.20/2.43  (c7_2 (a1241) zenon_X63)
% 2.20/2.43  (-. (c9_2 zenon_X18 (a1302)))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X73))
% 2.20/2.43  (zenon_X14 != zenon_X5)
% 2.20/2.43  (c7_2 (a1346) (a1277))
% 2.20/2.43  (c9_2 (a1223) (a1246))
% 2.20/2.43  ((a1220) != zenon_X8)
% 2.20/2.43  (-. (c5_1 (a1316)))
% 2.20/2.43  ((a1352) != zenon_X71)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X54))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X60))
% 2.20/2.43  (c3_2 (a1350) (a1352))
% 2.20/2.43  ((a1345) != zenon_X58)
% 2.20/2.43  (-. (c1_2 zenon_X27 (a1325)))
% 2.20/2.43  (zenon_X30 != zenon_X25)
% 2.20/2.43  (c7_2 (a1346) zenon_X103)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X31))
% 2.20/2.43  ((a1308) != (a1271))
% 2.20/2.43  (zenon_X31 != zenon_X52)
% 2.20/2.43  ((a1220) != zenon_X17)
% 2.20/2.43  (c7_2 (a1255) (a1364))
% 2.20/2.43  (zenon_X73 != (a1345))
% 2.20/2.43  (-. (c5_2 (a1307) (a1246)))
% 2.20/2.43  (zenon_X52 != zenon_X65)
% 2.20/2.43  (c10_1 (a1220))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X53))
% 2.20/2.43  ((a1255) != zenon_X25)
% 2.20/2.43  (c7_2 (a1220) (a1227))
% 2.20/2.43  ((a1352) != zenon_X102)
% 2.20/2.43  (c9_2 zenon_X8 (a1277))
% 2.20/2.43  ((a1246) != zenon_X57)
% 2.20/2.43  (c7_2 zenon_X35 (a1256))
% 2.20/2.43  ((a1293) != (a1287))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X71)
% 2.20/2.43  ((a1364) != (a1246))
% 2.20/2.43  (zenon_X6 != (a1241))
% 2.20/2.43  ((a1300) != zenon_X41)
% 2.20/2.43  ((a1345) != zenon_X46)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X58))
% 2.20/2.43  (c5_2 (a1223) zenon_X102)
% 2.20/2.43  (c7_2 (a1241) zenon_X55)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X16))
% 2.20/2.43  ((a1345) != zenon_X107)
% 2.20/2.43  (c7_2 (a1241) zenon_X57)
% 2.20/2.43  (c7_2 zenon_X35 (a1326))
% 2.20/2.43  (c9_2 (a1293) zenon_X73)
% 2.20/2.43  ((a1271) != zenon_X28)
% 2.20/2.43  ((a1352) != zenon_X4)
% 2.20/2.43  ((a1351) != zenon_X65)
% 2.20/2.43  ((a1345) != zenon_X82)
% 2.20/2.43  ((a1246) != zenon_X63)
% 2.20/2.43  ((a1277) != zenon_X52)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X33))
% 2.20/2.43  (zenon_X103 != zenon_X52)
% 2.20/2.43  (zenon_X73 != zenon_X46)
% 2.20/2.43  (c7_2 (a1346) (a1271))
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X53))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X58))
% 2.20/2.43  (zenon_X31 != zenon_X102)
% 2.20/2.43  (c1_2 (a1215) (a1336))
% 2.20/2.43  ((a1345) != zenon_X102)
% 2.20/2.43  ((a1246) != zenon_X107)
% 2.20/2.43  (zenon_X52 != zenon_X3)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X42))
% 2.20/2.43  (c9_2 zenon_X8 (a1345))
% 2.20/2.43  ((a1216) != zenon_X32)
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X3))
% 2.20/2.43  (c9_2 (a1270) zenon_X71)
% 2.20/2.43  ((a1220) != (a1214))
% 2.20/2.43  ((a1255) != (a1287))
% 2.20/2.43  (zenon_X14 != zenon_X63)
% 2.20/2.43  (c2_2 (a1220) (a1326))
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X33))
% 2.20/2.43  ((a1255) != zenon_X17)
% 2.20/2.43  (-. (c1_2 (a1208) (a1246)))
% 2.20/2.43  ((a1246) != zenon_X54)
% 2.20/2.43  ((a1256) != zenon_X29)
% 2.20/2.43  (zenon_X55 != zenon_X59)
% 2.20/2.43  (c7_2 (a1241) zenon_X16)
% 2.20/2.43  (c7_2 (a1241) zenon_X59)
% 2.20/2.43  (zenon_X71 != zenon_X46)
% 2.20/2.43  (c7_2 (a1220) zenon_X82)
% 2.20/2.43  ((a1345) != (a1260))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X52))
% 2.20/2.43  (zenon_X107 != zenon_X54)
% 2.20/2.43  (c9_2 (a1223) (a1282))
% 2.20/2.43  ((a1336) != (a1325))
% 2.20/2.43  ((a1347) != (a1351))
% 2.20/2.43  (zenon_X42 != zenon_X103)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X5))
% 2.20/2.43  ((a1277) != zenon_X28)
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X55))
% 2.20/2.43  (c7_2 (a1346) zenon_X33)
% 2.20/2.43  (zenon_X16 != zenon_X42)
% 2.20/2.43  ((a1351) != zenon_X76)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X71))
% 2.20/2.43  (zenon_X3 != (a1227))
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X3))
% 2.20/2.43  ((a1345) != (a1256))
% 2.20/2.43  ((a1352) != zenon_X87)
% 2.20/2.43  (zenon_X73 != zenon_X57)
% 2.20/2.43  ((a1282) != zenon_X82)
% 2.20/2.43  (c9_2 (a1255) (a1347))
% 2.20/2.43  ((a1345) != zenon_X52)
% 2.20/2.43  ((a1216) != zenon_X41)
% 2.20/2.43  (zenon_X60 != zenon_X57)
% 2.20/2.43  ((a1300) != zenon_X71)
% 2.20/2.43  (zenon_X33 != zenon_X53)
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X3))
% 2.20/2.43  (-. (c1_2 zenon_X35 (a1302)))
% 2.20/2.43  (c3_2 (a1350) zenon_X46)
% 2.20/2.43  (c7_2 (a1293) (a1345))
% 2.20/2.43  ((a1345) != zenon_X41)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X59))
% 2.20/2.43  (c8_2 (a1346) (a1294))
% 2.20/2.43  (zenon_X57 != zenon_X65)
% 2.20/2.43  (c9_2 (a1293) (a1256))
% 2.20/2.43  ((a1294) != zenon_X20)
% 2.20/2.43  (-. (c5_2 (a1214) (a1300)))
% 2.20/2.43  (-. (c7_2 (a1363) (a1364)))
% 2.20/2.43  ((a1283) != (a1294))
% 2.20/2.43  ((a1294) != zenon_X15)
% 2.20/2.43  ((a1283) != (a1345))
% 2.20/2.43  ((a1227) != zenon_X73)
% 2.20/2.43  ((a1294) != (a1246))
% 2.20/2.43  (zenon_X31 != (a1326))
% 2.20/2.43  (ndr1_1 zenon_X27)
% 2.20/2.43  (c9_2 zenon_X39 (a1300))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X14))
% 2.20/2.43  (c9_2 (a1270) zenon_X103)
% 2.20/2.43  (zenon_X35 != (a1307))
% 2.20/2.43  ((a1308) != zenon_X103)
% 2.20/2.43  (zenon_X97 != (a1352))
% 2.20/2.43  ((a1352) != zenon_X85)
% 2.20/2.43  (zenon_X33 != (a1300))
% 2.20/2.43  ((a1346) != (a1354))
% 2.20/2.43  (zenon_X42 != (a1336))
% 2.20/2.43  (zenon_X39 != zenon_X25)
% 2.20/2.43  (c9_2 zenon_X30 (a1308))
% 2.20/2.43  (c5_2 (a1350) (a1246))
% 2.20/2.43  (c7_1 (a1281))
% 2.20/2.43  (-. (c6_2 (a1276) (a1347)))
% 2.20/2.43  (-. (c1_2 zenon_X25 (a1246)))
% 2.20/2.43  ((a1347) != (a1300))
% 2.20/2.43  ((a1346) != (a1363))
% 2.20/2.43  ((a1270) != (a1226))
% 2.20/2.43  ((a1352) != zenon_X107)
% 2.20/2.43  (zenon_X52 != zenon_X57)
% 2.20/2.43  ((a1363) != zenon_X25)
% 2.20/2.43  ((a1308) != zenon_X107)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X102))
% 2.20/2.43  (zenon_X43 != zenon_X102)
% 2.20/2.43  ((a1282) != zenon_X32)
% 2.20/2.43  ((a1216) != (a1330))
% 2.20/2.43  (zenon_X14 != zenon_X82)
% 2.20/2.43  (c6_2 (a1350) (a1352))
% 2.20/2.43  (c6_2 (a1350) zenon_X107)
% 2.20/2.43  ((a1300) != zenon_X75)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X65))
% 2.20/2.43  (-. (c9_2 zenon_X39 (a1302)))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X32))
% 2.20/2.43  (c7_2 (a1241) (a1300))
% 2.20/2.43  ((a1351) != zenon_X3)
% 2.20/2.43  (c9_2 (a1220) (a1345))
% 2.20/2.43  (c9_2 zenon_X30 (a1227))
% 2.20/2.43  (c7_2 (a1255) zenon_X52)
% 2.20/2.43  (c9_2 (a1226) (a1260))
% 2.20/2.43  ((a1260) != (a1246))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X31))
% 2.20/2.43  (zenon_X5 != zenon_X65)
% 2.20/2.43  ((a1283) != (a1300))
% 2.20/2.43  (zenon_X14 != zenon_X52)
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X55))
% 2.20/2.43  (zenon_X73 != zenon_X50)
% 2.20/2.43  (zenon_X71 != zenon_X3)
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X57))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X81))
% 2.20/2.43  (zenon_X35 != zenon_X17)
% 2.20/2.43  (-. (c6_2 (a1346) (a1345)))
% 2.20/2.43  ((a1220) != (a1223))
% 2.20/2.43  (zenon_X43 != zenon_X57)
% 2.20/2.43  (c3_2 (a1350) zenon_X33)
% 2.20/2.43  (c9_2 (a1346) (a1227))
% 2.20/2.43  ((a1227) != (a1326))
% 2.20/2.43  ((a1345) != (a1282))
% 2.20/2.43  ((a1336) != (a1300))
% 2.20/2.43  (c9_2 zenon_X17 (a1302))
% 2.20/2.43  (c7_2 (a1293) (a1347))
% 2.20/2.43  (zenon_X14 != zenon_X64)
% 2.20/2.43  ((a1256) != zenon_X103)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X102))
% 2.20/2.43  ((a1282) != zenon_X15)
% 2.20/2.43  ((a1351) != (a1330))
% 2.20/2.43  (-. (c9_2 zenon_X39 (a1246)))
% 2.20/2.43  (c7_2 (a1346) (a1227))
% 2.20/2.43  (c7_2 (a1255) zenon_X97)
% 2.20/2.43  (c2_2 (a1354) (a1326))
% 2.20/2.43  (-. (c8_2 (a1293) (a1277)))
% 2.20/2.43  (zenon_X11 != (a1220))
% 2.20/2.43  (-. (c6_2 (a1276) (a1227)))
% 2.20/2.43  ((a1294) != zenon_X87)
% 2.20/2.43  (c7_2 (a1220) (a1347))
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X33))
% 2.20/2.43  (zenon_X38 != (a1354))
% 2.20/2.43  (c9_2 zenon_X38 (a1294))
% 2.20/2.43  (c7_2 (a1255) (a1347))
% 2.20/2.43  (zenon_X16 != zenon_X57)
% 2.20/2.43  ((a1293) != zenon_X30)
% 2.20/2.43  (c9_2 (a1281) (a1308))
% 2.20/2.43  (c3_0)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X60))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X31))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X103))
% 2.20/2.43  (c7_2 (a1346) (a1300))
% 2.20/2.43  (c8_2 (a1223) (a1277))
% 2.20/2.43  (zenon_X14 != zenon_X49)
% 2.20/2.43  ((a1293) != zenon_X38)
% 2.20/2.43  (zenon_X35 != (a1214))
% 2.20/2.43  ((a1352) != zenon_X103)
% 2.20/2.43  (c9_2 zenon_X18 (a1256))
% 2.20/2.43  (-. (c2_2 zenon_X18 (a1352)))
% 2.20/2.43  (zenon_X42 != zenon_X81)
% 2.20/2.43  (c9_2 (a1223) (a1294))
% 2.20/2.43  (c1_0)
% 2.20/2.43  (c7_2 (a1281) (a1283))
% 2.20/2.43  (-. (c9_2 zenon_X8 (a1326)))
% 2.20/2.43  ((a1246) != zenon_X67)
% 2.20/2.43  (zenon_X55 != zenon_X49)
% 2.20/2.43  (-. (c8_2 (a1226) (a1227)))
% 2.20/2.43  (-. (c1_1 zenon_X39))
% 2.20/2.43  (zenon_X30 != (a1208))
% 2.20/2.43  (c9_2 zenon_X38 (a1326))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X41))
% 2.20/2.43  ((a1216) != zenon_X5)
% 2.20/2.43  ((a1364) != zenon_X32)
% 2.20/2.43  (zenon_X82 != zenon_X103)
% 2.20/2.43  (c6_2 (a1350) zenon_X53)
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X3))
% 2.20/2.43  (c5_2 zenon_X25 (a1246))
% 2.20/2.43  ((a1293) != (a1214))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1300)))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X59))
% 2.20/2.43  ((a1363) != zenon_X38)
% 2.20/2.43  ((a1256) != zenon_X56)
% 2.20/2.43  (c9_2 zenon_X17 (a1352))
% 2.20/2.43  (c1_1 zenon_X30)
% 2.20/2.43  (zenon_X71 != zenon_X54)
% 2.20/2.43  (-. (c1_2 (a1287) (a1347)))
% 2.20/2.43  ((a1283) != zenon_X82)
% 2.20/2.43  (c2_1 (a1354))
% 2.20/2.43  (zenon_X42 != (a1256))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X58))
% 2.20/2.43  (c7_2 (a1346) (a1283))
% 2.20/2.43  (-. (c4_2 zenon_X1 zenon_X2))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X16))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X54))
% 2.20/2.43  (c9_2 (a1281) (a1352))
% 2.20/2.43  (c3_2 (a1346) (a1347))
% 2.20/2.43  (zenon_X16 != zenon_X32)
% 2.20/2.43  ((a1271) != zenon_X71)
% 2.20/2.43  ((a1352) != zenon_X20)
% 2.20/2.43  (c9_2 zenon_X38 (a1347))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X14))
% 2.20/2.43  (-. (c9_2 (a1354) (a1326)))
% 2.20/2.43  (c5_2 (a1223) (a1282))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X65))
% 2.20/2.43  (zenon_X11 != (a1363))
% 2.20/2.43  (-. (c9_2 (a1354) (a1302)))
% 2.20/2.43  ((a1300) != zenon_X52)
% 2.20/2.43  (zenon_X12 != (a1363))
% 2.20/2.43  (zenon_X43 != (a1282))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X31))
% 2.20/2.43  ((a1246) != zenon_X46)
% 2.20/2.43  (ndr1_1 zenon_X8)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X107))
% 2.20/2.43  (c1_2 (a1215) (a1277))
% 2.20/2.43  (c9_2 (a1220) (a1246))
% 2.20/2.43  (c7_2 (a1220) zenon_X73)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X46))
% 2.20/2.43  (c9_2 (a1241) (a1216))
% 2.20/2.43  (c9_1 zenon_X24)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X49))
% 2.20/2.43  (-. (c10_2 (a1354) zenon_X76))
% 2.20/2.43  ((a1294) != zenon_X54)
% 2.20/2.43  (-. (c5_2 (a1307) (a1345)))
% 2.20/2.43  (zenon_X33 != zenon_X43)
% 2.20/2.43  (c9_2 (a1241) zenon_X102)
% 2.20/2.43  (zenon_X3 != (a1300))
% 2.20/2.43  ((a1246) != zenon_X53)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X71))
% 2.20/2.43  (c8_2 (a1270) (a1271))
% 2.20/2.43  ((a1346) != zenon_X13)
% 2.20/2.43  (-. (c6_2 (a1350) zenon_X42))
% 2.20/2.43  (c1_2 (a1215) zenon_X102)
% 2.20/2.43  (-. (c8_1 (a1316)))
% 2.20/2.43  (c7_1 (a1241))
% 2.20/2.43  (zenon_X39 != zenon_X27)
% 2.20/2.43  ((a1220) != (a1208))
% 2.20/2.43  (c6_1 (a1215))
% 2.20/2.43  ((a1220) != (a1307))
% 2.20/2.43  (c7_2 (a1220) (a1246))
% 2.20/2.43  (zenon_X107 != zenon_X57)
% 2.20/2.43  (zenon_X18 != (a1255))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X82))
% 2.20/2.43  (zenon_X33 != (a1352))
% 2.20/2.43  (-. (c3_2 (a1307) (a1345)))
% 2.20/2.43  (zenon_X14 != zenon_X60)
% 2.20/2.43  (zenon_X97 != zenon_X82)
% 2.20/2.43  ((a1241) != (a1281))
% 2.20/2.43  (zenon_X55 != (a1282))
% 2.20/2.43  (c9_2 zenon_X17 (a1283))
% 2.20/2.43  ((a1214) != zenon_X38)
% 2.20/2.43  (-. (c6_2 (a1276) (a1246)))
% 2.20/2.43  (zenon_X3 != zenon_X57)
% 2.20/2.43  (-. (c6_2 (a1346) (a1364)))
% 2.20/2.43  ((a1208) != (a1307))
% 2.20/2.43  ((a1300) != zenon_X65)
% 2.20/2.43  (zenon_X58 != zenon_X42)
% 2.20/2.43  (c7_1 (a1307))
% 2.20/2.43  (-. (c2_1 zenon_X8))
% 2.20/2.43  (c7_2 (a1293) (a1277))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X64))
% 2.20/2.43  ((a1345) != zenon_X71)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X41))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X57))
% 2.20/2.43  (c7_2 (a1255) (a1216))
% 2.20/2.43  (-. (c6_2 (a1346) (a1352)))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X16))
% 2.20/2.43  (zenon_X33 != (a1308))
% 2.20/2.43  (c5_2 (a1307) (a1308))
% 2.20/2.43  (c7_2 (a1350) (a1271))
% 2.20/2.43  (zenon_X31 != zenon_X82)
% 2.20/2.43  (c9_2 zenon_X27 (a1364))
% 2.20/2.43  (-. (c9_2 (a1287) (a1246)))
% 2.20/2.43  ((a1220) != zenon_X30)
% 2.20/2.43  (c3_2 (a1350) (a1246))
% 2.20/2.43  (-. (c6_2 (a1276) (a1300)))
% 2.20/2.43  (zenon_X97 != zenon_X60)
% 2.20/2.43  (c9_2 (a1241) (a1282))
% 2.20/2.43  ((a1223) != zenon_X8)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X107))
% 2.20/2.43  (c9_2 (a1208) (a1345))
% 2.20/2.43  ((a1246) != zenon_X34)
% 2.20/2.43  ((a1208) != (a1214))
% 2.20/2.43  ((a1269) != (a1354))
% 2.20/2.43  ((a1330) != (a1326))
% 2.20/2.43  (c9_2 (a1220) (a1294))
% 2.20/2.43  ((a1277) != (a1336))
% 2.20/2.43  (zenon_X81 != (a1364))
% 2.20/2.43  (c9_2 (a1346) (a1246))
% 2.20/2.43  (c9_2 zenon_X18 (a1308))
% 2.20/2.43  (c1_2 (a1215) (a1300))
% 2.20/2.43  (c7_2 (a1270) (a1308))
% 2.20/2.43  (zenon_X97 != (a1300))
% 2.20/2.43  (c5_2 (a1223) (a1308))
% 2.20/2.43  ((a1346) != zenon_X38)
% 2.20/2.43  (c9_2 (a1281) (a1271))
% 2.20/2.43  (c7_2 (a1346) zenon_X71)
% 2.20/2.43  (c6_2 (a1350) (a1277))
% 2.20/2.43  (zenon_X97 != zenon_X53)
% 2.20/2.43  (zenon_X81 != zenon_X57)
% 2.20/2.43  ((a1271) != zenon_X75)
% 2.20/2.43  (c9_2 zenon_X30 (a1271))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X107))
% 2.20/2.43  ((a1346) != (a1208))
% 2.20/2.43  (c9_2 (a1346) zenon_X107)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X59))
% 2.20/2.43  (-. (c8_2 (a1293) (a1271)))
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X65))
% 2.20/2.43  ((a1256) != zenon_X32)
% 2.20/2.43  ((a1246) != zenon_X49)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X16))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X32))
% 2.20/2.43  (c5_2 (a1223) zenon_X71)
% 2.20/2.43  (zenon_X53 != zenon_X52)
% 2.20/2.43  ((a1347) != zenon_X81)
% 2.20/2.43  ((a1277) != (a1246))
% 2.20/2.43  (zenon_X63 != zenon_X43)
% 2.20/2.43  ((a1300) != zenon_X63)
% 2.20/2.43  ((a1277) != zenon_X81)
% 2.20/2.43  (-. (c9_2 zenon_X25 (a1302)))
% 2.20/2.43  (-. (c6_2 (a1276) (a1364)))
% 2.20/2.43  (zenon_X42 != zenon_X5)
% 2.20/2.43  (zenon_X55 != (a1352))
% 2.20/2.43  (zenon_X35 != (a1363))
% 2.20/2.43  ((a1283) != zenon_X65)
% 2.20/2.43  ((a1351) != (a1260))
% 2.20/2.43  (zenon_X59 != zenon_X71)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X54))
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X57))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X41))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X82))
% 2.20/2.43  ((a1352) != zenon_X3)
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X32))
% 2.20/2.43  ((a1294) != (a1352))
% 2.20/2.43  (-. (c6_2 (a1276) (a1271)))
% 2.20/2.43  (c7_2 (a1270) zenon_X59)
% 2.20/2.43  ((a1352) != zenon_X53)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X63))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X73))
% 2.20/2.43  (zenon_X53 != zenon_X65)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X59)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X57))
% 2.20/2.43  ((a1256) != zenon_X20)
% 2.20/2.43  (-. (c6_2 (a1346) (a1351)))
% 2.20/2.43  (c7_1 zenon_X17)
% 2.20/2.43  (zenon_X73 != (a1364))
% 2.20/2.43  (c9_2 zenon_X7 (a1330))
% 2.20/2.43  (c5_2 (a1223) (a1345))
% 2.20/2.43  (c5_2 (a1223) (a1283))
% 2.20/2.43  (zenon_X3 != (a1277))
% 2.20/2.43  ((a1277) != zenon_X64)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X41))
% 2.20/2.43  (c1_2 (a1215) (a1283))
% 2.20/2.43  ((a1336) != (a1308))
% 2.20/2.43  (c7_2 (a1223) (a1277))
% 2.20/2.43  ((a1346) != zenon_X39)
% 2.20/2.43  (c7_1 (a1270))
% 2.20/2.43  (-. (c6_2 (a1346) (a1336)))
% 2.20/2.43  (c9_2 (a1270) zenon_X102)
% 2.20/2.43  (zenon_X3 != (a1364))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X64))
% 2.20/2.43  ((a1282) != zenon_X31)
% 2.20/2.43  (-. (c1_1 (a1241)))
% 2.20/2.43  (c7_2 (a1220) zenon_X63)
% 2.20/2.43  (c7_2 (a1241) (a1271))
% 2.20/2.43  ((a1346) != (a1226))
% 2.20/2.43  (c7_2 (a1220) zenon_X32)
% 2.20/2.43  (-. (c5_2 zenon_X18 (a1302)))
% 2.20/2.43  (c9_2 (a1270) (a1345))
% 2.20/2.43  (zenon_X42 != zenon_X46)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X60))
% 2.20/2.43  (c9_2 zenon_X17 (a1345))
% 2.20/2.43  ((a1246) != zenon_X50)
% 2.20/2.43  ((a1347) != (a1227))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1330)))
% 2.20/2.43  ((a1223) != (a1281))
% 2.20/2.43  (zenon_X71 != zenon_X57)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X55))
% 2.20/2.43  (c7_2 (a1270) (a1216))
% 2.20/2.43  (c4_2 (a1281) (a1283))
% 2.20/2.43  ((a1326) != (a1246))
% 2.20/2.43  ((a1270) != zenon_X1)
% 2.20/2.43  (c9_2 (a1223) zenon_X71)
% 2.20/2.43  ((a1215) != zenon_X39)
% 2.20/2.43  (zenon_X35 != zenon_X38)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X82))
% 2.20/2.43  (zenon_X53 != zenon_X3)
% 2.20/2.43  ((a1220) != (a1354))
% 2.20/2.43  (zenon_X58 != (a1364))
% 2.20/2.43  (c8_2 (a1223) (a1227))
% 2.20/2.43  (c7_2 (a1220) zenon_X55)
% 2.20/2.43  ((a1300) != zenon_X102)
% 2.20/2.43  (c7_1 zenon_X35)
% 2.20/2.43  (zenon_X43 != (a1352))
% 2.20/2.43  ((a1350) != (a1215))
% 2.20/2.43  (-. (c1_2 (a1350) (a1302)))
% 2.20/2.43  (c9_2 zenon_X35 (a1282))
% 2.20/2.43  (-. (c10_1 (a1293)))
% 2.20/2.43  ((a1271) != zenon_X22)
% 2.20/2.43  ((a1363) != zenon_X17)
% 2.20/2.43  (-. (c3_2 (a1287) (a1246)))
% 2.20/2.43  ((a1277) != zenon_X42)
% 2.20/2.43  (zenon_X35 != zenon_X18)
% 2.20/2.43  ((a1256) != (a1260))
% 2.20/2.43  (c9_2 zenon_X18 (a1352))
% 2.20/2.43  (c7_2 (a1223) zenon_X55)
% 2.20/2.43  ((a1283) != zenon_X73)
% 2.20/2.43  (c7_2 (a1293) zenon_X16)
% 2.20/2.43  (c7_2 (a1270) zenon_X43)
% 2.20/2.43  (zenon_X39 != (a1270))
% 2.20/2.43  ((a1260) != (a1302))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1326)))
% 2.20/2.43  (zenon_X14 != zenon_X81)
% 2.20/2.43  (c7_2 (a1346) (a1345))
% 2.20/2.43  (-. (c10_2 (a1270) zenon_X87))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X73))
% 2.20/2.43  (c7_2 (a1255) zenon_X73)
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X55))
% 2.20/2.43  ((a1271) != (a1246))
% 2.20/2.43  ((a1345) != zenon_X54)
% 2.20/2.43  ((a1308) != zenon_X23)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X14)
% 2.20/2.43  (zenon_X14 != zenon_X54)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X53))
% 2.20/2.43  (c9_2 (a1220) (a1300))
% 2.20/2.43  (c5_2 (a1223) (a1294))
% 2.20/2.43  (-. (c4_1 zenon_X27))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X49))
% 2.20/2.43  (-. (c9_2 zenon_X25 (a1246)))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X32))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X63))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X53))
% 2.20/2.43  (zenon_X33 != zenon_X60)
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X32))
% 2.20/2.43  ((a1216) != (a1308))
% 2.20/2.43  (c1_2 (a1215) (a1352))
% 2.20/2.43  ((a1345) != zenon_X81)
% 2.20/2.43  (-. (c2_2 zenon_X8 (a1352)))
% 2.20/2.43  (zenon_X32 != zenon_X49)
% 2.20/2.43  (zenon_X3 != zenon_X65)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X57))
% 2.20/2.43  ((a1215) != zenon_X25)
% 2.20/2.43  (zenon_X33 != (a1294))
% 2.20/2.43  (-. (c9_2 (a1293) (a1302)))
% 2.20/2.43  (c9_2 (a1241) (a1352))
% 2.20/2.43  ((a1277) != zenon_X59)
% 2.20/2.43  ((a1282) != zenon_X5)
% 2.20/2.43  (-. (c1_2 (a1287) (a1364)))
% 2.20/2.43  (zenon_X57 != (a1271))
% 2.20/2.43  (zenon_X63 != zenon_X107)
% 2.20/2.43  ((a1308) != zenon_X43)
% 2.20/2.43  (zenon_X31 != zenon_X64)
% 2.20/2.43  (c7_2 (a1241) (a1352))
% 2.20/2.43  (-. (c5_2 zenon_X39 zenon_X68))
% 2.20/2.43  (c9_2 zenon_X17 (a1347))
% 2.20/2.43  ((a1277) != zenon_X63)
% 2.20/2.43  (zenon_X55 != (a1271))
% 2.20/2.43  ((a1293) != (a1281))
% 2.20/2.43  (zenon_X60 != zenon_X32)
% 2.20/2.43  (c7_2 (a1307) (a1308))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X63))
% 2.20/2.43  ((a1294) != (a1271))
% 2.20/2.43  (c6_2 (a1350) zenon_X31)
% 2.20/2.43  (c5_2 (a1223) zenon_X31)
% 2.20/2.43  ((a1227) != zenon_X49)
% 2.20/2.43  (zenon_X35 != (a1281))
% 2.20/2.43  (c7_1 zenon_X38)
% 2.20/2.43  (c7_2 (a1270) zenon_X63)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X97))
% 2.20/2.43  (c3_2 (a1363) (a1352))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X60))
% 2.20/2.43  (zenon_X43 != zenon_X82)
% 2.20/2.43  ((a1330) != (a1256))
% 2.20/2.43  (c9_2 zenon_X18 (a1246))
% 2.20/2.43  (zenon_X25 != (a1307))
% 2.20/2.43  ((a1308) != zenon_X50)
% 2.20/2.43  ((a1220) != zenon_X38)
% 2.20/2.43  ((a1271) != zenon_X32)
% 2.20/2.43  (c9_2 (a1223) zenon_X102)
% 2.20/2.43  (zenon_X16 != zenon_X53)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X3))
% 2.20/2.43  (c9_2 (a1223) (a1300))
% 2.20/2.43  (zenon_X17 != (a1350))
% 2.20/2.43  (-. (c5_2 (a1214) (a1294)))
% 2.20/2.43  ((a1345) != (a1246))
% 2.20/2.43  (zenon_X16 != (a1271))
% 2.20/2.43  ((a1352) != zenon_X105)
% 2.20/2.43  (zenon_X14 != (a1345))
% 2.20/2.43  (c3_2 (a1350) (a1347))
% 2.20/2.43  (-. (c10_1 zenon_X39))
% 2.20/2.43  (zenon_X55 != zenon_X64)
% 2.20/2.43  (c9_2 (a1223) zenon_X31)
% 2.20/2.43  ((a1351) != (a1227))
% 2.20/2.43  (zenon_X38 != zenon_X8)
% 2.20/2.43  (c7_2 (a1350) zenon_X65)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X73))
% 2.20/2.43  (c9_2 (a1270) (a1283))
% 2.20/2.43  (c9_2 (a1270) (a1294))
% 2.20/2.43  (zenon_X63 != zenon_X52)
% 2.20/2.43  (zenon_X54 != zenon_X65)
% 2.20/2.43  (-. (c10_2 (a1363) zenon_X0))
% 2.20/2.43  (zenon_X33 != zenon_X103)
% 2.20/2.43  ((a1283) != zenon_X107)
% 2.20/2.43  (zenon_X35 != (a1354))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X97))
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X16))
% 2.20/2.43  (c6_2 (a1350) (a1283))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X41))
% 2.20/2.43  ((a1227) != zenon_X64)
% 2.20/2.43  (c9_2 (a1281) (a1277))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X43))
% 2.20/2.43  (c9_2 (a1281) zenon_X82)
% 2.20/2.43  (zenon_X97 != (a1345))
% 2.20/2.43  (c1_1 (a1363))
% 2.20/2.43  (zenon_X58 != (a1256))
% 2.20/2.43  (-. (c9_2 zenon_X35 (a1326)))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X64))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X59))
% 2.20/2.43  ((a1227) != zenon_X82)
% 2.20/2.43  (zenon_X16 != (a1283))
% 2.20/2.43  ((a1281) != zenon_X25)
% 2.20/2.43  ((a1364) != (a1302))
% 2.20/2.43  (zenon_X33 != zenon_X52)
% 2.20/2.43  (-. (c5_2 (a1223) zenon_X65))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X63))
% 2.20/2.43  (zenon_X71 != (a1260))
% 2.20/2.43  (zenon_X97 != zenon_X3)
% 2.20/2.43  (c9_2 (a1241) (a1256))
% 2.20/2.43  ((a1293) != zenon_X35)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X33))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X41))
% 2.20/2.43  (c9_2 zenon_X18 (a1300))
% 2.20/2.43  (-. (c8_1 (a1363)))
% 2.20/2.43  ((a1336) != zenon_X32)
% 2.20/2.43  (zenon_X31 != zenon_X50)
% 2.20/2.43  (zenon_X16 != (a1294))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X32)
% 2.20/2.43  (zenon_X6 != (a1335))
% 2.20/2.43  (zenon_X58 != zenon_X57)
% 2.20/2.43  (zenon_X60 != zenon_X65)
% 2.20/2.43  ((a1352) != (a1302))
% 2.20/2.43  (c7_2 (a1241) zenon_X32)
% 2.20/2.43  (c7_2 (a1220) (a1271))
% 2.20/2.43  (zenon_X18 != zenon_X25)
% 2.20/2.43  ((a1364) != zenon_X102)
% 2.20/2.43  (c9_2 (a1255) (a1294))
% 2.20/2.43  ((a1326) != (a1352))
% 2.20/2.43  (c7_2 (a1293) zenon_X71)
% 2.20/2.43  (c9_2 (a1346) zenon_X73)
% 2.20/2.43  (-. (c2_2 (a1346) (a1347)))
% 2.20/2.43  (c9_2 (a1293) (a1216))
% 2.20/2.43  (c7_2 (a1255) (a1308))
% 2.20/2.43  (c1_2 (a1215) (a1347))
% 2.20/2.43  (c9_2 zenon_X17 (a1336))
% 2.20/2.43  (c1_2 (a1215) zenon_X103)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X33))
% 2.20/2.43  (zenon_X14 != (a1283))
% 2.20/2.43  (zenon_X3 != zenon_X33)
% 2.20/2.43  (zenon_X33 != (a1364))
% 2.20/2.43  (c9_2 (a1220) (a1271))
% 2.20/2.43  ((a1256) != zenon_X80)
% 2.20/2.43  (c9_2 zenon_X8 (a1283))
% 2.20/2.43  (-. (c10_2 zenon_X27 (a1351)))
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X42))
% 2.20/2.43  (c6_2 (a1350) zenon_X3)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X63))
% 2.20/2.43  (zenon_X50 != zenon_X65)
% 2.20/2.43  ((a1354) != (a1287))
% 2.20/2.43  (zenon_X73 != zenon_X32)
% 2.20/2.43  ((a1352) != zenon_X54)
% 2.20/2.43  (c1_2 zenon_X19 (a1300))
% 2.20/2.43  ((a1294) != zenon_X50)
% 2.20/2.43  ((a1364) != (a1345))
% 2.20/2.43  ((a1256) != zenon_X57)
% 2.20/2.43  (c2_2 (a1223) (a1326))
% 2.20/2.43  (c9_2 zenon_X38 (a1283))
% 2.20/2.43  (c9_2 (a1346) (a1283))
% 2.20/2.43  (c9_2 (a1270) (a1271))
% 2.20/2.43  ((a1223) != zenon_X17)
% 2.20/2.43  (c7_2 (a1270) zenon_X102)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X33))
% 2.20/2.43  (-. (c10_2 (a1270) (a1294)))
% 2.20/2.43  (-. (c5_2 zenon_X8 (a1302)))
% 2.20/2.43  ((a1351) != (a1302))
% 2.20/2.43  ((a1300) != zenon_X32)
% 2.20/2.43  (-. (c6_2 (a1350) (a1364)))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X43))
% 2.20/2.43  (zenon_X42 != (a1345))
% 2.20/2.43  (zenon_X32 != zenon_X52)
% 2.20/2.43  (zenon_X35 != (a1270))
% 2.20/2.43  (zenon_X73 != zenon_X107)
% 2.20/2.43  (c7_2 (a1223) zenon_X42)
% 2.20/2.43  (-. (c8_2 (a1307) (a1352)))
% 2.20/2.43  (c7_2 (a1346) (a1364))
% 2.20/2.43  (-. (c10_2 (a1241) (a1294)))
% 2.20/2.43  ((a1255) != (a1214))
% 2.20/2.43  (zenon_X43 != (a1271))
% 2.20/2.43  (c7_2 (a1255) zenon_X3)
% 2.20/2.43  (zenon_X32 != zenon_X31)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X65))
% 2.20/2.43  ((a1282) != zenon_X75)
% 2.20/2.43  ((a1294) != zenon_X32)
% 2.20/2.43  (c7_2 (a1293) zenon_X14)
% 2.20/2.43  (zenon_X82 != zenon_X54)
% 2.20/2.43  ((a1283) != (a1347))
% 2.20/2.43  (-. (c9_2 (a1270) (a1326)))
% 2.20/2.43  ((a1255) != (a1241))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X52))
% 2.20/2.43  (zenon_X81 != zenon_X65)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X59))
% 2.20/2.43  (zenon_X39 != (a1293))
% 2.20/2.43  ((a1308) != (a1256))
% 2.20/2.43  (zenon_X33 != zenon_X64)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X42)
% 2.20/2.43  ((a1271) != (a1336))
% 2.20/2.43  ((a1364) != (a1256))
% 2.20/2.43  ((a1364) != zenon_X107)
% 2.20/2.43  (-. (c1_2 zenon_X18 (a1302)))
% 2.20/2.43  (c7_2 (a1220) (a1345))
% 2.20/2.43  (c9_2 (a1270) (a1227))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X54))
% 2.20/2.43  ((a1308) != zenon_X3)
% 2.20/2.43  ((a1345) != zenon_X63)
% 2.20/2.43  (-. (c1_1 zenon_X25))
% 2.20/2.43  (zenon_X33 != (a1256))
% 2.20/2.43  ((a1227) != (a1302))
% 2.20/2.43  (c5_2 (a1223) (a1352))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X73))
% 2.20/2.43  (zenon_X60 != (a1294))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X55))
% 2.20/2.43  (c7_1 zenon_X18)
% 2.20/2.43  (c7_2 (a1241) (a1336))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X50))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X46))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X52))
% 2.20/2.43  ((a1227) != (a1260))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X65))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X58))
% 2.20/2.43  ((a1300) != zenon_X101)
% 2.20/2.43  (c9_2 zenon_X38 (a1302))
% 2.20/2.43  (zenon_X42 != zenon_X49)
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1260)))
% 2.20/2.43  (-. (c8_2 zenon_X18 (a1352)))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X3))
% 2.20/2.43  (c7_2 (a1346) zenon_X82)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X65))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X63))
% 2.20/2.43  (c1_2 (a1215) (a1246))
% 2.20/2.43  (zenon_X30 != (a1255))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X31))
% 2.20/2.43  (zenon_X38 != zenon_X18)
% 2.20/2.43  ((a1336) != zenon_X28)
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1283)))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X81)
% 2.20/2.43  (zenon_X43 != zenon_X52)
% 2.20/2.43  (-. (c9_2 (a1346) (a1302)))
% 2.20/2.43  ((a1364) != zenon_X97)
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X58))
% 2.20/2.43  (c7_2 (a1255) zenon_X32)
% 2.20/2.43  (zenon_X14 != (a1326))
% 2.20/2.43  (-. (c3_2 (a1281) (a1282)))
% 2.20/2.43  (c9_0)
% 2.20/2.43  ((a1227) != zenon_X81)
% 2.20/2.43  (-. (c9_2 (a1255) (a1256)))
% 2.20/2.43  (c1_2 (a1215) zenon_X14)
% 2.20/2.43  ((a1271) != (a1302))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X52))
% 2.20/2.43  (zenon_X42 != zenon_X52)
% 2.20/2.43  (c7_2 (a1241) zenon_X65)
% 2.20/2.43  (zenon_X14 != (a1216))
% 2.20/2.43  (c7_2 zenon_X35 (a1260))
% 2.20/2.43  (c2_1 (a1255))
% 2.20/2.43  ((a1256) != zenon_X0)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X82))
% 2.20/2.43  (c5_2 (a1208) (a1246))
% 2.20/2.43  ((a1208) != (a1363))
% 2.20/2.43  (-. (c2_2 (a1214) (a1352)))
% 2.20/2.43  (zenon_X60 != (a1271))
% 2.20/2.43  (zenon_X30 != zenon_X27)
% 2.20/2.43  (-. (c1_2 zenon_X39 (a1246)))
% 2.20/2.43  (-. (c2_1 zenon_X25))
% 2.20/2.43  ((a1216) != (a1283))
% 2.20/2.43  (zenon_X16 != zenon_X81)
% 2.20/2.43  (zenon_X43 != (a1364))
% 2.20/2.43  (zenon_X16 != zenon_X64)
% 2.20/2.43  (zenon_X64 != zenon_X3)
% 2.20/2.43  ((a1347) != zenon_X57)
% 2.20/2.43  (c9_2 (a1293) (a1308))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X33))
% 2.20/2.43  (c7_2 (a1350) (a1364))
% 2.20/2.43  (c7_2 (a1270) zenon_X65)
% 2.20/2.43  (zenon_X46 != zenon_X65)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X82))
% 2.20/2.43  (-. (c10_1 (a1223)))
% 2.20/2.43  (c9_2 zenon_X30 (a1260))
% 2.20/2.43  ((a1300) != zenon_X110)
% 2.20/2.43  (c3_2 (a1350) zenon_X60)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X42))
% 2.20/2.43  ((a1308) != (a1364))
% 2.20/2.43  (zenon_X59 != zenon_X103)
% 2.20/2.43  (c9_2 (a1293) (a1300))
% 2.20/2.43  (c9_2 zenon_X8 (a1271))
% 2.20/2.43  (-. (c3_1 (a1241)))
% 2.20/2.43  (c2_2 zenon_X8 (a1326))
% 2.20/2.43  (zenon_X31 != (a1260))
% 2.20/2.43  ((a1308) != zenon_X15)
% 2.20/2.43  (c9_2 zenon_X27 (a1283))
% 2.20/2.43  (zenon_X33 != zenon_X5)
% 2.20/2.43  (c7_2 (a1241) zenon_X107)
% 2.20/2.43  (c7_2 zenon_X35 (a1300))
% 2.20/2.43  (c9_2 (a1241) zenon_X82)
% 2.20/2.43  ((a1336) != zenon_X3)
% 2.20/2.43  (c3_2 (a1350) (a1282))
% 2.20/2.43  (zenon_X106 != (a1364))
% 2.20/2.43  (zenon_X59 != zenon_X52)
% 2.20/2.43  ((a1277) != (a1364))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1302)))
% 2.20/2.43  ((a1246) != zenon_X58)
% 2.20/2.43  ((a1308) != (a1326))
% 2.20/2.43  ((a1214) != (a1335))
% 2.20/2.43  (-. (c9_2 (a1363) (a1246)))
% 2.20/2.43  (-. (c6_2 (a1215) (a1216)))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X103))
% 2.20/2.43  (c5_2 (a1270) (a1271))
% 2.20/2.43  (-. (c1_1 (a1354)))
% 2.20/2.43  (c3_2 (a1363) (a1256))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X65))
% 2.20/2.43  (ndr1_1 (a1270))
% 2.20/2.43  ((a1256) != zenon_X97)
% 2.20/2.43  (c7_2 (a1241) zenon_X102)
% 2.20/2.43  (zenon_X42 != (a1294))
% 2.20/2.43  ((a1282) != (a1300))
% 2.20/2.43  (zenon_X26 != (a1226))
% 2.20/2.43  ((a1294) != zenon_X3)
% 2.20/2.43  (zenon_X73 != zenon_X5)
% 2.20/2.43  ((a1223) != (a1214))
% 2.20/2.43  (c9_2 zenon_X18 (a1271))
% 2.20/2.43  (-. (c8_2 (a1215) (a1352)))
% 2.20/2.43  ((a1308) != zenon_X57)
% 2.20/2.43  (c7_1 (a1346))
% 2.20/2.43  (-. (c1_2 (a1270) (a1302)))
% 2.20/2.43  ((a1241) != (a1307))
% 2.20/2.43  (zenon_X32 != zenon_X71)
% 2.20/2.43  (-. (c5_2 (a1307) (a1271)))
% 2.20/2.43  (c7_2 (a1255) (a1227))
% 2.20/2.43  ((a1241) != (a1208))
% 2.20/2.43  (-. (c9_2 (a1208) (a1302)))
% 2.20/2.43  ((a1246) != zenon_X60)
% 2.20/2.43  ((a1216) != zenon_X31)
% 2.20/2.43  (c5_2 (a1335) (a1345))
% 2.20/2.43  (zenon_X41 != (a1271))
% 2.20/2.43  (-. (c10_1 zenon_X17))
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X49))
% 2.20/2.43  ((a1293) != zenon_X27)
% 2.20/2.43  (-. (c9_2 (a1350) (a1246)))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X43))
% 2.20/2.43  (zenon_X97 != zenon_X63)
% 2.20/2.43  (c9_2 (a1270) (a1216))
% 2.20/2.43  (-. (c1_2 (a1255) (a1326)))
% 2.20/2.43  (c8_2 (a1223) (a1347))
% 2.20/2.43  (-. (c10_2 (a1363) zenon_X91))
% 2.20/2.43  ((a1364) != zenon_X31)
% 2.20/2.43  (c9_2 zenon_X30 (a1302))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1345)))
% 2.20/2.43  (zenon_X14 != zenon_X50)
% 2.20/2.43  ((a1300) != zenon_X59)
% 2.20/2.43  (c2_1 (a1293))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X59))
% 2.20/2.43  ((a1336) != (a1227))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X57))
% 2.20/2.43  (c9_2 zenon_X17 (a1294))
% 2.20/2.43  (c9_2 zenon_X18 (a1227))
% 2.20/2.43  ((a1256) != zenon_X60)
% 2.20/2.43  (c3_2 (a1350) zenon_X16)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X73)
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X33))
% 2.20/2.43  (c3_1 (a1287))
% 2.20/2.43  (c7_2 (a1241) (a1308))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X103))
% 2.20/2.43  (c9_2 (a1281) zenon_X14)
% 2.20/2.43  (zenon_X16 != zenon_X102)
% 2.20/2.43  (zenon_X97 != zenon_X102)
% 2.20/2.43  (c9_2 zenon_X30 (a1294))
% 2.20/2.43  (zenon_X19 != (a1214))
% 2.20/2.43  (c2_1 (a1208))
% 2.20/2.43  (zenon_X39 != (a1255))
% 2.20/2.43  ((a1294) != zenon_X75)
% 2.20/2.43  ((a1270) != zenon_X27)
% 2.20/2.43  ((a1246) != (a1227))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X33))
% 2.20/2.43  (c3_2 (a1350) zenon_X52)
% 2.20/2.43  (zenon_X31 != zenon_X65)
% 2.20/2.43  (zenon_X41 != (a1256))
% 2.20/2.43  (-. (c6_2 (a1226) (a1216)))
% 2.20/2.43  (c3_2 (a1350) zenon_X49)
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X55))
% 2.20/2.43  (-. (c10_1 (a1270)))
% 2.20/2.43  (-. (c4_2 (a1287) zenon_X22))
% 2.20/2.43  (c5_2 (a1241) (a1345))
% 2.20/2.43  (-. (c10_2 zenon_X39 zenon_X70))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X59))
% 2.20/2.43  (c9_2 (a1255) zenon_X73)
% 2.20/2.43  (zenon_X103 != zenon_X46)
% 2.20/2.43  (zenon_X14 != zenon_X53)
% 2.20/2.43  (c7_2 (a1255) (a1300))
% 2.20/2.43  (-. (c2_1 (a1287)))
% 2.20/2.43  ((a1351) != (a1282))
% 2.20/2.43  ((a1277) != zenon_X57)
% 2.20/2.43  ((a1294) != zenon_X49)
% 2.20/2.43  ((a1246) != zenon_X43)
% 2.20/2.43  ((a1271) != zenon_X21)
% 2.20/2.43  (zenon_X55 != zenon_X63)
% 2.20/2.43  (zenon_X38 != (a1287))
% 2.20/2.43  (c5_2 (a1223) zenon_X103)
% 2.20/2.43  ((a1345) != zenon_X110)
% 2.20/2.43  ((a1277) != zenon_X50)
% 2.20/2.43  (c3_2 (a1350) (a1216))
% 2.20/2.43  (-. (c10_1 zenon_X38))
% 2.20/2.43  (c7_2 (a1220) (a1282))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X5))
% 2.20/2.43  (ndr1_1 (a1350))
% 2.20/2.43  (c7_2 (a1223) zenon_X33)
% 2.20/2.43  (-. (c10_2 (a1208) (a1352)))
% 2.20/2.43  (c9_1 zenon_X10)
% 2.20/2.43  (c9_2 (a1346) (a1300))
% 2.20/2.43  (c9_2 (a1293) (a1277))
% 2.20/2.43  ((a1352) != (a1300))
% 2.20/2.43  (-. (c1_1 zenon_X18))
% 2.20/2.43  (zenon_X32 != zenon_X5)
% 2.20/2.43  (zenon_X60 != (a1282))
% 2.20/2.43  ((a1227) != zenon_X102)
% 2.20/2.43  ((a1300) != (a1325))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X42))
% 2.20/2.43  (c9_2 zenon_X27 (a1302))
% 2.20/2.43  (-. (c10_2 (a1354) (a1352)))
% 2.20/2.43  ((a1300) != zenon_X81)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X54)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X97))
% 2.20/2.43  (c7_2 (a1293) zenon_X31)
% 2.20/2.43  (c7_2 (a1220) zenon_X71)
% 2.20/2.43  ((a1277) != (a1308))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X5))
% 2.20/2.43  (ndr1_1 (a1287))
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X16))
% 2.20/2.43  (c3_2 (a1350) zenon_X54)
% 2.20/2.43  (zenon_X102 != zenon_X49)
% 2.20/2.43  (c7_2 (a1241) (a1364))
% 2.20/2.43  (c7_2 (a1346) zenon_X43)
% 2.20/2.43  (ndr1_1 (a1226))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X57))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X31))
% 2.20/2.43  (ndr1_1 (a1307))
% 2.20/2.43  (zenon_X3 != (a1246))
% 2.20/2.43  (c7_2 (a1223) (a1364))
% 2.20/2.43  (c5_2 (a1223) zenon_X32)
% 2.20/2.43  (c7_2 (a1354) (a1364))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X16))
% 2.20/2.43  (c5_2 (a1281) (a1282))
% 2.20/2.43  ((a1216) != zenon_X52)
% 2.20/2.43  ((a1336) != zenon_X82)
% 2.20/2.43  ((a1256) != (a1302))
% 2.20/2.43  (-. (c5_2 (a1307) (a1294)))
% 2.20/2.43  ((a1220) != zenon_X39)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X103))
% 2.20/2.43  (-. (c2_2 (a1215) (a1352)))
% 2.20/2.43  (c7_2 (a1220) (a1216))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X3))
% 2.20/2.43  ((a1336) != (a1246))
% 2.20/2.43  (zenon_X59 != zenon_X32)
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X3))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X71))
% 2.20/2.43  (c9_2 zenon_X38 (a1345))
% 2.20/2.43  ((a1281) != (a1350))
% 2.20/2.43  (-. (c2_1 zenon_X38))
% 2.20/2.43  (zenon_X3 != zenon_X58)
% 2.20/2.43  (zenon_X59 != (a1294))
% 2.20/2.43  ((a1208) != zenon_X17)
% 2.20/2.43  (zenon_X33 != zenon_X49)
% 2.20/2.43  ((a1277) != zenon_X41)
% 2.20/2.43  (c5_2 (a1223) (a1271))
% 2.20/2.43  ((a1300) != zenon_X54)
% 2.20/2.43  (zenon_X18 != zenon_X39)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X71))
% 2.20/2.43  (c7_2 (a1346) zenon_X73)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X16))
% 2.20/2.43  (zenon_X73 != (a1294))
% 2.20/2.43  (-. (c6_2 (a1350) (a1271)))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X53))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X54))
% 2.20/2.43  (zenon_X31 != zenon_X103)
% 2.20/2.43  (zenon_X16 != zenon_X5)
% 2.20/2.43  (zenon_X82 != zenon_X102)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X3))
% 2.20/2.43  (zenon_X33 != zenon_X57)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X53))
% 2.20/2.43  (-. (c5_0))
% 2.20/2.43  ((a1300) != (a1246))
% 2.20/2.43  (zenon_X63 != zenon_X73)
% 2.20/2.43  (c5_2 (a1223) zenon_X53)
% 2.20/2.43  (c10_1 zenon_X30)
% 2.20/2.43  (-. (c9_2 (a1241) (a1326)))
% 2.20/2.43  ((a1227) != zenon_X54)
% 2.20/2.43  ((a1223) != zenon_X38)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X33))
% 2.20/2.43  ((a1294) != zenon_X46)
% 2.20/2.43  (c2_1 zenon_X27)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X33))
% 2.20/2.43  ((a1277) != zenon_X33)
% 2.20/2.43  ((a1282) != zenon_X102)
% 2.20/2.43  (c3_2 (a1350) zenon_X55)
% 2.20/2.43  ((a1346) != zenon_X17)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X55))
% 2.20/2.43  (zenon_X107 != zenon_X49)
% 2.20/2.43  (-. (c7_0))
% 2.20/2.43  (zenon_X16 != zenon_X43)
% 2.20/2.43  ((a1223) != (a1350))
% 2.20/2.43  (c9_2 (a1220) zenon_X82)
% 2.20/2.43  ((a1294) != (a1336))
% 2.20/2.43  (-. (c6_2 (a1287) (a1283)))
% 2.20/2.43  (-. (c8_2 zenon_X39 (a1352)))
% 2.20/2.43  (-. (c7_2 (a1223) (a1300)))
% 2.20/2.43  ((a1271) != zenon_X62)
% 2.20/2.43  ((a1216) != zenon_X60)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X57))
% 2.20/2.43  (zenon_X8 != (a1241))
% 2.20/2.43  (c7_2 (a1255) zenon_X16)
% 2.20/2.43  ((a1255) != (a1307))
% 2.20/2.43  ((a1347) != zenon_X97)
% 2.20/2.43  (ndr1_1 (a1255))
% 2.20/2.43  ((a1241) != zenon_X25)
% 2.20/2.43  (zenon_X49 != zenon_X3)
% 2.20/2.43  (c9_2 zenon_X8 (a1282))
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X42))
% 2.20/2.43  (zenon_X19 != (a1307))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X102))
% 2.20/2.43  ((a1352) != zenon_X100)
% 2.20/2.43  ((a1277) != zenon_X65)
% 2.20/2.43  (zenon_X16 != (a1308))
% 2.20/2.43  (zenon_X42 != zenon_X43)
% 2.20/2.43  (zenon_X55 != zenon_X31)
% 2.20/2.43  (-. (c6_2 (a1346) (a1300)))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X58))
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X16))
% 2.20/2.43  ((a1352) != zenon_X42)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X57))
% 2.20/2.43  (c3_2 (a1350) zenon_X73)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X54))
% 2.20/2.43  (-. (c1_2 (a1350) (a1326)))
% 2.20/2.43  (-. (c9_2 (a1293) (a1326)))
% 2.20/2.43  (c9_2 (a1281) zenon_X73)
% 2.20/2.43  ((a1346) != (a1281))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X32))
% 2.20/2.43  (zenon_X107 != zenon_X52)
% 2.20/2.43  (c6_1 zenon_X12)
% 2.20/2.43  (c6_2 (a1350) zenon_X41)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X5))
% 2.20/2.43  (c7_2 (a1255) zenon_X57)
% 2.20/2.43  ((a1271) != zenon_X23)
% 2.20/2.43  (c7_2 (a1220) zenon_X3)
% 2.20/2.43  (-. (c1_2 (a1293) (a1326)))
% 2.20/2.43  (c7_2 (a1220) zenon_X33)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X97))
% 2.20/2.43  (zenon_X43 != zenon_X46)
% 2.20/2.43  (zenon_X8 != (a1363))
% 2.20/2.43  (c7_2 (a1270) (a1282))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X97))
% 2.20/2.43  (c9_2 zenon_X35 (a1345))
% 2.20/2.43  (c7_2 (a1255) zenon_X65)
% 2.20/2.43  ((a1282) != zenon_X23)
% 2.20/2.43  (zenon_X71 != zenon_X65)
% 2.20/2.43  ((a1277) != zenon_X5)
% 2.20/2.43  (c7_1 (a1220))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1256)))
% 2.20/2.43  (c3_2 (a1276) (a1277))
% 2.20/2.43  (c8_2 (a1287) (a1351))
% 2.20/2.43  ((a1283) != zenon_X103)
% 2.20/2.43  ((a1352) != (a1260))
% 2.20/2.43  ((a1347) != zenon_X14)
% 2.20/2.43  (c8_0)
% 2.20/2.43  ((a1255) != (a1363))
% 2.20/2.43  (c10_2 (a1255) (a1256))
% 2.20/2.43  ((a1347) != zenon_X5)
% 2.20/2.43  ((a1300) != zenon_X43)
% 2.20/2.43  (c9_2 (a1270) (a1308))
% 2.20/2.43  (c7_2 zenon_X27 zenon_X108)
% 2.20/2.43  (-. (c1_2 (a1241) (a1326)))
% 2.20/2.43  (-. (c3_2 zenon_X39 (a1246)))
% 2.20/2.43  ((a1352) != zenon_X29)
% 2.20/2.43  ((a1271) != (a1277))
% 2.20/2.43  ((a1282) != zenon_X49)
% 2.20/2.43  (c7_2 (a1255) zenon_X55)
% 2.20/2.43  (-. (c7_2 (a1223) (a1246)))
% 2.20/2.43  ((a1347) != zenon_X82)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X64)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X52))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1351)))
% 2.20/2.43  (c2_2 zenon_X35 (a1326))
% 2.20/2.43  (c9_2 zenon_X38 (a1227))
% 2.20/2.43  ((a1347) != (a1246))
% 2.20/2.43  (zenon_X55 != zenon_X81)
% 2.20/2.43  (c3_2 (a1350) (a1308))
% 2.20/2.43  (zenon_X17 != zenon_X38)
% 2.20/2.43  (c9_2 (a1270) zenon_X14)
% 2.20/2.43  (zenon_X14 != (a1308))
% 2.20/2.43  (c7_2 (a1270) zenon_X33)
% 2.20/2.43  ((a1347) != zenon_X46)
% 2.20/2.43  (zenon_X55 != (a1294))
% 2.20/2.43  (c9_2 zenon_X27 (a1227))
% 2.20/2.43  (zenon_X73 != zenon_X52)
% 2.20/2.43  (-. (c10_2 (a1208) (a1351)))
% 2.20/2.43  ((a1246) != zenon_X97)
% 2.20/2.43  (c3_1 (a1214))
% 2.20/2.43  ((a1300) != zenon_X82)
% 2.20/2.43  (zenon_X14 != zenon_X41)
% 2.20/2.43  (-. (c10_1 zenon_X8))
% 2.20/2.43  ((a1300) != zenon_X46)
% 2.20/2.43  (c7_2 (a1223) (a1216))
% 2.20/2.43  (zenon_X59 != zenon_X3)
% 2.20/2.43  (-. (c1_2 (a1287) zenon_X23))
% 2.20/2.43  ((a1271) != zenon_X2)
% 2.20/2.43  (c5_2 (a1223) (a1246))
% 2.20/2.43  (zenon_X73 != (a1271))
% 2.20/2.43  (zenon_X33 != (a1351))
% 2.20/2.43  (c7_2 (a1241) (a1282))
% 2.20/2.43  (-. (c10_1 zenon_X35))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X97))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X14))
% 2.20/2.43  (c7_2 (a1350) zenon_X32)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X49))
% 2.20/2.43  (-. (c8_2 (a1293) (a1294)))
% 2.20/2.43  (-. (c2_1 (a1307)))
% 2.20/2.43  ((a1300) != zenon_X50)
% 2.20/2.43  ((a1345) != zenon_X60)
% 2.20/2.43  ((a1270) != zenon_X30)
% 2.20/2.43  ((a1216) != zenon_X42)
% 2.20/2.43  (zenon_X42 != (a1271))
% 2.20/2.43  ((a1352) != zenon_X36)
% 2.20/2.43  (zenon_X42 != zenon_X32)
% 2.20/2.43  ((a1294) != (a1277))
% 2.20/2.43  ((a1255) != (a1208))
% 2.20/2.43  (zenon_X55 != (a1345))
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X57))
% 2.20/2.43  (c7_2 zenon_X35 (a1282))
% 2.20/2.43  (c9_2 zenon_X17 (a1277))
% 2.20/2.43  ((a1345) != zenon_X64)
% 2.20/2.43  ((a1216) != zenon_X81)
% 2.20/2.43  ((a1216) != (a1352))
% 2.20/2.43  ((a1283) != zenon_X46)
% 2.20/2.43  (-. (c9_2 (a1220) (a1326)))
% 2.20/2.43  ((a1347) != (a1256))
% 2.20/2.43  (ndr1_1 zenon_X7)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X3))
% 2.20/2.43  (-. (c1_2 (a1363) (a1246)))
% 2.20/2.43  ((a1346) != zenon_X18)
% 2.20/2.43  (ndr1_1 zenon_X19)
% 2.20/2.43  (c4_0)
% 2.20/2.43  (c9_2 (a1241) (a1246))
% 2.20/2.43  ((a1336) != (a1345))
% 2.20/2.43  (zenon_X42 != zenon_X59)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X82)
% 2.20/2.43  (c7_1 (a1293))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X60))
% 2.20/2.43  (c7_2 (a1241) zenon_X73)
% 2.20/2.43  (c6_2 (a1346) (a1347))
% 2.20/2.43  (c3_2 (a1350) zenon_X3)
% 2.20/2.43  ((a1336) != zenon_X102)
% 2.20/2.43  (-. (c1_2 (a1363) (a1364)))
% 2.20/2.43  (-. (c1_1 zenon_X8))
% 2.20/2.43  (c7_2 (a1350) (a1256))
% 2.20/2.43  ((a1347) != zenon_X33)
% 2.20/2.43  ((a1294) != zenon_X53)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X52))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X42))
% 2.20/2.43  (c7_2 zenon_X35 (a1364))
% 2.20/2.43  (c7_2 (a1220) zenon_X102)
% 2.20/2.43  (-. (c7_2 (a1223) (a1271)))
% 2.20/2.43  (zenon_X55 != zenon_X42)
% 2.20/2.43  ((a1283) != zenon_X61)
% 2.20/2.43  (c7_2 (a1220) zenon_X52)
% 2.20/2.43  (-. (c6_2 (a1346) (a1282)))
% 2.20/2.43  (c5_2 (a1223) zenon_X50)
% 2.20/2.43  (c7_2 (a1270) zenon_X103)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X31))
% 2.20/2.43  ((a1256) != zenon_X59)
% 2.20/2.43  (-. (c5_2 (a1226) (a1227)))
% 2.20/2.43  (c9_2 (a1241) (a1277))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X97))
% 2.20/2.43  (zenon_X31 != zenon_X46)
% 2.20/2.43  (c9_2 (a1354) (a1271))
% 2.20/2.43  (c9_2 (a1241) (a1294))
% 2.20/2.43  (c9_1 zenon_X26)
% 2.20/2.43  (-. (c6_2 (a1350) (a1256)))
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X97))
% 2.20/2.43  ((a1241) != zenon_X18)
% 2.20/2.43  ((a1282) != (a1227))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X33))
% 2.20/2.43  (c9_2 zenon_X27 (a1260))
% 2.20/2.43  (-. (c8_2 zenon_X38 (a1352)))
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X3))
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X57))
% 2.20/2.43  (c7_2 (a1346) (a1216))
% 2.20/2.43  ((a1364) != zenon_X64)
% 2.20/2.43  (-. (c3_2 (a1363) (a1246)))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X46))
% 2.20/2.43  (zenon_X54 != zenon_X57)
% 2.20/2.43  (zenon_X32 != zenon_X82)
% 2.20/2.43  (-. (c2_2 zenon_X38 (a1352)))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X31))
% 2.20/2.43  ((a1277) != zenon_X14)
% 2.20/2.43  (-. (c6_2 (a1226) (a1300)))
% 2.20/2.43  ((a1220) != (a1363))
% 2.20/2.43  (zenon_X43 != zenon_X3)
% 2.20/2.43  (zenon_X30 != (a1350))
% 2.20/2.43  (c9_2 (a1255) (a1227))
% 2.20/2.43  ((a1352) != zenon_X46)
% 2.20/2.43  (-. (c5_2 zenon_X8 (a1326)))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X54))
% 2.20/2.43  (c9_2 zenon_X8 (a1256))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X54))
% 2.20/2.43  (-. (c1_2 (a1287) (a1302)))
% 2.20/2.43  (c7_2 (a1346) zenon_X3)
% 2.20/2.43  (-. (c2_2 (a1335) (a1336)))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X71))
% 2.20/2.43  ((a1351) != (a1326))
% 2.20/2.43  (zenon_X107 != (a1326))
% 2.20/2.43  (zenon_X63 != zenon_X31)
% 2.20/2.43  (-. (c5_1 (a1350)))
% 2.20/2.43  (zenon_X42 != (a1282))
% 2.20/2.43  (c7_2 (a1241) zenon_X71)
% 2.20/2.43  (c7_2 (a1350) zenon_X57)
% 2.20/2.43  (-. (c8_2 (a1293) (a1352)))
% 2.20/2.43  ((a1352) != (a1282))
% 2.20/2.43  (-. (c8_1 (a1214)))
% 2.20/2.43  (c9_2 zenon_X25 (a1300))
% 2.20/2.43  (c1_1 zenon_X17)
% 2.20/2.43  (c9_2 (a1270) (a1277))
% 2.20/2.43  (c7_2 (a1241) zenon_X52)
% 2.20/2.43  ((a1246) != zenon_X64)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X32))
% 2.20/2.43  ((a1255) != (a1223))
% 2.20/2.43  (c7_2 (a1241) zenon_X97)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X59))
% 2.20/2.43  ((a1351) != (a1300))
% 2.20/2.43  (zenon_X59 != zenon_X46)
% 2.20/2.43  (zenon_X42 != (a1308))
% 2.20/2.43  ((a1352) != zenon_X32)
% 2.20/2.43  (c7_2 (a1270) zenon_X73)
% 2.20/2.43  (c7_2 (a1293) zenon_X32)
% 2.20/2.43  (zenon_X43 != zenon_X31)
% 2.20/2.43  (c6_2 (a1350) zenon_X52)
% 2.20/2.43  (c5_2 (a1223) zenon_X73)
% 2.20/2.43  ((a1256) != zenon_X73)
% 2.20/2.43  (c7_2 (a1241) (a1347))
% 2.20/2.43  (zenon_X107 != zenon_X5)
% 2.20/2.43  (c5_2 zenon_X27 (a1246))
% 2.20/2.43  (c9_2 zenon_X8 (a1352))
% 2.20/2.43  (zenon_X55 != zenon_X57)
% 2.20/2.43  (zenon_X103 != (a1302))
% 2.20/2.43  (zenon_X16 != (a1345))
% 2.20/2.43  ((a1346) != (a1287))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X81))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X3))
% 2.20/2.43  (c9_2 (a1223) zenon_X107)
% 2.20/2.43  (c7_2 (a1255) zenon_X33)
% 2.20/2.43  ((a1241) != (a1270))
% 2.20/2.43  ((a1300) != zenon_X60)
% 2.20/2.43  (c7_2 (a1270) zenon_X3)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X64))
% 2.20/2.43  ((a1350) != (a1307))
% 2.20/2.43  (zenon_X73 != (a1326))
% 2.20/2.43  (c1_2 (a1215) (a1294))
% 2.20/2.43  (c10_2 zenon_X18 (a1352))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X16))
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X65))
% 2.20/2.43  (c9_2 (a1241) zenon_X71)
% 2.20/2.43  (c9_2 (a1281) (a1294))
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X42))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X33))
% 2.20/2.43  ((a1216) != (a1271))
% 2.20/2.43  (zenon_X73 != (a1302))
% 2.20/2.43  ((a1351) != (a1271))
% 2.20/2.43  (-. (c4_2 (a1270) (a1283)))
% 2.20/2.43  ((a1216) != zenon_X50)
% 2.20/2.43  ((a1256) != (a1277))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X103))
% 2.20/2.43  (c5_2 (a1223) zenon_X82)
% 2.20/2.43  (-. (c10_1 (a1281)))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X55))
% 2.20/2.43  (c6_2 (a1350) zenon_X102)
% 2.20/2.43  (-. (c1_2 (a1350) (a1246)))
% 2.20/2.43  (c7_2 zenon_X35 (a1308))
% 2.20/2.43  (-. (c1_1 (a1350)))
% 2.20/2.43  ((a1214) != zenon_X18)
% 2.20/2.43  (zenon_X82 != zenon_X5)
% 2.20/2.43  (zenon_X60 != zenon_X73)
% 2.20/2.43  ((a1277) != zenon_X43)
% 2.20/2.43  ((a1345) != zenon_X5)
% 2.20/2.43  (c7_2 (a1346) zenon_X63)
% 2.20/2.43  ((a1351) != zenon_X66)
% 2.20/2.43  (zenon_X14 != (a1271))
% 2.20/2.43  (c10_2 (a1363) (a1352))
% 2.20/2.43  ((a1270) != zenon_X25)
% 2.20/2.43  (c6_1 zenon_X17)
% 2.20/2.43  ((a1282) != zenon_X34)
% 2.20/2.43  (c9_2 (a1223) (a1345))
% 2.20/2.43  (c7_2 (a1208) zenon_X106)
% 2.20/2.43  (zenon_X63 != zenon_X57)
% 2.20/2.43  (-. (c1_2 (a1208) (a1326)))
% 2.20/2.43  ((a1354) != (a1335))
% 2.20/2.43  ((a1214) != (a1350))
% 2.20/2.43  (zenon_X27 != (a1354))
% 2.20/2.43  ((a1287) != zenon_X27)
% 2.20/2.43  (-. (c9_2 (a1350) (a1326)))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X59))
% 2.20/2.43  (zenon_X60 != (a1352))
% 2.20/2.43  ((a1277) != (a1326))
% 2.20/2.43  ((a1347) != (a1308))
% 2.20/2.43  (c7_2 (a1241) zenon_X5)
% 2.20/2.43  (c7_2 (a1346) zenon_X32)
% 2.20/2.43  ((a1352) != zenon_X49)
% 2.20/2.43  ((a1271) != zenon_X31)
% 2.20/2.43  ((a1363) != (a1287))
% 2.20/2.43  (zenon_X81 != zenon_X71)
% 2.20/2.43  (zenon_X12 != (a1220))
% 2.20/2.43  (-. (c4_2 (a1293) zenon_X21))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X60))
% 2.20/2.43  ((a1283) != (a1308))
% 2.20/2.43  ((a1227) != zenon_X103)
% 2.20/2.43  (c7_2 (a1270) (a1256))
% 2.20/2.43  (zenon_X55 != (a1336))
% 2.20/2.43  (zenon_X59 != zenon_X102)
% 2.20/2.43  (-. (c1_2 (a1287) (a1256)))
% 2.20/2.43  ((a1216) != zenon_X58)
% 2.20/2.43  ((a1294) != zenon_X56)
% 2.20/2.43  ((a1283) != zenon_X32)
% 2.20/2.43  (c9_2 (a1220) zenon_X73)
% 2.20/2.43  (zenon_X55 != zenon_X52)
% 2.20/2.43  (c7_2 (a1346) zenon_X16)
% 2.20/2.43  (c3_2 (a1350) (a1300))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X5))
% 2.20/2.43  ((a1208) != (a1281))
% 2.20/2.43  (-. (c2_2 (a1307) (a1352)))
% 2.20/2.43  ((a1294) != zenon_X64)
% 2.20/2.43  (zenon_X73 != zenon_X54)
% 2.20/2.43  ((a1293) != zenon_X25)
% 2.20/2.43  ((a1277) != (a1260))
% 2.20/2.43  ((a1300) != zenon_X15)
% 2.20/2.43  (-. (c1_1 (a1270)))
% 2.20/2.43  (-. (c9_2 (a1208) (a1246)))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X16))
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X32))
% 2.20/2.43  (c3_2 zenon_X39 (a1352))
% 2.20/2.43  (c7_1 (a1215))
% 2.20/2.43  (zenon_X10 != (a1226))
% 2.20/2.43  (zenon_X81 != (a1271))
% 2.20/2.43  (c7_2 (a1350) zenon_X99)
% 2.20/2.43  (-. (c9_2 zenon_X27 (a1246)))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X58))
% 2.20/2.43  (zenon_X3 != zenon_X16)
% 2.20/2.43  (zenon_X33 != zenon_X32)
% 2.20/2.43  (zenon_X31 != zenon_X107)
% 2.20/2.43  (zenon_X53 != zenon_X57)
% 2.20/2.43  (c10_2 zenon_X39 (a1352))
% 2.20/2.43  (-. (c1_1 (a1223)))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X49))
% 2.20/2.43  (zenon_X63 != zenon_X65)
% 2.20/2.43  ((a1350) != (a1354))
% 2.20/2.43  (c1_2 (a1215) (a1282))
% 2.20/2.43  (c7_2 (a1293) zenon_X57)
% 2.20/2.43  (c2_1 (a1346))
% 2.20/2.43  (ndr1_1 (a1293))
% 2.20/2.43  (c9_2 (a1220) (a1227))
% 2.20/2.43  ((a1282) != (a1302))
% 2.20/2.43  (c6_2 (a1350) (a1216))
% 2.20/2.43  (-. (c1_1 (a1293)))
% 2.20/2.43  (c9_2 (a1346) (a1347))
% 2.20/2.43  (zenon_X14 != zenon_X33)
% 2.20/2.43  ((a1345) != zenon_X104)
% 2.20/2.43  ((a1352) != (a1246))
% 2.20/2.43  ((a1300) != (a1227))
% 2.20/2.43  (c9_2 zenon_X30 (a1277))
% 2.20/2.43  (-. (c3_2 (a1307) (a1277)))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X81))
% 2.20/2.43  (-. (c6_2 (a1226) (a1271)))
% 2.20/2.43  (c5_2 zenon_X39 (a1246))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X97))
% 2.20/2.43  (zenon_X77 != (a1364))
% 2.20/2.43  ((a1271) != (a1282))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X65))
% 2.20/2.43  ((a1336) != zenon_X57)
% 2.20/2.43  (zenon_X73 != zenon_X53)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X64))
% 2.20/2.43  ((a1294) != zenon_X102)
% 2.20/2.43  (zenon_X14 != zenon_X42)
% 2.20/2.43  (c5_2 (a1223) zenon_X41)
% 2.20/2.43  (-. (c4_2 (a1208) zenon_X37))
% 2.20/2.43  (-. (c7_2 (a1223) (a1294)))
% 2.20/2.43  (zenon_X8 != (a1287))
% 2.20/2.43  (c6_2 (a1350) zenon_X73)
% 2.20/2.43  ((a1227) != zenon_X42)
% 2.20/2.43  (c1_1 (a1214))
% 2.20/2.43  (-. (c9_2 (a1354) (a1246)))
% 2.20/2.43  (-. (c3_2 (a1307) (a1294)))
% 2.20/2.43  ((a1220) != (a1346))
% 2.20/2.43  (c6_2 (a1350) zenon_X5)
% 2.20/2.43  (-. (c3_2 (a1307) (a1271)))
% 2.20/2.43  (zenon_X97 != zenon_X81)
% 2.20/2.43  (c7_2 (a1293) zenon_X73)
% 2.20/2.43  (zenon_X55 != zenon_X58)
% 2.20/2.43  ((a1364) != zenon_X57)
% 2.20/2.43  (zenon_X33 != zenon_X73)
% 2.20/2.43  (c9_2 (a1281) (a1246))
% 2.20/2.43  (zenon_X3 != zenon_X41)
% 2.20/2.43  ((a1282) != zenon_X52)
% 2.20/2.43  (c9_2 zenon_X18 (a1364))
% 2.20/2.43  (zenon_X16 != zenon_X31)
% 2.20/2.43  ((a1294) != zenon_X23)
% 2.20/2.43  ((a1350) != zenon_X27)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X42))
% 2.20/2.43  ((a1223) != zenon_X18)
% 2.20/2.43  (c1_2 (a1215) zenon_X107)
% 2.20/2.43  ((a1277) != zenon_X20)
% 2.20/2.43  ((a1215) != zenon_X27)
% 2.20/2.43  ((a1227) != zenon_X33)
% 2.20/2.43  (zenon_X82 != zenon_X50)
% 2.20/2.43  ((a1335) != (a1307))
% 2.20/2.43  (zenon_X30 != (a1354))
% 2.20/2.43  (zenon_X38 != zenon_X27)
% 2.20/2.43  ((a1352) != zenon_X93)
% 2.20/2.43  (c9_2 (a1346) (a1352))
% 2.20/2.43  ((a1277) != (a1216))
% 2.20/2.43  (-. (c1_2 (a1354) (a1246)))
% 2.20/2.43  (zenon_X32 != zenon_X103)
% 2.20/2.43  (-. (c1_2 zenon_X25 (a1302)))
% 2.20/2.43  ((a1347) != zenon_X50)
% 2.20/2.43  ((a1246) != zenon_X65)
% 2.20/2.43  (-. (c7_2 (a1223) (a1308)))
% 2.20/2.43  (c4_1 (a1354))
% 2.20/2.43  (c9_2 (a1255) (a1246))
% 2.20/2.43  (zenon_X39 != (a1214))
% 2.20/2.43  (-. (c8_2 zenon_X8 (a1352)))
% 2.20/2.43  (zenon_X33 != zenon_X81)
% 2.20/2.43  (zenon_X97 != zenon_X32)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X41))
% 2.20/2.43  ((a1347) != zenon_X102)
% 2.20/2.43  (-. (c1_2 (a1220) (a1326)))
% 2.20/2.43  ((a1256) != zenon_X82)
% 2.20/2.43  (zenon_X97 != zenon_X59)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X63))
% 2.20/2.43  (zenon_X31 != zenon_X54)
% 2.20/2.43  ((a1294) != zenon_X31)
% 2.20/2.43  (zenon_X32 != zenon_X102)
% 2.20/2.43  (zenon_X33 != zenon_X46)
% 2.20/2.43  ((a1282) != zenon_X65)
% 2.20/2.43  ((a1283) != zenon_X21)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X46))
% 2.20/2.43  (zenon_X97 != (a1271))
% 2.20/2.43  ((a1347) != zenon_X31)
% 2.20/2.43  (zenon_X14 != (a1227))
% 2.20/2.43  (c3_2 (a1363) (a1351))
% 2.20/2.43  (zenon_X55 != zenon_X73)
% 2.20/2.43  (zenon_X32 != zenon_X65)
% 2.20/2.43  ((a1308) != zenon_X53)
% 2.20/2.43  ((a1300) != (a1302))
% 2.20/2.43  ((a1256) != zenon_X46)
% 2.20/2.43  ((a1350) != zenon_X13)
% 2.20/2.43  ((a1293) != zenon_X18)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X54))
% 2.20/2.43  (c7_2 (a1270) (a1364))
% 2.20/2.43  ((a1352) != zenon_X73)
% 2.20/2.43  (zenon_X71 != zenon_X5)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X43))
% 2.20/2.43  ((a1287) != (a1335))
% 2.20/2.43  (-. (c4_2 (a1281) zenon_X61))
% 2.20/2.43  (c8_2 zenon_X25 (a1351))
% 2.20/2.43  (c7_2 (a1220) (a1294))
% 2.20/2.43  (zenon_X33 != zenon_X50)
% 2.20/2.43  (zenon_X42 != zenon_X31)
% 2.20/2.43  ((a1351) != (a1246))
% 2.20/2.43  (c5_2 (a1223) zenon_X43)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X43))
% 2.20/2.43  (c7_1 zenon_X30)
% 2.20/2.43  (zenon_X43 != zenon_X65)
% 2.20/2.43  (ndr1_1 (a1346))
% 2.20/2.43  (c8_2 (a1335) (a1336))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1294)))
% 2.20/2.43  ((a1216) != zenon_X107)
% 2.20/2.43  ((a1223) != zenon_X25)
% 2.20/2.43  ((a1246) != zenon_X52)
% 2.20/2.43  (zenon_X33 != zenon_X97)
% 2.20/2.43  ((a1293) != (a1350))
% 2.20/2.43  ((a1294) != zenon_X29)
% 2.20/2.43  (-. (c9_2 (a1241) (a1302)))
% 2.20/2.43  ((a1246) != zenon_X82)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X42))
% 2.20/2.43  (c7_2 (a1255) (a1294))
% 2.20/2.43  (zenon_X43 != zenon_X5)
% 2.20/2.43  ((a1354) != (a1223))
% 2.20/2.43  ((a1215) != (a1363))
% 2.20/2.43  ((a1345) != zenon_X50)
% 2.20/2.43  (zenon_X63 != zenon_X32)
% 2.20/2.43  (c9_2 (a1241) zenon_X31)
% 2.20/2.43  ((a1216) != zenon_X46)
% 2.20/2.43  (zenon_X59 != zenon_X73)
% 2.20/2.43  (c7_2 (a1346) zenon_X107)
% 2.20/2.43  ((a1208) != (a1270))
% 2.20/2.43  (zenon_X55 != zenon_X65)
% 2.20/2.43  ((a1246) != zenon_X71)
% 2.20/2.43  (c2_0)
% 2.20/2.43  ((a1294) != zenon_X5)
% 2.20/2.43  ((a1300) != (a1364))
% 2.20/2.43  ((a1308) != zenon_X52)
% 2.20/2.43  (c7_2 (a1241) zenon_X33)
% 2.20/2.43  (zenon_X16 != zenon_X49)
% 2.20/2.43  ((a1294) != (a1216))
% 2.20/2.43  ((a1227) != zenon_X58)
% 2.20/2.43  (c5_2 (a1293) (a1294))
% 2.20/2.43  (c10_2 zenon_X38 (a1352))
% 2.20/2.43  (zenon_X16 != zenon_X50)
% 2.20/2.43  ((a1271) != zenon_X61)
% 2.20/2.43  (c8_2 (a1281) (a1282))
% 2.20/2.43  (c7_2 (a1293) (a1256))
% 2.20/2.43  ((a1256) != zenon_X91)
% 2.20/2.43  (c7_2 (a1255) zenon_X42)
% 2.20/2.43  (ndr1_1 zenon_X38)
% 2.20/2.43  (zenon_X55 != zenon_X41)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X49))
% 2.20/2.43  (-. (c10_2 zenon_X25 zenon_X85))
% 2.20/2.43  (zenon_X18 != (a1363))
% 2.20/2.43  (zenon_X97 != (a1283))
% 2.20/2.43  (-. (c5_2 (a1208) zenon_X104))
% 2.20/2.43  ((a1345) != zenon_X32)
% 2.20/2.43  ((a1246) != zenon_X73)
% 2.20/2.43  (-. (c8_2 (a1293) (a1256)))
% 2.20/2.43  (c9_2 (a1223) (a1352))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X97))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X53))
% 2.20/2.43  (zenon_X97 != zenon_X107)
% 2.20/2.43  (c3_2 (a1223) zenon_X3)
% 2.20/2.43  ((a1294) != zenon_X91)
% 2.20/2.43  ((a1277) != zenon_X32)
% 2.20/2.43  (c9_2 (a1223) (a1277))
% 2.20/2.43  (c7_2 (a1270) (a1347))
% 2.20/2.43  ((a1347) != zenon_X54)
% 2.20/2.43  ((a1352) != (a1330))
% 2.20/2.43  (c9_2 (a1293) (a1364))
% 2.20/2.43  ((a1336) != zenon_X20)
% 2.20/2.43  (zenon_X73 != zenon_X103)
% 2.20/2.43  (c3_2 (a1350) zenon_X43)
% 2.20/2.43  ((a1270) != (a1287))
% 2.20/2.43  (c2_1 (a1223))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X107))
% 2.20/2.43  (-. (c10_2 zenon_X35 (a1256)))
% 2.20/2.43  (-. (c2_2 (a1363) (a1352)))
% 2.20/2.43  ((a1282) != zenon_X53)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X49))
% 2.20/2.43  (zenon_X97 != zenon_X58)
% 2.20/2.43  ((a1256) != zenon_X4)
% 2.20/2.43  ((a1364) != zenon_X59)
% 2.20/2.43  (c9_2 (a1255) (a1352))
% 2.20/2.43  (c9_2 (a1220) zenon_X31)
% 2.20/2.43  (c3_2 (a1350) zenon_X14)
% 2.20/2.43  (c9_2 (a1281) (a1283))
% 2.20/2.43  (c3_2 (a1350) zenon_X81)
% 2.20/2.43  (zenon_X30 != zenon_X17)
% 2.20/2.43  (zenon_X81 != zenon_X3)
% 2.20/2.43  (-. (c8_2 (a1293) (a1336)))
% 2.20/2.43  (c7_2 (a1270) zenon_X14)
% 2.20/2.43  ((a1352) != zenon_X5)
% 2.20/2.43  (-. (c10_2 zenon_X27 (a1352)))
% 2.20/2.43  (c7_2 (a1241) zenon_X14)
% 2.20/2.43  ((a1283) != zenon_X2)
% 2.20/2.43  (zenon_X33 != zenon_X59)
% 2.20/2.43  (-. (c6_1 (a1220)))
% 2.20/2.43  (zenon_X55 != zenon_X107)
% 2.20/2.43  ((a1283) != zenon_X102)
% 2.20/2.43  ((a1216) != zenon_X64)
% 2.20/2.43  ((a1255) != zenon_X27)
% 2.20/2.43  (-. (c3_2 (a1255) (a1256)))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X42))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X33))
% 2.20/2.43  (c9_2 zenon_X8 (a1308))
% 2.20/2.43  (c7_2 (a1346) zenon_X57)
% 2.20/2.43  ((a1294) != zenon_X28)
% 2.20/2.43  (ndr1_1 (a1335))
% 2.20/2.43  ((a1336) != (a1352))
% 2.20/2.43  ((a1347) != (a1330))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X52))
% 2.20/2.43  ((a1227) != zenon_X53)
% 2.20/2.43  (c7_2 (a1346) (a1282))
% 2.20/2.43  (-. (c3_2 (a1307) (a1283)))
% 2.20/2.43  ((a1255) != (a1226))
% 2.20/2.43  (-. (c3_2 (a1307) (a1352)))
% 2.20/2.43  (zenon_X16 != (a1364))
% 2.20/2.43  ((a1294) != zenon_X82)
% 2.20/2.43  (c7_2 (a1270) zenon_X41)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X5)
% 2.20/2.43  (c9_2 zenon_X27 (a1345))
% 2.20/2.43  ((a1364) != zenon_X52)
% 2.20/2.43  ((a1336) != zenon_X31)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X43))
% 2.20/2.43  (zenon_X32 != zenon_X46)
% 2.20/2.43  ((a1364) != zenon_X71)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X3))
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X42))
% 2.20/2.43  (zenon_X60 != zenon_X103)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X43)
% 2.20/2.43  ((a1246) != zenon_X103)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X55))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X32))
% 2.20/2.43  (c9_2 (a1281) (a1345))
% 2.20/2.43  ((a1241) != (a1223))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X63))
% 2.20/2.43  (c7_2 (a1354) zenon_X77)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X65))
% 2.20/2.43  (c6_2 (a1350) (a1351))
% 2.20/2.43  (zenon_X35 != (a1208))
% 2.20/2.43  (zenon_X64 != zenon_X57)
% 2.20/2.43  (c7_2 (a1241) zenon_X42)
% 2.20/2.43  (c5_2 (a1223) zenon_X5)
% 2.20/2.43  (c7_2 (a1223) zenon_X16)
% 2.20/2.43  ((a1347) != zenon_X73)
% 2.20/2.43  (zenon_X35 != (a1287))
% 2.20/2.43  (c7_2 (a1270) zenon_X53)
% 2.20/2.43  ((a1352) != zenon_X70)
% 2.20/2.43  (-. (c10_0))
% 2.20/2.43  (zenon_X55 != zenon_X97)
% 2.20/2.43  (zenon_X58 != (a1271))
% 2.20/2.43  (zenon_X57 != zenon_X32)
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1216)))
% 2.20/2.43  ((a1351) != (a1216))
% 2.20/2.43  (zenon_X35 != (a1215))
% 2.20/2.43  (zenon_X42 != zenon_X50)
% 2.20/2.43  ((a1282) != zenon_X71)
% 2.20/2.43  ((a1283) != zenon_X22)
% 2.20/2.43  (zenon_X81 != zenon_X52)
% 2.20/2.43  (zenon_X25 != (a1208))
% 2.20/2.43  (c3_2 (a1350) (a1345))
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X65))
% 2.20/2.43  ((a1346) != (a1270))
% 2.20/2.43  ((a1256) != zenon_X52)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X57))
% 2.20/2.43  ((a1216) != (a1326))
% 2.20/2.43  (zenon_X33 != zenon_X58)
% 2.20/2.43  (zenon_X97 != zenon_X71)
% 2.20/2.43  ((a1335) != (a1293))
% 2.20/2.43  (c9_2 zenon_X18 (a1260))
% 2.20/2.43  (c5_2 (a1223) zenon_X57)
% 2.20/2.43  (zenon_X35 != zenon_X25)
% 2.20/2.43  (c3_2 (a1350) zenon_X82)
% 2.20/2.43  (-. (c5_2 (a1214) (a1282)))
% 2.20/2.43  (zenon_X97 != zenon_X73)
% 2.20/2.43  (-. (c1_2 (a1270) (a1326)))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X65))
% 2.20/2.43  (c7_2 (a1220) (a1352))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1347)))
% 2.20/2.43  ((a1294) != (a1300))
% 2.20/2.43  ((a1256) != zenon_X71)
% 2.20/2.43  (zenon_X3 != (a1271))
% 2.20/2.43  (c9_2 (a1293) zenon_X103)
% 2.20/2.43  (-. (c2_2 zenon_X17 (a1352)))
% 2.20/2.43  (zenon_X14 != zenon_X58)
% 2.20/2.43  (zenon_X64 != zenon_X65)
% 2.20/2.43  (zenon_X82 != zenon_X53)
% 2.20/2.43  (zenon_X55 != zenon_X54)
% 2.20/2.43  (c5_2 (a1223) zenon_X63)
% 2.20/2.43  (zenon_X32 != zenon_X54)
% 2.20/2.43  (c9_2 zenon_X18 (a1282))
% 2.20/2.43  (c1_2 (a1215) zenon_X31)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X59))
% 2.20/2.43  (c9_2 zenon_X27 (a1352))
% 2.20/2.43  (zenon_X107 != zenon_X65)
% 2.20/2.43  ((a1352) != (a1227))
% 2.20/2.43  (zenon_X14 != zenon_X65)
% 2.20/2.43  ((a1281) != (a1354))
% 2.20/2.43  ((a1364) != zenon_X65)
% 2.20/2.43  (zenon_X14 != zenon_X97)
% 2.20/2.43  ((a1307) != (a1354))
% 2.20/2.43  ((a1294) != zenon_X36)
% 2.20/2.43  ((a1363) != zenon_X39)
% 2.20/2.43  (zenon_X55 != zenon_X82)
% 2.20/2.43  ((a1345) != zenon_X3)
% 2.20/2.43  (-. (c9_2 (a1223) (a1326)))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X3))
% 2.20/2.43  (zenon_X102 != (a1302))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X46))
% 2.20/2.43  ((a1364) != (a1347))
% 2.20/2.43  (c9_2 (a1346) (a1308))
% 2.20/2.43  ((a1347) != zenon_X103)
% 2.20/2.43  ((a1283) != zenon_X3)
% 2.20/2.43  (zenon_X16 != zenon_X60)
% 2.20/2.43  ((a1271) != zenon_X20)
% 2.20/2.43  (c7_1 (a1255))
% 2.20/2.43  (ndr1_1 (a1354))
% 2.20/2.43  (c6_2 (a1350) (a1347))
% 2.20/2.43  (zenon_X42 != (a1300))
% 2.20/2.43  ((a1326) != (a1347))
% 2.20/2.43  (c7_2 (a1220) zenon_X97)
% 2.20/2.43  (zenon_X55 != (a1364))
% 2.20/2.43  (zenon_X58 != zenon_X52)
% 2.20/2.43  (zenon_X63 != (a1294))
% 2.20/2.43  (-. (c10_2 (a1354) (a1351)))
% 2.20/2.43  (-. (c10_2 (a1255) (a1294)))
% 2.20/2.43  (zenon_X30 != zenon_X8)
% 2.20/2.43  (zenon_X63 != zenon_X71)
% 2.20/2.43  ((a1241) != (a1215))
% 2.20/2.43  (c2_2 (a1208) (a1326))
% 2.20/2.43  ((a1345) != zenon_X53)
% 2.20/2.43  (c7_2 (a1270) (a1227))
% 2.20/2.43  (c5_2 zenon_X19 (a1300))
% 2.20/2.43  ((a1350) != (a1287))
% 2.20/2.43  (zenon_X55 != (a1351))
% 2.20/2.43  ((a1283) != zenon_X57)
% 2.20/2.43  (zenon_X82 != zenon_X107)
% 2.20/2.43  (c3_2 (a1350) zenon_X53)
% 2.20/2.43  (-. (c1_2 (a1287) (a1352)))
% 2.20/2.43  (zenon_X63 != (a1282))
% 2.20/2.43  (zenon_X39 != zenon_X35)
% 2.20/2.43  ((a1241) != zenon_X38)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X64))
% 2.20/2.43  ((a1256) != zenon_X53)
% 2.20/2.43  (zenon_X73 != zenon_X102)
% 2.20/2.43  (zenon_X18 != (a1208))
% 2.20/2.43  (zenon_X38 != (a1350))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X52))
% 2.20/2.43  ((a1216) != zenon_X43)
% 2.20/2.43  ((a1351) != (a1277))
% 2.20/2.43  ((a1227) != zenon_X57)
% 2.20/2.43  ((a1308) != (a1300))
% 2.20/2.43  ((a1300) != zenon_X31)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X42))
% 2.20/2.43  (c7_2 (a1346) zenon_X52)
% 2.20/2.43  ((a1364) != zenon_X49)
% 2.20/2.43  ((a1216) != zenon_X71)
% 2.20/2.43  ((a1294) != zenon_X34)
% 2.20/2.43  (c7_2 (a1223) zenon_X14)
% 2.20/2.43  ((a1345) != (a1326))
% 2.20/2.43  (zenon_X59 != (a1282))
% 2.20/2.43  ((a1294) != (a1260))
% 2.20/2.43  (c9_2 zenon_X18 (a1216))
% 2.20/2.43  (c7_2 (a1346) zenon_X59)
% 2.20/2.43  ((a1246) != (a1256))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X46))
% 2.20/2.43  (c1_2 (a1215) (a1271))
% 2.20/2.43  ((a1220) != (a1255))
% 2.20/2.43  ((a1330) != (a1246))
% 2.20/2.43  ((a1300) != zenon_X5)
% 2.20/2.43  (zenon_X14 != (a1294))
% 2.20/2.43  (zenon_X32 != zenon_X64)
% 2.20/2.43  ((a1282) != (a1330))
% 2.20/2.43  (c9_2 (a1241) (a1227))
% 2.20/2.43  (-. (c2_1 zenon_X17))
% 2.20/2.43  (zenon_X97 != (a1294))
% 2.20/2.43  (-. (c10_2 zenon_X35 (a1352)))
% 2.20/2.43  (c1_2 (a1215) (a1227))
% 2.20/2.43  (c2_2 (a1293) (a1326))
% 2.20/2.43  (zenon_X27 != (a1214))
% 2.20/2.43  (-. (c10_2 (a1241) (a1352)))
% 2.20/2.43  (c7_2 zenon_X35 (a1227))
% 2.20/2.43  (-. (c7_2 (a1223) (a1351)))
% 2.20/2.43  ((a1256) != zenon_X23)
% 2.20/2.43  (-. (c4_2 (a1346) (a1347)))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X65))
% 2.20/2.43  ((a1277) != zenon_X16)
% 2.20/2.43  (c6_2 (a1350) zenon_X58)
% 2.20/2.43  (-. (c5_2 (a1307) (a1300)))
% 2.20/2.43  (-. (c8_2 zenon_X30 (a1352)))
% 2.20/2.43  (c3_2 (a1350) zenon_X102)
% 2.20/2.43  (zenon_X31 != zenon_X53)
% 2.20/2.43  ((a1220) != zenon_X25)
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1352)))
% 2.20/2.43  (zenon_X14 != zenon_X102)
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X32))
% 2.20/2.43  (zenon_X63 != (a1364))
% 2.20/2.43  ((a1300) != zenon_X107)
% 2.20/2.43  (c5_2 (a1223) zenon_X54)
% 2.20/2.43  ((a1336) != zenon_X103)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X71))
% 2.20/2.43  ((a1346) != zenon_X25)
% 2.20/2.43  (c8_2 (a1223) (a1364))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X46))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X73))
% 2.20/2.43  ((a1287) != (a1241))
% 2.20/2.43  (c9_2 (a1293) (a1282))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X55)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X46))
% 2.20/2.43  (c9_2 zenon_X27 (a1308))
% 2.20/2.43  ((a1223) != zenon_X27)
% 2.20/2.43  (zenon_X32 != zenon_X107)
% 2.20/2.43  (-. (c9_2 (a1287) (a1302)))
% 2.20/2.43  (zenon_X16 != zenon_X107)
% 2.20/2.43  ((a1216) != zenon_X54)
% 2.20/2.43  (-. (c3_2 (a1307) (a1347)))
% 2.20/2.43  ((a1216) != (a1336))
% 2.20/2.43  ((a1256) != zenon_X63)
% 2.20/2.43  ((a1271) != zenon_X103)
% 2.20/2.43  (zenon_X32 != zenon_X53)
% 2.20/2.43  ((a1215) != (a1220))
% 2.20/2.43  (-. (c4_2 (a1270) zenon_X62))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X5))
% 2.20/2.43  (zenon_X55 != (a1246))
% 2.20/2.43  (-. (c10_2 (a1287) (a1352)))
% 2.20/2.43  (zenon_X39 != (a1307))
% 2.20/2.43  (c9_2 zenon_X18 (a1294))
% 2.20/2.43  (-. (c3_2 (a1307) (a1364)))
% 2.20/2.43  (zenon_X16 != (a1300))
% 2.20/2.43  (zenon_X14 != zenon_X73)
% 2.20/2.43  (zenon_X102 != (a1326))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X50))
% 2.20/2.43  (-. (c10_2 zenon_X25 (a1352)))
% 2.20/2.43  (c7_2 (a1293) zenon_X3)
% 2.20/2.43  (zenon_X97 != zenon_X65)
% 2.20/2.43  (zenon_X30 != (a1281))
% 2.20/2.43  ((a1294) != (a1326))
% 2.20/2.43  (c9_2 zenon_X30 (a1345))
% 2.20/2.43  (-. (c6_2 (a1346) (a1277)))
% 2.20/2.43  ((a1271) != (a1300))
% 2.20/2.43  ((a1271) != zenon_X82)
% 2.20/2.43  ((a1241) != (a1350))
% 2.20/2.43  (zenon_X39 != (a1241))
% 2.20/2.43  ((a1345) != zenon_X65)
% 2.20/2.43  (zenon_X8 != zenon_X25)
% 2.20/2.43  ((a1277) != (a1300))
% 2.20/2.43  (zenon_X55 != (a1256))
% 2.20/2.43  (zenon_X63 != (a1271))
% 2.20/2.43  ((a1223) != (a1226))
% 2.20/2.43  (-. (c6_2 (a1276) (a1256)))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X65))
% 2.20/2.43  ((a1246) != zenon_X104)
% 2.20/2.43  (zenon_X63 != zenon_X59)
% 2.20/2.43  (c6_2 (a1350) (a1300))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X103)
% 2.20/2.43  (zenon_X102 != zenon_X46)
% 2.20/2.43  (ndr1_1 (a1276))
% 2.20/2.43  (c3_2 (a1350) (a1227))
% 2.20/2.43  (c9_2 zenon_X27 (a1326))
% 2.20/2.43  (c9_2 (a1220) (a1347))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X5))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X65))
% 2.20/2.43  (c9_2 zenon_X27 (a1282))
% 2.20/2.43  (zenon_X60 != zenon_X31)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X32))
% 2.20/2.43  ((a1223) != (a1287))
% 2.20/2.43  ((a1294) != (a1256))
% 2.20/2.43  ((a1347) != zenon_X59)
% 2.20/2.43  (c9_2 (a1346) zenon_X102)
% 2.20/2.43  (-. (c10_2 zenon_X35 (a1294)))
% 2.20/2.43  ((a1308) != zenon_X34)
% 2.20/2.43  (c9_2 zenon_X30 (a1283))
% 2.20/2.43  (c6_2 (a1350) zenon_X55)
% 2.20/2.43  (c8_2 (a1223) (a1216))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1336)))
% 2.20/2.43  (c7_2 (a1346) (a1256))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X14))
% 2.20/2.43  (c3_2 (a1350) (a1283))
% 2.20/2.43  (c6_2 (a1350) zenon_X16)
% 2.20/2.43  (zenon_X42 != zenon_X97)
% 2.20/2.43  ((a1208) != (a1226))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X57))
% 2.20/2.43  (c5_2 (a1223) (a1351))
% 2.20/2.43  (zenon_X63 != (a1352))
% 2.20/2.43  (c9_2 (a1293) zenon_X107)
% 2.20/2.43  ((a1308) != zenon_X102)
% 2.20/2.43  (c6_2 (a1350) zenon_X46)
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X32))
% 2.20/2.43  ((a1246) != zenon_X5)
% 2.20/2.43  (c5_2 (a1363) (a1246))
% 2.20/2.43  ((a1282) != zenon_X20)
% 2.20/2.43  (c5_2 (a1223) zenon_X97)
% 2.20/2.43  ((a1294) != zenon_X52)
% 2.20/2.43  (c9_2 zenon_X27 (a1294))
% 2.20/2.43  ((a1363) != (a1270))
% 2.20/2.43  ((a1364) != zenon_X82)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X52))
% 2.20/2.43  ((a1227) != zenon_X63)
% 2.20/2.43  (zenon_X16 != (a1282))
% 2.20/2.43  (c6_2 (a1350) zenon_X50)
% 2.20/2.43  (c10_2 (a1293) (a1294))
% 2.20/2.43  (c7_2 (a1241) (a1277))
% 2.20/2.43  (c9_2 (a1255) zenon_X31)
% 2.20/2.43  (c9_2 (a1241) zenon_X107)
% 2.20/2.43  (c7_2 (a1270) zenon_X55)
% 2.20/2.43  (c7_2 (a1241) zenon_X3)
% 2.20/2.43  ((a1282) != (a1326))
% 2.20/2.43  (c9_2 (a1223) zenon_X14)
% 2.20/2.43  (c9_2 zenon_X8 (a1364))
% 2.20/2.43  (zenon_X42 != zenon_X71)
% 2.20/2.43  (-. (c9_1 (a1226)))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X5))
% 2.20/2.43  (zenon_X60 != zenon_X52)
% 2.20/2.43  (c9_2 zenon_X17 (a1364))
% 2.20/2.43  (c9_2 (a1220) (a1352))
% 2.20/2.43  (-. (c8_1 (a1220)))
% 2.20/2.43  (-. (c4_2 (a1281) (a1271)))
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X55))
% 2.20/2.43  ((a1246) != (a1216))
% 2.20/2.43  (c9_2 zenon_X30 (a1282))
% 2.20/2.43  ((a1283) != (a1227))
% 2.20/2.43  (-. (c10_2 (a1293) zenon_X56))
% 2.20/2.43  (zenon_X102 != (a1260))
% 2.20/2.43  (-. (c9_2 (a1208) (a1326)))
% 2.20/2.43  (zenon_X63 != zenon_X102)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X102))
% 2.20/2.43  (c5_2 (a1223) (a1300))
% 2.20/2.43  (c6_2 (a1350) zenon_X33)
% 2.20/2.43  (-. (c3_2 zenon_X19 (a1300)))
% 2.20/2.43  (c9_2 (a1223) (a1256))
% 2.20/2.43  ((a1271) != (a1347))
% 2.20/2.43  (c9_2 zenon_X27 (a1300))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X43))
% 2.20/2.43  (c7_2 (a1270) (a1246))
% 2.20/2.43  (zenon_X14 != (a1351))
% 2.20/2.43  (-. (c5_2 (a1223) zenon_X33))
% 2.20/2.43  (zenon_X73 != (a1260))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X50))
% 2.20/2.43  (zenon_X55 != zenon_X60)
% 2.20/2.43  ((a1308) != zenon_X82)
% 2.20/2.43  (-. (c3_2 zenon_X25 (a1246)))
% 2.20/2.43  (c6_2 (a1350) (a1282))
% 2.20/2.43  (-. (c1_2 zenon_X27 (a1246)))
% 2.20/2.43  (c9_2 zenon_X30 (a1364))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X31))
% 2.20/2.43  (zenon_X35 != (a1223))
% 2.20/2.43  (zenon_X31 != zenon_X71)
% 2.20/2.43  ((a1364) != (a1351))
% 2.20/2.43  (-. (c3_2 (a1307) (a1246)))
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X65))
% 2.20/2.43  ((a1277) != zenon_X58)
% 2.20/2.43  (zenon_X82 != zenon_X64)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X102))
% 2.20/2.43  (zenon_X35 != (a1350))
% 2.20/2.43  (zenon_X55 != zenon_X71)
% 2.20/2.43  ((a1271) != zenon_X46)
% 2.20/2.43  (-. (c3_2 (a1307) (a1282)))
% 2.20/2.43  (c7_2 (a1293) zenon_X97)
% 2.20/2.43  ((a1345) != zenon_X59)
% 2.20/2.43  (-. (c6_2 (a1226) (a1277)))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1282)))
% 2.20/2.43  (c7_2 (a1270) zenon_X16)
% 2.20/2.43  ((a1282) != zenon_X103)
% 2.20/2.43  (c8_2 (a1223) (a1256))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X55))
% 2.20/2.43  ((a1352) != zenon_X23)
% 2.20/2.43  (c8_2 (a1346) (a1352))
% 2.20/2.43  (zenon_X107 != (a1302))
% 2.20/2.43  ((a1347) != zenon_X32)
% 2.20/2.43  ((a1227) != zenon_X65)
% 2.20/2.43  (zenon_X60 != (a1364))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X49))
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X41))
% 2.20/2.43  ((a1300) != zenon_X68)
% 2.20/2.43  (-. (c4_2 zenon_X1 (a1283)))
% 2.20/2.43  (-. (c6_2 (a1226) (a1256)))
% 2.20/2.43  (c9_2 (a1241) zenon_X103)
% 2.20/2.43  (zenon_X38 != (a1208))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X3))
% 2.20/2.43  ((a1283) != zenon_X31)
% 2.20/2.43  (c9_2 (a1220) (a1256))
% 2.20/2.43  (zenon_X59 != zenon_X31)
% 2.20/2.43  (zenon_X8 != (a1293))
% 2.20/2.43  ((a1214) != zenon_X8)
% 2.20/2.43  ((a1351) != zenon_X91)
% 2.20/2.43  (c7_2 (a1293) (a1271))
% 2.20/2.43  ((a1271) != (a1260))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X55))
% 2.20/2.43  (c7_2 (a1255) (a1282))
% 2.20/2.43  (c7_2 (a1270) zenon_X5)
% 2.20/2.43  ((a1308) != (a1246))
% 2.20/2.43  ((a1351) != zenon_X105)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X73))
% 2.20/2.43  ((a1246) != zenon_X75)
% 2.20/2.43  ((a1300) != zenon_X104)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X46)
% 2.20/2.43  (zenon_X55 != (a1300))
% 2.20/2.43  ((a1227) != zenon_X97)
% 2.20/2.43  ((a1345) != zenon_X31)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X50)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X63))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X60))
% 2.20/2.43  ((a1271) != (a1227))
% 2.20/2.43  ((a1326) != (a1336))
% 2.20/2.43  (c1_2 (a1215) zenon_X71)
% 2.20/2.43  (zenon_X60 != zenon_X71)
% 2.20/2.43  (-. (c9_2 zenon_X35 (a1302)))
% 2.20/2.43  ((a1216) != zenon_X49)
% 2.20/2.43  (c10_1 (a1214))
% 2.20/2.43  (zenon_X33 != zenon_X63)
% 2.20/2.43  (-. (c10_1 (a1287)))
% 2.20/2.43  ((a1277) != (a1302))
% 2.20/2.43  ((a1363) != (a1214))
% 2.20/2.43  (-. (c6_2 (a1350) zenon_X57))
% 2.20/2.43  ((a1308) != zenon_X32)
% 2.20/2.43  (zenon_X81 != zenon_X32)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X60))
% 2.20/2.43  ((a1347) != zenon_X107)
% 2.20/2.43  (-. (c8_1 (a1208)))
% 2.20/2.43  ((a1277) != (a1227))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X60)
% 2.20/2.43  (-. (c6_2 (a1276) (a1216)))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X42))
% 2.20/2.43  (-. (c10_2 zenon_X35 zenon_X36))
% 2.20/2.43  (c9_2 (a1293) zenon_X102)
% 2.20/2.43  (-. (c8_2 (a1293) (a1282)))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X50))
% 2.20/2.43  (zenon_X103 != zenon_X49)
% 2.20/2.43  (c9_2 zenon_X39 (a1345))
% 2.20/2.43  (c9_2 zenon_X17 (a1300))
% 2.20/2.43  (zenon_X41 != zenon_X58)
% 2.20/2.43  (c2_1 (a1350))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X54))
% 2.20/2.43  (zenon_X59 != zenon_X107)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X82))
% 2.20/2.43  (c9_2 (a1363) (a1300))
% 2.20/2.43  (zenon_X14 != zenon_X43)
% 2.20/2.43  ((a1283) != zenon_X23)
% 2.20/2.43  ((a1300) != zenon_X49)
% 2.20/2.43  (zenon_X14 != (a1330))
% 2.20/2.43  ((a1300) != zenon_X57)
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1364)))
% 2.20/2.43  (c9_2 zenon_X38 (a1271))
% 2.20/2.43  (c9_2 zenon_X17 (a1308))
% 2.20/2.43  ((a1300) != zenon_X45)
% 2.20/2.43  (-. (c6_2 (a1346) (a1283)))
% 2.20/2.43  (c10_2 zenon_X8 (a1352))
% 2.20/2.43  (c3_2 (a1350) zenon_X58)
% 2.20/2.43  (c7_2 (a1220) zenon_X16)
% 2.20/2.43  (-. (c6_2 (a1226) (a1227)))
% 2.20/2.43  (zenon_X16 != (a1256))
% 2.20/2.43  ((a1293) != (a1307))
% 2.20/2.43  (zenon_X16 != zenon_X41)
% 2.20/2.43  (c7_2 (a1255) zenon_X82)
% 2.20/2.43  (c7_2 (a1346) (a1294))
% 2.20/2.43  (c1_1 (a1255))
% 2.20/2.43  ((a1363) != (a1281))
% 2.20/2.43  (c9_2 (a1270) (a1256))
% 2.20/2.43  (c9_2 (a1223) (a1283))
% 2.20/2.43  (c9_2 (a1241) zenon_X73)
% 2.20/2.43  (c10_2 zenon_X30 (a1352))
% 2.20/2.43  (c2_1 zenon_X35)
% 2.20/2.43  (c9_2 zenon_X25 (a1345))
% 2.20/2.43  ((a1347) != zenon_X64)
% 2.20/2.43  ((a1277) != zenon_X102)
% 2.20/2.43  ((a1308) != zenon_X71)
% 2.20/2.43  ((a1346) != zenon_X30)
% 2.20/2.43  (ndr1_1 (a1363))
% 2.20/2.43  (c6_2 (a1350) zenon_X43)
% 2.20/2.43  (c1_2 (a1215) (a1351))
% 2.20/2.43  ((a1241) != (a1363))
% 2.20/2.43  (zenon_X41 != zenon_X32)
% 2.20/2.43  (zenon_X97 != zenon_X43)
% 2.20/2.43  (c6_2 (a1350) zenon_X71)
% 2.20/2.43  ((a1277) != zenon_X55)
% 2.20/2.43  ((a1364) != zenon_X53)
% 2.20/2.43  ((a1351) != zenon_X87)
% 2.20/2.43  (-. (c2_1 zenon_X39))
% 2.20/2.43  ((a1255) != (a1270))
% 2.20/2.43  ((a1282) != zenon_X3)
% 2.20/2.43  (c10_1 (a1363))
% 2.20/2.43  (-. (c8_1 zenon_X30))
% 2.20/2.43  (-. (c5_2 (a1287) zenon_X67))
% 2.20/2.43  (c9_2 zenon_X8 (a1216))
% 2.20/2.43  ((a1255) != zenon_X35)
% 2.20/2.43  ((a1352) != (a1277))
% 2.20/2.43  (c7_2 (a1270) zenon_X60)
% 2.20/2.43  ((a1271) != zenon_X15)
% 2.20/2.43  (-. (c2_1 (a1215)))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X3))
% 2.20/2.43  (c9_2 zenon_X38 (a1352))
% 2.20/2.43  (zenon_X71 != (a1302))
% 2.20/2.43  (zenon_X31 != zenon_X5)
% 2.20/2.43  ((a1277) != zenon_X60)
% 2.20/2.43  ((a1336) != zenon_X71)
% 2.20/2.43  (c3_2 (a1350) zenon_X59)
% 2.20/2.43  (c7_2 (a1293) (a1282))
% 2.20/2.43  (-. (c3_1 (a1335)))
% 2.20/2.43  (c9_2 (a1270) (a1352))
% 2.20/2.43  (-. (c3_2 (a1208) (a1246)))
% 2.20/2.43  ((a1336) != zenon_X65)
% 2.20/2.43  ((a1227) != zenon_X31)
% 2.20/2.43  (-. (c6_0))
% 2.20/2.43  (c9_1 (a1270))
% 2.20/2.43  (c7_2 (a1255) (a1352))
% 2.20/2.43  (-. (c1_2 zenon_X8 (a1326)))
% 2.20/2.43  ((a1214) != (a1281))
% 2.20/2.43  ((a1208) != (a1287))
% 2.20/2.43  (-. (c8_1 (a1276)))
% 2.20/2.43  (-. (c5_2 (a1214) zenon_X34))
% 2.20/2.43  (c6_2 (a1350) zenon_X63)
% 2.20/2.43  (zenon_X63 != (a1283))
% 2.20/2.43  (-. (c1_1 zenon_X35))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X14))
% 2.20/2.43  (-. (c10_2 zenon_X27 (a1325)))
% 2.20/2.43  (-. (c9_2 (a1346) (a1326)))
% 2.20/2.43  (-. (c1_2 (a1287) (a1246)))
% 2.20/2.43  (zenon_X14 != zenon_X59)
% 2.20/2.43  ((a1270) != (a1350))
% 2.20/2.43  (c3_2 (a1350) zenon_X71)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X46))
% 2.20/2.43  (zenon_X50 != zenon_X57)
% 2.20/2.43  (-. (c7_2 (a1255) (a1256)))
% 2.20/2.43  (c7_2 (a1293) (a1227))
% 2.20/2.43  ((a1283) != (a1271))
% 2.20/2.43  (c9_2 (a1255) (a1364))
% 2.20/2.43  ((a1277) != zenon_X97)
% 2.20/2.43  (zenon_X3 != (a1256))
% 2.20/2.43  (-. (c10_2 (a1346) zenon_X4))
% 2.20/2.43  ((a1283) != (a1256))
% 2.20/2.43  ((a1347) != zenon_X71)
% 2.20/2.43  ((a1271) != zenon_X49)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X103))
% 2.20/2.43  (c6_2 (a1350) (a1336))
% 2.20/2.43  (ndr1_1 (a1223))
% 2.20/2.43  (c6_1 zenon_X11)
% 2.20/2.43  ((a1308) != zenon_X59)
% 2.20/2.43  (zenon_X73 != zenon_X49)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X60))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X97)
% 2.20/2.43  (-. (c10_2 (a1350) (a1351)))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X97))
% 2.20/2.43  (zenon_X46 != zenon_X57)
% 2.20/2.43  (zenon_X42 != zenon_X57)
% 2.20/2.43  (c7_2 (a1346) (a1352))
% 2.20/2.43  (zenon_X27 != zenon_X8)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X43))
% 2.20/2.43  (zenon_X103 != (a1326))
% 2.20/2.43  (zenon_X17 != zenon_X8)
% 2.20/2.43  (c9_2 zenon_X18 (a1283))
% 2.20/2.43  ((a1293) != (a1223))
% 2.20/2.43  (c9_2 zenon_X8 (a1300))
% 2.20/2.43  ((a1246) != zenon_X101)
% 2.20/2.43  ((a1216) != zenon_X73)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X63))
% 2.20/2.43  ((a1352) != zenon_X52)
% 2.20/2.43  ((a1216) != zenon_X59)
% 2.20/2.43  ((a1216) != (a1282))
% 2.20/2.43  ((a1300) != zenon_X53)
% 2.20/2.43  (c9_2 zenon_X38 (a1336))
% 2.20/2.43  (zenon_X14 != (a1246))
% 2.20/2.43  ((a1300) != zenon_X103)
% 2.20/2.43  (c9_2 (a1293) zenon_X31)
% 2.20/2.43  ((a1352) != zenon_X28)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X32))
% 2.20/2.43  (-. (c6_2 (a1350) zenon_X65))
% 2.20/2.43  (c9_2 (a1293) (a1347))
% 2.20/2.43  ((a1246) != zenon_X110)
% 2.20/2.43  (-. (c7_2 (a1270) (a1271)))
% 2.20/2.43  (-. (c1_2 (a1223) (a1326)))
% 2.20/2.43  (c9_2 (a1255) (a1282))
% 2.20/2.43  (c7_2 (a1270) zenon_X31)
% 2.20/2.43  (-. (c10_2 (a1241) (a1256)))
% 2.20/2.43  (c7_2 (a1220) (a1308))
% 2.20/2.43  (c7_2 (a1241) (a1246))
% 2.20/2.43  (c9_2 (a1293) (a1345))
% 2.20/2.43  ((a1241) != zenon_X17)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X46))
% 2.20/2.43  (c10_1 (a1255))
% 2.20/2.43  (-. (c1_2 (a1363) (a1326)))
% 2.20/2.43  (zenon_X33 != zenon_X82)
% 2.20/2.43  (c9_2 zenon_X30 (a1246))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X49)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X107)
% 2.20/2.43  (zenon_X103 != zenon_X3)
% 2.20/2.43  (c9_2 zenon_X18 (a1347))
% 2.20/2.43  (ndr1_0)
% 2.20/2.43  (-. (c8_1 (a1255)))
% 2.20/2.43  ((a1216) != (a1347))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X46))
% 2.20/2.43  (zenon_X82 != (a1326))
% 2.20/2.43  ((a1276) != (a1307))
% 2.20/2.43  (c6_2 (a1350) zenon_X59)
% 2.20/2.43  (zenon_X16 != zenon_X65)
% 2.20/2.43  ((a1227) != zenon_X5)
% 2.20/2.43  ((a1277) != zenon_X31)
% 2.20/2.43  (c9_2 (a1223) zenon_X82)
% 2.20/2.43  ((a1350) != zenon_X19)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X52))
% 2.20/2.43  (zenon_X8 != (a1255))
% 2.20/2.43  (zenon_X55 != zenon_X102)
% 2.20/2.43  ((a1271) != (a1256))
% 2.20/2.43  (-. (c10_1 (a1241)))
% 2.20/2.43  ((a1308) != (a1345))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X107))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X16)
% 2.20/2.43  (c3_2 (a1293) (a1294))
% 2.20/2.43  (c9_2 (a1270) zenon_X31)
% 2.20/2.43  (zenon_X71 != (a1326))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X43))
% 2.20/2.43  ((a1216) != zenon_X63)
% 2.20/2.43  (-. (c6_2 (a1287) (a1271)))
% 2.20/2.43  (zenon_X43 != (a1294))
% 2.20/2.43  (c9_2 (a1223) (a1351))
% 2.20/2.43  (c7_2 (a1220) zenon_X31)
% 2.20/2.43  (c8_2 (a1346) (a1256))
% 2.20/2.43  (-. (c3_2 (a1307) (a1256)))
% 2.20/2.43  ((a1300) != zenon_X23)
% 2.20/2.43  ((a1352) != zenon_X56)
% 2.20/2.43  (zenon_X102 != zenon_X65)
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X3))
% 2.20/2.43  (c2_2 (a1241) (a1326))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X64))
% 2.20/2.43  ((a1220) != zenon_X27)
% 2.20/2.43  (c7_2 (a1241) (a1256))
% 2.20/2.43  ((a1256) != (a1336))
% 2.20/2.43  ((a1271) != (a1326))
% 2.20/2.43  ((a1227) != (a1216))
% 2.20/2.43  (c7_2 (a1293) (a1308))
% 2.20/2.43  (zenon_X16 != zenon_X52)
% 2.20/2.43  (-. (c10_2 (a1270) (a1352)))
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X57))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X33))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X55))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X57))
% 2.20/2.43  ((a1345) != (a1300))
% 2.20/2.43  ((a1246) != zenon_X81)
% 2.20/2.43  (-. (c2_1 zenon_X18))
% 2.20/2.43  (c6_2 (a1350) (a1294))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X60))
% 2.20/2.43  (zenon_X14 != zenon_X32)
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X57))
% 2.20/2.43  (zenon_X49 != zenon_X65)
% 2.20/2.43  ((a1346) != (a1350))
% 2.20/2.43  (-. (c6_2 (a1226) (a1364)))
% 2.20/2.43  ((a1216) != zenon_X102)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X59))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X57))
% 2.20/2.43  ((a1277) != (a1325))
% 2.20/2.43  (c7_1 zenon_X9)
% 2.20/2.43  (-. (c9_2 zenon_X8 (a1302)))
% 2.20/2.43  (zenon_X102 != zenon_X5)
% 2.20/2.43  (c7_2 (a1293) (a1216))
% 2.20/2.43  (c3_2 (a1350) zenon_X107)
% 2.20/2.43  (zenon_X17 != (a1287))
% 2.20/2.43  (c7_1 zenon_X8)
% 2.20/2.43  (c9_2 zenon_X27 (a1347))
% 2.20/2.43  (zenon_X55 != zenon_X103)
% 2.20/2.43  (c7_2 (a1241) (a1227))
% 2.20/2.43  (ndr1_1 zenon_X25)
% 2.20/2.43  ((a1363) != zenon_X27)
% 2.20/2.43  ((a1346) != (a1276))
% 2.20/2.43  (-. (c7_2 (a1223) (a1345)))
% 2.20/2.43  (c5_2 (a1223) zenon_X60)
% 2.20/2.43  (c7_2 zenon_X35 (a1294))
% 2.20/2.43  (c6_2 (a1350) (a1345))
% 2.20/2.43  (c7_2 (a1270) zenon_X57)
% 2.20/2.43  ((a1220) != (a1350))
% 2.20/2.43  (zenon_X33 != (a1283))
% 2.20/2.43  (c1_2 (a1287) (a1271))
% 2.20/2.43  (c7_2 (a1220) (a1277))
% 2.20/2.43  (zenon_X53 != (a1271))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X73))
% 2.20/2.43  ((a1352) != zenon_X76)
% 2.20/2.43  ((a1308) != zenon_X63)
% 2.20/2.43  (c9_2 (a1270) zenon_X82)
% 2.20/2.43  (-. (c10_2 (a1287) zenon_X66))
% 2.20/2.43  ((a1347) != zenon_X23)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X5))
% 2.20/2.43  (c6_2 (a1350) (a1246))
% 2.20/2.43  ((a1300) != zenon_X34)
% 2.20/2.43  (zenon_X3 != (a1216))
% 2.20/2.43  ((a1346) != (a1307))
% 2.20/2.43  (c9_2 zenon_X27 (a1336))
% 2.20/2.43  (c9_2 (a1346) (a1364))
% 2.20/2.43  (-. (c5_2 (a1354) zenon_X75))
% 2.20/2.43  (c9_2 zenon_X17 (a1326))
% 2.20/2.43  (zenon_X35 != zenon_X27)
% 2.20/2.43  (zenon_X17 != zenon_X25)
% 2.20/2.43  (-. (c9_2 (a1363) (a1326)))
% 2.20/2.43  (c9_2 (a1241) (a1364))
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X55))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X63))
% 2.20/2.43  (zenon_X16 != zenon_X54)
% 2.20/2.43  (zenon_X3 != zenon_X55)
% 2.20/2.43  ((a1354) != (a1241))
% 2.20/2.43  ((a1277) != (a1283))
% 2.20/2.43  (c9_2 (a1346) (a1271))
% 2.20/2.43  (zenon_X14 != zenon_X107)
% 2.20/2.43  (zenon_X97 != (a1282))
% 2.20/2.43  ((a1271) != zenon_X64)
% 2.20/2.43  (c9_2 (a1346) (a1277))
% 2.20/2.43  (c1_2 (a1215) zenon_X82)
% 2.20/2.43  ((a1246) != zenon_X59)
% 2.20/2.43  (zenon_X5 != zenon_X3)
% 2.20/2.43  ((a1347) != (a1260))
% 2.20/2.43  ((a1241) != zenon_X30)
% 2.20/2.43  (c9_2 (a1281) (a1300))
% 2.20/2.43  ((a1308) != zenon_X46)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X63))
% 2.20/2.43  ((a1294) != zenon_X57)
% 2.20/2.43  ((a1307) != (a1214))
% 2.20/2.43  ((a1220) != zenon_X18)
% 2.20/2.43  (zenon_X42 != zenon_X60)
% 2.20/2.43  (c9_2 (a1223) (a1347))
% 2.20/2.43  (c7_2 (a1241) (a1216))
% 2.20/2.43  (-. (c6_2 (a1346) (a1308)))
% 2.20/2.43  (c9_2 (a1346) zenon_X71)
% 2.20/2.43  ((a1277) != (a1345))
% 2.20/2.43  ((a1246) != zenon_X68)
% 2.20/2.43  (c9_2 (a1346) (a1282))
% 2.20/2.43  (c9_2 (a1293) (a1294))
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X50))
% 2.20/2.43  ((a1277) != zenon_X46)
% 2.20/2.43  (c6_2 (a1350) zenon_X82)
% 2.20/2.43  ((a1347) != (a1282))
% 2.20/2.43  ((a1308) != zenon_X64)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X55))
% 2.20/2.43  ((a1294) != zenon_X71)
% 2.20/2.43  ((a1215) != (a1208))
% 2.20/2.43  (zenon_X14 != (a1364))
% 2.20/2.43  (c9_2 (a1293) (a1352))
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X42))
% 2.20/2.43  (zenon_X60 != zenon_X107)
% 2.20/2.43  (c9_2 zenon_X17 (a1260))
% 2.20/2.43  (-. (c1_2 (a1208) (a1302)))
% 2.20/2.43  (zenon_X103 != zenon_X57)
% 2.20/2.43  ((a1256) != zenon_X64)
% 2.20/2.43  (-. (c10_1 (a1346)))
% 2.20/2.43  (c3_1 (a1354))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X60))
% 2.20/2.43  (c5_2 (a1223) (a1336))
% 2.20/2.43  ((a1227) != zenon_X41)
% 2.20/2.43  (c3_2 (a1350) zenon_X97)
% 2.20/2.43  (-. (c1_2 (a1354) (a1326)))
% 2.20/2.43  (c6_2 (a1350) zenon_X97)
% 2.20/2.43  (zenon_X42 != (a1283))
% 2.20/2.43  (-. (c8_2 (a1363) (a1352)))
% 2.20/2.43  (zenon_X73 != zenon_X31)
% 2.20/2.43  (c9_2 (a1293) (a1227))
% 2.20/2.43  (zenon_X19 != (a1287))
% 2.20/2.43  ((a1260) != (a1326))
% 2.20/2.43  ((a1281) != (a1287))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X58))
% 2.20/2.43  ((a1282) != (a1260))
% 2.20/2.43  (zenon_X97 != zenon_X103)
% 2.20/2.43  (c7_2 (a1270) zenon_X32)
% 2.20/2.43  (zenon_X33 != (a1282))
% 2.20/2.43  (zenon_X71 != zenon_X49)
% 2.20/2.43  (c7_2 (a1270) zenon_X97)
% 2.20/2.43  (-. (c1_1 zenon_X38))
% 2.20/2.43  (c9_2 (a1255) (a1345))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X58))
% 2.20/2.43  ((a1350) != (a1226))
% 2.20/2.43  (ndr1_1 zenon_X39)
% 2.20/2.43  (c9_2 (a1220) (a1364))
% 2.20/2.43  (zenon_X73 != (a1282))
% 2.20/2.43  (-. (c2_2 (a1281) (a1352)))
% 2.20/2.43  (-. (c5_2 (a1214) (a1308)))
% 2.20/2.43  ((a1277) != zenon_X107)
% 2.20/2.43  (c9_2 (a1270) (a1246))
% 2.20/2.43  (-. (c2_2 zenon_X7 (a1330)))
% 2.20/2.43  ((a1246) != zenon_X41)
% 2.20/2.43  (c9_2 zenon_X8 (a1294))
% 2.20/2.43  (c7_2 (a1293) zenon_X42)
% 2.20/2.43  (zenon_X82 != zenon_X52)
% 2.20/2.43  (c9_1 (a1208))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X81))
% 2.20/2.43  (c9_2 (a1255) (a1277))
% 2.20/2.43  (c5_2 (a1223) zenon_X49)
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X65))
% 2.20/2.43  (zenon_X103 != zenon_X54)
% 2.20/2.43  (zenon_X82 != zenon_X65)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X102)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X5))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1227)))
% 2.20/2.43  (c2_2 (a1215) (a1216))
% 2.20/2.43  ((a1294) != zenon_X0)
% 2.20/2.43  ((a1256) != (a1227))
% 2.20/2.43  (c7_2 (a1346) zenon_X102)
% 2.20/2.43  (c7_2 (a1293) zenon_X82)
% 2.20/2.43  (zenon_X8 != zenon_X35)
% 2.20/2.43  ((a1220) != (a1270))
% 2.20/2.43  ((a1364) != (a1326))
% 2.20/2.43  (c7_2 (a1293) zenon_X55)
% 2.20/2.43  ((a1364) != (a1260))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X43))
% 2.20/2.43  ((a1255) != (a1346))
% 2.20/2.43  ((a1277) != zenon_X82)
% 2.20/2.43  (-. (c1_1 zenon_X27))
% 2.20/2.43  (-. (c5_2 (a1220) zenon_X64))
% 2.20/2.43  ((a1277) != zenon_X73)
% 2.20/2.43  (zenon_X55 != zenon_X46)
% 2.20/2.43  (zenon_X14 != (a1282))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X3)
% 2.20/2.43  (c4_2 (a1270) (a1271))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X97))
% 2.20/2.43  (c9_2 (a1220) (a1277))
% 2.20/2.43  (ndr1_1 (a1281))
% 2.20/2.43  (zenon_X33 != zenon_X41)
% 2.20/2.43  (c9_2 (a1293) (a1246))
% 2.20/2.43  (c2_2 (a1270) (a1326))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X14))
% 2.20/2.43  ((a1256) != zenon_X65)
% 2.20/2.43  (zenon_X16 != zenon_X63)
% 2.20/2.43  (-. (c5_2 (a1307) (a1282)))
% 2.20/2.43  (c9_2 (a1220) (a1216))
% 2.20/2.43  (c7_2 (a1270) (a1300))
% 2.20/2.43  (zenon_X18 != zenon_X8)
% 2.20/2.43  (zenon_X14 != (a1336))
% 2.20/2.43  (zenon_X14 != (a1260))
% 2.20/2.43  ((a1256) != zenon_X107)
% 2.20/2.43  (zenon_X42 != (a1351))
% 2.20/2.43  ((a1271) != zenon_X52)
% 2.20/2.43  (c7_2 (a1350) zenon_X42)
% 2.20/2.43  (c9_2 (a1293) zenon_X82)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X81))
% 2.20/2.43  (c7_2 (a1270) (a1277))
% 2.20/2.43  ((a1293) != (a1208))
% 2.20/2.43  (-. (c5_2 zenon_X35 zenon_X101))
% 2.20/2.43  ((a1287) != (a1214))
% 2.20/2.43  ((a1256) != zenon_X43)
% 2.20/2.43  ((a1276) != (a1226))
% 2.20/2.43  (zenon_X102 != zenon_X3)
% 2.20/2.43  (c6_2 (a1350) zenon_X103)
% 2.20/2.43  (zenon_X42 != zenon_X63)
% 2.20/2.43  (c7_2 (a1241) zenon_X31)
% 2.20/2.43  (c9_2 (a1270) (a1282))
% 2.20/2.43  ((a1227) != zenon_X107)
% 2.20/2.43  ((a1283) != (a1302))
% 2.20/2.43  (zenon_X30 != (a1363))
% 2.20/2.43  (zenon_X14 != zenon_X71)
% 2.20/2.43  ((a1347) != zenon_X55)
% 2.20/2.43  ((a1294) != zenon_X107)
% 2.20/2.43  (c1_2 (a1215) (a1308))
% 2.20/2.43  (c7_2 (a1241) zenon_X103)
% 2.20/2.43  ((a1246) != zenon_X15)
% 2.20/2.43  (-. (c5_2 (a1241) zenon_X54))
% 2.20/2.43  ((a1220) != (a1287))
% 2.20/2.43  (zenon_X39 != (a1208))
% 2.20/2.43  ((a1308) != (a1302))
% 2.20/2.43  (c9_2 (a1293) (a1271))
% 2.20/2.43  ((a1364) != (a1330))
% 2.20/2.43  ((a1277) != (a1282))
% 2.20/2.43  (ndr1_1 zenon_X18)
% 2.20/2.43  ((a1220) != (a1281))
% 2.20/2.43  (zenon_X58 != zenon_X65)
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X65))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X42))
% 2.20/2.43  ((a1347) != zenon_X16)
% 2.20/2.43  (zenon_X97 != zenon_X41)
% 2.20/2.43  (c3_2 (a1287) (a1351))
% 2.20/2.43  (zenon_X17 != zenon_X27)
% 2.20/2.43  (-. (c6_2 (a1226) (a1347)))
% 2.20/2.43  (zenon_X43 != zenon_X32)
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X46))
% 2.20/2.43  ((a1276) != (a1293))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X107))
% 2.20/2.43  (c9_2 (a1223) (a1364))
% 2.20/2.43  (-. (c3_2 (a1215) (a1216)))
% 2.20/2.43  (c7_2 (a1220) (a1256))
% 2.20/2.43  (c7_2 (a1241) zenon_X82)
% 2.20/2.43  (zenon_X3 != zenon_X32)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X102))
% 2.20/2.43  ((a1223) != (a1307))
% 2.20/2.43  (-. (c7_2 (a1223) (a1336)))
% 2.20/2.43  (-. (c5_2 (a1223) zenon_X3))
% 2.20/2.43  (zenon_X35 != zenon_X30)
% 2.20/2.43  (c7_2 (a1270) zenon_X71)
% 2.20/2.43  (c7_2 (a1270) zenon_X58)
% 2.20/2.43  (zenon_X55 != zenon_X5)
% 2.20/2.43  (c9_2 (a1363) (a1345))
% 2.20/2.43  ((a1351) != (a1352))
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X33))
% 2.20/2.43  ((a1347) != (a1294))
% 2.20/2.43  ((a1364) != (a1352))
% 2.20/2.43  ((a1215) != (a1287))
% 2.20/2.43  (-. (c3_2 (a1307) (a1351)))
% 2.20/2.43  (c3_2 (a1350) (a1351))
% 2.20/2.43  (-. (c1_2 zenon_X39 (a1302)))
% 2.20/2.43  (c9_2 zenon_X17 (a1271))
% 2.20/2.43  (c7_2 (a1293) zenon_X102)
% 2.20/2.43  ((a1255) != (a1281))
% 2.20/2.43  (c5_2 (a1223) zenon_X59)
% 2.20/2.43  (-. (c1_1 (a1346)))
% 2.20/2.43  ((a1283) != zenon_X71)
% 2.20/2.43  (c9_2 zenon_X8 (a1227))
% 2.20/2.43  ((a1216) != zenon_X33)
% 2.20/2.43  (c9_2 (a1223) (a1216))
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X43))
% 2.20/2.43  (c9_2 zenon_X38 (a1256))
% 2.20/2.43  ((a1208) != (a1350))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X59))
% 2.20/2.43  ((a1293) != (a1215))
% 2.20/2.43  (-. (c5_2 zenon_X25 zenon_X110))
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1277)))
% 2.20/2.43  ((a1277) != zenon_X103)
% 2.20/2.43  ((a1294) != (a1330))
% 2.20/2.43  (c7_2 (a1293) (a1364))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X5))
% 2.20/2.43  ((a1270) != (a1307))
% 2.20/2.43  ((a1308) != (a1227))
% 2.20/2.43  (c7_2 (a1220) zenon_X65)
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X54))
% 2.20/2.43  (zenon_X50 != zenon_X3)
% 2.20/2.43  ((a1223) != (a1215))
% 2.20/2.43  (zenon_X55 != zenon_X43)
% 2.20/2.43  (c9_2 zenon_X38 (a1260))
% 2.20/2.43  (c9_2 (a1281) (a1216))
% 2.20/2.43  (c6_2 (a1350) zenon_X81)
% 2.20/2.43  (c5_2 (a1223) zenon_X52)
% 2.20/2.43  (-. (c2_2 zenon_X39 (a1352)))
% 2.20/2.43  ((a1277) != (a1330))
% 2.20/2.43  (zenon_X55 != (a1283))
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X5))
% 2.20/2.43  ((a1271) != zenon_X5)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X64))
% 2.20/2.43  ((a1364) != zenon_X50)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X32))
% 2.20/2.43  ((a1281) != zenon_X27)
% 2.20/2.43  (c9_2 zenon_X18 (a1336))
% 2.20/2.43  (zenon_X41 != zenon_X65)
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X16))
% 2.20/2.43  ((a1347) != zenon_X49)
% 2.20/2.43  ((a1345) != (a1302))
% 2.20/2.43  (c3_2 (a1350) zenon_X103)
% 2.20/2.43  (zenon_X103 != zenon_X65)
% 2.20/2.43  ((a1347) != zenon_X43)
% 2.20/2.43  (ndr1_1 (a1215))
% 2.20/2.43  ((a1352) != zenon_X65)
% 2.20/2.43  (-. (c5_2 (a1363) zenon_X45))
% 2.20/2.43  ((a1294) != zenon_X103)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X65)
% 2.20/2.43  (zenon_X25 != (a1214))
% 2.20/2.43  (zenon_X8 != (a1350))
% 2.20/2.43  (c7_2 (a1293) zenon_X60)
% 2.20/2.43  (c7_2 (a1255) zenon_X81)
% 2.20/2.43  ((a1308) != zenon_X65)
% 2.20/2.43  (zenon_X17 != zenon_X18)
% 2.20/2.43  (c8_2 (a1276) (a1277))
% 2.20/2.43  (-. (c1_2 (a1346) (a1302)))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X49))
% 2.20/2.43  (zenon_X102 != zenon_X54)
% 2.20/2.43  (zenon_X59 != zenon_X82)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X97))
% 2.20/2.43  (c5_2 (a1287) (a1246))
% 2.20/2.43  ((a1283) != (a1246))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X52))
% 2.20/2.43  ((a1294) != zenon_X80)
% 2.20/2.43  ((a1346) != (a1293))
% 2.20/2.43  (c8_2 (a1223) zenon_X14)
% 2.20/2.43  (c9_2 (a1220) zenon_X14)
% 2.20/2.43  (c6_2 (a1350) zenon_X64)
% 2.20/2.43  (zenon_X30 != zenon_X39)
% 2.20/2.43  (-. (c2_1 (a1214)))
% 2.20/2.43  (c9_2 (a1208) (a1300))
% 2.20/2.43  (zenon_X60 != zenon_X3)
% 2.20/2.43  (zenon_X5 != zenon_X57)
% 2.20/2.43  (zenon_X59 != (a1352))
% 2.20/2.43  (c6_2 (a1350) zenon_X49)
% 2.20/2.43  ((a1246) != zenon_X45)
% 2.20/2.43  (zenon_X16 != zenon_X97)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X16))
% 2.20/2.43  ((a1227) != zenon_X32)
% 2.20/2.43  (c9_2 zenon_X17 (a1216))
% 2.20/2.43  (c2_2 (a1350) (a1326))
% 2.20/2.43  ((a1214) != (a1270))
% 2.20/2.43  (zenon_X16 != zenon_X71)
% 2.20/2.43  (-. (c10_2 (a1255) zenon_X80))
% 2.20/2.43  (-. (c10_2 zenon_X27 zenon_X100))
% 2.20/2.43  ((a1347) != zenon_X63)
% 2.20/2.43  (-. (c5_2 zenon_X17 zenon_X52))
% 2.20/2.43  (-. (c8_2 (a1241) zenon_X28))
% 2.20/2.43  (c7_2 (a1346) zenon_X31)
% 2.20/2.43  (c7_2 zenon_X35 (a1352))
% 2.20/2.43  (c7_2 (a1255) zenon_X31)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X82))
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X3))
% 2.20/2.43  (c9_2 (a1255) (a1216))
% 2.20/2.43  (c9_2 zenon_X17 (a1256))
% 2.20/2.43  (c9_2 (a1255) (a1271))
% 2.20/2.43  (-. (c4_1 zenon_X38))
% 2.20/2.43  ((a1277) != zenon_X23)
% 2.20/2.43  (c7_2 zenon_X35 (a1277))
% 2.20/2.43  (c9_2 (a1281) (a1256))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X54))
% 2.20/2.43  ((a1294) != (a1302))
% 2.20/2.43  (zenon_X33 != zenon_X102)
% 2.20/2.43  (zenon_X42 != zenon_X53)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X71))
% 2.20/2.43  ((a1270) != (a1223))
% 2.20/2.43  (zenon_X14 != zenon_X103)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X50))
% 2.20/2.43  ((a1364) != (a1294))
% 2.20/2.43  (c7_2 (a1223) (a1256))
% 2.20/2.43  (-. (c2_1 (a1363)))
% 2.20/2.43  (c5_2 (a1223) zenon_X46)
% 2.20/2.43  (zenon_X42 != zenon_X107)
% 2.20/2.43  (c9_2 zenon_X18 (a1326))
% 2.20/2.43  ((a1256) != zenon_X5)
% 2.20/2.43  (-. (c6_2 zenon_X13 (a1308)))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X49))
% 2.20/2.43  ((a1227) != zenon_X46)
% 2.20/2.43  (c9_2 (a1346) zenon_X82)
% 2.20/2.43  (c9_2 (a1223) (a1308))
% 2.20/2.43  (c3_1 zenon_X6)
% 2.20/2.43  (-. (c7_2 (a1223) (a1282)))
% 2.20/2.43  ((a1270) != (a1354))
% 2.20/2.43  (c9_2 zenon_X30 (a1256))
% 2.20/2.43  (-. (c8_2 (a1281) (a1352)))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X14))
% 2.20/2.43  (-. (c4_2 (a1307) (a1308)))
% 2.20/2.43  (zenon_X39 != (a1287))
% 2.20/2.43  (c9_2 zenon_X38 (a1282))
% 2.20/2.43  (zenon_X102 != zenon_X52)
% 2.20/2.43  ((a1283) != zenon_X5)
% 2.20/2.43  (zenon_X81 != (a1256))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X57))
% 2.20/2.43  (zenon_X43 != zenon_X71)
% 2.20/2.43  (zenon_X59 != zenon_X65)
% 2.20/2.43  ((a1214) != (a1354))
% 2.20/2.43  (c3_2 (a1350) (a1294))
% 2.20/2.43  (-. (c4_2 zenon_X1 (a1271)))
% 2.20/2.43  ((a1352) != zenon_X0)
% 2.20/2.43  (c7_2 zenon_X35 (a1345))
% 2.20/2.43  ((a1216) != (a1256))
% 2.20/2.43  (c9_2 zenon_X35 (a1246))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X32))
% 2.20/2.43  (zenon_X102 != zenon_X57)
% 2.20/2.43  (c9_2 (a1270) (a1364))
% 2.20/2.43  (zenon_X82 != zenon_X46)
% 2.20/2.43  (zenon_X30 != zenon_X38)
% 2.20/2.43  (zenon_X73 != (a1308))
% 2.20/2.43  (c1_2 (a1287) (a1283))
% 2.20/2.43  ((a1287) != (a1307))
% 2.20/2.43  ((a1282) != zenon_X57)
% 2.20/2.43  (c9_2 (a1346) zenon_X14)
% 2.20/2.43  (c9_2 (a1255) zenon_X82)
% 2.20/2.43  ((a1220) != (a1241))
% 2.20/2.43  ((a1345) != zenon_X45)
% 2.20/2.43  (zenon_X18 != (a1287))
% 2.20/2.43  ((a1308) != zenon_X5)
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X53))
% 2.20/2.43  ((a1256) != (a1326))
% 2.20/2.43  (ndr1_1 (a1208))
% 2.20/2.43  (c7_2 (a1293) (a1352))
% 2.20/2.43  (zenon_X3 != (a1347))
% 2.20/2.43  (c9_2 (a1255) (a1308))
% 2.20/2.43  ((a1227) != zenon_X43)
% 2.20/2.43  (-. (c2_1 (a1281)))
% 2.20/2.43  (c7_1 (a1223))
% 2.20/2.43  (c2_2 (a1255) (a1326))
% 2.20/2.43  ((a1281) != zenon_X39)
% 2.20/2.43  (-. (c1_2 (a1346) (a1326)))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X16))
% 2.20/2.43  (ndr1_1 zenon_X17)
% 2.20/2.43  (c9_2 zenon_X18 (a1277))
% 2.20/2.43  (c6_2 (a1350) (a1227))
% 2.20/2.43  (c7_2 (a1255) zenon_X14)
% 2.20/2.43  ((a1216) != zenon_X57)
% 2.20/2.43  (zenon_X97 != (a1308))
% 2.20/2.43  ((a1216) != zenon_X97)
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X50))
% 2.20/2.43  ((a1326) != (a1302))
% 2.20/2.43  ((a1282) != zenon_X28)
% 2.20/2.43  (zenon_X82 != zenon_X57)
% 2.20/2.43  (c6_2 (a1276) (a1277))
% 2.20/2.43  (c9_2 zenon_X27 (a1271))
% 2.20/2.43  (c7_2 (a1346) (a1246))
% 2.20/2.43  (c6_2 (a1350) zenon_X14)
% 2.20/2.43  (zenon_X33 != (a1345))
% 2.20/2.43  (c7_2 (a1220) zenon_X57)
% 2.20/2.43  ((a1256) != zenon_X36)
% 2.20/2.43  ((a1300) != zenon_X64)
% 2.20/2.43  ((a1345) != (a1294))
% 2.20/2.43  (c3_2 (a1350) zenon_X50)
% 2.20/2.43  (zenon_X39 != (a1354))
% 2.20/2.43  (-. (c8_2 zenon_X27 (a1325)))
% 2.20/2.43  (c7_2 (a1220) zenon_X14)
% 2.20/2.43  (c7_2 zenon_X35 (a1302))
% 2.20/2.43  ((a1363) != (a1354))
% 2.20/2.43  (zenon_X81 != (a1352))
% 2.20/2.43  (c5_2 (a1223) zenon_X64)
% 2.20/2.43  (zenon_X54 != zenon_X3)
% 2.20/2.43  ((a1336) != (a1260))
% 2.20/2.43  ((a1246) != zenon_X32)
% 2.20/2.43  ((a1364) != zenon_X5)
% 2.20/2.43  (c6_2 (a1350) zenon_X54)
% 2.20/2.43  ((a1227) != zenon_X60)
% 2.20/2.43  ((a1345) != (a1227))
% 2.20/2.43  (zenon_X81 != zenon_X102)
% 2.20/2.43  (c7_2 (a1241) (a1294))
% 2.20/2.43  (c7_2 (a1293) zenon_X103)
% 2.20/2.43  (c9_2 (a1241) (a1308))
% 2.20/2.43  (c9_2 zenon_X38 (a1364))
% 2.20/2.43  (-. (c10_2 (a1276) (a1277)))
% 2.20/2.43  ((a1308) != (a1282))
% 2.20/2.43  ((a1277) != (a1347))
% 2.20/2.43  (zenon_X55 != zenon_X53)
% 2.20/2.43  ((a1346) != (a1215))
% 2.20/2.43  (c10_2 (a1214) (a1352))
% 2.20/2.43  ((a1364) != (a1282))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X107))
% 2.20/2.43  (c3_2 (a1350) zenon_X41)
% 2.20/2.43  (zenon_X31 != zenon_X49)
% 2.20/2.43  (-. (c5_2 (a1307) zenon_X15))
% 2.20/2.43  (zenon_X82 != zenon_X71)
% 2.20/2.43  ((a1345) != zenon_X57)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X63)
% 2.20/2.43  (c9_2 (a1241) (a1347))
% 2.20/2.43  ((a1276) != zenon_X13)
% 2.20/2.43  (c3_2 (a1350) (a1277))
% 2.20/2.43  (-. (c3_2 (a1354) (a1246)))
% 2.20/2.43  ((a1283) != (a1364))
% 2.20/2.43  (zenon_X38 != zenon_X39)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X81))
% 2.20/2.43  ((a1354) != zenon_X25)
% 2.20/2.43  (zenon_X30 != zenon_X18)
% 2.20/2.43  (zenon_X81 != zenon_X73)
% 2.20/2.43  (zenon_X49 != zenon_X57)
% 2.20/2.43  (c9_2 (a1346) (a1294))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X63))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X81))
% 2.20/2.43  (c7_2 zenon_X35 (a1271))
% 2.20/2.43  (-. (c1_2 zenon_X35 (a1326)))
% 2.20/2.43  ((a1308) != zenon_X54)
% 2.20/2.43  (zenon_X8 != zenon_X39)
% 2.20/2.43  (-. (c1_2 (a1287) (a1282)))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X81))
% 2.20/2.43  (zenon_X73 != zenon_X65)
% 2.20/2.43  ((a1294) != zenon_X65)
% 2.20/2.43  (c10_1 (a1208))
% 2.20/2.43  ((a1282) != zenon_X54)
% 2.20/2.43  (-. (c7_1 (a1354)))
% 2.20/2.43  (c3_2 (a1350) zenon_X5)
% 2.20/2.43  (c10_2 (a1307) (a1352))
% 2.20/2.43  (zenon_X14 != (a1256))
% 2.20/2.43  (c7_1 (a1269))
% 2.20/2.43  (zenon_X14 != zenon_X57)
% 2.20/2.43  (ndr1_1 (a1214))
% 2.20/2.43  ((a1336) != (a1302))
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X82))
% 2.20/2.43  (zenon_X33 != (a1336))
% 2.20/2.43  (-. (c4_1 (a1269)))
% 2.20/2.43  (zenon_X81 != zenon_X31)
% 2.20/2.43  (c9_2 (a1223) (a1336))
% 2.20/2.43  (zenon_X3 != zenon_X14)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X57))
% 2.20/2.43  ((a1270) != zenon_X17)
% 2.20/2.43  (c2_1 (a1241))
% 2.20/2.43  (zenon_X16 != zenon_X82)
% 2.20/2.43  (zenon_X82 != zenon_X49)
% 2.20/2.43  (zenon_X33 != zenon_X31)
% 2.20/2.43  (-. (c5_2 (a1293) zenon_X16))
% 2.20/2.43  ((a1256) != zenon_X50)
% 2.20/2.43  ((a1345) != zenon_X68)
% 2.20/2.43  (c7_2 zenon_X35 (a1347))
% 2.20/2.43  (c3_2 (a1350) zenon_X64)
% 2.20/2.43  (c7_2 (a1346) (a1308))
% 2.20/2.43  (-. (c5_2 zenon_X30 zenon_X3))
% 2.20/2.43  (zenon_X8 != (a1208))
% 2.20/2.43  ((a1271) != zenon_X50)
% 2.20/2.43  (ndr1_1 (a1241))
% 2.20/2.43  (c9_2 zenon_X38 (a1277))
% 2.20/2.43  (c5_2 (a1223) zenon_X81)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X49))
% 2.20/2.43  ((a1277) != zenon_X53)
% 2.20/2.43  (c9_2 zenon_X30 (a1300))
% 2.20/2.43  ((a1352) != (a1271))
% 2.20/2.43  ((a1256) != zenon_X28)
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X60))
% 2.20/2.43  (c3_2 (a1350) (a1336))
% 2.20/2.43  ((a1300) != zenon_X58)
% 2.20/2.43  ((a1270) != (a1293))
% 2.20/2.43  (c2_2 (a1363) (a1326))
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X55))
% 2.20/2.43  (c7_2 (a1270) (a1294))
% 2.20/2.43  (zenon_X73 != zenon_X71)
% 2.20/2.43  (c9_2 zenon_X38 (a1308))
% 2.20/2.43  ((a1294) != (a1227))
% 2.20/2.43  (-. (c10_2 (a1350) (a1352)))
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X42))
% 2.20/2.43  (-. (c5_2 (a1346) zenon_X97))
% 2.20/2.43  (c9_2 (a1255) zenon_X14)
% 2.20/2.43  (c9_2 (a1270) (a1300))
% 2.20/2.43  (zenon_X107 != zenon_X46)
% 2.20/2.43  ((a1336) != (a1330))
% 2.20/2.43  (c7_2 zenon_X35 zenon_X52)
% 2.20/2.43  (zenon_X16 != zenon_X58)
% 2.20/2.43  (c7_2 (a1270) (a1352))
% 2.20/2.43  (-. (c5_2 (a1281) zenon_X65))
% 2.20/2.43  (-. (c6_2 (a1346) zenon_X3))
% 2.20/2.43  (zenon_X42 != (a1364))
% 2.20/2.43  ((a1256) != (a1352))
% 2.20/2.43  (c9_2 (a1346) (a1345))
% 2.20/2.43  ((a1283) != (a1282))
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X32))
% 2.20/2.43  (-. (c8_2 zenon_X7 (a1330)))
% 2.20/2.43  (zenon_X81 != zenon_X82)
% 2.20/2.43  (-. (c5_2 zenon_X18 zenon_X32))
% 2.20/2.43  ((a1345) != zenon_X49)
% 2.20/2.43  (zenon_X41 != zenon_X57)
% 2.20/2.43  (c7_2 zenon_X35 zenon_X33)
% 2.20/2.43  ((a1208) != (a1223))
% 2.20/2.43  ((a1282) != zenon_X107)
% 2.20/2.43  (zenon_X103 != (a1260))
% 2.20/2.43  ((a1271) != zenon_X107)
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X14))
% 2.20/2.43  (-. (c1_2 (a1287) (a1294)))
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X42))
% 2.20/2.43  (c9_2 (a1281) (a1364))
% 2.20/2.43  ((a1255) != (a1215))
% 2.20/2.43  ((a1352) != zenon_X91)
% 2.20/2.43  ((a1352) != zenon_X16)
% 2.20/2.43  ((a1352) != zenon_X66)
% 2.20/2.43  ((a1351) != zenon_X93)
% 2.20/2.43  (zenon_X59 != zenon_X5)
% 2.20/2.43  ((a1345) != zenon_X101)
% 2.20/2.43  (-. (c5_2 zenon_X38 zenon_X42))
% 2.20/2.43  ((a1271) != zenon_X65)
% 2.20/2.43  (-. (c10_1 zenon_X27))
% 2.20/2.43  (c2_1 (a1270))
% 2.20/2.43  (zenon_X73 != zenon_X3)
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X52))
% 2.20/2.43  (ndr1_1 zenon_X35)
% 2.20/2.43  (c6_2 (a1350) zenon_X60)
% 2.20/2.43  ((a1293) != zenon_X17)
% 2.20/2.43  (zenon_X33 != zenon_X65)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X16))
% 2.20/2.43  ((a1270) != zenon_X38)
% 2.20/2.43  (c5_2 (a1223) zenon_X107)
% 2.20/2.43  (c9_2 (a1346) (a1256))
% 2.20/2.43  (-. (c10_2 (a1293) (a1352)))
% 2.20/2.43  ((a1216) != (a1345))
% 2.20/2.43  (zenon_X33 != zenon_X107)
% 2.20/2.43  (c3_2 (a1223) zenon_X65)
% 2.20/2.43  (zenon_X14 != zenon_X46)
% 2.20/2.43  (zenon_X55 != (a1308))
% 2.20/2.43  ((a1351) != (a1256))
% 2.20/2.43  (zenon_X107 != (a1260))
% 2.20/2.43  (-. (c1_2 (a1226) (a1260)))
% 2.20/2.43  ((a1350) != (a1276))
% 2.20/2.43  (zenon_X14 != (a1300))
% 2.20/2.43  (c6_2 (a1350) (a1308))
% 2.20/2.43  (zenon_X41 != zenon_X42)
% 2.20/2.43  (zenon_X43 != zenon_X73)
% 2.20/2.43  (c9_2 (a1354) (a1294))
% 2.20/2.43  ((a1255) != (a1293))
% 2.20/2.43  (c10_2 (a1281) (a1352))
% 2.20/2.43  (c7_2 (a1223) (a1347))
% 2.20/2.43  ((a1300) != (a1256))
% 2.20/2.43  (c7_2 (a1346) zenon_X97)
% 2.20/2.43  (c9_2 (a1270) zenon_X107)
% 2.20/2.43  ((a1364) != zenon_X23)
% 2.20/2.43  (-. (c10_1 (a1350)))
% 2.20/2.43  ((a1271) != (a1330))
% 2.20/2.43  (c9_2 zenon_X17 (a1227))
% 2.20/2.43  (-. (c6_1 (a1363)))
% 2.20/2.43  ((a1351) != zenon_X32)
% 2.20/2.43  ((a1294) != (a1282))
% 2.20/2.43  (-. (c10_1 zenon_X25))
% 2.20/2.43  (c9_2 (a1293) zenon_X14)
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X50))
% 2.20/2.43  (c9_2 (a1281) (a1227))
% 2.20/2.43  (c7_2 (a1255) zenon_X71)
% 2.20/2.43  (c7_2 (a1293) zenon_X52)
% 2.20/2.43  (zenon_X97 != zenon_X5)
% 2.20/2.43  (zenon_X42 != zenon_X65)
% 2.20/2.43  (c9_2 zenon_X17 (a1246))
% 2.20/2.43  (-. (c1_2 zenon_X8 (a1302)))
% 2.20/2.43  (c5_2 (a1223) zenon_X58)
% 2.20/2.43  (c9_2 (a1241) zenon_X14)
% 2.20/2.43  (c7_2 (a1293) (a1283))
% 2.20/2.43  (zenon_X58 != zenon_X32)
% 2.20/2.43  (-. (c1_1 (a1287)))
% 2.20/2.43  (-. (c7_2 (a1223) (a1283)))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X103))
% 2.20/2.43  (c7_2 (a1220) zenon_X42)
% 2.20/2.43  (ndr1_1 zenon_X30)
% 2.20/2.43  (-. (c6_2 (a1226) (a1246)))
% 2.20/2.43  (c7_2 zenon_X35 (a1246))
% 2.20/2.43  ((a1308) != zenon_X49)
% 2.20/2.43  (zenon_X9 != (a1354))
% 2.20/2.43  (zenon_X33 != zenon_X54)
% 2.20/2.43  ((a1352) != zenon_X80)
% 2.20/2.43  ((a1282) != (a1246))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X31))
% 2.20/2.43  ((a1277) != zenon_X49)
% 2.20/2.43  (c9_2 (a1281) zenon_X31)
% 2.20/2.43  (-. (c6_2 (a1226) zenon_X52))
% 2.20/2.43  (zenon_X73 != zenon_X64)
% 2.20/2.43  (c7_2 (a1255) (a1277))
% 2.20/2.43  (zenon_X81 != (a1282))
% 2.20/2.43  (c7_2 (a1220) zenon_X43)
% 2.20/2.43  ((a1282) != zenon_X64)
% 2.20/2.43  (zenon_X8 != (a1354))
% 2.20/2.43  (c7_1 (a1226))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X43))
% 2.20/2.43  (c9_2 (a1220) (a1308))
% 2.20/2.43  ((a1281) != zenon_X1)
% 2.20/2.43  ((a1283) != zenon_X62)
% 2.20/2.43  ((a1351) != zenon_X85)
% 2.20/2.43  (zenon_X18 != (a1354))
% 2.20/2.43  (c9_2 zenon_X30 (a1347))
% 2.20/2.43  ((a1300) != (a1260))
% 2.20/2.43  (zenon_X3 != zenon_X42)
% 2.20/2.43  ((a1364) != (a1271))
% 2.20/2.43  (c9_2 (a1354) (a1300))
% 2.20/2.43  (zenon_X16 != (a1246))
% 2.20/2.43  ((a1227) != zenon_X50)
% 2.20/2.43  (-. (c6_2 (a1276) zenon_X14))
% 2.20/2.43  (c1_2 (a1215) zenon_X73)
% 2.20/2.43  (-. (c1_2 (a1241) (a1302)))
% 2.20/2.43  (zenon_X63 != zenon_X103)
% 2.20/2.43  ((a1293) != (a1354))
% 2.20/2.43  (zenon_X14 != (a1352))
% 2.20/2.43  ((a1351) != zenon_X16)
% 2.20/2.43  (zenon_X16 != (a1336))
% 2.20/2.43  ((a1283) != (a1326))
% 2.20/2.43  (c7_2 (a1346) zenon_X42)
% 2.20/2.43  (c7_2 (a1293) zenon_X33)
% 2.20/2.43  ((a1293) != (a1363))
% 2.20/2.43  (-. (c9_2 (a1270) (a1302)))
% 2.20/2.43  ((a1215) != (a1354))
% 2.20/2.43  (-. (c10_2 (a1208) zenon_X105))
% 2.20/2.43  ((a1346) != (a1214))
% 2.20/2.43  ((a1255) != zenon_X38)
% 2.20/2.43  ((a1363) != (a1307))
% 2.20/2.43  (-. (c6_2 (a1346) (a1294)))
% 2.20/2.43  ((a1271) != (a1345))
% 2.20/2.43  (-. (c5_2 zenon_X8 zenon_X57))
% 2.20/2.43  (c7_1 (a1214))
% 2.20/2.43  (zenon_X33 != zenon_X42)
% 2.20/2.43  ((a1346) != zenon_X8)
% 2.20/2.43  (-. (c10_2 (a1293) (a1256)))
% 2.20/2.43  ((a1352) != zenon_X57)
% 2.20/2.43  ((a1351) != zenon_X57)
% 2.20/2.43  (-. (c5_2 (a1270) zenon_X5))
% 2.20/2.43  (c2_2 (a1363) (a1364))
% 2.20/2.43  (c9_2 zenon_X18 (a1345))
% 2.20/2.43  (-. (c3_2 (a1307) zenon_X81))
% 2.20/2.43  (c1_2 (a1215) (a1256))
% 2.20/2.43  (c9_2 zenon_X8 (a1260))
% 2.20/2.43  ((a1283) != zenon_X52)
% 2.20/2.43  ((a1227) != zenon_X59)
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X52))
% 2.20/2.43  ((a1270) != zenon_X18)
% 2.20/2.43  (c7_2 (a1220) (a1364))
% 2.20/2.43  (-. (c1_2 (a1293) (a1302)))
% 2.20/2.43  (c7_2 (a1255) (a1345))
% 2.20/2.43  (c9_2 zenon_X30 (a1216))
% 2.20/2.43  (c1_2 (a1215) (a1345))
% 2.20/2.43  (zenon_X59 != zenon_X57)
% 2.20/2.43  (zenon_X14 != (a1302))
% 2.20/2.43  (c7_2 (a1270) (a1283))
% 2.20/2.43  (c5_2 (a1354) (a1246))
% 2.20/2.43  ((a1294) != zenon_X4)
% 2.20/2.43  ((a1347) != zenon_X60)
% 2.20/2.43  (c9_2 (a1241) (a1300))
% 2.20/2.43  (-. (c7_2 (a1223) (a1352)))
% 2.20/2.43  (zenon_X42 != zenon_X54)
% 2.20/2.43  (c7_2 (a1220) zenon_X46)
% 2.20/2.43  (c9_2 zenon_X8 (a1246))
% 2.20/2.43  ((a1347) != zenon_X58)
% 2.20/2.43  ((a1364) != zenon_X103)
% 2.20/2.43  ((a1346) != (a1223))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X53))
% 2.20/2.43  ((a1364) != (a1227))
% 2.20/2.43  (c3_2 zenon_X25 (a1351))
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X53))
% 2.20/2.43  ((a1246) != (a1302))
% 2.20/2.43  (c2_2 (a1346) (a1326))
% 2.20/2.43  (c7_2 zenon_X35 (a1216))
% 2.20/2.43  ((a1308) != zenon_X31)
% 2.20/2.43  ((a1255) != (a1350))
% 2.20/2.43  (zenon_X107 != zenon_X3)
% 2.20/2.43  (zenon_X16 != zenon_X46)
% 2.20/2.43  ((a1214) != (a1241))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X33))
% 2.20/2.43  (-. (c9_2 (a1255) (a1326)))
% 2.20/2.43  (c7_2 zenon_X35 (a1336))
% 2.20/2.43  (c9_2 (a1220) (a1282))
% 2.20/2.43  (c9_2 zenon_X27 (a1256))
% 2.20/2.43  (-. (c4_2 (a1241) (a1345)))
% 2.20/2.43  (c9_2 (a1255) (a1300))
% 2.20/2.43  (zenon_X42 != (a1246))
% 2.20/2.43  (zenon_X63 != zenon_X3)
% 2.20/2.43  (zenon_X5 != zenon_X52)
% 2.20/2.43  (c7_2 (a1223) (a1227))
% 2.20/2.43  (zenon_X31 != (a1302))
% 2.20/2.43  (zenon_X38 != zenon_X25)
% 2.20/2.43  (zenon_X55 != zenon_X50)
% 2.20/2.43  ((a1216) != (a1364))
% 2.20/2.43  (-. (c5_2 (a1255) zenon_X16))
% 2.20/2.43  ((a1347) != zenon_X52)
% 2.20/2.43  (-. (c3_2 (a1223) zenon_X32))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X46))
% 2.20/2.43  ((a1293) != (a1241))
% 2.20/2.43  (c7_2 (a1293) (a1246))
% 2.20/2.43  ((a1283) != (a1352))
% 2.20/2.43  (zenon_X46 != zenon_X3)
% 2.20/2.43  (zenon_X82 != (a1260))
% 2.20/2.43  (-. (c7_2 (a1223) zenon_X82))
% 2.20/2.43  ((a1256) != zenon_X31)
% 2.20/2.43  ((a1246) != zenon_X102)
% 2.20/2.43  (zenon_X33 != zenon_X71)
% 2.20/2.43  (c7_2 zenon_X35 (a1283))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X60))
% 2.20/2.43  (-. (c6_2 (a1215) zenon_X32))
% 2.20/2.43  (-. (c3_2 zenon_X27 (a1246)))
% 2.20/2.43  (-. (c6_2 zenon_X13 zenon_X49))
% 2.20/2.43  (-. (c5_2 zenon_X27 zenon_X102))
% 2.20/2.43  (zenon_X82 != zenon_X3)
% 2.20/2.44  (-. (c5_2 zenon_X8 zenon_X55))
% 2.20/2.44  (c9_2 (a1241) (a1271))
% 2.20/2.44  (c9_2 zenon_X30 (a1326))
% 2.20/2.44  ((a1277) != zenon_X71)
% 2.20/2.44  (-. (c10_2 (a1255) (a1352)))
% 2.20/2.44  ((a1363) != (a1223))
% 2.20/2.44  (zenon_X41 != zenon_X52)
% 2.20/2.44  (c9_2 (a1241) (a1345))
% 2.20/2.44  (-. (c8_2 (a1293) zenon_X20))
% 2.20/2.44  (c9_2 zenon_X8 (a1336))
% 2.20/2.44  (c1_1 (a1220))
% 2.20/2.44  (-. (c6_2 (a1350) zenon_X32))
% 2.20/2.44  (-. (c6_2 (a1346) (a1246)))
% 2.20/2.44  (c7_2 (a1220) (a1300))
% 2.20/2.44  (-. (c5_2 (a1346) zenon_X52))
% 2.20/2.44  (-. (c5_2 (a1241) zenon_X33))
% 2.20/2.44  (c9_2 (a1223) zenon_X73)
% 2.20/2.44  (-. (c4_1 (a1223)))
% 2.20/2.44  (c9_2 zenon_X17 (a1282))
% 2.20/2.44  (c9_2 (a1354) (a1282))
% 2.20/2.44  (zenon_X32 != zenon_X50)
% 2.20/2.44  (c7_2 (a1270) zenon_X107)
% 2.20/2.44  ((a1282) != zenon_X46)
% 2.20/2.44  (c9_2 zenon_X30 (a1336))
% 2.20/2.44  (-. (c6_2 (a1215) zenon_X57))
% 2.20/2.44  (zenon_X24 != (a1226))
% 2.20/2.44  (-. (c6_2 (a1215) zenon_X5))
% 2.20/2.44  (zenon_X97 != zenon_X57)
% 2.20/2.44  ((a1208) != zenon_X27)
% 2.20/2.44  (c5_2 (a1255) (a1256))
% 2.20/2.44  (-. (c6_2 zenon_X13 (a1246)))
% 2.20/2.44  (zenon_X81 != (a1294))
% 2.20/2.44  (zenon_X31 != zenon_X57)
% 2.20/2.44  (zenon_X14 != zenon_X31)
% 2.20/2.44  (-. (c6_2 (a1346) zenon_X65))
% 2.20/2.44  ((a1220) != (a1293))
% 2.20/2.44  ((a1364) != zenon_X46)
% 2.20/2.44  (-. (c6_2 (a1226) zenon_X42))
% 2.20/2.44  (zenon_X82 != (a1302))
% 2.20/2.44  ((a1346) != zenon_X27)
% 2.20/2.44  (c9_2 (a1223) zenon_X103)
% 2.20/2.44  (zenon_X60 != zenon_X102)
% 2.20/2.44  ((a1223) != zenon_X30)
% 2.20/2.44  ((a1300) != (a1216))
% 2.20/2.44  (zenon_X42 != zenon_X73)
% 2.20/2.44  (-. (c6_2 zenon_X13 zenon_X59))
% 2.20/2.44  ((a1347) != zenon_X53)
% 2.20/2.44  (zenon_X71 != zenon_X52)
% 2.20/2.44  (zenon_X63 != zenon_X82)
% 2.20/2.44  ((a1227) != (a1330))
% 2.20/2.44  ((a1283) != (a1260))
% 2.20/2.44  (-. (c6_2 (a1215) zenon_X81))
% 2.20/2.44  ((a1350) != zenon_X25)
% 2.20/2.44  (c7_2 zenon_X35 zenon_X53)
% 2.20/2.44  (c1_2 (a1215) (a1364))
% 2.20/2.44  (ndr1_1 (a1220))
% 2.20/2.44  (zenon_X18 != zenon_X27)
% 2.20/2.44  ((a1345) != zenon_X43)
% 2.20/2.44  (-. (c1_2 (a1287) (a1277)))
% 2.20/2.44  (-. (c6_2 zenon_X13 (a1271)))
% 2.20/2.44  (zenon_X39 != (a1350))
% 2.20/2.44  (c9_2 zenon_X8 (a1347))
% 2.20/2.44  (-. (c5_2 zenon_X8 zenon_X82))
% 2.20/2.44  (-. (c6_2 (a1346) (a1271)))
% 2.20/2.44  ((a1308) != (a1260))
% 2.20/2.44  (zenon_X73 != (a1300))
% 2.20/2.44  (-. (c5_2 zenon_X17 zenon_X49))
% 2.20/2.44  ((a1216) != (a1302))
% 2.20/2.44  (-. (c3_2 (a1307) (a1300)))
% 2.20/2.44  (-. (c8_2 (a1214) (a1352)))
% 2.20/2.44  (zenon_X17 != zenon_X39)
% 2.20/2.44  (c3_2 (a1350) zenon_X31)
% 2.20/2.44  (c7_2 (a1255) zenon_X102)
% 2.20/2.44  ((a1336) != zenon_X107)
% 2.20/2.44  (zenon_X97 != zenon_X31)
% 2.20/2.44  (-. (c10_1 zenon_X18))
% 2.20/2.44  ((a1271) != zenon_X54)
% 2.20/2.44  (c7_2 (a1220) zenon_X5)
% 2.20/2.44  ((a1241) != zenon_X27)
% 2.20/2.44  (c9_2 zenon_X27 (a1216))
% 2.20/2.44  (zenon_X16 != zenon_X73)
% 2.20/2.44  ((a1216) != zenon_X82)
% 2.20/2.44  ((a1308) != (a1294))
% 2.20/2.44  (zenon_X33 != (a1271))
% 2.20/2.44  (c3_2 (a1350) zenon_X63)
% 2.20/2.44  (c7_2 (a1241) zenon_X46)
% 2.20/2.44  ((a1347) != (a1336))
% 2.20/2.44  (zenon_X42 != zenon_X102)
% 2.20/2.44  (zenon_X42 != zenon_X82)
% 2.20/2.44  (-. (c5_2 (a1214) (a1246)))
% 2.20/2.44  ((a1277) != zenon_X54)
% 2.20/2.44  (c9_2 zenon_X27 (a1277))
% 2.20/2.44  ((a1345) != zenon_X15)
% 2.20/2.44  ((a1352) != zenon_X50)
% 2.20/2.44  (c2_1 (a1220))
% 2.20/2.44  ((a1227) != zenon_X71)
% 2.20/2.44  (c9_2 (a1270) zenon_X73)
% 2.20/2.44  (-. (c5_2 zenon_X30 zenon_X32))
% 2.20/2.44  (zenon_X8 != (a1270))
% 2.20/2.44  ((a1347) != zenon_X65)
% 2.20/2.44  (-. (c10_2 (a1350) zenon_X93))
% 2.20/2.44  (zenon_X18 != (a1350))
% 2.20/2.44  (c7_2 (a1255) (a1271))
% 2.20/2.44  ((a1336) != (a1282))
% 2.20/2.44  (c10_2 (a1287) (a1351))
% 2.20/2.44  ((a1352) != zenon_X64)
% 2.20/2.44  ((a1281) != (a1307))
% 2.20/2.44  ((a1214) != zenon_X17)
% 2.20/2.44  ((a1347) != zenon_X41)
% 2.20/2.44  (-. (c6_2 (a1346) zenon_X42))
% 2.20/2.44  (c7_2 (a1293) zenon_X107)
% 2.20/2.44  (c9_2 (a1346) zenon_X103)
% 2.20/2.44  (-. (c4_2 (a1335) (a1345)))
% 2.20/2.44  (zenon_X16 != zenon_X103)
% 2.20/2.44  ((a1345) != zenon_X103)
% 2.20/2.44  (c7_2 (a1346) zenon_X14)
% 2.20/2.44  (-. (c3_2 (a1307) (a1336)))
% 2.20/2.44  ((a1352) != zenon_X82)
% 2.20/2.44  (zenon_X31 != zenon_X3)
% 2.20/2.44  (-. (c6_2 (a1346) (a1256)))
% 2.20/2.44  (zenon_X30 != (a1287))
% 2.20/2.44  ((a1308) != zenon_X60)
% 2.20/2.44  (-. (c6_2 (a1226) (a1345)))
% 2.20/2.44  (c7_2 (a1270) zenon_X42)
% 2.20/2.44  (c7_2 (a1293) zenon_X65)
% 2.20/2.44  (-. (c5_2 zenon_X27 zenon_X81))
% 2.20/2.44  ((a1270) != (a1215))
% 2.20/2.44  (-. (c6_2 (a1276) (a1345)))
% 2.20/2.44  (c7_2 (a1346) zenon_X55)
% 2.20/2.44  (c9_2 zenon_X38 (a1300))
% 2.20/2.44  (c7_2 (a1208) (a1364))
% 2.20/2.44  (-. (c1_2 (a1287) (a1308)))
% 2.20/2.44  (c9_2 zenon_X38 (a1216))
% 2.20/2.44  (c7_2 (a1270) zenon_X82)
% 2.20/2.44  (zenon_X103 != zenon_X5)
% 2.20/2.44  (c9_2 (a1223) (a1227))
% 2.20/2.44  (-. (c1_2 (a1287) (a1300)))
% 2.20/2.44  (zenon_X41 != (a1364))
% 2.20/2.44  (zenon_X55 != zenon_X32)
% 2.20/2.44  (-. (c5_2 zenon_X8 zenon_X97))
% 2.20/2.44  (-. (c10_2 (a1270) (a1351)))
% 2.20/2.44  ((a1347) != (a1345))
% 2.20/2.44  (c7_2 (a1255) (a1246))
% 2.20/2.44  (-. (c2_1 zenon_X30))
% 2.20/2.44  (-. (c8_2 zenon_X17 (a1352)))
% 2.20/2.44  (zenon_X60 != zenon_X82)
% 2.20/2.44  (-. (c9_2 (a1350) (a1302)))
% 2.20/2.44  (c7_2 (a1293) (a1300))
% 2.20/2.44  (c9_2 (a1346) zenon_X31)
% 2.20/2.44  (zenon_X33 != (a1246))
% 2.20/2.44  ((a1216) != zenon_X53)
% 2.20/2.44  (-. (c5_2 zenon_X30 zenon_X97))
% 2.20/2.44  ((a1363) != (a1350))
% 2.20/2.44  (zenon_X16 != zenon_X59)
% 2.20/2.44  ((a1336) != zenon_X73)
% 2.20/2.44  ((a1256) != zenon_X54)
% 2.20/2.44  ((a1347) != (a1352))
% 2.20/2.44  (-. (c1_2 (a1354) (a1302)))
% 2.20/2.44  ((a1271) != zenon_X102)
% 2.20/2.44  ((a1216) != zenon_X65)
% 2.20/2.44  ((a1246) != zenon_X31)
% 2.20/2.44  ((a1351) != zenon_X0)
% 2.20/2.44  (c10_2 (a1215) (a1352))
% 2.20/2.44  ((a1364) != (a1336))
% 2.20/2.44  ((a1351) != zenon_X100)
% 2.20/2.44  ((a1216) != zenon_X103)
% 2.20/2.44  (c9_2 (a1223) (a1271))
% 2.20/2.44  (-. (c6_2 (a1346) zenon_X73))
% 2.20/2.44  ((a1255) != (a1354))
% 2.20/2.44  ((a1308) != zenon_X81)
% 2.20/2.44  (-. (c2_2 zenon_X30 (a1352)))
% 2.20/2.44  ((a1227) != zenon_X52)
% 2.20/2.44  (-. (c10_2 (a1241) zenon_X29))
% 2.20/2.44  (c9_2 (a1270) (a1347))
% 2.20/2.44  (-. (c4_2 (a1226) (a1260)))
% 2.20/2.44  ((a1270) != (a1281))
% 2.20/2.44  ((a1256) != zenon_X102)
% 2.20/2.44  ((a1226) != (a1354))
% 2.20/2.44  ((a1256) != zenon_X49)
% 2.20/2.44  (c7_2 (a1270) zenon_X81)
% 2.20/2.44  ((a1330) != (a1302))
% 2.20/2.44  (zenon_X42 != zenon_X64)
% 2.20/2.44  (c9_2 (a1346) (a1216))
% 2.20/2.44  ((a1220) != zenon_X35)
% 2.20/2.44  (c9_2 zenon_X38 (a1246))
% 2.20/2.44  ((a1347) != (a1302))
% 2.20/2.44  (c10_2 zenon_X17 (a1352))
% 2.20/2.44  (-. (c3_2 (a1307) zenon_X50))
% 2.20/2.44  (zenon_X25 != zenon_X27)
% 2.20/2.44  (c7_2 (a1270) (a1345))
% 2.20/2.44  *)
% 2.20/2.44  (* NO-PROOF *)
% 2.20/2.44  % SZS status GaveUp
% 2.20/2.44  Number of rewrites on terms: 0
% 2.20/2.44  Number of rewrites on props: 0
% 2.20/2.44  nodes searched: 60782
% 2.20/2.44  max branch formulas: 5097
% 2.20/2.44  proof nodes created: 976
% 2.20/2.44  formulas created: 50665
% 2.20/2.44  
%------------------------------------------------------------------------------