ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n011.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:34 EDT 2024

% Result   : Unknown 2.15s 2.31s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13  % Problem  : SYN420+1 : TPTP v8.2.0. Released v2.1.0.
% 0.12/0.13  % Command  : run_zenon_modulo %d %s
% 0.13/0.34  % Computer : n011.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Mon Jun 24 01:34:12 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 2.06/2.30  Zenon error: exhausted search space without finding a proof
% 2.06/2.30  (* Current branch:
% 2.06/2.30  ((a293) != (a290))
% 2.06/2.30  (c5_2 zenon_X22 (a299))
% 2.06/2.30  (zenon_X31 != zenon_X19)
% 2.06/2.30  (-. (c8_2 (a395) zenon_X59))
% 2.06/2.30  ((a294) != zenon_X13)
% 2.06/2.30  (-. (c5_2 (a448) (a279)))
% 2.06/2.30  ((a347) != zenon_X71)
% 2.06/2.30  ((a347) != zenon_X163)
% 2.06/2.30  (zenon_X8 != zenon_X23)
% 2.06/2.30  ((a291) != (a294))
% 2.06/2.30  (c6_2 zenon_X21 (a417))
% 2.06/2.30  (-. (c5_2 (a424) (a292)))
% 2.06/2.30  (zenon_X8 != (a319))
% 2.06/2.30  (-. (c6_2 zenon_X39 (a439)))
% 2.06/2.30  (-. (c3_2 (a369) zenon_X62))
% 2.06/2.30  (-. (c5_2 (a317) (a279)))
% 2.06/2.30  (c3_1 (a291))
% 2.06/2.30  (c1_1 (a271))
% 2.06/2.30  (c1_2 zenon_X22 (a440))
% 2.06/2.30  ((a409) != zenon_X69)
% 2.06/2.30  (zenon_X25 != (a443))
% 2.06/2.30  ((a353) != (a289))
% 2.06/2.30  ((a347) != zenon_X152)
% 2.06/2.30  ((a417) != zenon_X123)
% 2.06/2.30  ((a434) != (a302))
% 2.06/2.30  (-. (c4_1 zenon_X7))
% 2.06/2.30  ((a271) != (a416))
% 2.06/2.30  (c6_1 (a302))
% 2.06/2.30  ((a443) != (a327))
% 2.06/2.30  (ndr1_1 zenon_X18)
% 2.06/2.30  ((a389) != zenon_X4)
% 2.06/2.30  (c6_2 zenon_X13 (a425))
% 2.06/2.30  (-. (c5_2 (a332) (a290)))
% 2.06/2.30  ((a279) != zenon_X49)
% 2.06/2.30  (-. (c10_2 zenon_X43 (a338)))
% 2.06/2.30  (c1_1 (a352))
% 2.06/2.30  ((a395) != (a369))
% 2.06/2.30  (-. (c7_2 zenon_X13 (a425)))
% 2.06/2.30  (c3_2 zenon_X35 (a347))
% 2.06/2.30  ((a332) != zenon_X22)
% 2.06/2.30  ((a396) != (a439))
% 2.06/2.30  ((a280) != zenon_X28)
% 2.06/2.30  ((a347) != zenon_X174)
% 2.06/2.30  (zenon_X8 != zenon_X22)
% 2.06/2.30  (-. (c2_2 (a448) (a389)))
% 2.06/2.30  (zenon_X39 != zenon_X43)
% 2.06/2.30  ((a425) != zenon_X192)
% 2.06/2.30  ((a302) != (a280))
% 2.06/2.30  ((a379) != zenon_X63)
% 2.06/2.30  (-. (c3_2 (a291) zenon_X53))
% 2.06/2.30  ((a410) != zenon_X1)
% 2.06/2.30  ((a379) != zenon_X36)
% 2.06/2.30  ((a444) != (a343))
% 2.06/2.30  (zenon_X25 != (a280))
% 2.06/2.30  (zenon_X32 != (a369))
% 2.06/2.30  ((a289) != zenon_X171)
% 2.06/2.30  (-. (c8_2 zenon_X19 zenon_X20))
% 2.06/2.30  (-. (c1_1 zenon_X23))
% 2.06/2.30  ((a379) != zenon_X67)
% 2.06/2.30  ((a319) != (a405))
% 2.06/2.30  ((a405) != (a352))
% 2.06/2.30  (zenon_X25 != zenon_X7)
% 2.06/2.30  (zenon_X32 != (a332))
% 2.06/2.30  ((a279) != (a390))
% 2.06/2.30  ((a295) != zenon_X36)
% 2.06/2.30  ((a278) != zenon_X7)
% 2.06/2.30  ((a279) != zenon_X105)
% 2.06/2.30  (-. (c8_2 (a332) (a286)))
% 2.06/2.30  ((a279) != (a290))
% 2.06/2.30  (-. (c2_2 zenon_X25 (a389)))
% 2.06/2.30  ((a347) != (a440))
% 2.06/2.30  (-. (c4_2 (a448) zenon_X0))
% 2.06/2.30  (zenon_X35 != (a307))
% 2.06/2.30  (zenon_X39 != zenon_X25)
% 2.06/2.30  (-. (c7_2 zenon_X23 (a286)))
% 2.06/2.30  (-. (c5_2 zenon_X43 (a363)))
% 2.06/2.30  ((a448) != (a302))
% 2.06/2.30  (c6_2 (a444) (a279))
% 2.06/2.30  (c3_2 (a280) (a380))
% 2.06/2.30  (c6_2 (a444) (a292))
% 2.06/2.30  ((a417) != zenon_X121)
% 2.06/2.30  (c6_2 (a434) (a347))
% 2.06/2.30  (-. (c8_2 (a319) zenon_X84))
% 2.06/2.30  ((a409) != zenon_X29)
% 2.06/2.30  (zenon_X6 != zenon_X35)
% 2.06/2.30  (zenon_X6 != (a287))
% 2.06/2.30  (c4_2 (a280) (a417))
% 2.06/2.30  (-. (c10_2 (a332) (a347)))
% 2.06/2.30  (c1_1 (a291))
% 2.06/2.30  ((a431) != (a434))
% 2.06/2.30  (c6_2 zenon_X16 (a439))
% 2.06/2.30  (-. (c7_2 (a271) (a417)))
% 2.06/2.30  ((a395) != (a444))
% 2.06/2.30  ((a379) != zenon_X53)
% 2.06/2.30  (-. (c1_2 (a271) (a347)))
% 2.06/2.30  (zenon_X45 != zenon_X16)
% 2.06/2.30  (c4_2 zenon_X21 (a389))
% 2.06/2.30  ((a299) != zenon_X57)
% 2.06/2.30  ((a389) != (a279))
% 2.06/2.30  ((a416) != zenon_X23)
% 2.06/2.30  ((a440) != (a293))
% 2.06/2.30  ((a425) != zenon_X184)
% 2.06/2.30  ((a416) != (a332))
% 2.06/2.30  (ndr1_1 (a343))
% 2.06/2.30  ((a279) != zenon_X61)
% 2.06/2.30  ((a395) != zenon_X18)
% 2.06/2.30  ((a292) != zenon_X2)
% 2.06/2.30  ((a299) != zenon_X166)
% 2.06/2.30  (c7_2 zenon_X35 (a286))
% 2.06/2.30  ((a389) != (a379))
% 2.06/2.30  (-. (c7_2 (a317) (a338)))
% 2.06/2.30  (-. (c6_2 zenon_X43 (a425)))
% 2.06/2.30  (c6_2 zenon_X23 (a429))
% 2.06/2.30  ((a417) != zenon_X26)
% 2.06/2.30  (zenon_X43 != zenon_X8)
% 2.06/2.30  (zenon_X31 != (a352))
% 2.06/2.30  (-. (c5_2 zenon_X8 (a290)))
% 2.06/2.30  ((a410) != (a353))
% 2.06/2.30  (zenon_X13 != zenon_X23)
% 2.06/2.30  (-. (c8_2 (a395) (a286)))
% 2.06/2.30  (-. (c5_2 zenon_X31 (a439)))
% 2.06/2.30  (zenon_X1 != zenon_X42)
% 2.06/2.30  ((a448) != zenon_X22)
% 2.06/2.30  (-. (c8_2 zenon_X32 zenon_X176))
% 2.06/2.30  (-. (c7_2 zenon_X13 (a439)))
% 2.06/2.30  ((a279) != (a338))
% 2.06/2.30  (zenon_X43 != zenon_X32)
% 2.06/2.30  (c6_2 (a369) (a379))
% 2.06/2.30  ((a429) != (a290))
% 2.06/2.30  ((a429) != zenon_X194)
% 2.06/2.30  (c7_2 zenon_X39 (a347))
% 2.06/2.30  (-. (c2_2 (a431) (a389)))
% 2.06/2.30  (-. (c7_2 (a332) zenon_X67))
% 2.06/2.30  ((a280) != (a332))
% 2.06/2.30  (c6_2 zenon_X28 (a370))
% 2.06/2.30  (-. (c1_1 zenon_X28))
% 2.06/2.30  (c6_2 (a448) (a429))
% 2.06/2.30  ((a278) != (a280))
% 2.06/2.30  ((a418) != (a289))
% 2.06/2.30  (-. (c5_2 (a424) (a290)))
% 2.06/2.30  (-. (c10_1 (a369)))
% 2.06/2.30  ((a417) != zenon_X33)
% 2.06/2.30  ((a271) != (a405))
% 2.06/2.30  (zenon_X21 != (a332))
% 2.06/2.30  (zenon_X35 != (a395))
% 2.06/2.30  ((a417) != zenon_X175)
% 2.06/2.30  (-. (c3_2 zenon_X16 zenon_X188))
% 2.06/2.30  ((a290) != zenon_X135)
% 2.06/2.30  (c6_2 (a405) (a286))
% 2.06/2.30  ((a418) != (a390))
% 2.06/2.30  (c3_1 zenon_X16)
% 2.06/2.30  (-. (c6_2 zenon_X43 (a439)))
% 2.06/2.30  ((a299) != zenon_X195)
% 2.06/2.30  ((a289) != (a439))
% 2.06/2.30  (-. (c1_2 (a416) (a417)))
% 2.06/2.30  (c6_2 (a294) (a295))
% 2.06/2.30  ((a291) != (a327))
% 2.06/2.30  ((a290) != zenon_X110)
% 2.06/2.30  ((a279) != zenon_X190)
% 2.06/2.30  ((a347) != zenon_X122)
% 2.06/2.30  ((a279) != (a439))
% 2.06/2.30  ((a289) != zenon_X33)
% 2.06/2.30  ((a439) != zenon_X180)
% 2.06/2.30  ((a389) != (a410))
% 2.06/2.30  (c6_2 (a287) (a429))
% 2.06/2.30  (-. (c10_2 (a332) (a410)))
% 2.06/2.30  ((a379) != zenon_X194)
% 2.06/2.30  ((a286) != zenon_X180)
% 2.06/2.30  (zenon_X43 != zenon_X16)
% 2.06/2.30  (c6_2 (a352) (a417))
% 2.06/2.30  (-. (c6_1 (a416)))
% 2.06/2.30  ((a380) != zenon_X42)
% 2.06/2.30  (-. (c5_2 (a280) (a417)))
% 2.06/2.30  ((a292) != zenon_X26)
% 2.06/2.30  (c3_2 (a280) (a379))
% 2.06/2.30  ((a327) != (a332))
% 2.06/2.30  ((a396) != zenon_X189)
% 2.06/2.30  ((a396) != (a425))
% 2.06/2.30  ((a435) != (a379))
% 2.06/2.30  ((a291) != (a287))
% 2.06/2.30  (c1_1 zenon_X43)
% 2.06/2.30  (c6_2 zenon_X8 (a440))
% 2.06/2.30  ((a317) != (a307))
% 2.06/2.30  ((a417) != zenon_X82)
% 2.06/2.30  (c3_1 (a443))
% 2.06/2.30  ((a317) != (a278))
% 2.06/2.30  ((a431) != (a332))
% 2.06/2.30  (c5_2 zenon_X6 (a299))
% 2.06/2.30  (c6_2 (a444) (a439))
% 2.06/2.30  (c5_2 (a352) (a389))
% 2.06/2.30  ((a278) != (a444))
% 2.06/2.30  ((a352) != zenon_X27)
% 2.06/2.30  (-. (c10_1 zenon_X25))
% 2.06/2.30  (-. (c6_2 zenon_X39 (a279)))
% 2.06/2.30  ((a417) != zenon_X85)
% 2.06/2.30  (c4_1 zenon_X27)
% 2.06/2.30  (c6_2 zenon_X23 (a347))
% 2.06/2.30  (-. (c5_2 (a431) (a290)))
% 2.06/2.30  (zenon_X27 != zenon_X21)
% 2.06/2.30  (-. (c7_2 (a424) (a347)))
% 2.06/2.30  ((a429) != zenon_X80)
% 2.06/2.30  (zenon_X16 != (a405))
% 2.06/2.30  ((a352) != zenon_X13)
% 2.06/2.30  ((a279) != zenon_X98)
% 2.06/2.30  (zenon_X18 != (a307))
% 2.06/2.30  (zenon_X16 != (a332))
% 2.06/2.30  (c5_2 (a278) (a279))
% 2.06/2.30  ((a294) != (a327))
% 2.06/2.30  (c6_2 (a395) (a286))
% 2.06/2.30  ((a299) != zenon_X56)
% 2.06/2.30  (c3_2 zenon_X22 (a439))
% 2.06/2.30  (-. (c2_1 (a448)))
% 2.06/2.30  (-. (c1_2 (a307) (a390)))
% 2.06/2.30  ((a410) != zenon_X30)
% 2.06/2.30  (-. (c5_2 (a352) (a353)))
% 2.06/2.30  (zenon_X6 != (a431))
% 2.06/2.30  (-. (c7_2 zenon_X28 (a286)))
% 2.06/2.30  (-. (c2_2 (a278) (a344)))
% 2.06/2.30  (-. (c7_2 (a302) (a338)))
% 2.06/2.30  (c9_1 zenon_X18)
% 2.06/2.30  ((a439) != zenon_X139)
% 2.06/2.30  ((a363) != (a279))
% 2.06/2.30  ((a439) != zenon_X54)
% 2.06/2.30  (c6_2 (a416) (a286))
% 2.06/2.30  (c7_2 zenon_X31 (a439))
% 2.06/2.30  (zenon_X6 != (a405))
% 2.06/2.30  (c6_2 (a280) (a409))
% 2.06/2.30  (-. (c6_2 (a271) (a370)))
% 2.06/2.30  ((a379) != zenon_X184)
% 2.06/2.30  (-. (c7_2 (a317) (a417)))
% 2.06/2.30  (zenon_X25 != (a369))
% 2.06/2.30  (-. (c5_2 (a352) (a418)))
% 2.06/2.30  ((a434) != (a369))
% 2.06/2.30  (zenon_X43 != (a424))
% 2.06/2.30  (-. (c8_2 zenon_X39 zenon_X89))
% 2.06/2.30  (zenon_X35 != zenon_X23)
% 2.06/2.30  (-. (c2_2 zenon_X32 (a389)))
% 2.06/2.30  ((a425) != zenon_X63)
% 2.06/2.30  ((a431) != zenon_X18)
% 2.06/2.30  (c6_2 (a327) (a289))
% 2.06/2.30  ((a352) != (a395))
% 2.06/2.30  (-. (c4_2 (a280) (a379)))
% 2.06/2.30  ((a292) != zenon_X109)
% 2.06/2.30  (c6_2 zenon_X13 (a299))
% 2.06/2.30  ((a327) != (a448))
% 2.06/2.30  ((a363) != (a380))
% 2.06/2.30  ((a291) != zenon_X21)
% 2.06/2.30  (-. (c1_1 (a302)))
% 2.06/2.30  (c6_2 (a332) (a299))
% 2.06/2.30  (-. (c5_2 (a287) (a279)))
% 2.06/2.30  ((a431) != (a444))
% 2.06/2.30  ((a448) != zenon_X23)
% 2.06/2.30  ((a440) != zenon_X194)
% 2.06/2.30  ((a347) != zenon_X194)
% 2.06/2.30  ((a443) != (a444))
% 2.06/2.30  (zenon_X25 != (a307))
% 2.06/2.30  ((a439) != (a390))
% 2.06/2.30  (c3_1 (a327))
% 2.06/2.30  ((a405) != (a343))
% 2.06/2.30  (c3_0)
% 2.06/2.30  (c1_1 (a444))
% 2.06/2.30  ((a299) != zenon_X105)
% 2.06/2.30  ((a443) != zenon_X18)
% 2.06/2.30  ((a307) != zenon_X13)
% 2.06/2.30  (c6_2 (a424) (a396))
% 2.06/2.30  ((a344) != zenon_X70)
% 2.06/2.30  (c3_2 (a280) (a410))
% 2.06/2.30  ((a299) != zenon_X77)
% 2.06/2.30  (zenon_X16 != (a434))
% 2.06/2.30  (c6_2 zenon_X25 (a286))
% 2.06/2.30  ((a278) != (a424))
% 2.06/2.30  ((a352) != zenon_X7)
% 2.06/2.30  ((a295) != (a299))
% 2.06/2.30  ((a299) != zenon_X9)
% 2.06/2.30  (zenon_X25 != (a319))
% 2.06/2.30  (zenon_X22 != zenon_X25)
% 2.06/2.30  ((a443) != (a343))
% 2.06/2.30  ((a363) != (a370))
% 2.06/2.30  (c4_1 zenon_X18)
% 2.06/2.30  ((a290) != zenon_X137)
% 2.06/2.30  ((a299) != zenon_X101)
% 2.06/2.30  (-. (c8_2 (a291) zenon_X47))
% 2.06/2.30  (zenon_X19 != (a317))
% 2.06/2.30  ((a439) != zenon_X53)
% 2.06/2.30  (-. (c4_1 (a443)))
% 2.06/2.30  (zenon_X27 != zenon_X19)
% 2.06/2.30  (-. (c7_1 zenon_X22))
% 2.06/2.30  (-. (c9_1 (a280)))
% 2.06/2.30  (zenon_X25 != zenon_X27)
% 2.06/2.30  (c6_2 zenon_X19 (a417))
% 2.06/2.30  (c6_2 zenon_X31 (a417))
% 2.06/2.30  (-. (c5_2 (a352) (a439)))
% 2.06/2.30  ((a417) != zenon_X75)
% 2.06/2.30  ((a288) != (a344))
% 2.06/2.30  (-. (c6_2 (a317) (a425)))
% 2.06/2.30  (zenon_X7 != (a369))
% 2.06/2.30  ((a290) != zenon_X127)
% 2.06/2.30  ((a443) != (a352))
% 2.06/2.30  (zenon_X35 != (a424))
% 2.06/2.30  ((a429) != zenon_X179)
% 2.06/2.30  ((a439) != (a290))
% 2.06/2.30  (-. (c5_2 zenon_X43 (a289)))
% 2.06/2.30  (zenon_X31 != (a448))
% 2.06/2.30  ((a448) != zenon_X28)
% 2.06/2.30  ((a347) != (a299))
% 2.06/2.30  (zenon_X21 != (a369))
% 2.06/2.30  (ndr1_1 zenon_X35)
% 2.06/2.30  ((a319) != zenon_X7)
% 2.06/2.30  ((a290) != zenon_X47)
% 2.06/2.30  ((a279) != zenon_X103)
% 2.06/2.30  ((a440) != (a390))
% 2.06/2.30  (-. (c6_1 (a319)))
% 2.06/2.30  (-. (c8_2 (a444) (a286)))
% 2.06/2.30  ((a291) != (a271))
% 2.06/2.30  (c6_1 zenon_X21)
% 2.06/2.30  (-. (c5_2 (a416) (a299)))
% 2.06/2.30  (-. (c6_2 zenon_X39 (a425)))
% 2.06/2.30  ((a287) != (a271))
% 2.06/2.30  (c1_2 zenon_X8 (a440))
% 2.06/2.30  ((a299) != (a286))
% 2.06/2.30  (zenon_X25 != (a444))
% 2.06/2.30  (zenon_X19 != (a280))
% 2.06/2.30  ((a417) != zenon_X179)
% 2.06/2.30  (zenon_X8 != zenon_X28)
% 2.06/2.30  ((a347) != zenon_X188)
% 2.06/2.30  ((a299) != zenon_X140)
% 2.06/2.30  (-. (c5_2 (a434) (a299)))
% 2.06/2.30  ((a292) != zenon_X95)
% 2.06/2.30  (c6_2 (a332) (a418))
% 2.06/2.30  (zenon_X45 != zenon_X22)
% 2.06/2.30  ((a279) != zenon_X81)
% 2.06/2.30  (c6_2 (a424) (a417))
% 2.06/2.30  (-. (c7_2 (a280) (a417)))
% 2.06/2.30  ((a295) != zenon_X42)
% 2.06/2.30  ((a417) != zenon_X108)
% 2.06/2.30  (-. (c5_2 (a332) (a289)))
% 2.06/2.30  (zenon_X1 != (a295))
% 2.06/2.30  ((a409) != zenon_X11)
% 2.06/2.30  (-. (c5_2 (a307) (a418)))
% 2.06/2.30  (zenon_X8 != (a307))
% 2.06/2.30  (c7_2 (a327) (a347))
% 2.06/2.30  (zenon_X7 != zenon_X19)
% 2.06/2.30  ((a299) != zenon_X50)
% 2.06/2.30  (-. (c2_2 (a294) (a295)))
% 2.06/2.30  (c7_2 (a294) (a429))
% 2.06/2.30  ((a379) != zenon_X173)
% 2.06/2.30  (c6_2 (a443) (a286))
% 2.06/2.30  (c3_1 (a352))
% 2.06/2.30  (-. (c8_2 zenon_X23 (a286)))
% 2.06/2.30  (c6_2 (a395) (a299))
% 2.06/2.30  ((a286) != zenon_X173)
% 2.06/2.30  ((a289) != (a425))
% 2.06/2.30  (zenon_X39 != (a434))
% 2.06/2.30  (c6_2 (a307) (a417))
% 2.06/2.30  (c6_2 (a332) (a410))
% 2.06/2.30  (zenon_X25 != (a424))
% 2.06/2.30  ((a287) != zenon_X25)
% 2.06/2.30  ((a370) != zenon_X189)
% 2.06/2.30  (c3_2 (a319) (a347))
% 2.06/2.30  (-. (c8_1 zenon_X34))
% 2.06/2.30  (-. (c8_2 (a271) zenon_X74))
% 2.06/2.30  ((a417) != zenon_X57)
% 2.06/2.30  (zenon_X18 != (a369))
% 2.06/2.30  (-. (c1_2 (a302) (a347)))
% 2.06/2.30  (-. (c2_2 (a280) zenon_X1))
% 2.06/2.30  ((a292) != zenon_X98)
% 2.06/2.30  (c10_2 (a327) (a347))
% 2.06/2.30  (-. (c3_2 zenon_X32 zenon_X189))
% 2.06/2.30  ((a417) != zenon_X67)
% 2.06/2.30  (c6_2 (a280) (a380))
% 2.06/2.30  (zenon_X16 != (a416))
% 2.06/2.30  (c6_1 zenon_X31)
% 2.06/2.30  (zenon_X39 != (a369))
% 2.06/2.30  ((a347) != (a390))
% 2.06/2.30  ((a410) != (a380))
% 2.06/2.30  ((a292) != zenon_X57)
% 2.06/2.30  ((a434) != zenon_X23)
% 2.06/2.30  (c10_1 zenon_X31)
% 2.06/2.30  ((a271) != zenon_X23)
% 2.06/2.30  (-. (c5_2 (a278) (a439)))
% 2.06/2.30  ((a294) != (a280))
% 2.06/2.30  ((a439) != zenon_X123)
% 2.06/2.30  ((a396) != (a286))
% 2.06/2.30  ((a299) != zenon_X48)
% 2.06/2.30  ((a294) != (a369))
% 2.06/2.30  ((a287) != (a302))
% 2.06/2.30  (c3_1 (a319))
% 2.06/2.30  (c6_2 (a278) (a429))
% 2.06/2.30  (-. (c9_1 (a327)))
% 2.06/2.30  (-. (c9_1 zenon_X7))
% 2.06/2.30  ((a379) != (a370))
% 2.06/2.30  (c5_2 zenon_X19 (a418))
% 2.06/2.30  ((a448) != zenon_X21)
% 2.06/2.30  ((a319) != (a369))
% 2.06/2.30  (zenon_X35 != (a278))
% 2.06/2.30  (-. (c2_2 (a287) (a389)))
% 2.06/2.30  ((a380) != (a299))
% 2.06/2.30  (ndr1_1 (a327))
% 2.06/2.30  (c5_2 (a291) (a279))
% 2.06/2.30  ((a352) != zenon_X28)
% 2.06/2.30  (zenon_X35 != zenon_X43)
% 2.06/2.30  (zenon_X8 != zenon_X32)
% 2.06/2.30  ((a299) != zenon_X141)
% 2.06/2.30  ((a279) != zenon_X140)
% 2.06/2.30  ((a294) != (a319))
% 2.06/2.30  (-. (c10_2 zenon_X35 (a338)))
% 2.06/2.30  ((a389) != zenon_X107)
% 2.06/2.30  (c6_2 (a395) (a347))
% 2.06/2.30  (c10_1 (a317))
% 2.06/2.30  (c9_1 (a271))
% 2.06/2.30  (zenon_X32 != zenon_X45)
% 2.06/2.30  (-. (c10_1 zenon_X18))
% 2.06/2.30  (zenon_X1 != (a380))
% 2.06/2.30  (c1_1 zenon_X7)
% 2.06/2.30  ((a444) != zenon_X22)
% 2.06/2.30  (zenon_X21 != zenon_X8)
% 2.06/2.30  (c3_1 zenon_X43)
% 2.06/2.30  ((a293) != zenon_X112)
% 2.06/2.30  ((a363) != zenon_X98)
% 2.06/2.30  ((a417) != zenon_X194)
% 2.06/2.30  ((a417) != (a418))
% 2.06/2.30  ((a439) != zenon_X68)
% 2.06/2.30  ((a286) != zenon_X108)
% 2.06/2.30  ((a390) != zenon_X5)
% 2.06/2.30  (c6_2 zenon_X18 (a440))
% 2.06/2.30  (zenon_X8 != (a443))
% 2.06/2.30  (c2_2 (a444) (a344))
% 2.06/2.30  (c3_1 zenon_X19)
% 2.06/2.30  ((a409) != (a338))
% 2.06/2.30  ((a292) != zenon_X167)
% 2.06/2.30  ((a439) != zenon_X128)
% 2.06/2.30  ((a347) != zenon_X24)
% 2.06/2.30  (c4_1 zenon_X25)
% 2.06/2.30  (c6_2 (a332) (a439))
% 2.06/2.30  ((a347) != zenon_X193)
% 2.06/2.30  ((a347) != zenon_X175)
% 2.06/2.30  (-. (c4_2 (a416) (a417)))
% 2.06/2.30  ((a405) != (a434))
% 2.06/2.30  ((a287) != zenon_X27)
% 2.06/2.30  (c4_2 (a278) (a389))
% 2.06/2.30  ((a425) != zenon_X126)
% 2.06/2.30  ((a418) != zenon_X33)
% 2.06/2.30  ((a439) != zenon_X188)
% 2.06/2.30  ((a299) != zenon_X167)
% 2.06/2.30  (c3_2 (a408) (a286))
% 2.06/2.30  (-. (c2_2 (a280) zenon_X42))
% 2.06/2.30  (-. (c6_2 (a317) zenon_X108))
% 2.06/2.30  (-. (c9_1 (a448)))
% 2.06/2.30  ((a286) != zenon_X73)
% 2.06/2.30  (c9_1 (a294))
% 2.06/2.30  ((a418) != zenon_X135)
% 2.06/2.30  (c8_2 (a395) (a389))
% 2.06/2.30  (c6_2 (a431) (a379))
% 2.06/2.30  (c6_2 zenon_X19 (a439))
% 2.06/2.30  ((a347) != zenon_X196)
% 2.06/2.30  ((a410) != (a295))
% 2.06/2.30  ((a347) != zenon_X153)
% 2.06/2.30  ((a435) != (a344))
% 2.06/2.30  (-. (c10_2 (a405) zenon_X11))
% 2.06/2.30  (-. (c5_2 (a317) (a289)))
% 2.06/2.30  (c1_1 (a332))
% 2.06/2.30  (zenon_X6 != zenon_X43)
% 2.06/2.30  (zenon_X21 != zenon_X28)
% 2.06/2.30  (c6_2 (a287) (a292))
% 2.06/2.30  (-. (c5_2 zenon_X13 (a279)))
% 2.06/2.30  ((a396) != (a379))
% 2.06/2.30  ((a409) != zenon_X163)
% 2.06/2.30  (zenon_X6 != zenon_X23)
% 2.06/2.30  (-. (c5_2 (a291) zenon_X135))
% 2.06/2.30  (-. (c5_2 (a352) (a279)))
% 2.06/2.30  (c10_2 (a291) (a292))
% 2.06/2.30  (zenon_X43 != (a332))
% 2.06/2.30  (c6_2 zenon_X16 (a347))
% 2.06/2.30  ((a317) != zenon_X18)
% 2.06/2.30  (c5_2 zenon_X23 (a299))
% 2.06/2.30  ((a271) != zenon_X31)
% 2.06/2.30  (c3_1 zenon_X39)
% 2.06/2.30  (zenon_X6 != zenon_X27)
% 2.06/2.30  ((a327) != (a424))
% 2.06/2.30  (ndr1_1 zenon_X6)
% 2.06/2.30  (zenon_X6 != zenon_X13)
% 2.06/2.30  (zenon_X1 != zenon_X30)
% 2.06/2.30  (zenon_X19 != (a444))
% 2.06/2.30  ((a289) != zenon_X137)
% 2.06/2.30  (zenon_X8 != (a444))
% 2.06/2.30  ((a319) != zenon_X21)
% 2.06/2.30  (c1_1 (a448))
% 2.06/2.30  (-. (c5_2 zenon_X8 (a389)))
% 2.06/2.30  (-. (c5_2 (a424) zenon_X106))
% 2.06/2.30  (zenon_X43 != (a327))
% 2.06/2.30  ((a396) != zenon_X79)
% 2.06/2.30  ((a294) != (a307))
% 2.06/2.30  (c6_2 (a287) (a439))
% 2.06/2.30  (c6_2 (a443) (a279))
% 2.06/2.30  (-. (c8_2 (a424) zenon_X56))
% 2.06/2.30  (c6_2 zenon_X13 (a279))
% 2.06/2.30  (-. (c1_1 zenon_X18))
% 2.06/2.30  ((a379) != zenon_X122)
% 2.06/2.30  ((a289) != zenon_X76)
% 2.06/2.30  (-. (c6_2 (a271) (a347)))
% 2.06/2.30  (c8_2 (a291) (a289))
% 2.06/2.30  ((a429) != zenon_X36)
% 2.06/2.30  (zenon_X19 != (a431))
% 2.06/2.30  (-. (c6_1 (a317)))
% 2.06/2.30  ((a395) != (a280))
% 2.06/2.30  (zenon_X25 != (a332))
% 2.06/2.30  (c3_2 zenon_X35 (a286))
% 2.06/2.30  (c6_2 (a332) (a429))
% 2.06/2.30  ((a290) != (a353))
% 2.06/2.30  ((a317) != (a424))
% 2.06/2.30  (-. (c5_2 zenon_X8 (a417)))
% 2.06/2.30  ((a289) != (a338))
% 2.06/2.30  ((a327) != zenon_X7)
% 2.06/2.30  ((a417) != (a390))
% 2.06/2.30  (c8_1 (a444))
% 2.06/2.30  ((a288) != (a410))
% 2.06/2.30  ((a425) != zenon_X75)
% 2.06/2.30  (c6_2 (a434) (a344))
% 2.06/2.30  (c1_1 (a416))
% 2.06/2.30  (c1_1 (a294))
% 2.06/2.30  (zenon_X31 != zenon_X16)
% 2.06/2.30  (c5_2 (a317) (a363))
% 2.06/2.30  ((a278) != zenon_X22)
% 2.06/2.30  (-. (c7_2 zenon_X35 zenon_X193))
% 2.06/2.30  ((a289) != zenon_X167)
% 2.06/2.30  ((a299) != zenon_X106)
% 2.06/2.30  (c6_2 zenon_X8 (a299))
% 2.06/2.30  ((a380) != zenon_X0)
% 2.06/2.30  ((a429) != zenon_X54)
% 2.06/2.30  (-. (c3_2 (a405) zenon_X172))
% 2.06/2.30  ((a279) != zenon_X76)
% 2.06/2.30  (c6_2 (a431) (a289))
% 2.06/2.30  (c3_2 (a278) (a279))
% 2.06/2.30  ((a418) != zenon_X3)
% 2.06/2.30  ((a379) != zenon_X163)
% 2.06/2.30  ((a289) != zenon_X106)
% 2.06/2.30  (c5_2 zenon_X45 (a299))
% 2.06/2.30  (c8_2 zenon_X19 (a299))
% 2.06/2.30  (zenon_X6 != zenon_X8)
% 2.06/2.30  (c6_2 (a424) (a286))
% 2.06/2.30  (c6_2 (a443) (a292))
% 2.06/2.30  ((a379) != zenon_X70)
% 2.06/2.30  ((a347) != zenon_X125)
% 2.06/2.30  (-. (c1_1 (a443)))
% 2.06/2.30  (-. (c5_2 zenon_X8 (a390)))
% 2.06/2.30  (c6_2 (a294) (a425))
% 2.06/2.30  ((a302) != zenon_X45)
% 2.06/2.30  ((a347) != zenon_X126)
% 2.06/2.30  ((a347) != zenon_X145)
% 2.06/2.30  ((a292) != zenon_X137)
% 2.06/2.30  (c6_2 (a434) (a299))
% 2.06/2.30  ((a418) != zenon_X95)
% 2.06/2.30  ((a294) != (a416))
% 2.06/2.30  ((a395) != (a307))
% 2.06/2.30  (c6_2 (a448) (a380))
% 2.06/2.30  ((a347) != zenon_X192)
% 2.06/2.30  (zenon_X41 != (a417))
% 2.06/2.30  (ndr1_1 (a287))
% 2.06/2.30  (-. (c6_2 (a317) (a370)))
% 2.06/2.30  (-. (c5_2 (a443) (a439)))
% 2.06/2.30  (-. (c1_1 (a307)))
% 2.06/2.30  (c1_1 (a280))
% 2.06/2.30  (c8_2 zenon_X43 (a389))
% 2.06/2.30  ((a409) != zenon_X2)
% 2.06/2.30  ((a289) != zenon_X90)
% 2.06/2.30  ((a279) != zenon_X55)
% 2.06/2.30  ((a347) != zenon_X121)
% 2.06/2.30  (-. (c5_2 zenon_X6 (a440)))
% 2.06/2.30  (c6_2 (a332) (a347))
% 2.06/2.30  (zenon_X39 != zenon_X8)
% 2.06/2.30  (c6_2 zenon_X35 (a347))
% 2.06/2.30  ((a379) != (a290))
% 2.06/2.30  (c6_2 (a444) (a347))
% 2.06/2.30  ((a279) != zenon_X159)
% 2.06/2.30  (c4_2 (a431) (a389))
% 2.06/2.30  ((a429) != (a440))
% 2.06/2.30  ((a286) != zenon_X192)
% 2.06/2.30  (c6_2 (a424) (a410))
% 2.06/2.30  ((a294) != zenon_X31)
% 2.06/2.30  ((a290) != zenon_X4)
% 2.06/2.30  (ndr1_1 zenon_X37)
% 2.06/2.30  ((a344) != (a299))
% 2.06/2.30  (-. (c5_2 (a416) zenon_X127))
% 2.06/2.30  (-. (c6_2 (a271) (a379)))
% 2.06/2.30  (-. (c6_2 zenon_X39 (a429)))
% 2.06/2.30  ((a405) != zenon_X7)
% 2.06/2.30  (zenon_X16 != zenon_X6)
% 2.06/2.30  (zenon_X32 != (a302))
% 2.06/2.30  (c6_2 (a434) (a409))
% 2.06/2.30  ((a443) != zenon_X28)
% 2.06/2.30  (c6_2 zenon_X28 (a286))
% 2.06/2.30  (-. (c4_1 (a448)))
% 2.06/2.30  (-. (c5_2 zenon_X35 (a439)))
% 2.06/2.30  ((a425) != zenon_X80)
% 2.06/2.30  (c6_2 (a434) (a425))
% 2.06/2.30  (-. (c10_2 (a271) (a338)))
% 2.06/2.30  (zenon_X43 != (a319))
% 2.06/2.30  (c6_2 (a280) (a410))
% 2.06/2.30  (-. (c4_2 (a444) (a379)))
% 2.06/2.30  ((a425) != zenon_X189)
% 2.06/2.30  (c3_1 (a332))
% 2.06/2.30  ((a299) != zenon_X135)
% 2.06/2.30  (-. (c7_2 (a444) (a286)))
% 2.06/2.30  (-. (c7_2 zenon_X19 (a286)))
% 2.06/2.30  ((a317) != (a352))
% 2.06/2.30  (-. (c5_2 (a307) (a279)))
% 2.06/2.30  (c7_1 (a424))
% 2.06/2.30  ((a291) != zenon_X8)
% 2.06/2.30  (c6_2 zenon_X35 (a429))
% 2.06/2.30  ((a425) != (a440))
% 2.06/2.30  ((a344) != (a380))
% 2.06/2.30  ((a389) != (a370))
% 2.06/2.30  (zenon_X18 != zenon_X45)
% 2.06/2.30  (-. (c9_1 (a352)))
% 2.06/2.30  (-. (c3_2 (a434) zenon_X69))
% 2.06/2.30  ((a409) != zenon_X30)
% 2.06/2.30  (-. (c5_2 (a294) (a290)))
% 2.06/2.30  ((a347) != zenon_X73)
% 2.06/2.30  (c6_2 (a395) (a396))
% 2.06/2.30  (-. (c2_2 (a405) (a389)))
% 2.06/2.30  ((a379) != zenon_X166)
% 2.06/2.30  ((a396) != zenon_X175)
% 2.06/2.30  (c6_2 (a369) (a425))
% 2.06/2.30  (-. (c2_2 zenon_X45 (a389)))
% 2.06/2.30  (zenon_X22 != zenon_X28)
% 2.06/2.30  (c5_2 (a287) (a289))
% 2.06/2.30  (-. (c6_2 zenon_X43 (a286)))
% 2.06/2.30  (c4_2 (a278) (a279))
% 2.06/2.30  ((a292) != zenon_X87)
% 2.06/2.30  (c5_2 (a405) (a289))
% 2.06/2.30  ((a439) != zenon_X161)
% 2.06/2.30  (-. (c1_2 zenon_X25 (a347)))
% 2.06/2.30  ((a271) != (a319))
% 2.06/2.30  (c6_2 (a416) (a347))
% 2.06/2.30  ((a292) != zenon_X82)
% 2.06/2.30  (-. (c1_2 (a327) (a390)))
% 2.06/2.30  (zenon_X35 != (a444))
% 2.06/2.30  (c7_1 (a395))
% 2.06/2.30  (zenon_X25 != (a271))
% 2.06/2.30  ((a417) != (a289))
% 2.06/2.30  (c6_2 zenon_X23 (a417))
% 2.06/2.30  ((a347) != zenon_X79)
% 2.06/2.30  (zenon_X35 != zenon_X28)
% 2.06/2.30  (c6_2 (a280) (a347))
% 2.06/2.30  (c7_2 (a280) (a379))
% 2.06/2.30  (zenon_X43 != (a294))
% 2.06/2.30  ((a299) != zenon_X90)
% 2.06/2.30  ((a380) != (a370))
% 2.06/2.30  ((a287) != (a424))
% 2.06/2.30  ((a347) != zenon_X40)
% 2.06/2.30  (-. (c1_2 (a291) (a293)))
% 2.06/2.30  (-. (c8_2 zenon_X35 (a338)))
% 2.06/2.30  ((a271) != zenon_X13)
% 2.06/2.30  (c4_2 zenon_X32 (a389))
% 2.06/2.30  (c5_2 zenon_X39 (a299))
% 2.06/2.30  (-. (c5_2 (a416) (a418)))
% 2.06/2.30  (zenon_X38 != (a286))
% 2.06/2.30  ((a439) != zenon_X125)
% 2.06/2.30  (c1_2 zenon_X18 (a440))
% 2.06/2.30  ((a417) != zenon_X124)
% 2.06/2.30  ((a299) != zenon_X85)
% 2.06/2.30  ((a389) != zenon_X77)
% 2.06/2.30  (-. (c6_2 zenon_X6 (a279)))
% 2.06/2.30  ((a448) != zenon_X27)
% 2.06/2.30  ((a271) != (a369))
% 2.06/2.30  (c6_2 (a424) (a439))
% 2.06/2.30  ((a291) != zenon_X18)
% 2.06/2.30  ((a408) != (a278))
% 2.06/2.30  (c6_2 (a405) (a417))
% 2.06/2.30  ((a435) != (a410))
% 2.06/2.30  (-. (c4_1 zenon_X31))
% 2.06/2.30  ((a299) != zenon_X88)
% 2.06/2.30  (-. (c6_2 (a271) (a425)))
% 2.06/2.30  (-. (c5_2 (a327) zenon_X26))
% 2.06/2.30  ((a448) != (a369))
% 2.06/2.30  (c4_2 (a287) (a389))
% 2.06/2.30  (c6_2 zenon_X19 (a429))
% 2.06/2.30  ((a416) != zenon_X8)
% 2.06/2.30  (c6_2 zenon_X21 (a347))
% 2.06/2.30  (c7_2 (a405) (a439))
% 2.06/2.30  ((a287) != (a369))
% 2.06/2.30  ((a405) != (a424))
% 2.06/2.30  ((a279) != zenon_X146)
% 2.06/2.30  (zenon_X25 != (a405))
% 2.06/2.30  ((a299) != zenon_X156)
% 2.06/2.30  (c3_1 zenon_X6)
% 2.06/2.30  (-. (c4_2 (a369) (a370)))
% 2.06/2.30  (c7_2 (a317) (a347))
% 2.06/2.30  (-. (c5_2 (a395) (a418)))
% 2.06/2.30  ((a418) != zenon_X82)
% 2.06/2.30  ((a302) != zenon_X27)
% 2.06/2.30  (c7_2 (a443) (a439))
% 2.06/2.30  ((a418) != zenon_X100)
% 2.06/2.30  ((a299) != zenon_X116)
% 2.06/2.30  ((a279) != zenon_X87)
% 2.06/2.30  ((a299) != zenon_X3)
% 2.06/2.30  (-. (c8_2 (a431) zenon_X77))
% 2.06/2.30  ((a405) != zenon_X8)
% 2.06/2.30  (ndr1_1 zenon_X43)
% 2.06/2.30  (-. (c5_2 (a302) (a439)))
% 2.06/2.30  ((a417) != zenon_X106)
% 2.06/2.30  (-. (c5_2 (a307) (a289)))
% 2.06/2.30  (ndr1_1 (a424))
% 2.06/2.30  ((a347) != zenon_X128)
% 2.06/2.30  (-. (c5_2 (a448) zenon_X100))
% 2.06/2.30  (zenon_X16 != zenon_X32)
% 2.06/2.30  ((a439) != zenon_X181)
% 2.06/2.30  ((a439) != zenon_X121)
% 2.06/2.30  (c3_2 (a280) (a295))
% 2.06/2.30  (zenon_X7 != (a280))
% 2.06/2.30  (-. (c9_1 (a444)))
% 2.06/2.30  (c3_1 zenon_X21)
% 2.06/2.30  ((a290) != zenon_X9)
% 2.06/2.30  (c8_2 zenon_X19 (a289))
% 2.06/2.30  (c7_2 (a294) zenon_X65)
% 2.06/2.30  ((a370) != (a290))
% 2.06/2.30  ((a410) != zenon_X2)
% 2.06/2.30  (c3_2 (a408) (a417))
% 2.06/2.30  ((a379) != zenon_X126)
% 2.06/2.30  ((a389) != zenon_X47)
% 2.06/2.30  (-. (c10_2 (a444) zenon_X2))
% 2.06/2.30  ((a417) != zenon_X192)
% 2.06/2.30  ((a418) != zenon_X85)
% 2.06/2.30  ((a417) != zenon_X174)
% 2.06/2.30  ((a293) != (a299))
% 2.06/2.30  ((a292) != (a288))
% 2.06/2.30  ((a363) != (a389))
% 2.06/2.30  (c6_2 (a332) (a279))
% 2.06/2.30  ((a389) != (a439))
% 2.06/2.30  ((a417) != zenon_X180)
% 2.06/2.30  (-. (c1_2 zenon_X35 (a347)))
% 2.06/2.30  (c8_2 (a278) (a279))
% 2.06/2.30  (-. (c3_2 (a287) zenon_X54))
% 2.06/2.30  (c6_2 (a448) (a410))
% 2.06/2.30  (c3_1 zenon_X12)
% 2.06/2.30  (c6_2 (a291) (a347))
% 2.06/2.30  ((a448) != zenon_X13)
% 2.06/2.30  (-. (c5_2 zenon_X8 (a363)))
% 2.06/2.30  (zenon_X45 != (a278))
% 2.06/2.30  (zenon_X39 != (a332))
% 2.06/2.30  (c6_2 (a434) (a429))
% 2.06/2.30  ((a279) != (a417))
% 2.06/2.30  (c6_2 zenon_X7 (a379))
% 2.06/2.30  (-. (c2_2 zenon_X21 (a389)))
% 2.06/2.30  (c6_2 zenon_X16 (a370))
% 2.06/2.30  ((a327) != zenon_X16)
% 2.06/2.30  (-. (c8_2 (a307) zenon_X90))
% 2.06/2.30  ((a448) != (a416))
% 2.06/2.30  ((a417) != (a303))
% 2.06/2.30  ((a431) != zenon_X25)
% 2.06/2.30  (-. (c3_2 (a431) zenon_X73))
% 2.06/2.30  (zenon_X16 != zenon_X39)
% 2.06/2.30  ((a417) != zenon_X73)
% 2.06/2.30  (-. (c5_2 (a434) (a289)))
% 2.06/2.30  ((a417) != zenon_X188)
% 2.06/2.30  ((a299) != zenon_X119)
% 2.06/2.30  ((a286) != zenon_X67)
% 2.06/2.30  ((a425) != zenon_X174)
% 2.06/2.30  ((a363) != (a429))
% 2.06/2.30  (zenon_X45 != (a434))
% 2.06/2.30  (-. (c8_2 zenon_X7 (a286)))
% 2.06/2.30  ((a444) != zenon_X13)
% 2.06/2.30  ((a380) != (a417))
% 2.06/2.30  (-. (c7_2 zenon_X13 (a347)))
% 2.06/2.30  (zenon_X0 != (a379))
% 2.06/2.30  (zenon_X13 != zenon_X31)
% 2.06/2.30  ((a291) != zenon_X28)
% 2.06/2.30  (-. (c7_2 zenon_X6 zenon_X153))
% 2.06/2.30  (c4_2 (a271) (a363))
% 2.06/2.30  (-. (c5_2 zenon_X21 (a439)))
% 2.06/2.30  ((a424) != zenon_X23)
% 2.06/2.30  ((a299) != zenon_X137)
% 2.06/2.30  ((a302) != zenon_X18)
% 2.06/2.30  ((a429) != zenon_X63)
% 2.06/2.30  ((a279) != (a293))
% 2.06/2.30  (c7_1 zenon_X23)
% 2.06/2.30  ((a443) != (a395))
% 2.06/2.30  ((a429) != zenon_X180)
% 2.06/2.30  (zenon_X41 != (a410))
% 2.06/2.30  ((a292) != zenon_X107)
% 2.06/2.30  ((a409) != (a380))
% 2.06/2.30  (-. (c7_2 (a444) zenon_X123))
% 2.06/2.30  (c7_1 zenon_X8)
% 2.06/2.30  ((a286) != zenon_X79)
% 2.06/2.30  (c5_2 (a448) (a389))
% 2.06/2.30  ((a347) != (a286))
% 2.06/2.30  (-. (c5_2 (a448) (a439)))
% 2.06/2.30  ((a405) != (a302))
% 2.06/2.30  ((a289) != zenon_X55)
% 2.06/2.30  (zenon_X16 != (a369))
% 2.06/2.30  (-. (c2_2 (a352) (a389)))
% 2.06/2.30  (zenon_X6 != (a443))
% 2.06/2.30  ((a279) != zenon_X95)
% 2.06/2.30  ((a290) != (a418))
% 2.06/2.30  (c1_1 (a287))
% 2.06/2.30  (zenon_X27 != zenon_X7)
% 2.06/2.30  (-. (c7_1 (a302)))
% 2.06/2.30  ((a299) != zenon_X178)
% 2.06/2.30  (c3_1 (a405))
% 2.06/2.30  ((a353) != (a288))
% 2.06/2.30  (-. (c7_2 zenon_X16 zenon_X152))
% 2.06/2.30  ((a444) != (a280))
% 2.06/2.30  (-. (c5_2 (a443) (a389)))
% 2.06/2.30  (-. (c7_2 zenon_X13 (a286)))
% 2.06/2.30  (c6_2 (a448) (a344))
% 2.06/2.30  ((a299) != zenon_X100)
% 2.06/2.30  (c6_2 (a327) (a279))
% 2.06/2.30  ((a280) != (a434))
% 2.06/2.30  ((a289) != zenon_X109)
% 2.06/2.30  (c6_2 zenon_X8 (a286))
% 2.06/2.30  ((a292) != zenon_X3)
% 2.06/2.30  ((a289) != zenon_X47)
% 2.06/2.30  ((a299) != zenon_X146)
% 2.06/2.30  (-. (c5_2 (a271) (a290)))
% 2.06/2.30  (c7_1 (a307))
% 2.06/2.30  (zenon_X32 != zenon_X13)
% 2.06/2.30  (c6_2 zenon_X6 (a440))
% 2.06/2.30  (-. (c2_2 (a352) (a353)))
% 2.06/2.30  (zenon_X21 != (a443))
% 2.06/2.30  (-. (c7_1 zenon_X18))
% 2.06/2.30  (c1_1 zenon_X35)
% 2.06/2.30  (c7_1 (a431))
% 2.06/2.30  ((a317) != zenon_X28)
% 2.06/2.30  (-. (c7_2 (a434) (a347)))
% 2.06/2.30  (zenon_X32 != (a280))
% 2.06/2.30  ((a389) != zenon_X105)
% 2.06/2.30  (-. (c1_1 (a278)))
% 2.06/2.30  ((a448) != zenon_X7)
% 2.06/2.30  (-. (c7_2 zenon_X23 zenon_X139))
% 2.06/2.30  ((a363) != (a418))
% 2.06/2.30  (zenon_X39 != (a444))
% 2.06/2.30  ((a389) != zenon_X195)
% 2.06/2.30  ((a347) != zenon_X120)
% 2.06/2.30  (zenon_X35 != (a448))
% 2.06/2.30  (c4_2 zenon_X31 (a389))
% 2.06/2.30  ((a317) != (a431))
% 2.06/2.30  (c6_1 zenon_X25)
% 2.06/2.30  (zenon_X45 != zenon_X19)
% 2.06/2.30  ((a286) != (a288))
% 2.06/2.30  (c6_2 zenon_X16 (a425))
% 2.06/2.30  (-. (c6_2 (a287) (a289)))
% 2.06/2.30  (zenon_X21 != (a307))
% 2.06/2.30  (c7_2 zenon_X21 (a439))
% 2.06/2.30  ((a290) != (a289))
% 2.06/2.30  ((a429) != zenon_X71)
% 2.06/2.30  (c7_1 zenon_X28)
% 2.06/2.30  ((a319) != (a434))
% 2.06/2.30  ((a286) != (a440))
% 2.06/2.30  ((a410) != zenon_X44)
% 2.06/2.30  (c6_2 zenon_X16 (a429))
% 2.06/2.30  ((a286) != zenon_X65)
% 2.06/2.30  (-. (c5_2 (a416) (a292)))
% 2.06/2.30  ((a286) != (a290))
% 2.06/2.30  (-. (c7_2 zenon_X13 zenon_X120))
% 2.06/2.30  (-. (c7_2 (a280) (a425)))
% 2.06/2.30  (c6_1 (a448))
% 2.06/2.30  (-. (c6_1 (a444)))
% 2.06/2.30  (zenon_X27 != (a307))
% 2.06/2.30  (c7_1 (a352))
% 2.06/2.30  ((a417) != zenon_X80)
% 2.06/2.30  ((a292) != zenon_X106)
% 2.06/2.30  (c3_1 zenon_X31)
% 2.06/2.30  ((a443) != zenon_X13)
% 2.06/2.30  ((a299) != zenon_X33)
% 2.06/2.30  (c6_2 zenon_X16 (a286))
% 2.06/2.30  (-. (c4_2 (a448) zenon_X41))
% 2.06/2.30  ((a347) != zenon_X54)
% 2.06/2.30  (zenon_X43 != (a369))
% 2.06/2.30  (c6_2 (a405) (a396))
% 2.06/2.30  (c9_0)
% 2.06/2.30  ((a279) != (a429))
% 2.06/2.30  (-. (c5_2 (a443) (a429)))
% 2.06/2.30  (-. (c9_1 zenon_X13))
% 2.15/2.30  ((a295) != zenon_X108)
% 2.15/2.30  ((a352) != zenon_X8)
% 2.15/2.30  ((a299) != zenon_X47)
% 2.15/2.30  (-. (c5_2 (a416) (a289)))
% 2.15/2.30  ((a444) != zenon_X28)
% 2.15/2.30  ((a352) != zenon_X25)
% 2.15/2.30  (zenon_X32 != zenon_X39)
% 2.15/2.30  ((a425) != zenon_X62)
% 2.15/2.30  ((a417) != zenon_X38)
% 2.15/2.30  (c10_1 (a352))
% 2.15/2.30  ((a439) != zenon_X65)
% 2.15/2.30  (-. (c1_1 zenon_X21))
% 2.15/2.30  ((a440) != (a289))
% 2.15/2.30  (zenon_X32 != zenon_X19)
% 2.15/2.30  ((a417) != (a425))
% 2.15/2.30  (c7_2 zenon_X7 (a439))
% 2.15/2.30  (-. (c7_2 (a280) (a439)))
% 2.15/2.30  (c6_1 (a278))
% 2.15/2.30  ((a271) != (a424))
% 2.15/2.30  (-. (c6_2 zenon_X43 (a440)))
% 2.15/2.30  ((a279) != (a292))
% 2.15/2.30  ((a431) != (a369))
% 2.15/2.30  ((a294) != zenon_X22)
% 2.15/2.30  ((a289) != (a370))
% 2.15/2.30  (c6_2 zenon_X7 (a347))
% 2.15/2.30  (-. (c4_2 zenon_X35 (a425)))
% 2.15/2.30  (zenon_X16 != zenon_X28)
% 2.15/2.30  (-. (c5_2 (a291) (a290)))
% 2.15/2.30  (-. (c8_2 zenon_X45 zenon_X146))
% 2.15/2.30  (zenon_X35 != (a405))
% 2.15/2.30  (-. (c5_2 (a395) (a292)))
% 2.15/2.30  (c6_2 zenon_X13 (a286))
% 2.15/2.30  (zenon_X19 != (a332))
% 2.15/2.30  (zenon_X7 != zenon_X13)
% 2.15/2.30  ((a417) != zenon_X122)
% 2.15/2.30  (-. (c7_2 (a424) (a439)))
% 2.15/2.30  ((a396) != zenon_X68)
% 2.15/2.30  ((a363) != (a293))
% 2.15/2.30  (-. (c6_2 (a317) (a295)))
% 2.15/2.30  (-. (c6_2 zenon_X43 (a429)))
% 2.15/2.30  (-. (c7_2 (a271) (a379)))
% 2.15/2.30  (c6_2 (a287) (a379))
% 2.15/2.30  (c5_2 (a302) (a389))
% 2.15/2.30  ((a448) != (a307))
% 2.15/2.30  ((a302) != (a369))
% 2.15/2.30  (c6_2 zenon_X39 (a286))
% 2.15/2.30  (c2_2 (a444) (a389))
% 2.15/2.30  (c6_2 (a448) (a347))
% 2.15/2.30  (-. (c1_2 (a443) (a390)))
% 2.15/2.30  ((a288) != zenon_X0)
% 2.15/2.30  (-. (c10_2 (a280) zenon_X40))
% 2.15/2.30  (zenon_X19 != (a327))
% 2.15/2.30  ((a363) != (a396))
% 2.15/2.30  ((a287) != (a332))
% 2.15/2.30  (c6_2 (a434) (a410))
% 2.15/2.30  ((a439) != (a288))
% 2.15/2.30  ((a395) != zenon_X45)
% 2.15/2.30  ((a425) != zenon_X122)
% 2.15/2.30  ((a379) != zenon_X73)
% 2.15/2.30  (zenon_X31 != (a307))
% 2.15/2.30  (c6_2 zenon_X28 (a439))
% 2.15/2.30  (zenon_X43 != (a431))
% 2.15/2.30  (-. (c8_2 (a317) (a338)))
% 2.15/2.30  ((a292) != zenon_X110)
% 2.15/2.30  (zenon_X35 != (a434))
% 2.15/2.30  (c6_2 (a278) (a425))
% 2.15/2.30  (-. (c4_2 zenon_X35 (a429)))
% 2.15/2.30  (zenon_X32 != zenon_X18)
% 2.15/2.30  ((a439) != (a299))
% 2.15/2.30  ((a317) != zenon_X8)
% 2.15/2.30  ((a389) != (a440))
% 2.15/2.30  ((a289) != zenon_X101)
% 2.15/2.30  (-. (c6_2 zenon_X6 (a347)))
% 2.15/2.30  (-. (c10_2 (a319) zenon_X29))
% 2.15/2.30  ((a271) != zenon_X21)
% 2.15/2.30  (c6_2 (a424) (a380))
% 2.15/2.30  (-. (c8_2 zenon_X21 zenon_X159))
% 2.15/2.30  (c5_2 zenon_X25 (a389))
% 2.15/2.30  ((a327) != (a395))
% 2.15/2.30  (zenon_X16 != (a424))
% 2.15/2.30  (-. (c9_1 (a424)))
% 2.15/2.30  ((a417) != (a440))
% 2.15/2.30  (-. (c9_2 (a443) (a299)))
% 2.15/2.30  ((a278) != (a307))
% 2.15/2.30  (-. (c8_2 (a444) zenon_X78))
% 2.15/2.30  (c6_2 (a280) (a439))
% 2.15/2.30  (-. (c5_2 zenon_X13 (a292)))
% 2.15/2.30  (zenon_X18 != zenon_X43)
% 2.15/2.30  (-. (c5_2 (a424) (a418)))
% 2.15/2.30  ((a379) != zenon_X188)
% 2.15/2.30  (zenon_X35 != zenon_X16)
% 2.15/2.30  ((a294) != (a352))
% 2.15/2.30  ((a424) != zenon_X13)
% 2.15/2.30  ((a307) != zenon_X7)
% 2.15/2.30  ((a317) != (a319))
% 2.15/2.30  ((a294) != zenon_X27)
% 2.15/2.30  (-. (c5_2 (a327) (a290)))
% 2.15/2.30  (-. (c7_2 (a369) (a347)))
% 2.15/2.30  (c6_2 (a278) (a286))
% 2.15/2.30  ((a379) != zenon_X174)
% 2.15/2.30  (c6_2 (a416) (a425))
% 2.15/2.30  (c3_2 (a271) (a347))
% 2.15/2.30  (c6_2 (a307) (a396))
% 2.15/2.30  ((a439) != zenon_X112)
% 2.15/2.30  (-. (c5_2 (a317) (a292)))
% 2.15/2.30  (zenon_X39 != zenon_X28)
% 2.15/2.30  ((a410) != zenon_X24)
% 2.15/2.30  (c6_2 (a431) (a290))
% 2.15/2.30  (c6_2 (a332) (a344))
% 2.15/2.30  (zenon_X6 != (a352))
% 2.15/2.30  ((a302) != (a317))
% 2.15/2.30  (zenon_X43 != zenon_X7)
% 2.15/2.30  ((a299) != (a303))
% 2.15/2.30  (c7_1 (a332))
% 2.15/2.30  (zenon_X35 != (a416))
% 2.15/2.30  ((a293) != zenon_X166)
% 2.15/2.30  ((a429) != zenon_X175)
% 2.15/2.30  (ndr1_1 (a444))
% 2.15/2.30  (c5_2 (a327) (a418))
% 2.15/2.30  ((a291) != (a434))
% 2.15/2.30  (c6_2 (a307) (a425))
% 2.15/2.30  (-. (c6_2 zenon_X6 (a417)))
% 2.15/2.30  ((a379) != (a299))
% 2.15/2.30  (-. (c5_2 (a327) (a363)))
% 2.15/2.30  ((a429) != zenon_X79)
% 2.15/2.30  (-. (c9_1 (a319)))
% 2.15/2.30  ((a287) != (a416))
% 2.15/2.30  (-. (c8_2 (a332) zenon_X85))
% 2.15/2.30  (zenon_X35 != zenon_X27)
% 2.15/2.30  (zenon_X16 != (a278))
% 2.15/2.30  (zenon_X45 != (a416))
% 2.15/2.30  ((a444) != zenon_X31)
% 2.15/2.30  (zenon_X25 != (a327))
% 2.15/2.30  ((a396) != zenon_X70)
% 2.15/2.30  (-. (c5_2 (a332) (a418)))
% 2.15/2.30  ((a294) != zenon_X23)
% 2.15/2.30  (c6_2 (a302) (a286))
% 2.15/2.30  (zenon_X45 != zenon_X28)
% 2.15/2.30  (c7_2 zenon_X22 (a439))
% 2.15/2.30  (-. (c5_2 (a271) (a289)))
% 2.15/2.30  (c6_2 (a332) (a289))
% 2.15/2.30  ((a390) != (a370))
% 2.15/2.30  (-. (c9_1 zenon_X16))
% 2.15/2.30  (zenon_X7 != (a444))
% 2.15/2.30  ((a292) != zenon_X103)
% 2.15/2.30  (c9_1 (a291))
% 2.15/2.30  (-. (c7_2 (a369) (a439)))
% 2.15/2.30  (zenon_X45 != (a424))
% 2.15/2.30  ((a425) != zenon_X108)
% 2.15/2.30  (zenon_X18 != zenon_X22)
% 2.15/2.30  (-. (c10_1 zenon_X16))
% 2.15/2.30  ((a299) != (a290))
% 2.15/2.30  (c6_2 (a424) (a379))
% 2.15/2.30  (-. (c9_1 zenon_X21))
% 2.15/2.30  ((a443) != zenon_X23)
% 2.15/2.30  ((a396) != zenon_X181)
% 2.15/2.30  (c10_2 zenon_X18 (a347))
% 2.15/2.30  (-. (c7_2 (a302) (a286)))
% 2.15/2.30  ((a417) != zenon_X53)
% 2.15/2.30  (-. (c2_2 (a302) (a389)))
% 2.15/2.30  (-. (c6_2 zenon_X39 (a440)))
% 2.15/2.30  ((a292) != zenon_X86)
% 2.15/2.30  (c6_2 (a332) (a292))
% 2.15/2.30  (zenon_X6 != (a294))
% 2.15/2.30  (-. (c7_2 zenon_X21 (a286)))
% 2.15/2.30  ((a289) != zenon_X110)
% 2.15/2.30  (c6_2 zenon_X13 (a347))
% 2.15/2.30  (zenon_X25 != zenon_X16)
% 2.15/2.30  ((a418) != zenon_X26)
% 2.15/2.30  ((a343) != (a327))
% 2.15/2.30  (c5_2 (a369) (a299))
% 2.15/2.30  (c5_2 zenon_X27 (a299))
% 2.15/2.30  ((a418) != (a409))
% 2.15/2.30  (c5_2 (a291) (a289))
% 2.15/2.30  (ndr1_1 zenon_X27)
% 2.15/2.30  ((a279) != (a410))
% 2.15/2.30  (c3_1 (a369))
% 2.15/2.30  (ndr1_1 zenon_X13)
% 2.15/2.30  (-. (c5_2 zenon_X13 (a418)))
% 2.15/2.30  (c6_2 zenon_X16 (a417))
% 2.15/2.30  (zenon_X19 != (a424))
% 2.15/2.30  (zenon_X6 != (a444))
% 2.15/2.30  (ndr1_1 zenon_X25)
% 2.15/2.30  ((a278) != (a302))
% 2.15/2.30  ((a431) != zenon_X7)
% 2.15/2.30  (-. (c7_2 (a416) zenon_X124))
% 2.15/2.30  (c6_2 (a291) (a292))
% 2.15/2.30  ((a295) != zenon_X190)
% 2.15/2.30  (c8_2 zenon_X35 (a363))
% 2.15/2.30  ((a347) != (a290))
% 2.15/2.30  ((a299) != (a440))
% 2.15/2.30  (c7_1 (a405))
% 2.15/2.30  ((a292) != zenon_X108)
% 2.15/2.30  ((a289) != zenon_X116)
% 2.15/2.30  (c6_2 (a327) (a299))
% 2.15/2.30  (c9_1 (a443))
% 2.15/2.30  ((a429) != zenon_X145)
% 2.15/2.30  ((a319) != zenon_X23)
% 2.15/2.30  ((a294) != zenon_X7)
% 2.15/2.30  ((a294) != zenon_X16)
% 2.15/2.30  ((a417) != zenon_X10)
% 2.15/2.30  (c6_2 (a352) (a429))
% 2.15/2.30  (c6_2 (a291) (a439))
% 2.15/2.30  (-. (c8_2 (a443) (a429)))
% 2.15/2.30  (c8_2 zenon_X19 (a292))
% 2.15/2.30  (-. (c9_1 zenon_X27))
% 2.15/2.30  (c6_2 zenon_X13 (a439))
% 2.15/2.30  (-. (c10_1 (a332)))
% 2.15/2.30  ((a390) != (a435))
% 2.15/2.30  ((a291) != zenon_X7)
% 2.15/2.30  (zenon_X31 != zenon_X25)
% 2.15/2.30  ((a317) != (a444))
% 2.15/2.30  ((a299) != zenon_X155)
% 2.15/2.30  (zenon_X32 != (a319))
% 2.15/2.30  (-. (c5_0))
% 2.15/2.30  (c7_1 (a287))
% 2.15/2.30  ((a395) != zenon_X7)
% 2.15/2.30  ((a317) != zenon_X32)
% 2.15/2.30  (c6_2 zenon_X7 (a417))
% 2.15/2.30  (-. (c6_1 (a434)))
% 2.15/2.30  (c2_2 (a408) (a410))
% 2.15/2.30  ((a417) != zenon_X90)
% 2.15/2.30  ((a370) != zenon_X108)
% 2.15/2.30  (-. (c6_1 zenon_X13))
% 2.15/2.30  ((a431) != zenon_X27)
% 2.15/2.30  (zenon_X18 != zenon_X28)
% 2.15/2.30  ((a299) != zenon_X170)
% 2.15/2.30  (zenon_X43 != zenon_X23)
% 2.15/2.30  ((a418) != (a439))
% 2.15/2.30  (c6_2 (a444) (a396))
% 2.15/2.30  ((a380) != zenon_X70)
% 2.15/2.30  (c4_1 zenon_X43)
% 2.15/2.30  (c6_2 (a332) (a417))
% 2.15/2.30  (c8_2 (a287) (a290))
% 2.15/2.30  ((a439) != zenon_X145)
% 2.15/2.30  ((a439) != (a440))
% 2.15/2.30  (zenon_X22 != (a319))
% 2.15/2.30  (c6_2 (a332) (a379))
% 2.15/2.30  ((a379) != zenon_X108)
% 2.15/2.30  (c7_2 zenon_X35 (a347))
% 2.15/2.30  (zenon_X45 != (a444))
% 2.15/2.30  (zenon_X35 != (a302))
% 2.15/2.30  (c7_2 (a443) (a429))
% 2.15/2.30  (c6_2 (a280) (a425))
% 2.15/2.30  ((a425) != (a286))
% 2.15/2.30  (-. (c3_2 (a280) zenon_X79))
% 2.15/2.30  (-. (c10_1 (a395)))
% 2.15/2.30  ((a347) != zenon_X61)
% 2.15/2.30  (-. (c5_2 zenon_X31 (a429)))
% 2.15/2.30  ((a431) != zenon_X45)
% 2.15/2.30  (c9_1 zenon_X31)
% 2.15/2.30  (-. (c7_2 (a332) (a417)))
% 2.15/2.30  (c6_2 zenon_X32 (a439))
% 2.15/2.30  (c5_1 (a343))
% 2.15/2.30  (-. (c3_2 zenon_X13 zenon_X177))
% 2.15/2.30  (-. (c6_2 (a317) (a439)))
% 2.15/2.30  ((a299) != zenon_X138)
% 2.15/2.30  (c6_2 zenon_X23 (a370))
% 2.15/2.30  (c6_2 (a395) (a425))
% 2.15/2.30  (zenon_X6 != zenon_X28)
% 2.15/2.30  ((a299) != zenon_X26)
% 2.15/2.30  ((a347) != zenon_X80)
% 2.15/2.30  ((a307) != (a352))
% 2.15/2.30  ((a286) != zenon_X10)
% 2.15/2.30  (zenon_X43 != (a278))
% 2.15/2.30  (ndr1_1 zenon_X8)
% 2.15/2.30  (c6_2 (a448) (a425))
% 2.15/2.30  (-. (c6_1 zenon_X39))
% 2.15/2.30  ((a279) != zenon_X172)
% 2.15/2.30  (-. (c8_2 zenon_X32 (a286)))
% 2.15/2.30  (c4_1 zenon_X45)
% 2.15/2.30  (-. (c1_1 zenon_X25))
% 2.15/2.30  ((a299) != zenon_X49)
% 2.15/2.30  (c7_2 zenon_X22 (a429))
% 2.15/2.30  ((a390) != (a290))
% 2.15/2.30  (ndr1_1 (a332))
% 2.15/2.30  (zenon_X6 != (a307))
% 2.15/2.30  (-. (c5_2 zenon_X8 (a279)))
% 2.15/2.30  ((a425) != zenon_X79)
% 2.15/2.30  ((a417) != zenon_X190)
% 2.15/2.30  (-. (c1_0))
% 2.15/2.30  ((a443) != zenon_X27)
% 2.15/2.30  (c4_1 zenon_X22)
% 2.15/2.30  (-. (c5_2 (a416) (a290)))
% 2.15/2.30  (c10_1 (a431))
% 2.15/2.30  (ndr1_1 zenon_X16)
% 2.15/2.30  (c7_2 zenon_X16 (a347))
% 2.15/2.30  ((a439) != zenon_X124)
% 2.15/2.30  ((a271) != (a352))
% 2.15/2.30  (-. (c8_2 (a405) (a286)))
% 2.15/2.30  ((a288) != (a379))
% 2.15/2.30  (zenon_X7 != (a424))
% 2.15/2.30  ((a289) != zenon_X87)
% 2.15/2.30  (c5_2 (a291) (a299))
% 2.15/2.30  (-. (c1_1 zenon_X45))
% 2.15/2.30  (zenon_X35 != zenon_X19)
% 2.15/2.30  (c6_2 zenon_X23 (a425))
% 2.15/2.30  ((a410) != zenon_X163)
% 2.15/2.30  (-. (c10_1 zenon_X7))
% 2.15/2.30  ((a417) != zenon_X95)
% 2.15/2.30  ((a370) != (a440))
% 2.15/2.30  (-. (c8_2 (a327) zenon_X86))
% 2.15/2.30  (c6_2 (a352) (a347))
% 2.15/2.30  (c7_2 (a294) (a286))
% 2.15/2.30  (-. (c7_2 zenon_X28 zenon_X148))
% 2.15/2.30  ((a347) != zenon_X181)
% 2.15/2.30  (zenon_X31 != (a369))
% 2.15/2.30  (c8_2 (a317) (a363))
% 2.15/2.30  (c6_2 (a416) (a429))
% 2.15/2.30  ((a295) != zenon_X79)
% 2.15/2.30  (c6_2 (a307) (a418))
% 2.15/2.30  (c6_2 (a444) (a289))
% 2.15/2.30  (-. (c3_2 (a352) zenon_X63))
% 2.15/2.30  (-. (c6_2 (a271) (a396)))
% 2.15/2.30  (zenon_X19 != (a307))
% 2.15/2.30  ((a417) != (a290))
% 2.15/2.30  (c5_2 (a405) (a292))
% 2.15/2.30  (c9_2 (a395) (a396))
% 2.15/2.30  (-. (c6_2 zenon_X39 zenon_X192))
% 2.15/2.30  (c4_1 (a302))
% 2.15/2.30  (-. (c1_1 zenon_X31))
% 2.15/2.30  ((a294) != zenon_X21)
% 2.15/2.30  (c6_2 (a352) (a353))
% 2.15/2.30  (zenon_X38 != (a338))
% 2.15/2.30  ((a418) != zenon_X97)
% 2.15/2.30  ((a444) != (a302))
% 2.15/2.30  (c6_2 zenon_X8 (a379))
% 2.15/2.30  (zenon_X39 != (a431))
% 2.15/2.30  ((a389) != zenon_X9)
% 2.15/2.30  (c3_2 zenon_X27 (a347))
% 2.15/2.30  (-. (c5_2 (a291) (a292)))
% 2.15/2.30  (-. (c8_2 (a287) zenon_X48))
% 2.15/2.30  ((a405) != zenon_X28)
% 2.15/2.30  (-. (c9_1 zenon_X28))
% 2.15/2.30  (-. (c4_1 (a395)))
% 2.15/2.30  (c5_2 (a287) (a290))
% 2.15/2.30  (c7_2 zenon_X31 (a429))
% 2.15/2.30  ((a327) != zenon_X23)
% 2.15/2.30  (-. (c7_2 (a271) zenon_X121))
% 2.15/2.30  (c6_2 zenon_X35 (a379))
% 2.15/2.30  ((a417) != zenon_X4)
% 2.15/2.30  (zenon_X45 != (a443))
% 2.15/2.30  (c6_2 zenon_X35 (a370))
% 2.15/2.30  (-. (c7_2 (a332) (a439)))
% 2.15/2.30  (-. (c4_1 (a287)))
% 2.15/2.30  ((a292) != zenon_X171)
% 2.15/2.30  (-. (c5_2 (a271) (a279)))
% 2.15/2.30  ((a271) != zenon_X22)
% 2.15/2.30  ((a431) != (a302))
% 2.15/2.30  (zenon_X35 != (a291))
% 2.15/2.30  (c6_2 (a444) (a286))
% 2.15/2.30  (-. (c5_2 (a280) (a290)))
% 2.15/2.30  (-. (c5_2 (a443) (a418)))
% 2.15/2.30  ((a352) != (a332))
% 2.15/2.30  ((a299) != zenon_X59)
% 2.15/2.30  (c6_2 (a280) (a417))
% 2.15/2.30  ((a410) != zenon_X69)
% 2.15/2.30  (c4_2 zenon_X25 (a389))
% 2.15/2.30  (c3_1 zenon_X35)
% 2.15/2.30  (-. (c3_2 zenon_X23 zenon_X187))
% 2.15/2.30  ((a347) != zenon_X70)
% 2.15/2.30  ((a299) != zenon_X5)
% 2.15/2.30  ((a279) != zenon_X20)
% 2.15/2.30  ((a293) != zenon_X53)
% 2.15/2.30  (c3_2 (a408) (a425))
% 2.15/2.30  (-. (c8_2 zenon_X27 zenon_X156))
% 2.15/2.30  (-. (c6_2 (a317) (a286)))
% 2.15/2.30  ((a396) != zenon_X172)
% 2.15/2.30  (zenon_X18 != (a405))
% 2.15/2.30  ((a429) != (a286))
% 2.15/2.30  (-. (c5_2 (a443) (a292)))
% 2.15/2.30  (-. (c7_2 (a424) (a286)))
% 2.15/2.30  (zenon_X6 != (a448))
% 2.15/2.30  ((a299) != (a418))
% 2.15/2.30  (c3_1 zenon_X45)
% 2.15/2.30  (c6_2 zenon_X21 (a279))
% 2.15/2.30  ((a347) != zenon_X52)
% 2.15/2.30  (c3_1 (a302))
% 2.15/2.30  ((a410) != (a338))
% 2.15/2.30  ((a279) != (a286))
% 2.15/2.30  (c4_0)
% 2.15/2.30  (c9_1 (a287))
% 2.15/2.30  ((a418) != zenon_X4)
% 2.15/2.30  (-. (c5_2 (a444) (a279)))
% 2.15/2.30  (-. (c9_1 zenon_X19))
% 2.15/2.30  (-. (c2_1 (a369)))
% 2.15/2.30  ((a307) != zenon_X28)
% 2.15/2.30  (-. (c8_2 (a416) (a286)))
% 2.15/2.30  ((a429) != zenon_X53)
% 2.15/2.30  ((a443) != (a424))
% 2.15/2.30  (c6_2 (a424) (a299))
% 2.15/2.30  ((a291) != zenon_X23)
% 2.15/2.30  (c6_2 (a448) (a286))
% 2.15/2.30  (c5_1 (a317))
% 2.15/2.30  (-. (c2_2 zenon_X31 (a389)))
% 2.15/2.30  ((a289) != zenon_X85)
% 2.15/2.30  (zenon_X41 != (a370))
% 2.15/2.30  (c6_2 zenon_X22 (a440))
% 2.15/2.30  ((a302) != zenon_X13)
% 2.15/2.30  (zenon_X35 != zenon_X45)
% 2.15/2.30  ((a344) != zenon_X42)
% 2.15/2.30  ((a319) != (a416))
% 2.15/2.30  ((a405) != (a444))
% 2.15/2.30  (c5_2 zenon_X19 (a299))
% 2.15/2.30  (c6_2 zenon_X21 (a425))
% 2.15/2.30  ((a271) != zenon_X18)
% 2.15/2.30  (-. (c5_2 zenon_X19 zenon_X171))
% 2.15/2.30  ((a439) != zenon_X194)
% 2.15/2.30  ((a343) != zenon_X17)
% 2.15/2.30  (ndr1_1 (a280))
% 2.15/2.30  ((a294) != zenon_X25)
% 2.15/2.30  ((a425) != (a347))
% 2.15/2.30  (c7_2 (a294) (a417))
% 2.15/2.30  ((a290) != zenon_X82)
% 2.15/2.30  (-. (c6_1 zenon_X35))
% 2.15/2.30  ((a289) != zenon_X103)
% 2.15/2.30  (c8_2 (a431) (a389))
% 2.15/2.30  ((a425) != zenon_X166)
% 2.15/2.30  ((a429) != zenon_X38)
% 2.15/2.30  (c2_2 (a444) zenon_X42)
% 2.15/2.30  (c6_2 (a434) (a279))
% 2.15/2.30  (c2_2 (a444) (a380))
% 2.15/2.30  ((a290) != zenon_X95)
% 2.15/2.30  ((a396) != zenon_X164)
% 2.15/2.30  (c4_1 (a319))
% 2.15/2.30  (c6_2 (a395) (a417))
% 2.15/2.30  (-. (c5_2 (a395) (a299)))
% 2.15/2.30  ((a289) != zenon_X81)
% 2.15/2.30  ((a279) != zenon_X50)
% 2.15/2.30  (c6_2 (a280) (a396))
% 2.15/2.30  (zenon_X43 != (a434))
% 2.15/2.30  ((a279) != zenon_X192)
% 2.15/2.30  (c3_2 (a408) (a379))
% 2.15/2.30  ((a363) != (a379))
% 2.15/2.30  ((a289) != zenon_X108)
% 2.15/2.30  (-. (c5_2 (a431) (a279)))
% 2.15/2.30  ((a395) != zenon_X13)
% 2.15/2.30  ((a429) != zenon_X181)
% 2.15/2.30  (c7_2 (a294) (a425))
% 2.15/2.30  ((a439) != zenon_X164)
% 2.15/2.30  (c4_2 (a294) (a389))
% 2.15/2.30  ((a287) != zenon_X8)
% 2.15/2.30  (-. (c5_2 (a294) (a279)))
% 2.15/2.30  (c5_2 zenon_X21 (a389))
% 2.15/2.30  ((a379) != zenon_X180)
% 2.15/2.30  ((a435) != (a290))
% 2.15/2.30  ((a389) != (a429))
% 2.15/2.30  ((a279) != zenon_X9)
% 2.15/2.30  ((a396) != zenon_X62)
% 2.15/2.30  (zenon_X6 != zenon_X31)
% 2.15/2.30  (c6_2 (a278) (a347))
% 2.15/2.30  (-. (c2_2 (a278) zenon_X44))
% 2.15/2.30  (zenon_X45 != (a319))
% 2.15/2.30  (-. (c8_2 (a278) zenon_X49))
% 2.15/2.30  (-. (c7_2 (a278) (a286)))
% 2.15/2.30  ((a424) != (a332))
% 2.15/2.30  (c6_2 (a291) (a429))
% 2.15/2.30  (c3_1 zenon_X28)
% 2.15/2.30  (c10_2 (a302) (a347))
% 2.15/2.30  (c6_1 (a291))
% 2.15/2.30  ((a425) != zenon_X180)
% 2.15/2.30  (zenon_X35 != (a443))
% 2.15/2.30  ((a279) != zenon_X107)
% 2.15/2.30  (c6_2 (a307) (a379))
% 2.15/2.30  (ndr1_1 zenon_X7)
% 2.15/2.30  (-. (c5_2 (a294) (a439)))
% 2.15/2.30  (c6_2 zenon_X28 (a429))
% 2.15/2.30  ((a292) != zenon_X33)
% 2.15/2.30  (c5_2 zenon_X25 (a299))
% 2.15/2.30  ((a396) != (a299))
% 2.15/2.30  ((a291) != zenon_X45)
% 2.15/2.30  (c6_2 (a405) (a425))
% 2.15/2.30  (-. (c6_2 (a271) (a295)))
% 2.15/2.30  (-. (c7_2 (a271) (a425)))
% 2.15/2.30  (zenon_X6 != (a424))
% 2.15/2.30  (zenon_X6 != (a395))
% 2.15/2.30  (-. (c9_1 (a395)))
% 2.15/2.30  ((a418) != zenon_X20)
% 2.15/2.30  ((a294) != zenon_X45)
% 2.15/2.30  ((a343) != (a424))
% 2.15/2.30  (c5_2 zenon_X28 (a299))
% 2.15/2.30  ((a370) != zenon_X190)
% 2.15/2.30  (-. (c7_2 (a332) (a379)))
% 2.15/2.30  ((a443) != (a369))
% 2.15/2.30  (-. (c6_2 zenon_X43 zenon_X166))
% 2.15/2.30  ((a347) != zenon_X10)
% 2.15/2.30  ((a417) != zenon_X86)
% 2.15/2.30  ((a405) != zenon_X13)
% 2.15/2.30  (zenon_X6 != zenon_X7)
% 2.15/2.30  ((a299) != zenon_X176)
% 2.15/2.30  ((a289) != zenon_X97)
% 2.15/2.30  (-. (c7_2 (a434) (a286)))
% 2.15/2.30  (c6_2 (a307) (a279))
% 2.15/2.30  ((a431) != (a448))
% 2.15/2.30  ((a319) != zenon_X28)
% 2.15/2.30  (c6_1 (a431))
% 2.15/2.30  ((a290) != zenon_X105)
% 2.15/2.30  ((a408) != (a405))
% 2.15/2.30  ((a352) != (a280))
% 2.15/2.30  (-. (c5_2 (a416) zenon_X9))
% 2.15/2.30  (-. (c10_1 zenon_X28))
% 2.15/2.30  (c6_2 (a327) (a292))
% 2.15/2.30  (-. (c4_1 zenon_X28))
% 2.15/2.30  (-. (c7_2 zenon_X43 (a338)))
% 2.15/2.30  ((a440) != (a380))
% 2.15/2.30  ((a439) != zenon_X177)
% 2.15/2.30  ((a389) != zenon_X0)
% 2.15/2.30  ((a389) != zenon_X33)
% 2.15/2.30  (-. (c5_2 (a431) zenon_X105))
% 2.15/2.30  ((a291) != zenon_X32)
% 2.15/2.30  ((a417) != zenon_X52)
% 2.15/2.30  ((a409) != (a353))
% 2.15/2.30  (c4_2 (a434) (a435))
% 2.15/2.30  (-. (c5_2 zenon_X22 (a440)))
% 2.15/2.30  ((a299) != zenon_X108)
% 2.15/2.30  ((a278) != zenon_X28)
% 2.15/2.30  (zenon_X18 != (a434))
% 2.15/2.30  ((a295) != zenon_X166)
% 2.15/2.30  ((a395) != (a317))
% 2.15/2.30  ((a444) != zenon_X34)
% 2.15/2.30  ((a291) != (a332))
% 2.15/2.30  (-. (c8_1 (a343)))
% 2.15/2.30  ((a278) != (a443))
% 2.15/2.30  ((a380) != zenon_X69)
% 2.15/2.30  ((a347) != zenon_X148)
% 2.15/2.30  (c6_2 (a416) (a439))
% 2.15/2.30  (-. (c6_2 zenon_X6 (a370)))
% 2.15/2.30  (-. (c5_2 zenon_X43 (a279)))
% 2.15/2.30  (-. (c6_1 (a424)))
% 2.15/2.30  ((a417) != zenon_X184)
% 2.15/2.30  (-. (c5_2 (a352) (a299)))
% 2.15/2.30  (c6_1 (a327))
% 2.15/2.30  ((a418) != zenon_X137)
% 2.15/2.30  (c3_1 (a416))
% 2.15/2.30  ((a425) != zenon_X70)
% 2.15/2.30  ((a417) != zenon_X54)
% 2.15/2.30  (ndr1_1 (a448))
% 2.15/2.30  (-. (c7_2 (a395) (a286)))
% 2.15/2.30  (-. (c1_2 zenon_X6 (a347)))
% 2.15/2.30  (-. (c6_2 zenon_X43 (a370)))
% 2.15/2.30  (c6_2 zenon_X7 (a286))
% 2.15/2.30  ((a440) != (a435))
% 2.15/2.30  ((a347) != zenon_X189)
% 2.15/2.30  (-. (c8_1 (a352)))
% 2.15/2.30  (zenon_X21 != zenon_X19)
% 2.15/2.30  ((a279) != zenon_X68)
% 2.15/2.30  ((a347) != zenon_X69)
% 2.15/2.30  (c6_2 zenon_X23 (a396))
% 2.15/2.30  ((a395) != zenon_X19)
% 2.15/2.30  (c8_2 zenon_X32 (a299))
% 2.15/2.30  (c9_2 (a444) (a409))
% 2.15/2.30  (zenon_X27 != zenon_X28)
% 2.15/2.30  (c8_2 (a294) (a389))
% 2.15/2.30  ((a290) != (a409))
% 2.15/2.30  (c8_2 (a416) (a418))
% 2.15/2.30  ((a289) != zenon_X3)
% 2.15/2.30  (zenon_X19 != zenon_X8)
% 2.15/2.30  (-. (c8_2 zenon_X23 zenon_X155))
% 2.15/2.30  (c3_1 (a444))
% 2.15/2.30  (c4_2 (a317) (a363))
% 2.15/2.30  ((a370) != zenon_X192)
% 2.15/2.30  (-. (c7_2 (a424) (a417)))
% 2.15/2.30  ((a347) != zenon_X68)
% 2.15/2.30  (c4_2 (a287) (a288))
% 2.15/2.30  ((a299) != zenon_X20)
% 2.15/2.30  (-. (c8_2 (a443) zenon_X87))
% 2.15/2.30  (c6_2 (a416) (a289))
% 2.15/2.30  ((a389) != zenon_X135)
% 2.15/2.30  ((a363) != (a292))
% 2.15/2.30  (c5_2 (a431) (a389))
% 2.15/2.30  (c10_2 (a408) (a410))
% 2.15/2.30  (c2_2 (a444) zenon_X44)
% 2.15/2.30  (-. (c5_2 zenon_X43 (a418)))
% 2.15/2.30  ((a440) != (a295))
% 2.15/2.30  ((a271) != (a448))
% 2.15/2.30  (-. (c7_2 (a327) (a286)))
% 2.15/2.30  (zenon_X35 != zenon_X22)
% 2.15/2.30  (-. (c7_2 (a434) zenon_X65))
% 2.15/2.30  (zenon_X6 != zenon_X25)
% 2.15/2.30  ((a292) != (a338))
% 2.15/2.30  ((a291) != (a280))
% 2.15/2.30  (c6_2 zenon_X21 (a396))
% 2.15/2.30  (-. (c6_2 (a317) (a347)))
% 2.15/2.30  ((a425) != zenon_X61)
% 2.15/2.30  (c6_2 zenon_X28 (a425))
% 2.15/2.30  (zenon_X6 != zenon_X19)
% 2.15/2.30  (c6_2 (a395) (a370))
% 2.15/2.30  ((a425) != zenon_X187)
% 2.15/2.30  (-. (c5_2 (a271) (a417)))
% 2.15/2.30  ((a425) != zenon_X52)
% 2.15/2.30  (-. (c5_2 (a443) (a279)))
% 2.15/2.30  (c9_1 zenon_X6)
% 2.15/2.30  (c6_2 (a448) (a279))
% 2.15/2.30  ((a431) != zenon_X22)
% 2.15/2.30  ((a410) != zenon_X40)
% 2.15/2.30  ((a299) != (a292))
% 2.15/2.30  (-. (c5_2 (a294) (a418)))
% 2.15/2.30  ((a292) != zenon_X78)
% 2.15/2.30  ((a418) != zenon_X171)
% 2.15/2.30  (zenon_X32 != zenon_X28)
% 2.15/2.30  ((a291) != zenon_X13)
% 2.15/2.30  ((a444) != (a352))
% 2.15/2.30  ((a417) != zenon_X78)
% 2.15/2.30  ((a299) != zenon_X76)
% 2.15/2.30  ((a295) != zenon_X112)
% 2.15/2.30  (zenon_X32 != (a395))
% 2.15/2.30  (-. (c7_2 (a369) zenon_X128))
% 2.15/2.30  ((a389) != (a390))
% 2.15/2.30  (c6_2 zenon_X19 (a379))
% 2.15/2.30  ((a395) != zenon_X21)
% 2.15/2.30  ((a439) != zenon_X62)
% 2.15/2.30  (-. (c3_2 zenon_X28 zenon_X179))
% 2.15/2.30  (c8_2 (a291) (a418))
% 2.15/2.30  (-. (c5_2 (a416) (a389)))
% 2.15/2.30  (c6_2 (a332) (a396))
% 2.15/2.30  (-. (c2_0))
% 2.15/2.30  (zenon_X16 != (a444))
% 2.15/2.30  (c7_2 (a294) (a338))
% 2.15/2.30  ((a317) != (a443))
% 2.15/2.30  ((a291) != zenon_X25)
% 2.15/2.30  (c6_2 (a271) (a299))
% 2.15/2.30  (-. (c1_2 zenon_X39 (a347)))
% 2.15/2.30  (-. (c5_2 zenon_X18 (a429)))
% 2.15/2.30  ((a418) != zenon_X9)
% 2.15/2.30  (zenon_X6 != (a302))
% 2.15/2.30  (-. (c5_2 (a395) (a289)))
% 2.15/2.30  (c3_1 zenon_X22)
% 2.15/2.30  (-. (c5_2 zenon_X18 (a440)))
% 2.15/2.30  (-. (c5_2 (a443) zenon_X4))
% 2.15/2.30  ((a425) != zenon_X163)
% 2.15/2.30  ((a347) != zenon_X11)
% 2.15/2.30  (c3_2 zenon_X7 (a439))
% 2.15/2.30  ((a395) != (a271))
% 2.15/2.30  (-. (c5_2 (a307) zenon_X33))
% 2.15/2.30  ((a418) != zenon_X78)
% 2.15/2.30  ((a389) != (a289))
% 2.15/2.30  (zenon_X45 != zenon_X7)
% 2.15/2.30  ((a417) != zenon_X70)
% 2.15/2.30  (zenon_X7 != (a332))
% 2.15/2.30  (c7_1 (a416))
% 2.15/2.30  ((a396) != zenon_X71)
% 2.15/2.30  (-. (c5_2 (a424) (a279)))
% 2.15/2.30  (-. (c5_2 (a431) (a299)))
% 2.15/2.30  (zenon_X45 != (a332))
% 2.15/2.30  (zenon_X8 != (a332))
% 2.15/2.30  (zenon_X35 != (a280))
% 2.15/2.30  (-. (c4_1 (a307)))
% 2.15/2.30  (c7_2 (a271) (a347))
% 2.15/2.30  (c10_1 (a271))
% 2.15/2.30  ((a417) != zenon_X65)
% 2.15/2.30  ((a291) != (a444))
% 2.15/2.30  ((a418) != (a286))
% 2.15/2.30  ((a317) != zenon_X17)
% 2.15/2.30  (c6_2 (a448) (a435))
% 2.15/2.30  (c9_1 (a317))
% 2.15/2.30  (c10_2 zenon_X45 (a347))
% 2.15/2.30  (c6_2 (a280) (a299))
% 2.15/2.30  ((a396) != zenon_X108)
% 2.15/2.30  (c10_2 zenon_X43 (a347))
% 2.15/2.30  ((a440) != zenon_X190)
% 2.15/2.30  (zenon_X43 != (a352))
% 2.15/2.30  (c6_2 (a332) (a409))
% 2.15/2.30  (-. (c5_2 (a424) (a299)))
% 2.15/2.30  (-. (c6_2 (a287) (a288)))
% 2.15/2.30  (-. (c5_2 (a327) (a417)))
% 2.15/2.30  (-. (c10_2 (a332) (a292)))
% 2.15/2.30  ((a286) != zenon_X80)
% 2.15/2.30  (c5_2 zenon_X32 (a299))
% 2.15/2.30  ((a417) != zenon_X189)
% 2.15/2.30  (-. (c5_2 (a448) (a290)))
% 2.15/2.30  (c6_2 zenon_X32 (a417))
% 2.15/2.30  (-. (c5_1 (a327)))
% 2.15/2.30  ((a380) != zenon_X44)
% 2.15/2.30  ((a370) != zenon_X36)
% 2.15/2.30  (-. (c5_2 (a287) (a418)))
% 2.15/2.30  (zenon_X25 != (a278))
% 2.15/2.30  (c3_2 (a319) (a344))
% 2.15/2.30  ((a299) != (a353))
% 2.15/2.30  (-. (c5_2 (a352) zenon_X101))
% 2.15/2.30  ((a299) != zenon_X150)
% 2.15/2.30  ((a395) != (a416))
% 2.15/2.30  ((a299) != zenon_X4)
% 2.15/2.30  (zenon_X7 != (a317))
% 2.15/2.30  (-. (c6_2 zenon_X6 (a425)))
% 2.15/2.30  (-. (c7_2 zenon_X35 (a338)))
% 2.15/2.30  ((a390) != (a299))
% 2.15/2.30  (-. (c7_2 zenon_X13 (a417)))
% 2.15/2.30  (zenon_X31 != (a332))
% 2.15/2.30  ((a380) != (a379))
% 2.15/2.30  (-. (c8_2 (a280) zenon_X76))
% 2.15/2.30  ((a347) != zenon_X190)
% 2.15/2.30  ((a287) != (a448))
% 2.15/2.30  ((a429) != zenon_X75)
% 2.15/2.30  (-. (c2_2 (a317) zenon_X1))
% 2.15/2.30  ((a289) != zenon_X112)
% 2.15/2.30  ((a299) != zenon_X169)
% 2.15/2.30  (zenon_X39 != zenon_X45)
% 2.15/2.30  (-. (c7_2 (a332) (a425)))
% 2.15/2.30  ((a409) != zenon_X79)
% 2.15/2.30  ((a280) != (a271))
% 2.15/2.30  (-. (c8_2 (a424) (a286)))
% 2.15/2.30  (zenon_X43 != (a307))
% 2.15/2.30  ((a389) != zenon_X59)
% 2.15/2.30  ((a416) != zenon_X13)
% 2.15/2.30  (-. (c4_1 (a291)))
% 2.15/2.30  (c7_2 zenon_X18 (a439))
% 2.15/2.30  (-. (c6_2 zenon_X35 (a286)))
% 2.15/2.30  (zenon_X32 != (a307))
% 2.15/2.30  ((a418) != zenon_X81)
% 2.15/2.30  (zenon_X22 != zenon_X27)
% 2.15/2.30  ((a286) != zenon_X112)
% 2.15/2.30  ((a448) != zenon_X25)
% 2.15/2.30  (ndr1_1 zenon_X32)
% 2.15/2.30  ((a389) != (a293))
% 2.15/2.30  ((a287) != (a395))
% 2.15/2.30  (-. (c9_2 (a287) (a290)))
% 2.15/2.30  (-. (c5_2 (a280) (a418)))
% 2.15/2.30  (-. (c5_2 (a443) (a299)))
% 2.15/2.30  (-. (c5_2 (a443) (a290)))
% 2.15/2.30  ((a418) != zenon_X86)
% 2.15/2.30  (zenon_X22 != zenon_X23)
% 2.15/2.30  (-. (c3_2 (a294) zenon_X52))
% 2.15/2.30  ((a439) != zenon_X71)
% 2.15/2.30  (-. (c3_2 zenon_X37 (a299)))
% 2.15/2.30  (zenon_X6 != (a319))
% 2.15/2.30  ((a429) != zenon_X163)
% 2.15/2.30  ((a286) != zenon_X174)
% 2.15/2.30  ((a279) != zenon_X109)
% 2.15/2.30  (zenon_X16 != (a395))
% 2.15/2.30  ((a417) != zenon_X3)
% 2.15/2.30  ((a370) != zenon_X187)
% 2.15/2.30  ((a409) != zenon_X1)
% 2.15/2.30  (ndr1_1 zenon_X39)
% 2.15/2.30  ((a443) != zenon_X34)
% 2.15/2.30  (-. (c7_2 (a332) zenon_X38))
% 2.15/2.30  ((a418) != (a279))
% 2.15/2.30  ((a352) != zenon_X18)
% 2.15/2.30  (zenon_X43 != (a405))
% 2.15/2.30  (c9_1 zenon_X35)
% 2.15/2.30  ((a417) != zenon_X81)
% 2.15/2.30  (c3_2 (a395) (a396))
% 2.15/2.30  (zenon_X16 != zenon_X19)
% 2.15/2.30  (c3_1 zenon_X32)
% 2.15/2.30  (-. (c9_2 (a443) (a396)))
% 2.15/2.30  ((a271) != zenon_X8)
% 2.15/2.30  (-. (c7_2 (a416) (a286)))
% 2.15/2.30  ((a439) != zenon_X173)
% 2.15/2.30  (c3_2 (a424) (a425))
% 2.15/2.30  (-. (c5_2 (a444) zenon_X97))
% 2.15/2.30  (c6_2 zenon_X19 (a286))
% 2.15/2.30  ((a299) != zenon_X55)
% 2.15/2.30  (c6_2 zenon_X28 (a347))
% 2.15/2.30  ((a299) != (a338))
% 2.15/2.30  ((a302) != zenon_X16)
% 2.15/2.30  ((a271) != (a307))
% 2.15/2.30  (-. (c5_2 (a327) (a389)))
% 2.15/2.30  ((a287) != zenon_X28)
% 2.15/2.30  (-. (c5_2 zenon_X43 zenon_X167))
% 2.15/2.30  ((a379) != zenon_X177)
% 2.15/2.30  (c6_2 zenon_X32 (a425))
% 2.15/2.30  ((a344) != (a409))
% 2.15/2.30  (-. (c6_2 zenon_X39 (a417)))
% 2.15/2.30  (ndr1_1 (a431))
% 2.15/2.30  (c7_1 (a291))
% 2.15/2.30  (-. (c4_1 zenon_X8))
% 2.15/2.30  (c6_2 (a431) (a279))
% 2.15/2.30  (-. (c5_2 (a317) zenon_X98))
% 2.15/2.30  ((a290) != (a303))
% 2.15/2.30  ((a417) != (a410))
% 2.15/2.30  ((a434) != zenon_X22)
% 2.15/2.30  ((a286) != zenon_X69)
% 2.15/2.30  (-. (c1_2 (a294) (a295)))
% 2.15/2.30  ((a417) != zenon_X120)
% 2.15/2.30  ((a363) != (a439))
% 2.15/2.30  (c6_2 zenon_X32 (a286))
% 2.15/2.30  (-. (c6_1 (a271)))
% 2.15/2.30  (-. (c6_2 (a317) (a440)))
% 2.15/2.30  (-. (c8_2 (a416) zenon_X57))
% 2.15/2.30  ((a291) != (a317))
% 2.15/2.30  (c5_2 zenon_X31 (a389))
% 2.15/2.30  (-. (c8_2 zenon_X45 (a286)))
% 2.15/2.30  ((a370) != (a299))
% 2.15/2.30  ((a279) != zenon_X116)
% 2.15/2.30  ((a319) != (a332))
% 2.15/2.30  ((a352) != (a319))
% 2.15/2.30  ((a278) != (a369))
% 2.15/2.30  (-. (c4_2 zenon_X15 (a380)))
% 2.15/2.30  ((a429) != zenon_X166)
% 2.15/2.30  (c6_2 zenon_X13 (a379))
% 2.15/2.30  (-. (c9_2 (a443) zenon_X5))
% 2.15/2.30  ((a286) != zenon_X63)
% 2.15/2.30  (zenon_X6 != (a434))
% 2.15/2.30  (c6_2 (a280) (a279))
% 2.15/2.30  ((a352) != zenon_X23)
% 2.15/2.30  (c1_2 zenon_X6 (a440))
% 2.15/2.30  ((a347) != zenon_X65)
% 2.15/2.30  ((a290) != zenon_X3)
% 2.15/2.30  (c3_1 (a424))
% 2.15/2.30  ((a286) != zenon_X181)
% 2.15/2.30  (ndr1_1 (a302))
% 2.15/2.30  (-. (c7_2 zenon_X23 (a347)))
% 2.15/2.30  (zenon_X18 != zenon_X23)
% 2.15/2.30  (-. (c7_2 zenon_X39 zenon_X196))
% 2.15/2.30  (-. (c6_2 zenon_X43 (a417)))
% 2.15/2.30  (c1_1 (a317))
% 2.15/2.30  ((a291) != (a405))
% 2.15/2.30  (c6_2 (a424) (a409))
% 2.15/2.30  (-. (c3_2 (a278) zenon_X68))
% 2.15/2.30  (zenon_X39 != zenon_X21)
% 2.15/2.30  ((a290) != zenon_X77)
% 2.15/2.30  ((a291) != (a431))
% 2.15/2.30  ((a444) != (a424))
% 2.15/2.30  (c6_2 zenon_X21 (a379))
% 2.15/2.30  (c7_1 (a443))
% 2.15/2.30  ((a327) != (a405))
% 2.15/2.30  (c6_2 (a291) (a379))
% 2.15/2.30  (ndr1_1 (a319))
% 2.15/2.30  (c6_2 zenon_X16 (a409))
% 2.15/2.30  ((a307) != (a424))
% 2.15/2.30  ((a431) != (a395))
% 2.15/2.30  (-. (c5_2 (a424) (a417)))
% 2.15/2.30  ((a425) != zenon_X69)
% 2.15/2.30  (-. (c8_2 (a307) (a286)))
% 2.15/2.30  ((a417) != (a347))
% 2.15/2.30  (-. (c2_2 (a278) (a380)))
% 2.15/2.30  (-. (c5_2 (a280) zenon_X103))
% 2.15/2.30  (-. (c5_2 (a287) zenon_X107))
% 2.15/2.30  (c6_2 zenon_X31 (a286))
% 2.15/2.30  (zenon_X25 != zenon_X19)
% 2.15/2.30  ((a291) != (a424))
% 2.15/2.30  ((a279) != zenon_X97)
% 2.15/2.30  (c3_2 (a408) (a347))
% 2.15/2.30  ((a278) != (a434))
% 2.15/2.30  (c3_2 (a291) (a293))
% 2.15/2.30  ((a431) != zenon_X8)
% 2.15/2.30  ((a327) != zenon_X21)
% 2.15/2.30  (-. (c2_2 (a278) (a409)))
% 2.15/2.30  (zenon_X32 != zenon_X21)
% 2.15/2.30  ((a439) != zenon_X63)
% 2.15/2.30  (-. (c8_2 zenon_X22 (a429)))
% 2.15/2.30  (-. (c6_1 zenon_X16))
% 2.15/2.30  (c6_2 (a287) (a417))
% 2.15/2.30  (zenon_X31 != (a443))
% 2.15/2.30  (c4_2 (a280) (a380))
% 2.15/2.30  (zenon_X18 != zenon_X8)
% 2.15/2.30  (-. (c8_2 (a278) (a286)))
% 2.15/2.30  (c1_1 zenon_X6)
% 2.15/2.30  (zenon_X35 != (a431))
% 2.15/2.30  (-. (c5_2 zenon_X43 (a299)))
% 2.15/2.30  (c1_1 (a424))
% 2.15/2.30  (zenon_X6 != zenon_X18)
% 2.15/2.30  ((a363) != (a410))
% 2.15/2.30  (c4_2 (a291) (a389))
% 2.15/2.30  ((a347) != (a439))
% 2.15/2.30  (ndr1_1 zenon_X45)
% 2.15/2.30  (-. (c8_2 zenon_X16 (a286)))
% 2.15/2.30  (c6_2 (a307) (a286))
% 2.15/2.30  (-. (c7_2 (a405) (a286)))
% 2.15/2.30  (c6_2 zenon_X32 (a429))
% 2.15/2.30  ((a363) != (a347))
% 2.15/2.30  (-. (c4_1 zenon_X19))
% 2.15/2.30  ((a363) != (a289))
% 2.15/2.30  ((a280) != zenon_X22)
% 2.15/2.30  ((a327) != (a307))
% 2.15/2.30  (zenon_X19 != (a416))
% 2.15/2.30  (zenon_X18 != (a416))
% 2.15/2.30  (c10_2 (a408) (a409))
% 2.15/2.30  (-. (c10_0))
% 2.15/2.30  ((a292) != zenon_X101)
% 2.15/2.30  (zenon_X39 != (a317))
% 2.15/2.30  ((a288) != (a370))
% 2.15/2.30  ((a439) != zenon_X36)
% 2.15/2.30  ((a279) != (a379))
% 2.15/2.30  (zenon_X45 != zenon_X23)
% 2.15/2.30  (-. (c6_2 (a271) zenon_X112))
% 2.15/2.30  ((a299) != zenon_X98)
% 2.15/2.30  (zenon_X35 != zenon_X31)
% 2.15/2.30  (c3_1 zenon_X13)
% 2.15/2.30  ((a417) != zenon_X126)
% 2.15/2.30  (c1_1 (a395))
% 2.15/2.30  (zenon_X18 != (a332))
% 2.15/2.30  (-. (c3_2 (a332) zenon_X163))
% 2.15/2.30  ((a396) != zenon_X174)
% 2.15/2.30  ((a289) != zenon_X48)
% 2.15/2.30  ((a287) != zenon_X21)
% 2.15/2.30  ((a293) != (a286))
% 2.15/2.30  (c7_1 zenon_X21)
% 2.15/2.30  (zenon_X1 != (a389))
% 2.15/2.30  ((a443) != (a280))
% 2.15/2.30  (c6_2 zenon_X35 (a425))
% 2.15/2.30  ((a395) != zenon_X28)
% 2.15/2.30  (-. (c5_2 (a352) (a290)))
% 2.15/2.30  (c3_1 zenon_X8)
% 2.15/2.30  (zenon_X38 != zenon_X67)
% 2.15/2.30  ((a279) != zenon_X108)
% 2.15/2.30  (-. (c2_2 (a278) (a389)))
% 2.15/2.30  (c10_2 (a317) (a409))
% 2.15/2.30  ((a410) != zenon_X79)
% 2.15/2.30  ((a289) != (a293))
% 2.15/2.30  ((a319) != (a278))
% 2.15/2.30  (zenon_X25 != zenon_X13)
% 2.15/2.30  ((a434) != zenon_X31)
% 2.15/2.30  (zenon_X39 != zenon_X19)
% 2.15/2.30  ((a302) != (a332))
% 2.15/2.30  (c8_2 (a416) (a417))
% 2.15/2.30  (c4_2 (a280) zenon_X41)
% 2.15/2.30  ((a440) != (a288))
% 2.15/2.30  ((a448) != zenon_X45)
% 2.15/2.30  (c10_2 (a319) (a347))
% 2.15/2.30  ((a389) != (a292))
% 2.15/2.30  (zenon_X35 != (a327))
% 2.15/2.30  ((a429) != zenon_X174)
% 2.15/2.30  (zenon_X19 != (a443))
% 2.15/2.30  ((a425) != zenon_X124)
% 2.15/2.30  (ndr1_1 (a291))
% 2.15/2.30  ((a289) != zenon_X100)
% 2.15/2.30  (zenon_X35 != (a271))
% 2.15/2.30  ((a418) != zenon_X106)
% 2.15/2.30  ((a416) != zenon_X31)
% 2.15/2.30  (c3_1 zenon_X23)
% 2.15/2.30  (-. (c7_2 (a317) (a379)))
% 2.15/2.30  ((a347) != zenon_X36)
% 2.15/2.30  (-. (c2_2 (a395) (a389)))
% 2.15/2.30  (c5_2 zenon_X16 (a299))
% 2.15/2.30  ((a405) != zenon_X34)
% 2.15/2.30  ((a448) != (a444))
% 2.15/2.30  (zenon_X38 != zenon_X65)
% 2.15/2.30  ((a379) != zenon_X54)
% 2.15/2.30  ((a279) != zenon_X3)
% 2.15/2.30  (-. (c7_2 (a271) (a439)))
% 2.15/2.30  ((a347) != zenon_X161)
% 2.15/2.30  ((a292) != zenon_X97)
% 2.15/2.30  ((a352) != zenon_X32)
% 2.15/2.30  ((a363) != (a409))
% 2.15/2.30  (c10_1 (a302))
% 2.15/2.30  ((a416) != (a434))
% 2.15/2.30  (-. (c5_2 (a287) (a299)))
% 2.15/2.30  (ndr1_1 (a307))
% 2.15/2.30  (-. (c4_1 (a280)))
% 2.15/2.30  ((a425) != zenon_X10)
% 2.15/2.30  (c6_2 (a352) (a286))
% 2.15/2.30  (-. (c7_2 zenon_X27 (a286)))
% 2.15/2.30  ((a439) != zenon_X187)
% 2.15/2.30  (zenon_X39 != (a280))
% 2.15/2.30  (c6_2 (a369) (a417))
% 2.15/2.30  ((a431) != zenon_X32)
% 2.15/2.30  (zenon_X43 != (a444))
% 2.15/2.30  (-. (c7_2 (a448) (a286)))
% 2.15/2.30  ((a347) != zenon_X108)
% 2.15/2.30  (zenon_X39 != zenon_X31)
% 2.15/2.30  (zenon_X45 != zenon_X21)
% 2.15/2.30  (-. (c4_1 (a434)))
% 2.15/2.30  (zenon_X27 != (a332))
% 2.15/2.30  ((a410) != zenon_X188)
% 2.15/2.30  ((a271) != (a332))
% 2.15/2.30  (-. (c5_2 zenon_X7 (a439)))
% 2.15/2.30  (zenon_X35 != (a294))
% 2.15/2.30  ((a396) != (a295))
% 2.15/2.30  (zenon_X19 != zenon_X28)
% 2.15/2.30  (-. (c10_1 (a319)))
% 2.15/2.30  (c3_2 zenon_X16 (a347))
% 2.15/2.30  (ndr1_1 (a278))
% 2.15/2.30  ((a302) != zenon_X28)
% 2.15/2.30  ((a303) != (a288))
% 2.15/2.30  (c6_2 (a332) (a380))
% 2.15/2.30  (-. (c5_2 (a352) (a292)))
% 2.15/2.30  ((a425) != zenon_X120)
% 2.15/2.30  (c3_2 (a416) (a417))
% 2.15/2.30  (zenon_X8 != (a280))
% 2.15/2.30  (c6_2 (a280) (a418))
% 2.15/2.30  ((a435) != (a370))
% 2.15/2.30  (-. (c7_2 (a280) (a347)))
% 2.15/2.30  ((a327) != (a271))
% 2.15/2.30  ((a396) != zenon_X188)
% 2.15/2.30  (-. (c4_2 zenon_X35 (a370)))
% 2.15/2.30  ((a299) != zenon_X109)
% 2.15/2.30  (c7_1 zenon_X7)
% 2.15/2.30  (c4_1 zenon_X35)
% 2.15/2.30  ((a317) != zenon_X22)
% 2.15/2.30  ((a431) != zenon_X23)
% 2.15/2.30  (zenon_X31 != zenon_X23)
% 2.15/2.30  ((a279) != zenon_X86)
% 2.15/2.30  ((a307) != (a343))
% 2.15/2.30  ((a431) != zenon_X31)
% 2.15/2.30  (c7_2 (a352) (a439))
% 2.15/2.30  (c6_1 zenon_X8)
% 2.15/2.30  (zenon_X32 != (a278))
% 2.15/2.30  (-. (c4_2 zenon_X35 (a417)))
% 2.15/2.30  (-. (c5_2 (a294) zenon_X137))
% 2.15/2.30  (zenon_X16 != zenon_X23)
% 2.15/2.30  ((a363) != (a290))
% 2.15/2.30  ((a287) != (a443))
% 2.15/2.30  (-. (c5_2 (a332) (a417)))
% 2.15/2.30  ((a286) != (a338))
% 2.15/2.30  (-. (c2_2 (a317) zenon_X30))
% 2.15/2.30  (-. (c9_1 zenon_X39))
% 2.15/2.30  ((a370) != (a344))
% 2.15/2.30  ((a317) != zenon_X31)
% 2.15/2.30  (-. (c1_2 zenon_X8 (a390)))
% 2.15/2.30  ((a363) != zenon_X186)
% 2.15/2.30  ((a286) != (a439))
% 2.15/2.30  (c6_2 (a444) (a299))
% 2.15/2.30  ((a409) != zenon_X80)
% 2.15/2.30  ((a417) != (a292))
% 2.15/2.30  ((a290) != zenon_X103)
% 2.15/2.30  (-. (c10_1 zenon_X27))
% 2.15/2.30  ((a363) != (a295))
% 2.15/2.30  ((a417) != zenon_X177)
% 2.15/2.30  (zenon_X32 != (a444))
% 2.15/2.30  ((a379) != zenon_X189)
% 2.15/2.30  (-. (c5_2 zenon_X35 zenon_X186))
% 2.15/2.30  (zenon_X39 != zenon_X18)
% 2.15/2.30  (-. (c5_2 (a444) (a418)))
% 2.15/2.30  (c7_1 (a369))
% 2.15/2.30  (zenon_X43 != (a287))
% 2.15/2.30  (c9_2 zenon_X8 (a390))
% 2.15/2.30  (c6_2 zenon_X21 (a286))
% 2.15/2.30  (zenon_X32 != (a405))
% 2.15/2.30  ((a409) != (a295))
% 2.15/2.30  (-. (c7_2 (a317) (a439)))
% 2.15/2.30  ((a287) != zenon_X45)
% 2.15/2.30  (-. (c9_1 zenon_X32))
% 2.15/2.30  ((a290) != zenon_X101)
% 2.15/2.30  ((a429) != zenon_X62)
% 2.15/2.30  (-. (c5_2 (a416) (a279)))
% 2.15/2.30  (-. (c6_2 zenon_X39 (a379)))
% 2.15/2.30  (c6_2 (a431) (a417))
% 2.15/2.30  (zenon_X32 != (a434))
% 2.15/2.30  ((a417) != zenon_X112)
% 2.15/2.30  (zenon_X32 != (a424))
% 2.15/2.30  (c6_2 (a395) (a379))
% 2.15/2.30  (-. (c4_1 (a424)))
% 2.15/2.30  (-. (c3_2 zenon_X21 zenon_X175))
% 2.15/2.30  (-. (c8_2 (a369) (a286)))
% 2.15/2.30  ((a396) != zenon_X192)
% 2.15/2.30  (-. (c5_2 (a424) (a425)))
% 2.15/2.30  (-. (c6_2 (a271) (a293)))
% 2.15/2.30  (c7_2 zenon_X18 (a429))
% 2.15/2.30  (zenon_X6 != zenon_X45)
% 2.15/2.30  (-. (c8_2 zenon_X25 (a286)))
% 2.15/2.30  (zenon_X25 != (a434))
% 2.15/2.30  (-. (c2_2 (a291) (a389)))
% 2.15/2.30  ((a343) != (a278))
% 2.15/2.30  (c5_2 zenon_X45 (a279))
% 2.15/2.30  ((a294) != (a395))
% 2.15/2.30  (c7_2 zenon_X35 (a439))
% 2.15/2.30  ((a379) != (a440))
% 2.15/2.30  ((a299) != zenon_X78)
% 2.15/2.30  (zenon_X35 != zenon_X18)
% 2.15/2.30  ((a299) != zenon_X82)
% 2.15/2.30  (c9_2 (a444) (a410))
% 2.15/2.30  ((a429) != zenon_X172)
% 2.15/2.30  (c10_1 (a294))
% 2.15/2.30  ((a443) != zenon_X7)
% 2.15/2.30  (c3_2 (a280) (a409))
% 2.15/2.30  ((a396) != zenon_X5)
% 2.15/2.30  ((a287) != (a319))
% 2.15/2.30  (-. (c6_2 (a271) (a417)))
% 2.15/2.30  (-. (c6_1 zenon_X28))
% 2.15/2.30  ((a271) != zenon_X43)
% 2.15/2.30  (c1_1 zenon_X8)
% 2.15/2.30  ((a363) != zenon_X74)
% 2.15/2.30  (c6_2 (a307) (a299))
% 2.15/2.30  ((a389) != zenon_X48)
% 2.15/2.30  (c6_2 (a431) (a286))
% 2.15/2.30  ((a396) != zenon_X61)
% 2.15/2.30  ((a279) != zenon_X141)
% 2.15/2.30  (c5_2 (a405) (a290))
% 2.15/2.30  ((a440) != zenon_X112)
% 2.15/2.30  ((a347) != zenon_X184)
% 2.15/2.30  ((a347) != zenon_X53)
% 2.15/2.30  (zenon_X31 != zenon_X28)
% 2.15/2.30  (zenon_X31 != (a395))
% 2.15/2.30  (-. (c6_1 zenon_X22))
% 2.15/2.30  (-. (c7_2 zenon_X32 (a286)))
% 2.15/2.30  (zenon_X35 != (a369))
% 2.15/2.30  (c6_2 (a291) (a425))
% 2.15/2.30  ((a279) != zenon_X106)
% 2.15/2.30  ((a448) != (a424))
% 2.15/2.30  (zenon_X18 != (a319))
% 2.15/2.30  ((a444) != (a434))
% 2.15/2.30  ((a389) != zenon_X26)
% 2.15/2.30  (zenon_X19 != (a369))
% 2.15/2.30  ((a429) != zenon_X164)
% 2.15/2.30  (c6_2 (a280) (a429))
% 2.15/2.30  (-. (c5_2 (a294) (a292)))
% 2.15/2.30  ((a287) != zenon_X18)
% 2.15/2.30  (zenon_X6 != (a280))
% 2.15/2.30  ((a424) != zenon_X31)
% 2.15/2.30  (zenon_X43 != zenon_X13)
% 2.15/2.30  (c6_2 zenon_X43 (a299))
% 2.15/2.30  (c6_2 zenon_X16 (a396))
% 2.15/2.30  ((a347) != zenon_X2)
% 2.15/2.30  (c7_2 (a294) (a379))
% 2.15/2.30  (c8_2 (a291) (a299))
% 2.15/2.30  (c10_1 zenon_X35)
% 2.15/2.30  ((a344) != (a410))
% 2.15/2.30  ((a278) != zenon_X23)
% 2.15/2.30  (c6_2 zenon_X13 (a417))
% 2.15/2.30  ((a435) != (a299))
% 2.15/2.30  (zenon_X18 != zenon_X16)
% 2.15/2.30  (-. (c5_2 (a327) (a289)))
% 2.15/2.30  ((a363) != (a344))
% 2.15/2.30  (c9_1 zenon_X22)
% 2.15/2.30  (-. (c5_2 (a307) (a417)))
% 2.15/2.30  (-. (c5_2 (a271) (a299)))
% 2.15/2.30  ((a439) != zenon_X193)
% 2.15/2.30  (c8_1 (a443))
% 2.15/2.30  (-. (c5_2 (a307) (a390)))
% 2.15/2.30  (zenon_X8 != (a302))
% 2.15/2.30  (c5_2 zenon_X19 (a289))
% 2.15/2.30  (zenon_X7 != (a416))
% 2.15/2.30  (c6_2 zenon_X35 (a279))
% 2.15/2.30  (c5_2 (a294) (a389))
% 2.15/2.30  (-. (c7_2 (a319) zenon_X136))
% 2.15/2.30  ((a443) != (a416))
% 2.15/2.30  (zenon_X21 != zenon_X18)
% 2.15/2.30  (c8_2 (a287) (a389))
% 2.15/2.30  (zenon_X39 != zenon_X35)
% 2.15/2.30  ((a317) != zenon_X27)
% 2.15/2.30  (-. (c7_2 zenon_X19 zenon_X161))
% 2.15/2.30  (c6_2 zenon_X28 (a396))
% 2.15/2.30  (-. (c4_2 zenon_X35 (a295)))
% 2.15/2.30  (zenon_X45 != (a317))
% 2.15/2.30  (zenon_X43 != (a280))
% 2.15/2.30  (-. (c6_2 zenon_X6 (a439)))
% 2.15/2.30  (-. (c8_2 zenon_X43 zenon_X94))
% 2.15/2.30  (-. (c5_2 (a317) (a290)))
% 2.15/2.30  (c6_2 (a444) (a429))
% 2.15/2.30  ((a287) != zenon_X16)
% 2.15/2.30  (ndr1_1 (a395))
% 2.15/2.30  (ndr1_1 (a294))
% 2.15/2.30  (zenon_X27 != (a434))
% 2.15/2.30  ((a396) != (a288))
% 2.15/2.30  ((a289) != zenon_X26)
% 2.15/2.30  ((a307) != (a332))
% 2.15/2.30  ((a291) != zenon_X27)
% 2.15/2.30  (-. (c6_2 zenon_X6 (a379)))
% 2.15/2.30  (-. (c4_1 zenon_X32))
% 2.15/2.30  (-. (c1_2 zenon_X43 (a347)))
% 2.15/2.30  ((a417) != (a293))
% 2.15/2.30  ((a439) != zenon_X189)
% 2.15/2.30  ((a429) != zenon_X73)
% 2.15/2.30  (c3_1 (a307))
% 2.15/2.30  ((a448) != zenon_X8)
% 2.15/2.30  ((a289) != zenon_X107)
% 2.15/2.30  (c3_2 zenon_X39 (a347))
% 2.15/2.30  ((a279) != zenon_X85)
% 2.15/2.30  ((a317) != zenon_X43)
% 2.15/2.30  (-. (c5_2 (a395) zenon_X109))
% 2.15/2.30  ((a443) != (a307))
% 2.15/2.30  ((a280) != (a416))
% 2.15/2.30  (c3_1 zenon_X27)
% 2.15/2.30  (-. (c7_2 (a434) (a379)))
% 2.15/2.30  ((a417) != zenon_X187)
% 2.15/2.30  (-. (c6_2 (a317) (a379)))
% 2.15/2.30  ((a431) != (a307))
% 2.15/2.30  ((a352) != zenon_X45)
% 2.15/2.30  ((a405) != (a369))
% 2.15/2.30  (c8_1 (a405))
% 2.15/2.30  (c6_2 (a287) (a286))
% 2.15/2.30  (zenon_X41 != (a379))
% 2.15/2.30  (zenon_X6 != (a332))
% 2.15/2.30  ((a278) != (a332))
% 2.15/2.30  (-. (c5_2 (a434) (a292)))
% 2.15/2.30  (c6_2 zenon_X32 (a379))
% 2.15/2.30  ((a344) != zenon_X188)
% 2.15/2.30  (c10_2 zenon_X39 (a347))
% 2.15/2.30  ((a327) != (a369))
% 2.15/2.30  (c6_2 (a431) (a299))
% 2.15/2.30  ((a440) != zenon_X192)
% 2.15/2.30  (-. (c5_2 (a395) (a279)))
% 2.15/2.30  (-. (c7_2 (a444) (a439)))
% 2.15/2.30  (c2_2 (a444) zenon_X30)
% 2.15/2.30  ((a299) != zenon_X81)
% 2.15/2.30  ((a389) != (a344))
% 2.15/2.30  ((a286) != zenon_X189)
% 2.15/2.30  (zenon_X8 != zenon_X31)
% 2.15/2.30  ((a425) != zenon_X67)
% 2.15/2.30  ((a292) != (a439))
% 2.15/2.30  (zenon_X16 != zenon_X21)
% 2.15/2.30  ((a289) != zenon_X57)
% 2.15/2.30  ((a299) != zenon_X110)
% 2.15/2.30  ((a289) != zenon_X95)
% 2.15/2.30  (-. (c10_2 (a405) (a410)))
% 2.15/2.30  (c4_2 zenon_X35 (a363))
% 2.15/2.30  (-. (c5_2 (a434) (a418)))
% 2.15/2.30  (-. (c8_2 zenon_X22 zenon_X88))
% 2.15/2.30  (c7_2 zenon_X43 (a347))
% 2.15/2.30  (c6_1 (a287))
% 2.15/2.30  (-. (c8_2 (a448) (a286)))
% 2.15/2.30  ((a417) != zenon_X76)
% 2.15/2.30  (c6_2 (a443) (a379))
% 2.15/2.30  (c6_2 zenon_X35 (a417))
% 2.15/2.30  (zenon_X43 != zenon_X31)
% 2.15/2.30  ((a291) != zenon_X22)
% 2.15/2.30  (-. (c6_2 zenon_X43 (a379)))
% 2.15/2.30  (zenon_X13 != (a369))
% 2.15/2.30  (-. (c5_2 (a294) (a299)))
% 2.15/2.30  ((a416) != zenon_X28)
% 2.15/2.30  ((a439) != zenon_X108)
% 2.15/2.30  (zenon_X13 != zenon_X28)
% 2.15/2.30  (-. (c3_2 (a395) zenon_X61))
% 2.15/2.30  (-. (c7_1 zenon_X6))
% 2.15/2.30  ((a417) != zenon_X62)
% 2.15/2.30  ((a431) != (a278))
% 2.15/2.30  (zenon_X8 != (a434))
% 2.15/2.30  (c6_2 (a424) (a289))
% 2.15/2.30  (-. (c3_2 (a287) (a290)))
% 2.15/2.30  ((a370) != zenon_X61)
% 2.15/2.30  (zenon_X19 != (a291))
% 2.15/2.30  (zenon_X27 != (a369))
% 2.15/2.30  (ndr1_1 zenon_X28)
% 2.15/2.30  (zenon_X45 != (a405))
% 2.15/2.30  ((a286) != zenon_X177)
% 2.15/2.30  ((a344) != (a295))
% 2.15/2.30  (-. (c6_2 (a271) (a286)))
% 2.15/2.30  ((a295) != zenon_X52)
% 2.15/2.30  (-. (c6_2 zenon_X6 zenon_X194))
% 2.15/2.30  (c9_2 (a443) (a390))
% 2.15/2.30  (zenon_X45 != (a307))
% 2.15/2.30  (zenon_X21 != (a424))
% 2.15/2.30  ((a379) != (a338))
% 2.15/2.30  ((a389) != zenon_X116)
% 2.15/2.30  (zenon_X0 != (a344))
% 2.15/2.30  (-. (c3_2 zenon_X35 zenon_X36))
% 2.15/2.30  (-. (c2_2 (a278) zenon_X1))
% 2.15/2.30  ((a292) != (a286))
% 2.15/2.30  ((a417) != (a299))
% 2.15/2.30  ((a429) != (a390))
% 2.15/2.30  (-. (c4_1 (a369)))
% 2.15/2.30  ((a448) != (a443))
% 2.15/2.30  (zenon_X25 != (a317))
% 2.15/2.30  (-. (c5_2 (a408) (a409)))
% 2.15/2.30  ((a347) != zenon_X180)
% 2.15/2.30  ((a279) != zenon_X33)
% 2.15/2.30  (c6_2 (a307) (a439))
% 2.15/2.30  (c1_1 (a431))
% 2.15/2.30  (-. (c5_2 (a434) (a417)))
% 2.15/2.30  ((a379) != zenon_X175)
% 2.15/2.30  (c5_2 (a369) (a279))
% 2.15/2.30  ((a299) != zenon_X171)
% 2.15/2.30  (c6_2 zenon_X16 (a379))
% 2.15/2.30  ((a395) != zenon_X27)
% 2.15/2.30  (c6_2 zenon_X23 (a439))
% 2.15/2.30  (-. (c7_2 (a317) zenon_X125))
% 2.15/2.30  ((a418) != zenon_X56)
% 2.15/2.30  (c6_2 (a369) (a286))
% 2.15/2.30  (-. (c10_2 (a332) (a409)))
% 2.15/2.30  (c6_2 (a431) (a347))
% 2.15/2.30  (c6_1 (a443))
% 2.15/2.30  (zenon_X6 != (a278))
% 2.15/2.30  ((a417) != zenon_X110)
% 2.15/2.30  ((a370) != zenon_X179)
% 2.15/2.30  ((a440) != zenon_X166)
% 2.15/2.30  ((a292) != zenon_X138)
% 2.15/2.30  (c9_2 (a307) (a390))
% 2.15/2.30  ((a279) != zenon_X0)
% 2.15/2.30  ((a410) != zenon_X42)
% 2.15/2.30  ((a299) != (a409))
% 2.15/2.30  (-. (c8_2 (a405) zenon_X116))
% 2.15/2.30  (zenon_X1 != zenon_X44)
% 2.15/2.30  ((a379) != zenon_X124)
% 2.15/2.30  (c1_1 zenon_X19)
% 2.15/2.30  (zenon_X31 != (a302))
% 2.15/2.30  (ndr1_1 (a369))
% 2.15/2.30  (c6_2 (a434) (a380))
% 2.15/2.30  (c4_1 (a271))
% 2.15/2.30  ((a380) != zenon_X79)
% 2.15/2.30  (c9_1 zenon_X8)
% 2.15/2.30  ((a327) != zenon_X13)
% 2.15/2.30  (-. (c10_1 zenon_X23))
% 2.15/2.30  (zenon_X45 != (a369))
% 2.15/2.30  ((a418) != zenon_X107)
% 2.15/2.30  ((a294) != zenon_X18)
% 2.15/2.30  ((a439) != zenon_X174)
% 2.15/2.30  (zenon_X31 != (a327))
% 2.15/2.30  (-. (c5_1 (a424)))
% 2.15/2.30  ((a417) != zenon_X103)
% 2.15/2.30  ((a292) != zenon_X81)
% 2.15/2.30  (zenon_X43 != zenon_X28)
% 2.15/2.30  ((a396) != zenon_X187)
% 2.15/2.30  ((a280) != zenon_X31)
% 2.15/2.30  ((a352) != (a278))
% 2.15/2.30  ((a425) != zenon_X53)
% 2.15/2.30  (-. (c3_2 (a448) zenon_X75))
% 2.15/2.30  (c6_2 (a443) (a347))
% 2.15/2.30  ((a294) != (a405))
% 2.15/2.30  ((a429) != zenon_X52)
% 2.15/2.30  (-. (c7_2 (a307) (a286)))
% 2.15/2.30  (c5_2 zenon_X45 (a389))
% 2.15/2.30  (c6_2 (a395) (a429))
% 2.15/2.30  (c6_2 (a434) (a417))
% 2.15/2.30  ((a286) != zenon_X54)
% 2.15/2.30  (c6_2 zenon_X35 (a439))
% 2.15/2.30  ((a279) != zenon_X167)
% 2.15/2.30  (c6_2 (a291) (a293))
% 2.15/2.30  (zenon_X32 != zenon_X23)
% 2.15/2.30  ((a417) != zenon_X173)
% 2.15/2.30  ((a344) != zenon_X24)
% 2.15/2.30  ((a431) != (a416))
% 2.15/2.30  ((a299) != zenon_X107)
% 2.15/2.30  (c6_2 (a405) (a347))
% 2.15/2.30  ((a379) != zenon_X112)
% 2.15/2.30  ((a448) != (a395))
% 2.15/2.30  ((a418) != zenon_X57)
% 2.15/2.30  ((a439) != zenon_X79)
% 2.15/2.30  (c6_2 zenon_X35 (a396))
% 2.15/2.30  (c6_2 zenon_X35 (a293))
% 2.15/2.30  ((a294) != (a448))
% 2.15/2.30  (-. (c9_1 (a278)))
% 2.15/2.30  ((a287) != (a280))
% 2.15/2.30  ((a416) != (a369))
% 2.15/2.30  (-. (c5_2 (a431) (a289)))
% 2.15/2.30  ((a291) != zenon_X16)
% 2.15/2.30  ((a439) != zenon_X166)
% 2.15/2.30  ((a344) != (a353))
% 2.15/2.30  (-. (c5_2 zenon_X45 (a439)))
% 2.15/2.30  (c3_2 zenon_X22 (a347))
% 2.15/2.30  ((a286) != zenon_X62)
% 2.15/2.30  ((a417) != zenon_X68)
% 2.15/2.30  (c6_2 zenon_X35 (a295))
% 2.15/2.30  (c5_2 zenon_X21 (a299))
% 2.15/2.30  ((a431) != zenon_X16)
% 2.15/2.30  ((a347) != zenon_X173)
% 2.15/2.30  ((a439) != zenon_X52)
% 2.15/2.30  (-. (c5_2 (a327) (a279)))
% 2.15/2.30  (c2_2 (a444) (a410))
% 2.15/2.30  ((a271) != zenon_X16)
% 2.15/2.30  (zenon_X18 != (a444))
% 2.15/2.30  ((a292) != (a289))
% 2.15/2.30  ((a347) != (a338))
% 2.15/2.30  (-. (c3_2 (a416) zenon_X71))
% 2.15/2.30  (c7_0)
% 2.15/2.30  (-. (c5_2 zenon_X43 (a292)))
% 2.15/2.30  (-. (c5_2 (a327) (a292)))
% 2.15/2.30  ((a425) != zenon_X54)
% 2.15/2.30  (c4_2 (a352) (a389))
% 2.15/2.30  (zenon_X6 != (a369))
% 2.15/2.30  (zenon_X18 != zenon_X25)
% 2.15/2.30  (c3_2 zenon_X22 (a429))
% 2.15/2.30  (c7_2 (a416) (a417))
% 2.15/2.30  (zenon_X43 != (a416))
% 2.15/2.30  (c6_2 (a280) (a289))
% 2.15/2.30  (c6_2 (a434) (a292))
% 2.15/2.30  ((a290) != zenon_X81)
% 2.15/2.30  (-. (c6_2 (a317) (a417)))
% 2.15/2.30  (-. (c5_2 zenon_X8 (a418)))
% 2.15/2.30  (-. (c4_1 (a294)))
% 2.15/2.30  ((a279) != zenon_X137)
% 2.15/2.30  (c4_2 (a280) (a389))
% 2.15/2.30  (-. (c3_2 zenon_X8 zenon_X184))
% 2.15/2.30  (c6_2 zenon_X45 (a286))
% 2.15/2.30  ((a317) != (a369))
% 2.15/2.30  (zenon_X18 != zenon_X19)
% 2.15/2.30  ((a344) != zenon_X29)
% 2.15/2.30  (c6_2 (a448) (a288))
% 2.15/2.30  (-. (c4_1 (a278)))
% 2.15/2.30  (-. (c6_0))
% 2.15/2.30  (-. (c9_1 zenon_X23))
% 2.15/2.30  ((a279) != zenon_X112)
% 2.15/2.30  ((a418) != zenon_X101)
% 2.15/2.30  (-. (c7_2 zenon_X7 zenon_X147))
% 2.15/2.30  (-. (c8_2 zenon_X16 zenon_X117))
% 2.15/2.30  ((a302) != zenon_X23)
% 2.15/2.30  ((a286) != zenon_X36)
% 2.15/2.30  (c5_2 (a291) (a389))
% 2.15/2.30  (c5_2 (a291) (a418))
% 2.15/2.30  (zenon_X43 != (a302))
% 2.15/2.30  (c7_2 (a278) (a439))
% 2.15/2.30  (-. (c5_2 (a317) (a299)))
% 2.15/2.30  ((a416) != (a444))
% 2.15/2.30  ((a429) != zenon_X192)
% 2.15/2.30  ((a379) != zenon_X69)
% 2.15/2.30  (c8_2 zenon_X37 (a299))
% 2.15/2.30  ((a290) != zenon_X100)
% 2.15/2.30  (c5_2 zenon_X18 (a389))
% 2.15/2.30  (-. (c5_2 (a395) (a417)))
% 2.15/2.30  ((a439) != zenon_X192)
% 2.15/2.30  ((a416) != zenon_X22)
% 2.15/2.30  (-. (c4_2 zenon_X39 (a286)))
% 2.15/2.30  (c4_1 zenon_X16)
% 2.15/2.30  (zenon_X39 != zenon_X22)
% 2.15/2.30  ((a289) != zenon_X86)
% 2.15/2.30  (c1_1 zenon_X32)
% 2.15/2.30  (c6_2 (a443) (a418))
% 2.15/2.30  (-. (c5_2 zenon_X8 (a292)))
% 2.15/2.30  ((a302) != zenon_X21)
% 2.15/2.30  (-. (c6_2 zenon_X39 (a396)))
% 2.15/2.30  ((a291) != (a302))
% 2.15/2.30  (-. (c5_1 zenon_X17))
% 2.15/2.30  (c6_2 zenon_X13 (a396))
% 2.15/2.30  (-. (c1_2 (a317) (a347)))
% 2.15/2.30  ((a302) != zenon_X19)
% 2.15/2.30  (c6_2 (a424) (a279))
% 2.15/2.30  ((a289) != (a286))
% 2.15/2.30  ((a448) != (a280))
% 2.15/2.30  (c6_1 zenon_X18)
% 2.15/2.30  ((a294) != (a332))
% 2.15/2.30  (zenon_X21 != (a280))
% 2.15/2.30  (-. (c6_2 zenon_X39 (a370)))
% 2.15/2.30  ((a405) != (a332))
% 2.15/2.30  ((a417) != zenon_X36)
% 2.15/2.30  ((a429) != zenon_X187)
% 2.15/2.30  (zenon_X31 != zenon_X45)
% 2.15/2.30  (zenon_X19 != zenon_X13)
% 2.15/2.30  ((a307) != zenon_X23)
% 2.15/2.30  ((a287) != (a431))
% 2.15/2.30  (c7_2 (a294) zenon_X67)
% 2.15/2.30  ((a424) != zenon_X22)
% 2.15/2.30  (zenon_X39 != (a424))
% 2.15/2.30  (-. (c5_2 zenon_X7 zenon_X170))
% 2.15/2.30  ((a418) != zenon_X55)
% 2.15/2.30  (-. (c6_2 (a271) (a439)))
% 2.15/2.30  (-. (c5_2 zenon_X6 zenon_X150))
% 2.15/2.30  (-. (c8_2 zenon_X43 (a338)))
% 2.15/2.30  ((a347) != zenon_X63)
% 2.15/2.30  ((a418) != zenon_X110)
% 2.15/2.30  (-. (c5_2 (a280) (a299)))
% 2.15/2.30  (zenon_X25 != zenon_X23)
% 2.15/2.30  ((a418) != zenon_X47)
% 2.15/2.30  (ndr1_1 (a405))
% 2.15/2.30  ((a405) != (a443))
% 2.15/2.30  ((a286) != zenon_X164)
% 2.15/2.30  (c6_2 zenon_X7 (a429))
% 2.15/2.30  ((a389) != (a353))
% 2.15/2.30  ((a396) != zenon_X179)
% 2.15/2.30  ((a307) != (a434))
% 2.15/2.30  (c6_2 (a434) (a396))
% 2.15/2.30  ((a295) != (a286))
% 2.15/2.30  ((a380) != (a295))
% 2.15/2.30  ((a389) != zenon_X94)
% 2.15/2.30  ((a425) != zenon_X188)
% 2.15/2.30  ((a286) != zenon_X70)
% 2.15/2.30  (c2_1 (a431))
% 2.15/2.30  ((a327) != (a444))
% 2.15/2.30  (ndr1_0)
% 2.15/2.30  (zenon_X31 != (a319))
% 2.15/2.30  (-. (c5_2 (a448) (a292)))
% 2.15/2.30  ((a370) != (a410))
% 2.15/2.30  ((a347) != zenon_X139)
% 2.15/2.30  ((a379) != zenon_X164)
% 2.15/2.30  (-. (c8_2 zenon_X19 (a286)))
% 2.15/2.30  (c8_2 zenon_X19 (a279))
% 2.15/2.30  (zenon_X32 != zenon_X7)
% 2.15/2.30  (zenon_X19 != zenon_X22)
% 2.15/2.30  (c3_2 (a319) (a292))
% 2.15/2.30  ((a290) != zenon_X116)
% 2.15/2.30  (-. (c10_1 zenon_X32))
% 2.15/2.30  ((a448) != (a405))
% 2.15/2.30  (-. (c2_2 (a317) zenon_X42))
% 2.15/2.30  (-. (c7_2 zenon_X23 (a439)))
% 2.15/2.30  (-. (c7_2 (a416) (a347)))
% 2.15/2.30  (-. (c9_1 (a434)))
% 2.15/2.30  ((a299) != zenon_X149)
% 2.15/2.30  (-. (c10_1 zenon_X19))
% 2.15/2.30  ((a286) != zenon_X188)
% 2.15/2.30  (c6_2 (a319) (a286))
% 2.15/2.30  (zenon_X6 != (a291))
% 2.15/2.30  ((a290) != (a389))
% 2.15/2.30  ((a379) != zenon_X190)
% 2.15/2.30  ((a293) != zenon_X190)
% 2.15/2.30  (c6_1 (a352))
% 2.15/2.30  (c7_1 (a278))
% 2.15/2.30  ((a439) != zenon_X163)
% 2.15/2.30  ((a363) != (a417))
% 2.15/2.30  (c8_2 zenon_X39 (a299))
% 2.15/2.30  ((a417) != zenon_X97)
% 2.15/2.30  ((a379) != (a425))
% 2.15/2.30  (-. (c7_2 (a408) zenon_X10))
% 2.15/2.30  (-. (c10_1 (a327)))
% 2.15/2.30  (-. (c7_2 (a434) (a425)))
% 2.15/2.30  ((a344) != zenon_X79)
% 2.15/2.30  ((a294) != (a278))
% 2.15/2.30  (ndr1_1 zenon_X23)
% 2.15/2.30  (zenon_X18 != (a424))
% 2.15/2.30  ((a347) != zenon_X112)
% 2.15/2.30  ((a292) != zenon_X100)
% 2.15/2.30  ((a429) != zenon_X184)
% 2.15/2.30  ((a279) != zenon_X166)
% 2.15/2.30  (-. (c10_1 zenon_X22))
% 2.15/2.30  ((a443) != zenon_X32)
% 2.15/2.30  (-. (c8_2 (a434) zenon_X55))
% 2.15/2.30  (c3_1 zenon_X18)
% 2.15/2.30  ((a396) != zenon_X36)
% 2.15/2.30  (c5_2 zenon_X32 (a389))
% 2.15/2.30  (c6_2 (a443) (a425))
% 2.15/2.30  ((a418) != zenon_X167)
% 2.15/2.30  (-. (c10_1 zenon_X6))
% 2.15/2.30  (zenon_X22 != (a327))
% 2.15/2.30  ((a286) != zenon_X175)
% 2.15/2.30  (c7_2 zenon_X27 (a347))
% 2.15/2.30  ((a405) != (a280))
% 2.15/2.30  ((a417) != (a338))
% 2.15/2.30  ((a299) != (a425))
% 2.15/2.30  (c6_2 (a434) (a439))
% 2.15/2.30  (c6_2 zenon_X23 (a379))
% 2.15/2.30  (-. (c7_2 (a444) (a425)))
% 2.15/2.30  ((a370) != zenon_X166)
% 2.15/2.30  (-. (c7_2 (a424) (a379)))
% 2.15/2.30  (c6_2 zenon_X23 (a286))
% 2.15/2.30  (c3_2 (a408) (a439))
% 2.15/2.30  (-. (c5_2 (a280) (a289)))
% 2.15/2.30  ((a395) != zenon_X25)
% 2.15/2.30  (zenon_X45 != zenon_X13)
% 2.15/2.30  (-. (c8_2 (a327) (a286)))
% 2.15/2.30  (zenon_X31 != zenon_X21)
% 2.15/2.30  (zenon_X19 != (a352))
% 2.15/2.30  (c7_1 (a434))
% 2.15/2.30  ((a395) != zenon_X23)
% 2.15/2.30  ((a279) != (a440))
% 2.15/2.30  ((a379) != zenon_X38)
% 2.15/2.30  (zenon_X25 != zenon_X21)
% 2.15/2.30  ((a294) != (a408))
% 2.15/2.30  (-. (c3_2 zenon_X19 zenon_X181))
% 2.15/2.30  (c1_1 zenon_X39)
% 2.15/2.30  ((a379) != zenon_X179)
% 2.15/2.30  ((a395) != (a424))
% 2.15/2.30  (-. (c6_2 (a271) (a440)))
% 2.15/2.30  (c6_2 zenon_X32 (a396))
% 2.15/2.30  (c6_2 (a424) (a429))
% 2.15/2.30  (-. (c5_2 (a444) (a290)))
% 2.15/2.30  ((a327) != zenon_X28)
% 2.15/2.30  (c3_2 (a319) (a410))
% 2.15/2.30  ((a279) != (a409))
% 2.15/2.30  ((a271) != (a431))
% 2.15/2.30  (c6_2 zenon_X8 (a279))
% 2.15/2.30  (-. (c5_2 zenon_X22 (a429)))
% 2.15/2.30  (-. (c7_2 (a416) (a425)))
% 2.15/2.30  (c3_2 zenon_X6 (a347))
% 2.15/2.30  ((a287) != zenon_X13)
% 2.15/2.30  (c10_1 zenon_X43)
% 2.15/2.30  (c4_2 (a448) (a389))
% 2.15/2.30  (zenon_X22 != (a369))
% 2.15/2.30  ((a279) != zenon_X188)
% 2.15/2.30  (-. (c6_2 zenon_X6 (a429)))
% 2.15/2.30  ((a425) != zenon_X123)
% 2.15/2.30  (c10_2 zenon_X35 (a347))
% 2.15/2.30  ((a289) != zenon_X82)
% 2.15/2.30  ((a389) != zenon_X100)
% 2.15/2.30  (zenon_X21 != (a416))
% 2.15/2.30  (c10_2 zenon_X25 (a347))
% 2.15/2.30  (c6_2 (a294) (a417))
% 2.15/2.30  ((a429) != (a289))
% 2.15/2.30  (-. (c5_2 (a307) (a299)))
% 2.15/2.30  ((a347) != zenon_X38)
% 2.15/2.30  (c6_2 (a424) (a344))
% 2.15/2.30  ((a344) != zenon_X44)
% 2.15/2.30  ((a431) != zenon_X21)
% 2.15/2.30  ((a389) != zenon_X101)
% 2.15/2.30  ((a379) != zenon_X120)
% 2.15/2.30  ((a271) != zenon_X28)
% 2.15/2.30  ((a299) != zenon_X113)
% 2.15/2.30  (c3_2 (a280) (a344))
% 2.15/2.30  (zenon_X7 != zenon_X28)
% 2.15/2.30  (c4_1 (a327))
% 2.15/2.30  ((a291) != (a448))
% 2.15/2.30  ((a352) != (a302))
% 2.15/2.30  (c7_1 (a280))
% 2.15/2.30  ((a389) != (a425))
% 2.15/2.30  ((a278) != zenon_X13)
% 2.15/2.30  (zenon_X35 != (a287))
% 2.15/2.30  (-. (c3_2 (a424) zenon_X70))
% 2.15/2.30  ((a287) != (a307))
% 2.15/2.30  (-. (c6_2 zenon_X35 (a440)))
% 2.15/2.30  ((a352) != (a434))
% 2.15/2.30  (c10_2 (a317) (a410))
% 2.15/2.30  (c6_2 (a405) (a429))
% 2.15/2.30  ((a389) != zenon_X137)
% 2.15/2.30  ((a409) != zenon_X188)
% 2.15/2.30  ((a290) != zenon_X106)
% 2.15/2.30  (zenon_X25 != zenon_X28)
% 2.15/2.30  ((a435) != (a380))
% 2.15/2.30  ((a425) != zenon_X36)
% 2.15/2.30  ((a291) != (a369))
% 2.15/2.30  (-. (c5_2 zenon_X13 (a299)))
% 2.15/2.30  (zenon_X27 != zenon_X23)
% 2.15/2.30  ((a299) != zenon_X74)
% 2.15/2.30  (-. (c5_2 (a448) (a289)))
% 2.15/2.30  (c7_2 zenon_X45 (a347))
% 2.15/2.30  (zenon_X39 != (a291))
% 2.15/2.30  ((a417) != (a286))
% 2.15/2.30  (zenon_X6 != zenon_X21)
% 2.15/2.30  ((a317) != (a416))
% 2.15/2.30  (-. (c3_2 zenon_X7 zenon_X164))
% 2.15/2.30  ((a347) != zenon_X144)
% 2.15/2.30  ((a396) != zenon_X69)
% 2.15/2.30  (c8_2 (a291) (a389))
% 2.15/2.30  (c5_2 zenon_X7 (a299))
% 2.15/2.30  ((a294) != (a302))
% 2.15/2.30  ((a290) != (a425))
% 2.15/2.30  ((a299) != zenon_X89)
% 2.15/2.30  ((a344) != zenon_X30)
% 2.15/2.30  (-. (c10_1 (a280)))
% 2.15/2.30  (c7_1 zenon_X19)
% 2.15/2.30  (-. (c7_2 zenon_X45 (a286)))
% 2.15/2.30  ((a444) != (a332))
% 2.15/2.30  ((a344) != (a338))
% 2.15/2.30  (c10_2 (a317) (a347))
% 2.15/2.30  (c4_1 (a317))
% 2.15/2.30  (c3_1 (a343))
% 2.15/2.30  ((a409) != zenon_X70)
% 2.15/2.30  (zenon_X35 != zenon_X7)
% 2.15/2.30  ((a347) != zenon_X177)
% 2.15/2.30  ((a396) != zenon_X112)
% 2.15/2.30  (zenon_X22 != (a307))
% 2.15/2.30  ((a389) != zenon_X95)
% 2.15/2.30  ((a370) != zenon_X194)
% 2.15/2.30  (c6_2 (a352) (a379))
% 2.15/2.30  ((a417) != zenon_X61)
% 2.15/2.30  (c5_2 zenon_X43 (a389))
% 2.15/2.30  (c6_2 (a443) (a289))
% 2.15/2.30  (-. (c5_2 (a287) (a292)))
% 2.15/2.30  ((a443) != (a332))
% 2.15/2.30  (c2_2 (a408) (a409))
% 2.15/2.30  ((a279) != zenon_X101)
% 2.15/2.30  (c6_2 (a443) (a417))
% 2.15/2.30  (-. (c3_2 (a443) (a390)))
% 2.15/2.30  (c6_2 zenon_X31 (a379))
% 2.15/2.30  ((a417) != zenon_X63)
% 2.15/2.30  (zenon_X8 != (a369))
% 2.15/2.30  ((a448) != (a332))
% 2.15/2.30  (-. (c4_2 zenon_X35 (a279)))
% 2.15/2.30  (zenon_X39 != (a443))
% 2.15/2.30  ((a389) != zenon_X176)
% 2.15/2.30  (-. (c4_2 (a408) (a410)))
% 2.15/2.30  (-. (c4_1 (a444)))
% 2.15/2.30  (-. (c5_2 (a443) (a417)))
% 2.15/2.30  (c4_2 zenon_X43 (a389))
% 2.15/2.30  (c3_1 (a287))
% 2.15/2.30  ((a417) != zenon_X181)
% 2.15/2.30  (c6_2 zenon_X31 (a347))
% 2.15/2.30  ((a292) != zenon_X29)
% 2.15/2.30  ((a429) != zenon_X68)
% 2.15/2.30  ((a292) != zenon_X188)
% 2.15/2.30  ((a396) != (a290))
% 2.15/2.30  (c7_2 (a294) zenon_X10)
% 2.15/2.30  ((a319) != (a424))
% 2.15/2.30  (-. (c6_1 zenon_X23))
% 2.15/2.30  (c3_2 zenon_X35 (a439))
% 2.15/2.30  (c8_2 zenon_X32 (a389))
% 2.15/2.30  (-. (c5_2 (a448) (a299)))
% 2.15/2.30  ((a396) != zenon_X80)
% 2.15/2.30  (-. (c7_2 (a424) zenon_X122))
% 2.15/2.30  (-. (c3_2 zenon_X31 zenon_X180))
% 2.15/2.30  ((a287) != (a434))
% 2.15/2.30  ((a332) != zenon_X28)
% 2.15/2.30  (c6_2 (a416) (a299))
% 2.15/2.30  ((a410) != zenon_X70)
% 2.15/2.30  (c6_2 zenon_X7 (a396))
% 2.15/2.30  ((a352) != (a416))
% 2.15/2.30  ((a418) != zenon_X76)
% 2.15/2.30  ((a292) != zenon_X85)
% 2.15/2.30  (-. (c5_2 (a405) (a439)))
% 2.15/2.30  (c6_2 (a307) (a429))
% 2.15/2.30  ((a347) != zenon_X164)
% 2.15/2.30  (-. (c8_2 zenon_X28 (a286)))
% 2.15/2.30  (-. (c2_2 zenon_X18 (a389)))
% 2.15/2.30  (-. (c7_2 zenon_X13 (a379)))
% 2.15/2.30  ((a417) != zenon_X125)
% 2.15/2.30  (-. (c6_1 (a369)))
% 2.15/2.30  ((a280) != (a369))
% 2.15/2.30  (-. (c10_1 (a444)))
% 2.15/2.30  (-. (c5_2 (a271) (a418)))
% 2.15/2.30  ((a444) != (a369))
% 2.15/2.30  (-. (c7_2 zenon_X7 (a286)))
% 2.15/2.30  (-. (c5_2 (a448) (a418)))
% 2.15/2.30  (c6_1 zenon_X43)
% 2.15/2.30  (c7_1 (a444))
% 2.15/2.30  (-. (c8_2 zenon_X13 zenon_X141))
% 2.15/2.30  ((a405) != zenon_X19)
% 2.15/2.30  ((a279) != zenon_X77)
% 2.15/2.30  (-. (c9_1 zenon_X45))
% 2.15/2.30  (-. (c2_2 zenon_X15 (a380)))
% 2.15/2.30  ((a290) != zenon_X97)
% 2.15/2.30  ((a363) != zenon_X95)
% 2.15/2.30  ((a380) != zenon_X163)
% 2.15/2.30  (c6_2 (a416) (a279))
% 2.15/2.30  (c4_1 zenon_X6)
% 2.15/2.30  (c4_2 (a302) (a389))
% 2.15/2.30  (zenon_X35 != (a352))
% 2.15/2.30  (c6_2 (a332) (a425))
% 2.15/2.30  (c10_2 zenon_X16 (a347))
% 2.15/2.30  (-. (c7_2 (a434) (a417)))
% 2.15/2.30  (zenon_X35 != zenon_X25)
% 2.15/2.30  (c2_1 (a327))
% 2.15/2.30  (c1_1 zenon_X13)
% 2.15/2.30  ((a289) != zenon_X74)
% 2.15/2.30  (zenon_X39 != (a278))
% 2.15/2.30  ((a279) != zenon_X189)
% 2.15/2.30  (zenon_X8 != (a395))
% 2.15/2.30  (-. (c7_2 zenon_X28 (a347)))
% 2.15/2.30  (-. (c6_1 zenon_X6))
% 2.15/2.30  (zenon_X39 != (a307))
% 2.15/2.30  (c6_2 (a332) (a286))
% 2.15/2.30  ((a395) != (a434))
% 2.15/2.30  (-. (c2_2 (a280) zenon_X30))
% 2.15/2.30  ((a429) != zenon_X177)
% 2.15/2.30  (c6_2 (a369) (a396))
% 2.15/2.30  (zenon_X21 != (a444))
% 2.15/2.30  (-. (c6_2 (a317) (a396)))
% 2.15/2.30  (c4_1 zenon_X39)
% 2.15/2.30  ((a425) != zenon_X73)
% 2.15/2.30  (zenon_X21 != zenon_X23)
% 2.15/2.30  ((a363) != (a299))
% 2.15/2.30  ((a307) != (a416))
% 2.15/2.30  ((a280) != zenon_X23)
% 2.15/2.30  (c6_1 (a405))
% 2.15/2.30  (c8_2 (a271) (a363))
% 2.15/2.30  ((a418) != (a292))
% 2.15/2.30  ((a278) != zenon_X8)
% 2.15/2.30  ((a439) != zenon_X184)
% 2.15/2.30  (c10_2 zenon_X6 (a347))
% 2.15/2.30  ((a425) != zenon_X121)
% 2.15/2.30  ((a299) != zenon_X93)
% 2.15/2.30  ((a424) != (a369))
% 2.15/2.30  (c3_1 zenon_X7)
% 2.15/2.30  ((a279) != zenon_X171)
% 2.15/2.30  (zenon_X32 != (a416))
% 2.15/2.30  (c7_2 (a302) (a439))
% 2.15/2.30  ((a286) != zenon_X187)
% 2.15/2.30  (zenon_X6 != zenon_X39)
% 2.15/2.30  ((a396) != zenon_X194)
% 2.15/2.30  (-. (c8_2 zenon_X18 (a429)))
% 2.15/2.30  (zenon_X37 != (a443))
% 2.15/2.30  ((a443) != zenon_X22)
% 2.15/2.30  (c6_2 (a327) (a363))
% 2.15/2.30  ((a289) != (a347))
% 2.15/2.30  ((a439) != zenon_X147)
% 2.15/2.30  ((a291) != (a416))
% 2.15/2.30  ((a363) != (a338))
% 2.15/2.30  (c6_2 (a291) (a417))
% 2.15/2.30  (-. (c5_2 (a431) (a292)))
% 2.15/2.30  ((a425) != zenon_X68)
% 2.15/2.30  ((a292) != zenon_X40)
% 2.15/2.30  ((a417) != (a353))
% 2.15/2.30  ((a363) != zenon_X110)
% 2.15/2.30  ((a352) != (a369))
% 2.15/2.30  ((a294) != zenon_X28)
% 2.15/2.30  (-. (c8_2 zenon_X21 (a286)))
% 2.15/2.30  (c3_1 (a448))
% 2.15/2.30  ((a317) != (a294))
% 2.15/2.30  (c6_2 (a395) (a279))
% 2.15/2.30  ((a299) != zenon_X95)
% 2.15/2.30  (ndr1_1 (a408))
% 2.15/2.30  (c6_1 zenon_X45)
% 2.15/2.30  (c10_1 zenon_X8)
% 2.15/2.30  ((a363) != zenon_X26)
% 2.15/2.30  ((a444) != zenon_X23)
% 2.15/2.30  ((a299) != zenon_X94)
% 2.15/2.30  (-. (c5_2 (a280) (a279)))
% 2.15/2.30  ((a417) != zenon_X55)
% 2.15/2.30  (c7_2 (a327) (a439))
% 2.15/2.30  (-. (c4_1 (a405)))
% 2.15/2.30  (c6_2 zenon_X19 (a347))
% 2.15/2.30  ((a416) != (a424))
% 2.15/2.30  (-. (c5_2 (a317) (a418)))
% 2.15/2.30  (-. (c8_2 (a302) (a286)))
% 2.15/2.30  ((a286) != zenon_X166)
% 2.15/2.30  ((a286) != zenon_X179)
% 2.15/2.30  (zenon_X21 != zenon_X7)
% 2.15/2.30  ((a347) != zenon_X75)
% 2.15/2.30  (c1_1 (a434))
% 2.15/2.30  (-. (c5_2 (a307) (a389)))
% 2.15/2.30  ((a352) != zenon_X21)
% 2.15/2.30  ((a370) != (a286))
% 2.15/2.30  ((a417) != zenon_X69)
% 2.15/2.30  ((a289) != (a295))
% 2.15/2.30  (-. (c5_2 (a444) (a289)))
% 2.15/2.30  (c3_2 (a408) (a429))
% 2.15/2.30  (c6_2 (a280) (a295))
% 2.15/2.30  ((a439) != zenon_X80)
% 2.15/2.30  ((a279) != zenon_X48)
% 2.15/2.30  (-. (c5_2 zenon_X13 (a289)))
% 2.15/2.30  ((a409) != zenon_X24)
% 2.15/2.30  (c6_2 (a434) (a286))
% 2.15/2.30  (c3_1 (a271))
% 2.15/2.30  ((a292) != zenon_X48)
% 2.15/2.30  ((a429) != (a288))
% 2.15/2.30  ((a299) != zenon_X103)
% 2.15/2.30  (-. (c5_2 zenon_X8 zenon_X95))
% 2.15/2.30  (c7_2 (a431) (a439))
% 2.15/2.30  ((a389) != (a303))
% 2.15/2.30  (zenon_X22 != zenon_X16)
% 2.15/2.30  (c3_2 (a319) (a409))
% 2.15/2.30  ((a289) != (a409))
% 2.15/2.30  ((a289) != zenon_X77)
% 2.15/2.30  (c3_1 (a280))
% 2.15/2.30  ((a292) != zenon_X4)
% 2.15/2.30  (zenon_X21 != (a434))
% 2.15/2.30  ((a429) != zenon_X173)
% 2.15/2.31  ((a352) != (a424))
% 2.15/2.31  (-. (c5_2 (a302) (a303)))
% 2.15/2.31  (c5_2 (a405) (a299))
% 2.15/2.31  ((a379) != zenon_X125)
% 2.15/2.31  (-. (c6_2 (a317) (a293)))
% 2.15/2.31  (zenon_X41 != (a380))
% 2.15/2.31  (ndr1_1 zenon_X21)
% 2.15/2.31  (zenon_X32 != zenon_X6)
% 2.15/2.31  ((a286) != zenon_X61)
% 2.15/2.31  ((a280) != (a424))
% 2.15/2.31  (zenon_X41 != zenon_X0)
% 2.15/2.31  (-. (c5_2 (a352) (a289)))
% 2.15/2.31  (c3_2 (a444) (a379))
% 2.15/2.31  (-. (c1_1 (a369)))
% 2.15/2.31  (c7_1 zenon_X31)
% 2.15/2.31  ((a347) != zenon_X187)
% 2.15/2.31  ((a278) != (a416))
% 2.15/2.31  (c6_2 (a369) (a439))
% 2.15/2.31  ((a389) != zenon_X3)
% 2.15/2.31  (-. (c2_2 zenon_X43 (a389)))
% 2.15/2.31  (c6_2 zenon_X21 (a429))
% 2.15/2.31  ((a287) != zenon_X7)
% 2.15/2.31  (zenon_X6 != (a271))
% 2.15/2.31  ((a327) != (a280))
% 2.15/2.31  ((a439) != zenon_X10)
% 2.15/2.31  ((a292) != zenon_X90)
% 2.15/2.31  (zenon_X27 != (a405))
% 2.15/2.31  (c5_2 (a416) (a417))
% 2.15/2.31  (c7_2 zenon_X6 (a347))
% 2.15/2.31  ((a429) != zenon_X188)
% 2.15/2.31  ((a425) != zenon_X112)
% 2.15/2.31  ((a424) != zenon_X28)
% 2.15/2.31  (zenon_X13 != zenon_X22)
% 2.15/2.31  (c6_2 zenon_X32 (a370))
% 2.15/2.31  ((a370) != zenon_X188)
% 2.15/2.31  ((a289) != zenon_X20)
% 2.15/2.31  (c6_2 (a327) (a286))
% 2.15/2.31  (-. (c5_2 (a434) (a290)))
% 2.15/2.31  ((a279) != zenon_X82)
% 2.15/2.31  ((a389) != (a417))
% 2.15/2.31  ((a290) != zenon_X98)
% 2.15/2.31  ((a307) != zenon_X34)
% 2.15/2.31  (zenon_X6 != (a317))
% 2.15/2.31  (c6_1 (a395))
% 2.15/2.31  (c9_2 (a444) (a347))
% 2.15/2.31  (c6_2 zenon_X27 (a286))
% 2.15/2.31  (c6_2 zenon_X8 (a425))
% 2.15/2.31  (zenon_X31 != zenon_X32)
% 2.15/2.31  ((a395) != zenon_X39)
% 2.15/2.31  (c6_1 zenon_X32)
% 2.15/2.31  ((a317) != (a448))
% 2.15/2.31  ((a395) != (a405))
% 2.15/2.31  ((a279) != (a288))
% 2.15/2.31  (c6_2 (a352) (a425))
% 2.15/2.31  ((a292) != zenon_X24)
% 2.15/2.31  ((a352) != zenon_X16)
% 2.15/2.31  (-. (c5_2 zenon_X22 (a439)))
% 2.15/2.31  ((a425) != zenon_X194)
% 2.15/2.31  (c6_2 (a271) (a289))
% 2.15/2.31  ((a279) != zenon_X138)
% 2.15/2.31  (c5_2 (a287) (a389))
% 2.15/2.31  (-. (c6_1 (a332)))
% 2.15/2.31  (-. (c1_2 zenon_X15 (a380)))
% 2.15/2.31  (-. (c8_2 (a434) (a286)))
% 2.15/2.31  (zenon_X19 != (a271))
% 2.15/2.31  ((a271) != zenon_X27)
% 2.15/2.31  ((a291) != (a307))
% 2.15/2.31  ((a289) != zenon_X4)
% 2.15/2.31  ((a439) != zenon_X61)
% 2.15/2.31  (c9_1 (a431))
% 2.15/2.31  ((a317) != (a327))
% 2.15/2.31  (c3_2 (a369) (a370))
% 2.15/2.31  ((a418) != zenon_X109)
% 2.15/2.31  (c8_2 zenon_X6 (a299))
% 2.15/2.31  (-. (c1_1 (a405)))
% 2.15/2.31  (-. (c8_2 zenon_X13 (a286)))
% 2.15/2.31  ((a389) != (a299))
% 2.15/2.31  (-. (c7_2 zenon_X19 (a439)))
% 2.15/2.31  (-. (c2_2 (a294) (a389)))
% 2.15/2.31  (c6_2 (a444) (a418))
% 2.15/2.31  ((a395) != (a302))
% 2.15/2.31  (c5_2 zenon_X18 (a299))
% 2.15/2.31  ((a288) != (a380))
% 2.15/2.31  ((a279) != (a380))
% 2.15/2.31  ((a319) != (a307))
% 2.15/2.31  (-. (c7_2 zenon_X25 (a286)))
% 2.15/2.31  (zenon_X45 != zenon_X27)
% 2.15/2.31  ((a290) != zenon_X48)
% 2.15/2.31  ((a429) != zenon_X10)
% 2.15/2.31  (-. (c5_2 zenon_X39 zenon_X149))
% 2.15/2.31  (c7_2 (a294) zenon_X38)
% 2.15/2.31  ((a294) != zenon_X32)
% 2.15/2.31  (-. (c7_2 (a332) (a286)))
% 2.15/2.31  ((a352) != (a327))
% 2.15/2.31  ((a425) != zenon_X172)
% 2.15/2.31  ((a389) != (a380))
% 2.15/2.31  ((a294) != (a424))
% 2.15/2.31  (-. (c10_2 (a302) (a338)))
% 2.15/2.31  ((a439) != zenon_X126)
% 2.15/2.31  (-. (c10_1 (a416)))
% 2.15/2.31  ((a396) != zenon_X190)
% 2.15/2.31  ((a396) != zenon_X166)
% 2.15/2.31  (-. (c5_2 (a327) (a299)))
% 2.15/2.31  (-. (c5_2 (a327) (a390)))
% 2.15/2.31  (c6_2 (a278) (a279))
% 2.15/2.31  ((a347) != zenon_X67)
% 2.15/2.31  (c6_2 zenon_X16 (a410))
% 2.15/2.31  ((a389) != (a286))
% 2.15/2.31  (c8_2 zenon_X19 (a418))
% 2.15/2.31  (-. (c5_2 zenon_X32 zenon_X195))
% 2.15/2.31  (zenon_X7 != zenon_X22)
% 2.15/2.31  (-. (c1_2 zenon_X22 (a347)))
% 2.15/2.31  ((a396) != zenon_X163)
% 2.15/2.31  ((a409) != zenon_X44)
% 2.15/2.31  ((a279) != zenon_X90)
% 2.15/2.31  (-. (c5_2 (a434) (a279)))
% 2.15/2.31  (-. (c6_2 zenon_X35 zenon_X190))
% 2.15/2.31  ((a302) != (a271))
% 2.15/2.31  (zenon_X43 != (a448))
% 2.15/2.31  ((a417) != zenon_X109)
% 2.15/2.31  (-. (c5_2 (a294) (a289)))
% 2.15/2.31  ((a395) != zenon_X43)
% 2.15/2.31  (zenon_X35 != zenon_X32)
% 2.15/2.31  (-. (c10_2 (a405) (a347)))
% 2.15/2.31  (c8_1 (a307))
% 2.15/2.31  (-. (c5_2 (a444) (a299)))
% 2.15/2.31  ((a289) != zenon_X105)
% 2.15/2.31  (c7_2 (a444) (a379))
% 2.15/2.31  (-. (c5_2 (a332) (a299)))
% 2.15/2.31  ((a418) != zenon_X103)
% 2.15/2.31  (c6_2 (a280) (a344))
% 2.15/2.31  (zenon_X7 != zenon_X23)
% 2.15/2.31  (-. (c5_2 zenon_X13 zenon_X138))
% 2.15/2.31  (-. (c6_2 zenon_X39 (a347)))
% 2.15/2.31  ((a344) != zenon_X40)
% 2.15/2.31  ((a431) != (a405))
% 2.15/2.31  (c3_2 (a317) (a347))
% 2.15/2.31  ((a439) != zenon_X190)
% 2.15/2.31  (c6_2 (a369) (a347))
% 2.15/2.31  (zenon_X43 != (a443))
% 2.15/2.31  (c6_2 (a280) (a292))
% 2.15/2.31  (ndr1_1 (a271))
% 2.15/2.31  ((a425) != zenon_X65)
% 2.15/2.31  (-. (c10_1 zenon_X45))
% 2.15/2.31  ((a425) != (a439))
% 2.15/2.31  ((a302) != (a319))
% 2.15/2.31  (-. (c6_1 zenon_X27))
% 2.15/2.31  (zenon_X39 != (a327))
% 2.15/2.31  (-. (c5_2 (a424) (a289)))
% 2.15/2.31  ((a429) != zenon_X190)
% 2.15/2.31  ((a425) != zenon_X181)
% 2.15/2.31  (zenon_X31 != zenon_X18)
% 2.15/2.31  (c6_2 (a416) (a418))
% 2.15/2.31  (c4_2 zenon_X18 (a389))
% 2.15/2.31  (c6_2 (a369) (a429))
% 2.15/2.31  ((a347) != zenon_X166)
% 2.15/2.31  (zenon_X43 != zenon_X27)
% 2.15/2.31  ((a429) != zenon_X61)
% 2.15/2.31  ((a287) != zenon_X31)
% 2.15/2.31  (-. (c10_1 zenon_X13))
% 2.15/2.31  ((a405) != (a307))
% 2.15/2.31  ((a317) != (a405))
% 2.15/2.31  (c4_2 (a280) (a370))
% 2.15/2.31  (-. (c5_2 (a444) (a417)))
% 2.15/2.31  (c6_1 (a307))
% 2.15/2.31  (c10_2 zenon_X27 (a347))
% 2.15/2.31  ((a290) != zenon_X107)
% 2.15/2.31  ((a439) != zenon_X69)
% 2.15/2.31  (zenon_X39 != zenon_X27)
% 2.15/2.31  ((a271) != (a444))
% 2.15/2.31  (zenon_X27 != (a424))
% 2.15/2.31  ((a291) != zenon_X31)
% 2.15/2.31  ((a363) != zenon_X86)
% 2.15/2.31  (zenon_X31 != (a278))
% 2.15/2.31  (zenon_X39 != (a448))
% 2.15/2.31  (-. (c10_1 (a434)))
% 2.15/2.31  (-. (c8_2 (a280) (a286)))
% 2.15/2.31  ((a292) != zenon_X116)
% 2.15/2.31  ((a307) != (a280))
% 2.15/2.31  ((a417) != zenon_X56)
% 2.15/2.31  (-. (c7_2 zenon_X22 zenon_X145))
% 2.15/2.31  ((a379) != (a289))
% 2.15/2.31  ((a293) != zenon_X108)
% 2.15/2.31  ((a317) != (a280))
% 2.15/2.31  (zenon_X30 != zenon_X42)
% 2.15/2.31  (zenon_X8 != zenon_X16)
% 2.15/2.31  ((a431) != (a443))
% 2.15/2.31  (ndr1_1 (a416))
% 2.15/2.31  ((a425) != zenon_X164)
% 2.15/2.31  (c7_1 (a448))
% 2.15/2.31  (ndr1_1 zenon_X31)
% 2.15/2.31  ((a425) != zenon_X38)
% 2.15/2.31  (zenon_X8 != (a327))
% 2.15/2.31  (zenon_X43 != zenon_X21)
% 2.15/2.31  ((a327) != zenon_X27)
% 2.15/2.31  ((a429) != zenon_X189)
% 2.15/2.31  ((a317) != zenon_X21)
% 2.15/2.31  (c10_2 (a271) (a347))
% 2.15/2.31  (ndr1_1 (a434))
% 2.15/2.31  (c6_2 (a424) (a418))
% 2.15/2.31  ((a279) != zenon_X56)
% 2.15/2.31  ((a369) != (a307))
% 2.15/2.31  (ndr1_1 zenon_X19)
% 2.15/2.31  (c6_2 (a287) (a279))
% 2.15/2.31  ((a271) != (a278))
% 2.15/2.31  ((a299) != zenon_X112)
% 2.15/2.31  (c5_2 (a278) (a299))
% 2.15/2.31  (zenon_X45 != (a327))
% 2.15/2.31  ((a425) != zenon_X179)
% 2.15/2.31  (-. (c4_1 (a416)))
% 2.15/2.31  (c6_2 (a395) (a439))
% 2.15/2.31  ((a291) != (a319))
% 2.15/2.31  (zenon_X32 != zenon_X22)
% 2.15/2.31  (zenon_X16 != zenon_X13)
% 2.15/2.31  ((a448) != zenon_X18)
% 2.15/2.31  (ndr1_1 (a317))
% 2.15/2.31  ((a417) != zenon_X164)
% 2.15/2.31  ((a307) != (a444))
% 2.15/2.31  (c6_2 (a431) (a425))
% 2.15/2.31  ((a439) != zenon_X179)
% 2.15/2.31  (-. (c4_1 zenon_X21))
% 2.15/2.31  ((a317) != (a332))
% 2.15/2.31  ((a302) != (a416))
% 2.15/2.31  ((a396) != (a390))
% 2.15/2.31  ((a286) != zenon_X75)
% 2.15/2.31  (-. (c5_2 zenon_X8 (a440)))
% 2.15/2.31  (-. (c8_2 zenon_X28 zenon_X169))
% 2.15/2.31  ((a396) != (a440))
% 2.15/2.31  (ndr1_1 zenon_X22)
% 2.15/2.31  (c6_2 (a327) (a418))
% 2.15/2.31  ((a379) != zenon_X123)
% 2.15/2.31  (c7_2 (a448) (a439))
% 2.15/2.31  (zenon_X27 != zenon_X13)
% 2.15/2.31  ((a299) != zenon_X159)
% 2.15/2.31  ((a280) != zenon_X13)
% 2.15/2.31  (c2_2 (a444) (a295))
% 2.15/2.31  ((a439) != zenon_X122)
% 2.15/2.31  (zenon_X43 != (a291))
% 2.15/2.31  (zenon_X18 != zenon_X13)
% 2.15/2.31  (-. (c5_2 (a280) (a292)))
% 2.15/2.31  (zenon_X43 != zenon_X45)
% 2.15/2.31  ((a389) != zenon_X178)
% 2.15/2.31  (zenon_X39 != zenon_X13)
% 2.15/2.31  ((a431) != zenon_X28)
% 2.15/2.31  ((a439) != zenon_X38)
% 2.15/2.31  ((a291) != (a278))
% 2.15/2.31  ((a287) != (a405))
% 2.15/2.31  ((a431) != (a319))
% 2.15/2.31  (-. (c5_2 (a434) zenon_X81))
% 2.15/2.31  ((a279) != (a299))
% 2.15/2.31  ((a294) != zenon_X39)
% 2.15/2.31  (-. (c1_2 zenon_X18 (a347)))
% 2.15/2.31  (zenon_X16 != (a307))
% 2.15/2.31  ((a417) != zenon_X163)
% 2.15/2.31  (c6_2 (a291) (a286))
% 2.15/2.31  ((a319) != zenon_X19)
% 2.15/2.31  ((a292) != (a409))
% 2.15/2.31  ((a395) != (a332))
% 2.15/2.31  ((a271) != (a294))
% 2.15/2.31  ((a439) != zenon_X120)
% 2.15/2.31  (c6_2 (a434) (a418))
% 2.15/2.31  ((a286) != zenon_X193)
% 2.15/2.31  ((a439) != zenon_X175)
% 2.15/2.31  ((a319) != (a444))
% 2.15/2.31  (-. (c4_2 zenon_X35 (a396)))
% 2.15/2.31  (c3_1 (a431))
% 2.15/2.31  (-. (c6_2 zenon_X43 (a347)))
% 2.15/2.31  (c6_2 (a416) (a396))
% 2.15/2.31  ((a425) != zenon_X190)
% 2.15/2.31  ((a379) != zenon_X79)
% 2.15/2.31  ((a271) != (a443))
% 2.15/2.31  (c6_2 (a307) (a347))
% 2.15/2.31  (c6_2 (a280) (a379))
% 2.15/2.31  (zenon_X6 != (a416))
% 2.15/2.31  (c7_2 (a424) (a425))
% 2.15/2.31  (c6_2 (a448) (a417))
% 2.15/2.31  (zenon_X7 != (a271))
% 2.15/2.31  (c6_2 (a327) (a417))
% 2.15/2.31  (-. (c7_2 zenon_X19 (a347)))
% 2.15/2.31  ((a379) != zenon_X80)
% 2.15/2.31  (zenon_X32 != (a327))
% 2.15/2.31  (c6_2 zenon_X19 (a396))
% 2.15/2.31  (c9_2 (a327) (a390))
% 2.15/2.31  (c6_2 zenon_X7 (a425))
% 2.15/2.31  (-. (c7_2 (a434) zenon_X38))
% 2.15/2.31  ((a435) != (a417))
% 2.15/2.31  ((a448) != (a434))
% 2.15/2.31  ((a307) != (a302))
% 2.15/2.31  ((a302) != (a424))
% 2.15/2.31  ((a405) != zenon_X22)
% 2.15/2.31  ((a379) != zenon_X61)
% 2.15/2.31  (c5_2 zenon_X19 (a292))
% 2.15/2.31  ((a435) != zenon_X5)
% 2.15/2.31  ((a448) != (a278))
% 2.15/2.31  ((a347) != (a288))
% 2.15/2.31  (c3_1 (a294))
% 2.15/2.31  (c6_2 (a278) (a396))
% 2.15/2.31  ((a444) != zenon_X15)
% 2.15/2.31  (-. (c1_2 zenon_X27 (a347)))
% 2.15/2.31  ((a389) != (a409))
% 2.15/2.31  (-. (c7_2 zenon_X39 (a286)))
% 2.15/2.31  ((a292) != zenon_X11)
% 2.15/2.31  ((a417) != zenon_X87)
% 2.15/2.31  ((a425) != zenon_X175)
% 2.15/2.31  (c6_2 (a369) (a370))
% 2.15/2.31  ((a295) != (a290))
% 2.15/2.31  (c10_1 (a291))
% 2.15/2.31  (zenon_X39 != (a271))
% 2.15/2.31  (-. (c7_2 (a280) (a286)))
% 2.15/2.31  (-. (c5_2 (a307) (a290)))
% 2.15/2.31  ((a431) != (a352))
% 2.15/2.31  (zenon_X8 != zenon_X27)
% 2.15/2.31  (c6_2 zenon_X19 (a425))
% 2.15/2.31  (-. (c1_1 zenon_X22))
% 2.15/2.31  ((a294) != (a443))
% 2.15/2.31  ((a288) != (a417))
% 2.15/2.31  (zenon_X21 != zenon_X22)
% 2.15/2.31  (zenon_X39 != (a405))
% 2.15/2.31  ((a289) != (a279))
% 2.15/2.31  (c5_2 zenon_X19 (a279))
% 2.15/2.31  ((a287) != zenon_X22)
% 2.15/2.31  ((a287) != (a317))
% 2.15/2.31  (-. (c4_1 (a332)))
% 2.15/2.31  (zenon_X19 != (a434))
% 2.15/2.31  ((a417) != zenon_X71)
% 2.15/2.31  (zenon_X0 != (a410))
% 2.15/2.31  (-. (c8_2 zenon_X7 zenon_X113))
% 2.15/2.31  (-. (c10_1 zenon_X39))
% 2.15/2.31  (c6_2 zenon_X8 (a439))
% 2.15/2.31  (zenon_X27 != (a444))
% 2.15/2.31  (c7_2 zenon_X22 (a347))
% 2.15/2.31  ((a286) != zenon_X190)
% 2.15/2.31  (-. (c6_2 zenon_X43 (a293)))
% 2.15/2.31  ((a409) != zenon_X42)
% 2.15/2.31  ((a279) != (a370))
% 2.15/2.31  (zenon_X8 != zenon_X25)
% 2.15/2.31  ((a418) != (a288))
% 2.15/2.31  (c7_2 zenon_X25 (a347))
% 2.15/2.31  (-. (c4_2 zenon_X35 (a379)))
% 2.15/2.31  (-. (c7_2 (a319) (a286)))
% 2.15/2.31  (c3_2 (a294) (a295))
% 2.15/2.31  ((a395) != zenon_X22)
% 2.15/2.31  (-. (c5_2 (a443) (a390)))
% 2.15/2.31  (c3_1 zenon_X25)
% 2.15/2.31  (-. (c7_2 (a280) zenon_X126))
% 2.15/2.31  (-. (c4_2 zenon_X35 (a293)))
% 2.15/2.31  ((a418) != zenon_X90)
% 2.15/2.31  (c5_2 (a278) (a389))
% 2.15/2.31  (c9_2 zenon_X37 (a299))
% 2.15/2.31  (c8_2 (a291) (a292))
% 2.15/2.31  (-. (c8_2 (a302) (a338)))
% 2.15/2.31  (-. (c8_2 zenon_X8 zenon_X140))
% 2.15/2.31  (-. (c8_2 zenon_X18 zenon_X178))
% 2.15/2.31  (c4_2 (a395) (a389))
% 2.15/2.31  (-. (c1_1 zenon_X16))
% 2.15/2.31  (-. (c4_1 (a431)))
% 2.15/2.31  ((a327) != (a434))
% 2.15/2.31  ((a389) != zenon_X109)
% 2.15/2.31  ((a379) != zenon_X71)
% 2.15/2.31  (-. (c4_1 zenon_X23))
% 2.15/2.31  (-. (c5_2 (a332) (a292)))
% 2.15/2.31  ((a443) != (a302))
% 2.15/2.31  (c3_1 (a434))
% 2.15/2.31  (c7_1 zenon_X13)
% 2.15/2.31  (-. (c5_2 (a271) zenon_X110))
% 2.15/2.31  (ndr1_1 zenon_X15)
% 2.15/2.31  ((a434) != zenon_X28)
% 2.15/2.31  (-. (c5_2 (a271) (a292)))
% 2.15/2.31  (c6_2 (a444) (a425))
% 2.15/2.31  (c8_2 (a448) (a389))
% 2.15/2.31  (c7_2 zenon_X45 (a439))
% 2.15/2.31  (-. (c5_2 (a431) (a418)))
% 2.15/2.31  ((a347) != zenon_X124)
% 2.15/2.31  (c7_2 (a294) (a439))
% 2.15/2.31  (-. (c10_2 (a332) (a344)))
% 2.15/2.31  ((a439) != zenon_X73)
% 2.15/2.31  (c7_2 zenon_X18 (a347))
% 2.15/2.31  ((a379) != zenon_X65)
% 2.15/2.31  (c6_2 (a280) (a286))
% 2.15/2.31  (c6_2 zenon_X28 (a379))
% 2.15/2.31  (zenon_X21 != zenon_X13)
% 2.15/2.31  (-. (c8_2 (a369) zenon_X50))
% 2.15/2.31  (c9_1 zenon_X43)
% 2.15/2.31  ((a294) != (a444))
% 2.15/2.31  (-. (c8_2 (a319) (a286)))
% 2.15/2.31  ((a289) != zenon_X78)
% 2.15/2.31  (zenon_X19 != (a448))
% 2.15/2.31  (-. (c3_2 (a307) zenon_X174))
% 2.15/2.31  (c6_2 (a405) (a279))
% 2.15/2.31  (c10_1 (a443))
% 2.15/2.31  (c6_2 zenon_X16 (a292))
% 2.15/2.31  ((a389) != zenon_X167)
% 2.15/2.31  ((a389) != (a338))
% 2.15/2.31  (zenon_X8 != zenon_X13)
% 2.15/2.31  (-. (c5_2 (a332) (a279)))
% 2.15/2.31  (zenon_X31 != zenon_X7)
% 2.15/2.31  ((a317) != (a434))
% 2.15/2.31  ((a395) != (a278))
% 2.15/2.31  ((a410) != (a299))
% 2.15/2.31  (-. (c9_2 (a369) (a370)))
% 2.15/2.31  (-. (c8_2 zenon_X27 (a286)))
% 2.15/2.31  ((a279) != zenon_X78)
% 2.15/2.31  ((a425) != (a288))
% 2.15/2.31  ((a292) != zenon_X105)
% 2.15/2.31  (zenon_X8 != zenon_X7)
% 2.15/2.31  (zenon_X32 != zenon_X27)
% 2.15/2.31  (-. (c9_1 (a302)))
% 2.15/2.31  (zenon_X45 != (a280))
% 2.15/2.31  ((a287) != zenon_X32)
% 2.15/2.31  (-. (c2_2 (a278) (a410)))
% 2.15/2.31  ((a287) != (a352))
% 2.15/2.31  (c6_2 zenon_X16 (a344))
% 2.15/2.31  ((a299) != zenon_X86)
% 2.15/2.31  (-. (c9_1 (a416)))
% 2.15/2.31  (c8_2 zenon_X7 (a299))
% 2.15/2.31  (c2_2 (a444) zenon_X1)
% 2.15/2.31  (c6_2 zenon_X16 (a279))
% 2.15/2.31  ((a425) != zenon_X177)
% 2.15/2.31  (-. (c8_0))
% 2.15/2.31  (c3_1 (a317))
% 2.15/2.31  (zenon_X0 != (a417))
% 2.15/2.31  ((a379) != zenon_X121)
% 2.15/2.31  (zenon_X35 != (a319))
% 2.15/2.31  (c6_2 zenon_X8 (a417))
% 2.15/2.31  ((a292) != zenon_X47)
% 2.15/2.31  (c5_2 (a395) (a389))
% 2.15/2.31  (c6_2 (a416) (a379))
% 2.15/2.31  ((a396) != (a289))
% 2.15/2.31  ((a410) != zenon_X29)
% 2.15/2.31  (-. (c7_2 (a434) (a439)))
% 2.15/2.31  ((a292) != zenon_X55)
% 2.15/2.31  (zenon_X32 != zenon_X25)
% 2.15/2.31  (-. (c4_1 (a352)))
% 2.15/2.31  ((a291) != (a352))
% 2.15/2.31  (-. (c8_2 zenon_X25 zenon_X93))
% 2.15/2.31  (-. (c5_2 (a444) (a292)))
% 2.15/2.31  (-. (c1_2 zenon_X16 (a347)))
% 2.15/2.31  (c6_2 (a448) (a389))
% 2.15/2.31  (c10_2 zenon_X22 (a347))
% 2.15/2.31  ((a292) != zenon_X9)
% 2.15/2.31  ((a379) != zenon_X192)
% 2.15/2.31  (zenon_X6 != (a327))
% 2.15/2.31  (c6_2 (a434) (a289))
% 2.15/2.31  (-. (c1_2 (a327) (a347)))
% 2.15/2.31  (zenon_X31 != zenon_X27)
% 2.15/2.31  (c6_2 (a287) (a299))
% 2.15/2.31  ((a278) != zenon_X19)
% 2.15/2.31  ((a417) != zenon_X172)
% 2.15/2.31  (-. (c3_2 (a443) zenon_X173))
% 2.15/2.31  (ndr1_1 (a352))
% 2.15/2.31  ((a417) != (a409))
% 2.15/2.31  ((a287) != (a444))
% 2.15/2.31  ((a417) != zenon_X9)
% 2.15/2.31  ((a332) != zenon_X23)
% 2.15/2.31  (c6_1 (a294))
% 2.15/2.31  (-. (c5_2 (a431) (a439)))
% 2.15/2.31  (c6_2 zenon_X13 (a429))
% 2.15/2.31  ((a439) != zenon_X67)
% 2.15/2.31  (-. (c9_1 (a369)))
% 2.15/2.31  ((a290) != (a292))
% 2.15/2.31  (c6_2 (a444) (a417))
% 2.15/2.31  ((a352) != zenon_X22)
% 2.15/2.31  ((a279) != (a344))
% 2.15/2.31  ((a389) != zenon_X41)
% 2.15/2.31  ((a287) != (a294))
% 2.15/2.31  (-. (c9_2 (a443) (a435)))
% 2.15/2.31  ((a389) != (a418))
% 2.15/2.31  ((a289) != zenon_X135)
% 2.15/2.31  (c6_2 (a448) (a379))
% 2.15/2.31  (c2_2 (a444) (a409))
% 2.15/2.31  (zenon_X19 != zenon_X23)
% 2.15/2.31  (-. (c5_2 (a443) zenon_X3))
% 2.15/2.31  (-. (c7_2 (a352) (a286)))
% 2.15/2.31  ((a389) != (a288))
% 2.15/2.31  (-. (c5_2 (a443) (a289)))
% 2.15/2.31  (-. (c7_2 (a416) (a439)))
% 2.15/2.31  ((a417) != zenon_X127)
% 2.15/2.31  ((a286) != zenon_X53)
% 2.15/2.31  (c6_2 zenon_X8 (a347))
% 2.15/2.31  (-. (c5_2 zenon_X8 (a299)))
% 2.15/2.31  ((a279) != zenon_X175)
% 2.15/2.31  ((a343) != (a332))
% 2.15/2.31  (zenon_X41 != (a344))
% 2.15/2.31  (-. (c9_1 (a307)))
% 2.15/2.31  ((a289) != zenon_X9)
% 2.15/2.31  (c6_2 (a307) (a289))
% 2.15/2.31  (c5_2 zenon_X35 (a363))
% 2.15/2.31  ((a347) != zenon_X29)
% 2.15/2.31  (c6_2 (a434) (a379))
% 2.15/2.31  ((a379) != (a390))
% 2.15/2.31  (-. (c2_1 (a395)))
% 2.15/2.31  ((a405) != zenon_X23)
% 2.15/2.31  (-. (c1_2 zenon_X45 (a347)))
% 2.15/2.31  (c6_2 zenon_X31 (a425))
% 2.15/2.31  (-. (c1_1 zenon_X27))
% 2.15/2.31  (c6_2 zenon_X32 (a347))
% 2.15/2.31  (zenon_X27 != (a416))
% 2.15/2.31  ((a448) != (a319))
% 2.15/2.31  ((a425) != (a338))
% 2.15/2.31  ((a417) != zenon_X79)
% 2.15/2.31  (c8_2 (a352) (a389))
% 2.15/2.31  ((a344) != zenon_X69)
% 2.15/2.31  (-. (c8_2 zenon_X39 (a286)))
% 2.15/2.31  (zenon_X18 != zenon_X27)
% 2.15/2.31  (-. (c4_2 (a343) (a344)))
% 2.15/2.31  (-. (c5_2 zenon_X18 (a439)))
% 2.15/2.31  (-. (c6_2 zenon_X43 (a295)))
% 2.15/2.31  ((a379) != (a439))
% 2.15/2.31  ((a418) != (a338))
% 2.15/2.31  ((a286) != zenon_X184)
% 2.15/2.31  (-. (c7_2 zenon_X16 (a286)))
% 2.15/2.31  ((a418) != zenon_X98)
% 2.15/2.31  ((a439) != zenon_X75)
% 2.15/2.31  (c3_1 (a395))
% 2.15/2.31  (-. (c6_1 zenon_X19))
% 2.15/2.31  (zenon_X18 != (a280))
% 2.15/2.31  (zenon_X16 != (a280))
% 2.15/2.31  ((a435) != zenon_X0)
% 2.15/2.31  (c4_2 (a405) (a389))
% 2.15/2.31  ((a379) != (a347))
% 2.15/2.31  ((a405) != (a416))
% 2.15/2.31  (c6_2 (a431) (a295))
% 2.15/2.31  (-. (c3_2 (a444) zenon_X80))
% 2.15/2.31  ((a291) != (a395))
% 2.15/2.31  ((a347) != zenon_X62)
% 2.15/2.31  ((a370) != zenon_X112)
% 2.15/2.31  (zenon_X38 != zenon_X10)
% 2.15/2.31  (-. (c5_2 (a332) zenon_X82))
% 2.15/2.31  (c5_2 (a405) (a279))
% 2.15/2.31  ((a290) != zenon_X26)
% 2.15/2.31  (-. (c10_2 (a332) zenon_X24))
% 2.15/2.31  ((a287) != zenon_X23)
% 2.15/2.31  ((a424) != (a434))
% 2.15/2.31  (c6_2 (a444) (a379))
% 2.15/2.31  (c6_2 (a444) (a409))
% 2.15/2.31  ((a303) != (a289))
% 2.15/2.31  (-. (c4_1 zenon_X13))
% 2.15/2.31  (c5_2 (a405) (a389))
% 2.15/2.31  (zenon_X25 != (a416))
% 2.15/2.31  (zenon_X39 != (a352))
% 2.15/2.31  ((a292) != zenon_X20)
% 2.15/2.31  (zenon_X35 != (a332))
% 2.15/2.31  (c10_2 (a317) (a344))
% 2.15/2.31  ((a396) != (a370))
% 2.15/2.31  ((a417) != (a379))
% 2.15/2.31  (zenon_X43 != zenon_X25)
% 2.15/2.31  ((a327) != (a319))
% 2.15/2.31  ((a448) != zenon_X32)
% 2.15/2.31  (-. (c6_2 zenon_X6 (a396)))
% 2.15/2.31  ((a299) != (a289))
% 2.15/2.31  ((a395) != (a319))
% 2.15/2.31  ((a431) != (a327))
% 2.15/2.31  ((a279) != zenon_X4)
% 2.15/2.31  (-. (c1_1 (a327)))
% 2.15/2.31  ((a363) != (a425))
% 2.15/2.31  (ndr1_1 (a443))
% 2.15/2.31  ((a417) != zenon_X166)
% 2.15/2.31  (zenon_X39 != zenon_X7)
% 2.15/2.31  (-. (c7_2 (a369) (a286)))
% 2.15/2.31  ((a417) != (a439))
% 2.15/2.31  ((a379) != zenon_X187)
% 2.15/2.31  ((a440) != zenon_X108)
% 2.15/2.31  ((a418) != zenon_X138)
% 2.15/2.31  (c9_2 (a434) (a435))
% 2.15/2.31  ((a379) != zenon_X62)
% 2.15/2.31  ((a302) != zenon_X25)
% 2.15/2.31  ((a289) != zenon_X138)
% 2.15/2.31  ((a347) != zenon_X136)
% 2.15/2.31  ((a418) != zenon_X87)
% 2.15/2.31  ((a431) != (a424))
% 2.15/2.31  ((a443) != (a319))
% 2.15/2.31  ((a327) != (a278))
% 2.15/2.31  (c4_2 zenon_X45 (a389))
% 2.15/2.31  (zenon_X35 != zenon_X8)
% 2.15/2.31  ((a417) != (a344))
% 2.15/2.31  (zenon_X18 != zenon_X7)
% 2.15/2.31  ((a431) != zenon_X13)
% 2.15/2.31  (zenon_X35 != zenon_X21)
% 2.15/2.31  (-. (c7_2 (a444) (a417)))
% 2.15/2.31  ((a294) != zenon_X8)
% 2.15/2.31  ((a429) != zenon_X70)
% 2.15/2.31  (zenon_X8 != (a424))
% 2.15/2.31  (zenon_X35 != zenon_X13)
% 2.15/2.31  ((a332) != (a369))
% 2.15/2.31  ((a279) != zenon_X110)
% 2.15/2.31  (zenon_X8 != zenon_X45)
% 2.15/2.31  (c7_2 (a294) (a347))
% 2.15/2.31  ((a302) != zenon_X22)
% 2.15/2.31  ((a289) != zenon_X98)
% 2.15/2.31  (-. (c7_2 (a271) (a338)))
% 2.15/2.31  ((a443) != zenon_X16)
% 2.15/2.31  ((a327) != (a416))
% 2.15/2.31  ((a431) != (a280))
% 2.15/2.31  ((a439) != zenon_X172)
% 2.15/2.31  ((a286) != (a390))
% 2.15/2.31  ((a347) != zenon_X179)
% 2.15/2.31  ((a379) != zenon_X181)
% 2.15/2.31  ((a429) != zenon_X69)
% 2.15/2.31  (c7_1 zenon_X32)
% 2.15/2.31  ((a293) != zenon_X36)
% 2.15/2.31  ((a279) != zenon_X57)
% 2.15/2.31  (zenon_X39 != (a302))
% 2.15/2.31  (c5_2 (a271) (a363))
% 2.15/2.31  ((a302) != zenon_X7)
% 2.15/2.31  (-. (c9_1 (a405)))
% 2.15/2.31  (-. (c10_1 (a424)))
% 2.15/2.31  ((a425) != zenon_X173)
% 2.15/2.31  (-. (c6_1 zenon_X7))
% 2.15/2.31  ((a295) != zenon_X73)
% 2.15/2.31  (c3_1 (a278))
% 2.15/2.31  (zenon_X27 != (a278))
% 2.15/2.31  (zenon_X39 != zenon_X23)
% 2.15/2.31  ((a279) != zenon_X100)
% 2.15/2.31  ((a418) != (a293))
% 2.15/2.31  (c6_2 (a291) (a290))
% 2.15/2.31  (c10_1 (a448))
% 2.15/2.31  (zenon_X27 != (a280))
% 2.15/2.31  (c6_2 (a287) (a347))
% 2.15/2.31  ((a299) != (a288))
% 2.15/2.31  ((a286) != zenon_X71)
% 2.15/2.31  (-. (c1_2 (a319) (a347)))
% 2.15/2.31  (c7_2 (a319) (a347))
% 2.15/2.31  (c8_2 (a287) (a289))
% 2.15/2.31  ((a317) != zenon_X16)
% 2.15/2.31  (c6_2 (a424) (a347))
% 2.15/2.31  ((a418) != zenon_X105)
% 2.15/2.31  ((a280) != zenon_X15)
% 2.15/2.31  ((a344) != zenon_X1)
% 2.15/2.31  ((a279) != zenon_X47)
% 2.15/2.31  ((a319) != (a280))
% 2.15/2.31  ((a299) != zenon_X117)
% 2.15/2.31  (zenon_X19 != zenon_X43)
% 2.15/2.31  (c8_2 (a291) (a279))
% 2.15/2.31  (zenon_X43 != zenon_X22)
% 2.15/2.31  ((a379) != zenon_X10)
% 2.15/2.31  (-. (c5_2 (a291) (a293)))
% 2.15/2.31  ((a287) != (a327))
% 2.15/2.31  ((a279) != zenon_X36)
% 2.15/2.31  (c6_2 (a287) (a425))
% 2.15/2.31  (zenon_X7 != (a434))
% 2.15/2.31  ((a317) != zenon_X13)
% 2.15/2.31  ((a409) != zenon_X40)
% 2.15/2.31  (c7_1 (a294))
% 2.15/2.31  ((a291) != (a443))
% 2.15/2.31  ((a425) != (a390))
% 2.15/2.31  (c4_2 (a280) zenon_X0)
% 2.15/2.31  (zenon_X6 != zenon_X22)
% 2.15/2.31  (c6_2 (a302) (a303))
% 2.15/2.31  (zenon_X45 != (a271))
% 2.15/2.31  (zenon_X31 != zenon_X22)
% 2.15/2.31  ((a396) != (a347))
% 2.15/2.31  ((a379) != (a286))
% 2.15/2.31  (-. (c8_2 zenon_X31 (a429)))
% 2.15/2.31  ((a299) != zenon_X97)
% 2.15/2.31  (zenon_X19 != (a287))
% 2.15/2.31  (-. (c8_2 (a352) (a286)))
% 2.15/2.31  (zenon_X31 != (a405))
% 2.15/2.31  ((a443) != (a434))
% 2.15/2.31  ((a299) != zenon_X84)
% 2.15/2.31  ((a363) != zenon_X167)
% 2.15/2.31  ((a410) != zenon_X11)
% 2.15/2.31  (c6_2 (a416) (a292))
% 2.15/2.31  (-. (c6_2 zenon_X43 (a396)))
% 2.15/2.31  (-. (c1_1 (a319)))
% 2.15/2.31  (zenon_X19 != (a294))
% 2.15/2.31  (zenon_X18 != (a278))
% 2.15/2.31  (c6_2 (a307) (a292))
% 2.15/2.31  ((a289) != zenon_X56)
% 2.15/2.31  (c6_2 (a431) (a429))
% 2.15/2.31  ((a425) != zenon_X71)
% 2.15/2.31  (-. (c10_2 (a317) (a338)))
% 2.15/2.31  (c2_2 (a343) (a344))
% 2.15/2.31  ((a271) != (a434))
% 2.15/2.31  (-. (c9_1 (a332)))
% 2.15/2.31  (-. (c5_2 zenon_X8 (a289)))
% 2.15/2.31  (-. (c7_2 zenon_X27 zenon_X144))
% 2.15/2.31  ((a370) != zenon_X62)
% 2.15/2.31  (c7_2 (a302) (a347))
% 2.15/2.31  (c6_2 zenon_X28 (a417))
% 2.15/2.31  (zenon_X16 != zenon_X7)
% 2.15/2.31  (c6_2 (a278) (a417))
% 2.15/2.31  (-. (c10_2 (a405) (a292)))
% 2.15/2.31  ((a439) != (a338))
% 2.15/2.31  ((a299) != (a429))
% 2.15/2.31  (c10_2 (a343) (a344))
% 2.15/2.31  (-. (c8_2 (a271) (a338)))
% 2.15/2.31  ((a408) != (a332))
% 2.15/2.31  (zenon_X18 != (a327))
% 2.15/2.31  (zenon_X35 != (a317))
% 2.15/2.31  (-. (c5_2 (a327) (a439)))
% 2.15/2.31  ((a287) != (a278))
% 2.15/2.31  (-. (c1_2 (a434) (a435)))
% 2.15/2.31  ((a271) != zenon_X32)
% 2.15/2.31  (zenon_X39 != (a319))
% 2.15/2.31  (-. (c7_2 (a416) (a379)))
% 2.15/2.31  (zenon_X39 != (a287))
% 2.15/2.31  ((a317) != zenon_X23)
% 2.15/2.31  ((a448) != zenon_X16)
% 2.15/2.31  (-. (c9_1 zenon_X25))
% 2.15/2.31  (c5_2 (a319) (a299))
% 2.15/2.31  ((a344) != zenon_X163)
% 2.15/2.31  (-. (c6_1 (a280)))
% 2.15/2.31  (c6_2 zenon_X32 (a279))
% 2.15/2.31  ((a294) != (a434))
% 2.15/2.31  ((a379) != zenon_X75)
% 2.15/2.31  ((a439) != zenon_X70)
% 2.15/2.31  ((a279) != zenon_X194)
% 2.15/2.31  ((a279) != zenon_X135)
% 2.15/2.31  (-. (c10_2 (a405) (a409)))
% 2.15/2.31  ((a302) != (a327))
% 2.15/2.31  (-. (c8_2 zenon_X6 zenon_X119))
% 2.15/2.31  (-. (c7_2 (a408) zenon_X38))
% 2.15/2.31  ((a396) != zenon_X177)
% 2.15/2.31  (zenon_X39 != (a416))
% 2.15/2.31  (-. (c5_2 (a307) (a292)))
% 2.15/2.31  (-. (c4_2 zenon_X35 (a347)))
% 2.15/2.31  ((a290) != (a440))
% 2.15/2.31  (c6_2 zenon_X8 (a429))
% 2.15/2.31  ((a290) != zenon_X33)
% 2.15/2.31  ((a279) != zenon_X26)
% 2.15/2.31  ((a319) != zenon_X13)
% 2.15/2.31  ((a347) != zenon_X172)
% 2.15/2.31  (c10_1 (a287))
% 2.15/2.31  *)
% 2.15/2.31  (* NO-PROOF *)
% 2.15/2.31  % SZS status GaveUp
% 2.15/2.31  Number of rewrites on terms: 0
% 2.15/2.31  Number of rewrites on props: 0
% 2.15/2.31  nodes searched: 78417
% 2.15/2.31  max branch formulas: 5479
% 2.15/2.31  proof nodes created: 2350
% 2.15/2.31  formulas created: 88551
% 2.15/2.31  
%------------------------------------------------------------------------------