ZenonModulo---0.5.0.UNK-Non.f

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

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

% Result   : Unknown 2.08s 2.29s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SYN544+1 : TPTP v8.2.0. Released v2.1.0.
% 0.00/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.33  % Computer : n012.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Sun Jun 23 23:55:53 EDT 2024
% 0.12/0.33  % CPUTime  : 
% 2.08/2.28  Zenon error: exhausted search space without finding a proof
% 2.08/2.28  (* Current branch:
% 2.08/2.28  (zenon_X36 != (a93))
% 2.08/2.28  ((a82) != zenon_X112)
% 2.08/2.28  ((a68) != (a47))
% 2.08/2.28  ((a57) != zenon_X173)
% 2.08/2.28  ((a30) != (a95))
% 2.08/2.28  (c6_2 zenon_X20 (a82))
% 2.08/2.28  (zenon_X11 != (a68))
% 2.08/2.28  (-. (c7_1 zenon_X18))
% 2.08/2.28  ((a137) != zenon_X34)
% 2.08/2.28  ((a57) != zenon_X196)
% 2.08/2.28  (-. (c5_2 (a122) zenon_X82))
% 2.08/2.28  ((a58) != (a115))
% 2.08/2.28  ((a63) != (a115))
% 2.08/2.28  ((a95) != (a97))
% 2.08/2.28  (zenon_X20 != zenon_X11)
% 2.08/2.28  ((a82) != (a48))
% 2.08/2.28  ((a57) != zenon_X117)
% 2.08/2.28  (zenon_X29 != zenon_X82)
% 2.08/2.28  (zenon_X21 != (a41))
% 2.08/2.28  ((a82) != zenon_X91)
% 2.08/2.28  ((a30) != zenon_X77)
% 2.08/2.28  (c8_1 (a127))
% 2.08/2.28  (c8_2 (a122) (a114))
% 2.08/2.28  (-. (c6_2 (a39) (a108)))
% 2.08/2.28  (c8_2 (a93) zenon_X101)
% 2.08/2.28  ((a137) != (a57))
% 2.08/2.28  (-. (ndr1_1 zenon_X28))
% 2.08/2.28  (c1_2 (a47) (a137))
% 2.08/2.28  (c7_1 (a117))
% 2.08/2.28  ((a95) != zenon_X145)
% 2.08/2.28  (-. (c8_2 (a59) zenon_X78))
% 2.08/2.28  (zenon_X22 != (a95))
% 2.08/2.28  (-. (c5_2 zenon_X38 (a130)))
% 2.08/2.28  (-. (c3_2 zenon_X36 zenon_X165))
% 2.08/2.28  (c5_2 (a59) zenon_X39)
% 2.08/2.28  (-. (c6_2 zenon_X9 (a130)))
% 2.08/2.28  ((a114) != (a30))
% 2.08/2.28  (c8_2 zenon_X27 (a123))
% 2.08/2.28  ((a114) != (a41))
% 2.08/2.28  (-. (c7_2 (a93) zenon_X101))
% 2.08/2.28  ((a95) != zenon_X188)
% 2.08/2.28  (c6_2 (a129) (a40))
% 2.08/2.28  ((a40) != zenon_X94)
% 2.08/2.28  ((a108) != zenon_X29)
% 2.08/2.28  ((a59) != (a122))
% 2.08/2.28  ((a96) != (a39))
% 2.08/2.28  ((a58) != zenon_X95)
% 2.08/2.28  (c1_2 zenon_X23 (a63))
% 2.08/2.28  (c1_2 (a129) (a30))
% 2.08/2.28  (c6_1 zenon_X27)
% 2.08/2.28  (c6_2 zenon_X20 (a58))
% 2.08/2.28  (-. (c3_2 zenon_X27 zenon_X170))
% 2.08/2.28  (c5_2 (a59) (a114))
% 2.08/2.28  (-. (c3_2 (a68) zenon_X84))
% 2.08/2.28  (-. (c5_2 zenon_X6 (a30)))
% 2.08/2.28  ((a82) != zenon_X13)
% 2.08/2.28  (c1_2 zenon_X36 (a95))
% 2.08/2.28  (c6_2 (a68) (a58))
% 2.08/2.28  (c6_2 zenon_X23 (a95))
% 2.08/2.28  (-. (c2_2 zenon_X20 zenon_X173))
% 2.08/2.28  ((a130) != zenon_X189)
% 2.08/2.28  ((a137) != zenon_X165)
% 2.08/2.28  (zenon_X35 != zenon_X101)
% 2.08/2.28  (-. (c5_2 (a122) zenon_X22))
% 2.08/2.28  (c6_2 zenon_X23 (a40))
% 2.08/2.28  ((a96) != (a93))
% 2.08/2.28  (-. (c5_2 (a39) zenon_X22))
% 2.08/2.28  (-. (c4_1 (a129)))
% 2.08/2.28  (c5_2 zenon_X23 (a114))
% 2.08/2.28  (ndr1_1 (a81))
% 2.08/2.28  ((a31) != zenon_X39)
% 2.08/2.28  ((a57) != zenon_X193)
% 2.08/2.28  ((a68) != zenon_X24)
% 2.08/2.28  (zenon_X7 != zenon_X11)
% 2.08/2.28  (c1_2 (a121) (a95))
% 2.08/2.28  (zenon_X14 != zenon_X32)
% 2.08/2.28  (c1_2 (a121) (a40))
% 2.08/2.28  ((a58) != zenon_X87)
% 2.08/2.28  (zenon_X21 != zenon_X12)
% 2.08/2.28  ((a59) != zenon_X15)
% 2.08/2.28  ((a95) != (a57))
% 2.08/2.28  ((a130) != zenon_X152)
% 2.08/2.28  (c4_2 zenon_X36 (a63))
% 2.08/2.28  ((a130) != zenon_X26)
% 2.08/2.28  (c1_2 (a51) (a31))
% 2.08/2.28  (c7_2 (a39) zenon_X35)
% 2.08/2.28  ((a40) != (a123))
% 2.08/2.28  (-. (c3_2 (a59) zenon_X97))
% 2.08/2.28  (-. (c2_2 zenon_X38 zenon_X216))
% 2.08/2.28  (c5_2 (a59) zenon_X104)
% 2.08/2.28  ((a131) != zenon_X14)
% 2.08/2.28  (c6_2 (a122) (a82))
% 2.08/2.28  (c1_2 (a18) zenon_X104)
% 2.08/2.28  ((a108) != zenon_X104)
% 2.08/2.28  (-. (c8_1 zenon_X17))
% 2.08/2.28  (-. (c8_2 (a65) zenon_X29))
% 2.08/2.28  (-. (c5_2 (a81) zenon_X160))
% 2.08/2.28  (zenon_X21 != (a97))
% 2.08/2.28  (-. (c5_2 (a122) (a57)))
% 2.08/2.28  (zenon_X153 != (a115))
% 2.08/2.28  (c1_2 (a51) (a95))
% 2.08/2.28  ((a29) != zenon_X27)
% 2.08/2.28  ((a81) != zenon_X36)
% 2.08/2.28  ((a114) != (a137))
% 2.08/2.28  (-. (c1_1 zenon_X24))
% 2.08/2.28  ((a30) != zenon_X155)
% 2.08/2.28  ((a57) != (a33))
% 2.08/2.28  (ndr1_1 (a121))
% 2.08/2.28  ((a31) != (a40))
% 2.08/2.28  (-. (c8_2 (a122) (a123)))
% 2.08/2.28  ((a95) != zenon_X189)
% 2.08/2.28  (zenon_X29 != (a97))
% 2.08/2.28  ((a82) != zenon_X63)
% 2.08/2.28  (-. (c5_2 (a117) (a97)))
% 2.08/2.28  (c4_2 zenon_X20 (a63))
% 2.08/2.28  (zenon_X78 != (a97))
% 2.08/2.28  (c8_2 (a129) zenon_X14)
% 2.08/2.28  ((a95) != zenon_X2)
% 2.08/2.28  ((a57) != zenon_X147)
% 2.08/2.28  (c8_2 (a18) (a97))
% 2.08/2.28  (-. (c3_2 zenon_X7 zenon_X125))
% 2.08/2.28  (-. (c4_1 (a47)))
% 2.08/2.28  (zenon_X20 != (a129))
% 2.08/2.28  (c1_2 (a122) (a115))
% 2.08/2.28  ((a40) != zenon_X37)
% 2.08/2.28  ((a39) != zenon_X15)
% 2.08/2.28  (-. (c6_2 (a18) (a40)))
% 2.08/2.28  (c1_2 (a47) (a57))
% 2.08/2.28  ((a68) != zenon_X10)
% 2.08/2.28  (-. (c4_2 (a122) zenon_X45))
% 2.08/2.28  ((a40) != (a49))
% 2.08/2.28  (-. (c3_1 (a104)))
% 2.08/2.28  ((a63) != zenon_X49)
% 2.08/2.28  ((a18) != zenon_X18)
% 2.08/2.28  (-. (c2_1 (a136)))
% 2.08/2.28  (-. (c8_2 zenon_X15 (a63)))
% 2.08/2.28  (-. (c8_2 zenon_X15 (a40)))
% 2.08/2.28  (c1_1 zenon_X27)
% 2.08/2.28  (-. (c6_2 (a93) (a130)))
% 2.08/2.28  ((a39) != (a104))
% 2.08/2.28  (c5_2 (a59) zenon_X78)
% 2.08/2.28  (c1_1 zenon_X40)
% 2.08/2.28  ((a31) != (a95))
% 2.08/2.28  ((a30) != (a57))
% 2.08/2.28  (-. (c2_2 (a136) (a63)))
% 2.08/2.28  (-. (c5_2 (a65) (a115)))
% 2.08/2.28  ((a33) != (a123))
% 2.08/2.28  (zenon_X74 != (a130))
% 2.08/2.28  (-. (c2_1 (a122)))
% 2.08/2.28  (ndr1_1 (a29))
% 2.08/2.28  (zenon_X11 != (a129))
% 2.08/2.28  (c1_2 (a18) (a63))
% 2.08/2.28  (c3_2 (a136) (a30))
% 2.08/2.28  ((a29) != (a104))
% 2.08/2.28  (c6_2 (a93) (a63))
% 2.08/2.28  (zenon_X86 != zenon_X82)
% 2.08/2.28  (zenon_X6 != zenon_X40)
% 2.08/2.28  (c1_2 (a39) (a82))
% 2.08/2.28  ((a68) != zenon_X30)
% 2.08/2.28  (zenon_X32 != (a130))
% 2.08/2.28  (zenon_X27 != (a129))
% 2.08/2.28  ((a68) != zenon_X17)
% 2.08/2.28  ((a68) != (a34))
% 2.08/2.28  (c8_2 (a93) (a95))
% 2.08/2.28  ((a57) != zenon_X150)
% 2.08/2.28  ((a63) != (a130))
% 2.08/2.28  (c8_2 (a47) zenon_X14)
% 2.08/2.28  ((a40) != zenon_X86)
% 2.08/2.28  (-. (c8_2 (a39) zenon_X73))
% 2.08/2.28  (-. (c8_2 (a65) zenon_X78))
% 2.08/2.28  ((a57) != (a123))
% 2.08/2.28  (zenon_X42 != zenon_X73)
% 2.08/2.28  (c1_2 (a47) (a58))
% 2.08/2.28  ((a31) != zenon_X88)
% 2.08/2.28  ((a57) != zenon_X66)
% 2.08/2.28  ((a41) != (a82))
% 2.08/2.28  (c8_2 (a29) (a97))
% 2.08/2.28  (-. (c6_2 (a47) zenon_X189))
% 2.08/2.28  (-. (c4_2 (a93) zenon_X13))
% 2.08/2.28  ((a65) != (a47))
% 2.08/2.28  ((a95) != zenon_X103)
% 2.08/2.28  ((a49) != zenon_X72)
% 2.08/2.28  (zenon_X35 != zenon_X42)
% 2.08/2.28  ((a65) != zenon_X30)
% 2.08/2.28  (c3_1 zenon_X6)
% 2.08/2.28  ((a39) != (a34))
% 2.08/2.28  (-. (c3_1 (a34)))
% 2.08/2.28  (c6_2 (a127) (a30))
% 2.08/2.28  (-. (c5_2 (a121) (a58)))
% 2.08/2.28  ((a122) != (a47))
% 2.08/2.28  (c7_2 (a39) (a41))
% 2.08/2.28  ((a114) != zenon_X73)
% 2.08/2.28  ((a18) != zenon_X30)
% 2.08/2.28  (-. (c8_2 zenon_X15 (a131)))
% 2.08/2.28  ((a136) != (a34))
% 2.08/2.28  ((a58) != zenon_X103)
% 2.08/2.28  (-. (c3_1 zenon_X24))
% 2.08/2.28  (-. (c5_2 zenon_X6 (a49)))
% 2.08/2.28  ((a122) != (a104))
% 2.08/2.28  ((a123) != (a31))
% 2.08/2.28  (-. (c7_2 zenon_X6 (a108)))
% 2.08/2.28  (-. (c2_2 zenon_X23 zenon_X144))
% 2.08/2.28  (-. (c8_2 (a39) zenon_X72))
% 2.08/2.28  ((a115) != zenon_X136)
% 2.08/2.28  (c6_1 (a93))
% 2.08/2.28  (zenon_X40 != zenon_X15)
% 2.08/2.28  (c1_2 zenon_X23 (a137))
% 2.08/2.28  ((a57) != zenon_X32)
% 2.08/2.28  (c6_2 (a18) (a57))
% 2.08/2.28  (zenon_X23 != zenon_X9)
% 2.08/2.28  ((a58) != zenon_X104)
% 2.08/2.28  ((a82) != zenon_X50)
% 2.08/2.28  (c4_1 (a121))
% 2.08/2.28  (zenon_X22 != (a63))
% 2.08/2.28  (-. (c8_2 (a68) (a115)))
% 2.08/2.28  (-. (c4_1 zenon_X36))
% 2.08/2.28  ((a18) != (a93))
% 2.08/2.28  (c1_2 (a39) zenon_X74)
% 2.08/2.28  (-. (c2_2 (a29) zenon_X61))
% 2.08/2.28  (-. (c6_2 zenon_X11 (a137)))
% 2.08/2.28  ((a57) != zenon_X114)
% 2.08/2.28  (c8_2 (a18) zenon_X79)
% 2.08/2.28  (c7_1 (a136))
% 2.08/2.28  (c5_2 (a47) (a130))
% 2.08/2.28  (c8_2 (a93) (a130))
% 2.08/2.28  (c1_2 zenon_X27 (a137))
% 2.08/2.28  (-. (c7_2 (a96) (a115)))
% 2.08/2.28  (zenon_X23 != zenon_X10)
% 2.08/2.28  (-. (c7_2 (a127) (a115)))
% 2.08/2.28  ((a18) != (a47))
% 2.08/2.28  (zenon_X3 != zenon_X24)
% 2.08/2.28  (c5_2 (a65) zenon_X22)
% 2.08/2.28  (zenon_X29 != (a49))
% 2.08/2.28  ((a81) != (a34))
% 2.08/2.28  (c1_2 (a18) (a123))
% 2.08/2.28  ((a41) != (a49))
% 2.08/2.28  ((a18) != zenon_X11)
% 2.08/2.28  (c4_2 zenon_X23 (a63))
% 2.08/2.28  ((a129) != (a34))
% 2.08/2.28  (c7_1 (a39))
% 2.08/2.28  (c4_2 (a117) (a63))
% 2.08/2.28  ((a59) != (a39))
% 2.08/2.28  ((a40) != zenon_X117)
% 2.08/2.28  ((a30) != zenon_X65)
% 2.08/2.28  (zenon_X53 != zenon_X14)
% 2.08/2.28  ((a97) != zenon_X32)
% 2.08/2.28  (-. (c5_2 (a122) (a49)))
% 2.08/2.28  ((a93) != (a34))
% 2.08/2.28  ((a117) != zenon_X40)
% 2.08/2.28  (-. (c2_1 (a39)))
% 2.08/2.28  (-. (c7_2 (a122) (a115)))
% 2.08/2.28  (-. (ndr1_1 zenon_X30))
% 2.08/2.28  ((a41) != zenon_X189)
% 2.08/2.28  ((a108) != zenon_X79)
% 2.08/2.28  (-. (c8_2 (a59) zenon_X82))
% 2.08/2.28  ((a115) != zenon_X147)
% 2.08/2.28  ((a96) != (a122))
% 2.08/2.28  (c1_0)
% 2.08/2.28  (ndr1_1 (a122))
% 2.08/2.28  ((a122) != zenon_X40)
% 2.08/2.28  (-. (c8_2 (a65) zenon_X22))
% 2.08/2.28  ((a104) != (a129))
% 2.08/2.28  ((a108) != zenon_X88)
% 2.08/2.28  ((a130) != zenon_X196)
% 2.08/2.28  ((a49) != (a115))
% 2.08/2.28  (zenon_X78 != zenon_X82)
% 2.08/2.28  (zenon_X11 != (a96))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a130)))
% 2.08/2.28  ((a108) != zenon_X197)
% 2.08/2.28  ((a65) != (a121))
% 2.08/2.28  (-. (c6_2 (a29) (a130)))
% 2.08/2.28  ((a49) != zenon_X136)
% 2.08/2.28  (-. (c3_2 zenon_X23 zenon_X117))
% 2.08/2.28  ((a127) != zenon_X28)
% 2.08/2.28  ((a59) != zenon_X36)
% 2.08/2.28  ((a30) != zenon_X188)
% 2.08/2.28  (c7_2 (a39) (a82))
% 2.08/2.28  (zenon_X78 != zenon_X79)
% 2.08/2.28  (c8_2 (a136) (a49))
% 2.08/2.28  (-. (c3_2 zenon_X27 (a58)))
% 2.08/2.28  ((a114) != zenon_X91)
% 2.08/2.28  (c5_1 (a68))
% 2.08/2.28  (c6_2 (a121) (a130))
% 2.08/2.28  (-. (c4_2 (a96) zenon_X46))
% 2.08/2.28  (-. (c5_2 zenon_X38 zenon_X8))
% 2.08/2.28  (zenon_X36 != (a34))
% 2.08/2.28  (c8_2 (a93) (a137))
% 2.08/2.28  ((a82) != zenon_X134)
% 2.08/2.28  (c5_2 (a29) (a40))
% 2.08/2.28  ((a82) != zenon_X14)
% 2.08/2.28  ((a137) != zenon_X197)
% 2.08/2.28  ((a57) != zenon_X96)
% 2.08/2.28  (-. (c6_2 (a18) (a58)))
% 2.08/2.28  ((a130) != zenon_X103)
% 2.08/2.28  (c5_2 (a65) (a95))
% 2.08/2.28  (-. (c5_2 (a93) zenon_X103))
% 2.08/2.28  (-. (c2_1 (a34)))
% 2.08/2.28  ((a82) != zenon_X133)
% 2.08/2.28  ((a59) != zenon_X38)
% 2.08/2.28  ((a57) != zenon_X69)
% 2.08/2.28  ((a82) != zenon_X55)
% 2.08/2.28  (zenon_X151 != (a31))
% 2.08/2.28  (-. (c6_2 zenon_X9 (a57)))
% 2.08/2.28  (c1_2 (a51) (a137))
% 2.08/2.28  (c6_2 (a122) (a40))
% 2.08/2.28  ((a123) != (a49))
% 2.08/2.28  (c5_2 (a39) (a40))
% 2.08/2.28  (-. (c5_2 (a39) (a49)))
% 2.08/2.28  (c3_2 zenon_X36 (a57))
% 2.08/2.28  ((a30) != zenon_X193)
% 2.08/2.28  (zenon_X133 != (a97))
% 2.08/2.28  ((a63) != zenon_X147)
% 2.08/2.28  ((a123) != zenon_X153)
% 2.08/2.28  (-. (c3_1 (a93)))
% 2.08/2.28  ((a33) != (a49))
% 2.08/2.28  (zenon_X20 != (a47))
% 2.08/2.28  ((a95) != zenon_X121)
% 2.08/2.28  ((a63) != zenon_X45)
% 2.08/2.28  (c6_2 (a68) (a57))
% 2.08/2.28  (-. (c8_2 zenon_X15 (a95)))
% 2.08/2.28  (zenon_X20 != (a122))
% 2.08/2.28  ((a82) != zenon_X8)
% 2.08/2.28  (c8_2 zenon_X23 (a115))
% 2.08/2.28  ((a82) != zenon_X68)
% 2.08/2.28  ((a130) != zenon_X158)
% 2.08/2.28  ((a114) != (a57))
% 2.08/2.28  ((a40) != zenon_X87)
% 2.08/2.28  (zenon_X40 != (a104))
% 2.08/2.28  ((a33) != (a41))
% 2.08/2.28  ((a127) != zenon_X36)
% 2.08/2.28  (zenon_X26 != (a137))
% 2.08/2.28  (c1_2 zenon_X23 (a40))
% 2.08/2.28  (c6_2 (a136) (a33))
% 2.08/2.28  (zenon_X21 != (a108))
% 2.08/2.28  ((a30) != (a49))
% 2.08/2.28  ((a137) != (a48))
% 2.08/2.28  (c1_2 (a65) (a31))
% 2.08/2.28  (zenon_X72 != zenon_X35)
% 2.08/2.28  (zenon_X42 != (a130))
% 2.08/2.28  (-. (c6_2 (a96) (a97)))
% 2.08/2.28  (zenon_X23 != zenon_X30)
% 2.08/2.28  (-. (c5_2 (a96) (a58)))
% 2.08/2.28  (-. (c5_2 (a129) (a114)))
% 2.08/2.28  ((a117) != zenon_X9)
% 2.08/2.28  ((a114) != zenon_X26)
% 2.08/2.28  (c4_2 (a127) (a63))
% 2.08/2.28  ((a68) != zenon_X40)
% 2.08/2.28  (zenon_X14 != zenon_X8)
% 2.08/2.28  (-. (c6_1 (a81)))
% 2.08/2.28  (c5_2 (a65) (a31))
% 2.08/2.28  (c8_2 (a29) (a114))
% 2.08/2.28  ((a130) != zenon_X96)
% 2.08/2.28  ((a127) != zenon_X9)
% 2.08/2.28  ((a49) != zenon_X73)
% 2.08/2.28  ((a33) != zenon_X79)
% 2.08/2.28  ((a122) != (a51))
% 2.08/2.28  (zenon_X14 != zenon_X83)
% 2.08/2.28  (c7_2 (a39) (a49))
% 2.08/2.28  (-. (c6_2 (a104) (a108)))
% 2.08/2.28  ((a108) != zenon_X195)
% 2.08/2.28  ((a30) != zenon_X207)
% 2.08/2.28  ((a63) != zenon_X16)
% 2.08/2.28  (c1_2 (a65) (a123))
% 2.08/2.28  ((a82) != zenon_X37)
% 2.08/2.28  ((a130) != zenon_X87)
% 2.08/2.28  ((a57) != zenon_X89)
% 2.08/2.28  (zenon_X36 != zenon_X11)
% 2.08/2.28  ((a122) != zenon_X15)
% 2.08/2.28  ((a82) != zenon_X65)
% 2.08/2.28  (-. (c5_2 zenon_X38 (a114)))
% 2.08/2.28  (c4_1 (a122))
% 2.08/2.28  ((a123) != zenon_X74)
% 2.08/2.28  ((a40) != (a58))
% 2.08/2.28  (c8_2 (a39) (a97))
% 2.08/2.28  (-. (c6_2 (a39) (a137)))
% 2.08/2.28  (c1_2 (a96) (a82))
% 2.08/2.28  ((a18) != zenon_X15)
% 2.08/2.28  ((a48) != zenon_X32)
% 2.08/2.28  ((a57) != zenon_X78)
% 2.08/2.28  (zenon_X104 != (a30))
% 2.08/2.28  ((a57) != zenon_X108)
% 2.08/2.28  (c5_2 zenon_X7 (a95))
% 2.08/2.28  (c6_2 zenon_X20 (a130))
% 2.08/2.28  ((a95) != zenon_X191)
% 2.08/2.28  ((a33) != zenon_X197)
% 2.08/2.28  (c4_2 (a65) (a30))
% 2.08/2.28  ((a31) != (a30))
% 2.08/2.28  (-. (c5_2 (a127) (a58)))
% 2.08/2.28  ((a95) != zenon_X136)
% 2.08/2.28  ((a39) != zenon_X38)
% 2.08/2.28  (-. (c6_2 (a47) (a40)))
% 2.08/2.28  (c1_2 (a121) (a82))
% 2.08/2.28  ((a82) != zenon_X111)
% 2.08/2.28  ((a30) != zenon_X120)
% 2.08/2.28  (c5_2 (a59) zenon_X26)
% 2.08/2.28  (-. (c6_2 zenon_X9 (a30)))
% 2.08/2.28  (zenon_X10 != zenon_X9)
% 2.08/2.28  ((a95) != zenon_X39)
% 2.08/2.28  (c1_2 (a122) (a63))
% 2.08/2.28  (c5_2 (a65) (a114))
% 2.08/2.28  ((a97) != zenon_X136)
% 2.08/2.28  (c6_2 (a127) (a95))
% 2.08/2.28  (zenon_X42 != zenon_X8)
% 2.08/2.28  (zenon_X42 != zenon_X14)
% 2.08/2.28  ((a57) != zenon_X97)
% 2.08/2.28  (c5_2 (a29) (a137))
% 2.08/2.28  ((a40) != zenon_X124)
% 2.08/2.28  ((a130) != zenon_X82)
% 2.08/2.28  (-. (c5_2 zenon_X38 zenon_X26))
% 2.08/2.28  (c1_2 zenon_X23 (a95))
% 2.08/2.28  ((a31) != (a58))
% 2.08/2.28  ((a82) != (a40))
% 2.08/2.28  ((a59) != (a104))
% 2.08/2.28  (-. (c6_2 (a29) zenon_X21))
% 2.08/2.28  ((a130) != zenon_X29)
% 2.08/2.28  (zenon_X73 != zenon_X35)
% 2.08/2.28  ((a97) != (a57))
% 2.08/2.28  (c7_2 (a136) (a108))
% 2.08/2.28  ((a33) != zenon_X155)
% 2.08/2.28  ((a41) != zenon_X91)
% 2.08/2.28  (c5_2 (a18) (a114))
% 2.08/2.28  (zenon_X42 != (a131))
% 2.08/2.28  ((a40) != zenon_X95)
% 2.08/2.28  ((a65) != zenon_X20)
% 2.08/2.28  (-. (c4_2 (a18) zenon_X82))
% 2.08/2.28  (c3_1 (a136))
% 2.08/2.28  (c5_2 (a29) (a31))
% 2.08/2.28  ((a47) != zenon_X40)
% 2.08/2.28  (-. (c6_2 (a47) (a130)))
% 2.08/2.28  (zenon_X70 != zenon_X35)
% 2.08/2.28  ((a59) != zenon_X30)
% 2.08/2.28  (c6_2 (a68) (a30))
% 2.08/2.28  (zenon_X22 != zenon_X86)
% 2.08/2.28  ((a117) != zenon_X28)
% 2.08/2.28  (-. (c7_2 (a68) (a115)))
% 2.08/2.28  ((a136) != zenon_X9)
% 2.08/2.28  ((a65) != (a96))
% 2.08/2.28  (c6_2 (a47) (a108))
% 2.08/2.28  (-. (c5_2 (a39) (a123)))
% 2.08/2.28  ((a63) != zenon_X95)
% 2.08/2.28  (c8_2 (a122) zenon_X35)
% 2.08/2.28  (zenon_X86 != zenon_X147)
% 2.08/2.28  (zenon_X38 != (a117))
% 2.08/2.28  (-. (c8_2 (a39) zenon_X32))
% 2.08/2.28  (-. (c6_2 (a39) (a95)))
% 2.08/2.28  ((a30) != zenon_X34)
% 2.08/2.28  (-. (c2_2 (a47) (a63)))
% 2.08/2.28  ((a41) != zenon_X87)
% 2.08/2.28  ((a137) != zenon_X155)
% 2.08/2.28  (-. (c4_2 (a18) zenon_X29))
% 2.08/2.28  ((a63) != zenon_X78)
% 2.08/2.28  (zenon_X6 != (a129))
% 2.08/2.28  (-. (c5_2 (a81) (a97)))
% 2.08/2.28  ((a68) != (a104))
% 2.08/2.28  ((a123) != zenon_X8)
% 2.08/2.28  (c8_2 (a117) zenon_X14)
% 2.08/2.28  (zenon_X7 != (a34))
% 2.08/2.28  ((a59) != (a136))
% 2.08/2.28  ((a130) != zenon_X109)
% 2.08/2.28  ((a57) != zenon_X52)
% 2.08/2.28  (c8_2 (a122) (a130))
% 2.08/2.28  (-. (c5_2 (a117) (a95)))
% 2.08/2.28  ((a68) != zenon_X28)
% 2.08/2.28  (-. (c5_2 (a122) (a108)))
% 2.08/2.28  ((a63) != zenon_X46)
% 2.08/2.28  ((a47) != zenon_X28)
% 2.08/2.28  (zenon_X11 != (a104))
% 2.08/2.28  (-. (c2_2 zenon_X36 (a63)))
% 2.08/2.28  (c1_2 (a96) (a130))
% 2.08/2.28  (c5_2 (a65) (a41))
% 2.08/2.28  ((a136) != (a47))
% 2.08/2.28  ((a122) != zenon_X24)
% 2.08/2.28  ((a96) != zenon_X38)
% 2.08/2.28  ((a122) != zenon_X3)
% 2.08/2.28  ((a137) != zenon_X185)
% 2.08/2.28  (-. (c5_2 zenon_X6 (a97)))
% 2.08/2.28  (c1_2 (a51) (a40))
% 2.08/2.28  ((a95) != zenon_X43)
% 2.08/2.28  (c1_2 (a96) (a57))
% 2.08/2.28  ((a30) != (a48))
% 2.08/2.28  ((a41) != zenon_X37)
% 2.08/2.28  ((a95) != zenon_X110)
% 2.08/2.28  ((a58) != (a95))
% 2.08/2.28  ((a137) != zenon_X183)
% 2.08/2.28  (c1_2 (a18) (a40))
% 2.08/2.28  (zenon_X71 != (a130))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a82)))
% 2.08/2.28  (c8_2 (a93) (a115))
% 2.08/2.28  (c6_2 (a122) (a137))
% 2.08/2.28  ((a30) != (a58))
% 2.08/2.28  (zenon_X26 != zenon_X79)
% 2.08/2.28  (c1_2 (a39) (a30))
% 2.08/2.28  (c3_2 (a29) (a30))
% 2.08/2.28  (c1_1 zenon_X18)
% 2.08/2.28  ((a136) != zenon_X7)
% 2.08/2.28  (c8_2 (a93) (a114))
% 2.08/2.28  ((a114) != zenon_X42)
% 2.08/2.28  (zenon_X27 != zenon_X15)
% 2.08/2.28  (-. (c3_1 zenon_X18))
% 2.08/2.28  (zenon_X7 != zenon_X30)
% 2.08/2.28  (-. (c5_2 (a127) zenon_X119))
% 2.08/2.28  ((a57) != zenon_X37)
% 2.08/2.28  ((a131) != (a48))
% 2.08/2.28  ((a31) != zenon_X100)
% 2.08/2.28  (-. (c3_2 (a81) (a58)))
% 2.08/2.28  ((a82) != zenon_X161)
% 2.08/2.28  (ndr1_1 zenon_X6)
% 2.08/2.28  (zenon_X22 != (a31))
% 2.08/2.28  ((a57) != zenon_X49)
% 2.08/2.28  ((a40) != zenon_X96)
% 2.08/2.28  ((a97) != zenon_X220)
% 2.08/2.28  (c1_2 (a39) zenon_X101)
% 2.08/2.28  (c8_2 (a129) (a131))
% 2.08/2.28  (zenon_X70 != (a130))
% 2.08/2.28  (c5_2 (a121) (a97))
% 2.08/2.28  ((a59) != (a93))
% 2.08/2.28  (ndr1_1 zenon_X11)
% 2.08/2.28  (c1_2 (a29) (a63))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a137)))
% 2.08/2.28  (c8_2 (a117) (a130))
% 2.08/2.28  ((a82) != zenon_X46)
% 2.08/2.28  (-. (c3_2 (a136) zenon_X69))
% 2.08/2.28  (zenon_X23 != (a34))
% 2.08/2.28  (c6_2 (a29) (a30))
% 2.08/2.28  (-. (ndr1_1 zenon_X24))
% 2.08/2.28  (-. (c5_2 zenon_X6 (a58)))
% 2.08/2.28  ((a63) != (a49))
% 2.08/2.28  ((a108) != zenon_X39)
% 2.08/2.28  (zenon_X27 != (a34))
% 2.08/2.28  (-. (c7_2 (a34) zenon_X33))
% 2.08/2.28  (zenon_X39 != zenon_X79)
% 2.08/2.28  (c1_2 (a65) (a130))
% 2.08/2.28  (c3_1 (a96))
% 2.08/2.28  (zenon_X73 != (a115))
% 2.08/2.28  (c8_2 (a117) (a123))
% 2.08/2.28  ((a127) != (a93))
% 2.08/2.28  ((a57) != zenon_X184)
% 2.08/2.28  ((a30) != zenon_X75)
% 2.08/2.28  ((a82) != zenon_X195)
% 2.08/2.28  (-. (c5_2 zenon_X6 (a108)))
% 2.08/2.28  ((a39) != zenon_X18)
% 2.08/2.28  ((a129) != zenon_X40)
% 2.08/2.28  ((a130) != zenon_X155)
% 2.08/2.28  (c1_2 (a129) (a40))
% 2.08/2.28  ((a108) != (a115))
% 2.08/2.28  ((a31) != zenon_X95)
% 2.08/2.28  (zenon_X7 != zenon_X23)
% 2.08/2.28  (-. (c5_2 (a93) (a40)))
% 2.08/2.28  ((a65) != (a51))
% 2.08/2.28  (-. (c5_2 zenon_X11 zenon_X22))
% 2.08/2.28  (c6_2 zenon_X36 (a108))
% 2.08/2.28  ((a40) != zenon_X196)
% 2.08/2.28  (c1_1 (a81))
% 2.08/2.28  (-. (c1_2 (a47) (a49)))
% 2.08/2.28  (c7_2 (a59) (a31))
% 2.08/2.28  (-. (c5_2 (a136) (a31)))
% 2.08/2.28  (zenon_X7 != zenon_X40)
% 2.08/2.28  (-. (c3_2 (a18) zenon_X148))
% 2.08/2.28  (-. (c6_2 zenon_X9 (a41)))
% 2.08/2.28  ((a137) != (a123))
% 2.08/2.28  ((a39) != zenon_X40)
% 2.08/2.28  (-. (c3_2 (a96) zenon_X54))
% 2.08/2.28  (zenon_X38 != zenon_X24)
% 2.08/2.28  ((a29) != zenon_X15)
% 2.08/2.28  ((a130) != zenon_X21)
% 2.08/2.28  (c1_2 (a136) (a95))
% 2.08/2.28  (c8_2 (a93) (a41))
% 2.08/2.28  ((a63) != zenon_X8)
% 2.08/2.28  (-. (c5_2 zenon_X27 zenon_X191))
% 2.08/2.28  (zenon_X6 != (a104))
% 2.08/2.28  ((a114) != zenon_X39)
% 2.08/2.28  (c1_2 (a51) (a63))
% 2.08/2.28  (c1_2 (a47) (a130))
% 2.08/2.28  ((a59) != (a68))
% 2.08/2.28  (-. (c5_2 (a65) (a97)))
% 2.08/2.28  ((a41) != zenon_X193)
% 2.08/2.28  (c1_2 zenon_X7 (a58))
% 2.08/2.28  ((a40) != zenon_X115)
% 2.08/2.28  (zenon_X53 != (a123))
% 2.08/2.28  ((a82) != zenon_X193)
% 2.08/2.28  (-. (c7_2 (a93) zenon_X72))
% 2.08/2.28  (c6_2 (a81) (a57))
% 2.08/2.28  ((a130) != zenon_X8)
% 2.08/2.28  ((a58) != zenon_X35)
% 2.08/2.28  (c4_2 (a51) (a115))
% 2.08/2.28  (c5_2 (a59) zenon_X147)
% 2.08/2.28  ((a82) != zenon_X16)
% 2.08/2.28  (c1_2 (a47) (a40))
% 2.08/2.28  (-. (c6_2 (a93) zenon_X21))
% 2.08/2.28  ((a49) != zenon_X22)
% 2.08/2.28  (c1_2 (a39) (a130))
% 2.08/2.28  ((a68) != (a96))
% 2.08/2.28  ((a51) != zenon_X38)
% 2.08/2.28  (zenon_X10 != zenon_X15)
% 2.08/2.28  (c6_2 zenon_X20 (a30))
% 2.08/2.28  (zenon_X7 != zenon_X15)
% 2.08/2.28  ((a95) != zenon_X32)
% 2.08/2.28  ((a136) != zenon_X28)
% 2.08/2.28  ((a30) != zenon_X117)
% 2.08/2.28  (-. (c6_2 (a93) (a137)))
% 2.08/2.28  (zenon_X20 != zenon_X27)
% 2.08/2.28  ((a30) != zenon_X197)
% 2.08/2.28  (-. (c8_2 (a59) zenon_X153))
% 2.08/2.28  ((a127) != zenon_X3)
% 2.08/2.28  (c6_2 (a127) (a58))
% 2.08/2.28  (c7_1 zenon_X23)
% 2.08/2.28  (zenon_X9 != zenon_X28)
% 2.08/2.28  ((a48) != (a115))
% 2.08/2.28  ((a30) != (a130))
% 2.08/2.28  ((a47) != zenon_X15)
% 2.08/2.28  ((a59) != zenon_X40)
% 2.08/2.28  ((a18) != (a29))
% 2.08/2.28  (c8_2 (a104) (a40))
% 2.08/2.28  ((a108) != zenon_X2)
% 2.08/2.28  (c6_2 (a68) (a63))
% 2.08/2.28  ((a130) != zenon_X195)
% 2.08/2.28  (zenon_X16 != zenon_X193)
% 2.08/2.28  ((a30) != zenon_X33)
% 2.08/2.28  (c7_2 (a39) (a63))
% 2.08/2.28  (c6_2 zenon_X7 (a82))
% 2.08/2.28  ((a136) != (a104))
% 2.08/2.28  (-. (c3_1 zenon_X3))
% 2.08/2.28  (-. (c6_2 zenon_X11 zenon_X142))
% 2.08/2.28  (-. (c5_2 zenon_X38 (a108)))
% 2.08/2.28  ((a51) != (a39))
% 2.08/2.28  (ndr1_1 zenon_X7)
% 2.08/2.28  (c8_2 (a29) zenon_X73)
% 2.08/2.28  (c5_2 (a65) zenon_X153)
% 2.08/2.28  ((a97) != zenon_X71)
% 2.08/2.28  (c1_1 (a18))
% 2.08/2.28  ((a39) != zenon_X3)
% 2.08/2.28  (c4_1 (a51))
% 2.08/2.28  (-. (c2_2 zenon_X11 zenon_X130))
% 2.08/2.28  ((a130) != zenon_X165)
% 2.08/2.28  (zenon_X36 != zenon_X24)
% 2.08/2.28  ((a121) != (a34))
% 2.08/2.28  (zenon_X27 != (a39))
% 2.08/2.28  (c4_1 zenon_X7)
% 2.08/2.28  ((a114) != zenon_X153)
% 2.08/2.28  ((a48) != (a97))
% 2.08/2.28  (c8_2 (a47) zenon_X72)
% 2.08/2.28  (-. (c6_2 (a39) (a40)))
% 2.08/2.28  ((a96) != (a51))
% 2.08/2.28  ((a123) != zenon_X101)
% 2.08/2.28  ((a31) != (a130))
% 2.08/2.28  (-. (c5_2 (a59) (a137)))
% 2.08/2.28  (c3_2 (a65) (a57))
% 2.08/2.28  (zenon_X36 != (a18))
% 2.08/2.28  ((a137) != zenon_X123)
% 2.08/2.28  ((a65) != (a39))
% 2.08/2.28  (c8_2 (a39) zenon_X42)
% 2.08/2.28  ((a18) != (a68))
% 2.08/2.28  (c1_2 zenon_X11 (a95))
% 2.08/2.28  ((a137) != zenon_X65)
% 2.08/2.28  (-. (c6_2 zenon_X23 (a33)))
% 2.08/2.28  ((a57) != (a40))
% 2.08/2.28  ((a49) != zenon_X39)
% 2.08/2.28  (zenon_X20 != zenon_X7)
% 2.08/2.28  ((a131) != zenon_X147)
% 2.08/2.28  ((a57) != zenon_X189)
% 2.08/2.28  (c5_2 (a65) zenon_X151)
% 2.08/2.28  ((a130) != zenon_X111)
% 2.08/2.28  (-. (c5_2 (a47) (a108)))
% 2.08/2.28  (c1_2 (a59) (a108))
% 2.08/2.28  (-. (c7_2 (a93) zenon_X42))
% 2.08/2.28  (c5_2 (a29) (a108))
% 2.08/2.28  (zenon_X11 != zenon_X18)
% 2.08/2.28  ((a95) != zenon_X79)
% 2.08/2.28  (zenon_X18 != (a104))
% 2.08/2.28  (-. (c6_2 zenon_X11 (a108)))
% 2.08/2.28  (c4_2 (a51) (a123))
% 2.08/2.28  (c6_2 zenon_X7 (a130))
% 2.08/2.28  ((a137) != (a40))
% 2.08/2.28  (zenon_X9 != (a47))
% 2.08/2.28  ((a82) != zenon_X51)
% 2.08/2.28  ((a40) != zenon_X78)
% 2.08/2.28  (-. (c8_1 (a47)))
% 2.08/2.28  (zenon_X38 != zenon_X18)
% 2.08/2.28  ((a68) != zenon_X7)
% 2.08/2.28  ((a137) != zenon_X152)
% 2.08/2.28  (zenon_X16 != zenon_X133)
% 2.08/2.28  (c1_2 (a29) (a95))
% 2.08/2.28  ((a81) != zenon_X30)
% 2.08/2.28  (-. (c2_1 (a29)))
% 2.08/2.28  ((a33) != zenon_X158)
% 2.08/2.28  (c1_2 (a93) (a63))
% 2.08/2.28  ((a63) != zenon_X145)
% 2.08/2.28  ((a30) != (a137))
% 2.08/2.28  ((a122) != zenon_X9)
% 2.08/2.28  (-. (c5_2 (a136) (a108)))
% 2.08/2.28  (zenon_X6 != zenon_X23)
% 2.08/2.28  (-. (c5_2 (a129) (a123)))
% 2.08/2.28  (-. (c4_2 (a93) (a82)))
% 2.08/2.28  ((a58) != zenon_X193)
% 2.08/2.28  ((a40) != zenon_X147)
% 2.08/2.28  ((a115) != zenon_X101)
% 2.08/2.28  ((a130) != zenon_X69)
% 2.08/2.28  ((a130) != (a49))
% 2.08/2.28  (c8_2 (a93) (a97))
% 2.08/2.28  (-. (c1_1 (a39)))
% 2.08/2.28  (c8_2 (a104) (a30))
% 2.08/2.28  ((a108) != zenon_X78)
% 2.08/2.28  ((a58) != zenon_X8)
% 2.08/2.28  (c7_1 (a29))
% 2.08/2.28  ((a108) != zenon_X189)
% 2.08/2.28  (c1_2 (a47) (a82))
% 2.08/2.28  (-. (c5_2 (a96) zenon_X120))
% 2.08/2.28  (-. (c3_0))
% 2.08/2.28  (-. (c5_2 (a39) (a31)))
% 2.08/2.28  (c4_2 (a29) (a30))
% 2.08/2.28  ((a51) != zenon_X28)
% 2.08/2.28  (-. (c5_2 (a136) (a123)))
% 2.08/2.28  (zenon_X23 != (a68))
% 2.08/2.28  (-. (c8_1 (a129)))
% 2.08/2.28  ((a40) != (a48))
% 2.08/2.28  (c3_2 (a18) (a57))
% 2.08/2.28  (c8_2 (a104) (a108))
% 2.08/2.28  (-. (c5_2 (a68) zenon_X121))
% 2.08/2.28  ((a130) != (a115))
% 2.08/2.28  (-. (c5_2 zenon_X38 zenon_X153))
% 2.08/2.28  (ndr1_1 zenon_X38)
% 2.08/2.28  ((a63) != (a40))
% 2.08/2.28  (ndr1_1 (a68))
% 2.08/2.28  (c6_2 (a39) (a130))
% 2.08/2.28  (-. (c4_2 (a18) zenon_X79))
% 2.08/2.28  ((a136) != zenon_X40)
% 2.08/2.28  (c1_2 (a59) (a41))
% 2.08/2.28  ((a82) != zenon_X89)
% 2.08/2.28  (-. (c2_2 (a81) (a63)))
% 2.08/2.28  (-. (c5_2 zenon_X11 zenon_X82))
% 2.08/2.28  ((a59) != zenon_X23)
% 2.08/2.28  (c6_2 (a68) (a33))
% 2.08/2.28  (c6_2 (a129) (a137))
% 2.08/2.28  (c8_2 (a129) zenon_X35)
% 2.08/2.28  (zenon_X22 != (a123))
% 2.08/2.28  (-. (c3_2 (a127) (a115)))
% 2.08/2.28  ((a114) != (a95))
% 2.08/2.28  ((a108) != zenon_X87)
% 2.08/2.28  ((a95) != zenon_X96)
% 2.08/2.28  (-. (c4_1 zenon_X27))
% 2.08/2.28  ((a40) != zenon_X75)
% 2.08/2.28  ((a31) != zenon_X32)
% 2.08/2.28  (zenon_X26 != zenon_X22)
% 2.08/2.28  (zenon_X23 != zenon_X15)
% 2.08/2.28  (c3_2 (a39) (a30))
% 2.08/2.28  ((a63) != zenon_X87)
% 2.08/2.28  ((a31) != zenon_X16)
% 2.08/2.28  (c1_2 (a121) (a57))
% 2.08/2.28  (-. (c7_1 zenon_X15))
% 2.08/2.28  (c7_2 (a136) (a48))
% 2.08/2.28  (zenon_X153 != zenon_X22)
% 2.08/2.28  (-. (c2_1 (a117)))
% 2.08/2.28  (zenon_X22 != zenon_X82)
% 2.08/2.28  (-. (c5_2 (a122) zenon_X26))
% 2.08/2.28  (zenon_X29 != zenon_X79)
% 2.08/2.28  (c1_2 (a29) (a58))
% 2.08/2.28  ((a51) != zenon_X23)
% 2.08/2.28  ((a40) != zenon_X195)
% 2.08/2.28  (-. (c6_2 (a47) (a41)))
% 2.08/2.28  (c6_2 (a81) (a95))
% 2.08/2.28  (-. (c3_2 (a129) zenon_X55))
% 2.08/2.28  (-. (ndr1_1 (a104)))
% 2.08/2.28  ((a117) != (a29))
% 2.08/2.28  ((a95) != zenon_X207)
% 2.08/2.28  (-. (c2_2 zenon_X38 (a63)))
% 2.08/2.28  ((a40) != zenon_X21)
% 2.08/2.28  ((a68) != (a117))
% 2.08/2.28  ((a137) != zenon_X50)
% 2.08/2.28  ((a68) != (a29))
% 2.08/2.28  ((a97) != (a131))
% 2.08/2.28  ((a18) != zenon_X38)
% 2.08/2.28  ((a30) != zenon_X13)
% 2.08/2.28  ((a127) != zenon_X17)
% 2.08/2.28  (-. (c6_2 (a104) (a130)))
% 2.08/2.28  ((a30) != zenon_X211)
% 2.08/2.28  (c6_2 (a29) (a31))
% 2.08/2.28  ((a121) != (a104))
% 2.08/2.28  ((a82) != zenon_X79)
% 2.08/2.28  ((a49) != zenon_X88)
% 2.08/2.28  ((a108) != zenon_X196)
% 2.08/2.28  ((a68) != zenon_X36)
% 2.08/2.28  ((a114) != zenon_X22)
% 2.08/2.28  (c7_2 (a29) (a30))
% 2.08/2.28  ((a58) != zenon_X16)
% 2.08/2.28  (zenon_X151 != (a30))
% 2.08/2.28  (-. (c2_1 zenon_X18))
% 2.08/2.28  (-. (c3_2 zenon_X7 zenon_X158))
% 2.08/2.28  (c2_2 (a65) (a57))
% 2.08/2.28  (zenon_X36 != (a129))
% 2.08/2.28  ((a97) != zenon_X70)
% 2.08/2.28  ((a57) != zenon_X158)
% 2.08/2.28  ((a130) != zenon_X100)
% 2.08/2.28  (c1_2 (a136) (a40))
% 2.08/2.28  (zenon_X7 != (a117))
% 2.08/2.28  ((a95) != (a33))
% 2.08/2.28  ((a130) != zenon_X66)
% 2.08/2.28  ((a130) != zenon_X110)
% 2.08/2.28  ((a58) != zenon_X88)
% 2.08/2.28  ((a49) != zenon_X2)
% 2.08/2.28  (c6_2 zenon_X36 (a95))
% 2.08/2.28  (c8_2 (a47) (a123))
% 2.08/2.28  (zenon_X151 != zenon_X147)
% 2.08/2.28  ((a47) != zenon_X27)
% 2.08/2.28  (zenon_X6 != zenon_X10)
% 2.08/2.28  (zenon_X151 != zenon_X79)
% 2.08/2.28  ((a123) != zenon_X29)
% 2.08/2.28  ((a115) != (a123))
% 2.08/2.28  (zenon_X7 != zenon_X9)
% 2.08/2.28  ((a30) != zenon_X69)
% 2.08/2.28  ((a30) != zenon_X115)
% 2.08/2.28  (-. (c5_2 (a18) zenon_X22))
% 2.08/2.28  (c7_2 (a136) zenon_X101)
% 2.08/2.28  ((a122) != zenon_X6)
% 2.08/2.28  (zenon_X21 != (a58))
% 2.08/2.28  (c3_1 zenon_X36)
% 2.08/2.28  ((a33) != (a108))
% 2.08/2.28  ((a81) != zenon_X18)
% 2.08/2.28  ((a57) != zenon_X148)
% 2.08/2.28  ((a137) != zenon_X69)
% 2.08/2.28  (c1_2 (a59) zenon_X104)
% 2.08/2.28  ((a108) != (a40))
% 2.08/2.28  (zenon_X27 != (a117))
% 2.08/2.28  (zenon_X53 != (a97))
% 2.08/2.28  (zenon_X22 != zenon_X79)
% 2.08/2.28  (c5_2 (a59) (a131))
% 2.08/2.28  ((a49) != zenon_X111)
% 2.08/2.28  ((a129) != (a93))
% 2.08/2.28  ((a68) != (a127))
% 2.08/2.28  ((a95) != (a130))
% 2.08/2.28  ((a30) != zenon_X8)
% 2.08/2.28  (-. (c5_2 zenon_X20 (a58)))
% 2.08/2.28  (-. (c4_1 (a39)))
% 2.08/2.28  (c1_2 zenon_X7 (a82))
% 2.08/2.28  ((a117) != zenon_X5)
% 2.08/2.28  (c4_1 zenon_X23)
% 2.08/2.28  (-. (c5_2 (a39) zenon_X26))
% 2.08/2.28  (c1_2 (a121) (a97))
% 2.08/2.28  ((a114) != (a31))
% 2.08/2.28  (zenon_X9 != (a29))
% 2.08/2.28  ((a18) != (a96))
% 2.08/2.28  (-. (c5_2 (a51) zenon_X29))
% 2.08/2.28  ((a59) != zenon_X24)
% 2.08/2.28  ((a137) != zenon_X147)
% 2.08/2.28  (-. (c2_2 (a68) (a63)))
% 2.08/2.28  ((a93) != zenon_X38)
% 2.08/2.28  ((a18) != zenon_X3)
% 2.08/2.28  (c6_1 (a34))
% 2.08/2.28  (c1_2 zenon_X23 (a130))
% 2.08/2.28  (c5_2 (a129) (a130))
% 2.08/2.28  (zenon_X22 != zenon_X104)
% 2.08/2.28  ((a49) != zenon_X14)
% 2.08/2.28  ((a97) != zenon_X73)
% 2.08/2.28  (c8_2 (a122) zenon_X32)
% 2.08/2.28  (c5_2 zenon_X6 (a95))
% 2.08/2.28  ((a39) != zenon_X28)
% 2.08/2.28  ((a81) != zenon_X28)
% 2.08/2.28  ((a57) != zenon_X75)
% 2.08/2.28  (zenon_X11 != (a127))
% 2.08/2.28  ((a18) != (a136))
% 2.08/2.28  (c7_2 (a59) (a115))
% 2.08/2.28  ((a117) != (a93))
% 2.08/2.28  (c1_2 (a65) (a33))
% 2.08/2.28  (zenon_X14 != zenon_X70)
% 2.08/2.28  ((a65) != (a127))
% 2.08/2.28  (-. (c3_1 zenon_X28))
% 2.08/2.28  ((a95) != zenon_X193)
% 2.08/2.28  ((a29) != zenon_X3)
% 2.08/2.28  (zenon_X151 != (a97))
% 2.08/2.28  (-. (c4_2 (a129) zenon_X44))
% 2.08/2.28  (zenon_X9 != zenon_X24)
% 2.08/2.28  ((a48) != (a123))
% 2.08/2.28  (c1_2 (a65) (a57))
% 2.08/2.28  ((a95) != (a131))
% 2.08/2.28  (-. (c7_1 zenon_X28))
% 2.08/2.28  (-. (c5_2 (a65) (a30)))
% 2.08/2.28  (-. (c6_2 zenon_X7 (a137)))
% 2.08/2.28  (zenon_X20 != zenon_X28)
% 2.08/2.28  (-. (c5_2 (a117) zenon_X211))
% 2.08/2.28  ((a130) != zenon_X55)
% 2.08/2.28  (c1_2 (a18) (a95))
% 2.08/2.28  ((a59) != (a47))
% 2.08/2.28  ((a58) != zenon_X189)
% 2.08/2.28  (c7_2 (a39) (a123))
% 2.08/2.28  (zenon_X22 != (a108))
% 2.08/2.28  (zenon_X105 != (a130))
% 2.08/2.28  (c7_2 (a39) (a95))
% 2.08/2.28  ((a33) != zenon_X52)
% 2.08/2.28  (c6_1 zenon_X18)
% 2.08/2.28  (c8_2 zenon_X38 zenon_X226)
% 2.08/2.28  (-. (c3_2 (a127) zenon_X89))
% 2.08/2.28  (c5_2 (a65) zenon_X78)
% 2.08/2.28  ((a127) != (a47))
% 2.08/2.28  ((a130) != zenon_X193)
% 2.08/2.28  (zenon_X9 != (a129))
% 2.08/2.28  ((a130) != zenon_X78)
% 2.08/2.28  (c4_1 (a18))
% 2.08/2.28  (c3_2 (a117) (a30))
% 2.08/2.28  ((a47) != (a34))
% 2.08/2.28  (-. (c8_2 (a96) (a115)))
% 2.08/2.28  (c6_1 (a104))
% 2.08/2.28  (-. (c8_2 (a39) zenon_X83))
% 2.08/2.28  ((a96) != zenon_X5)
% 2.08/2.28  (-. (c3_1 zenon_X9))
% 2.08/2.28  ((a57) != zenon_X116)
% 2.08/2.28  (zenon_X9 != zenon_X15)
% 2.08/2.28  (-. (c6_2 zenon_X7 zenon_X21))
% 2.08/2.28  ((a130) != zenon_X147)
% 2.08/2.28  (-. (c7_2 (a93) zenon_X71))
% 2.08/2.28  (-. (c5_2 (a122) (a63)))
% 2.08/2.28  (c7_2 (a136) zenon_X2)
% 2.08/2.28  ((a30) != zenon_X81)
% 2.08/2.28  (-. (c5_2 (a39) (a95)))
% 2.08/2.28  (c1_2 zenon_X11 (a57))
% 2.08/2.28  (-. (c5_2 (a51) zenon_X82))
% 2.08/2.28  ((a104) != zenon_X28)
% 2.08/2.28  (-. (c6_2 zenon_X9 (a82)))
% 2.08/2.28  (c8_2 (a129) (a114))
% 2.08/2.28  (-. (c3_2 zenon_X11 zenon_X116))
% 2.08/2.28  (c1_2 (a121) (a137))
% 2.08/2.28  (c4_2 (a65) (a97))
% 2.08/2.28  (c7_2 (a39) (a130))
% 2.08/2.28  ((a137) != zenon_X133)
% 2.08/2.28  (c8_2 (a129) zenon_X53)
% 2.08/2.28  ((a30) != zenon_X26)
% 2.08/2.28  (-. (c6_2 zenon_X23 (a108)))
% 2.08/2.28  (zenon_X27 != zenon_X24)
% 2.08/2.28  (-. (c5_2 (a122) (a58)))
% 2.08/2.28  (-. (c6_2 (a29) (a82)))
% 2.08/2.28  (zenon_X40 != zenon_X9)
% 2.08/2.28  (-. (c5_2 (a39) (a41)))
% 2.08/2.28  (-. (ndr1_1 zenon_X15))
% 2.08/2.28  ((a34) != zenon_X30)
% 2.08/2.28  (-. (c6_2 (a104) (a58)))
% 2.08/2.28  (c6_2 zenon_X23 (a30))
% 2.08/2.28  (c1_2 zenon_X11 (a114))
% 2.08/2.28  (c5_2 (a65) (a63))
% 2.08/2.28  ((a122) != zenon_X36)
% 2.08/2.28  (c8_2 (a18) zenon_X22)
% 2.08/2.28  ((a51) != zenon_X24)
% 2.08/2.28  (c1_2 zenon_X27 (a95))
% 2.08/2.28  (c8_2 (a104) (a57))
% 2.08/2.28  (c8_2 (a93) (a49))
% 2.08/2.28  (-. (c7_1 (a34)))
% 2.08/2.28  ((a48) != zenon_X42)
% 2.08/2.28  (c5_2 (a136) (a137))
% 2.08/2.28  ((a57) != zenon_X21)
% 2.08/2.28  (-. (c8_2 (a104) zenon_X197))
% 2.08/2.28  (zenon_X53 != zenon_X72)
% 2.08/2.28  ((a65) != (a18))
% 2.08/2.28  (c1_2 (a136) (a33))
% 2.08/2.28  (zenon_X27 != zenon_X38)
% 2.08/2.28  ((a121) != (a47))
% 2.08/2.28  (-. (c4_1 zenon_X28))
% 2.08/2.28  ((a115) != zenon_X110)
% 2.08/2.28  (-. (c5_2 (a81) (a58)))
% 2.08/2.28  ((a137) != zenon_X86)
% 2.08/2.28  ((a30) != zenon_X96)
% 2.08/2.28  (c8_2 (a136) (a115))
% 2.08/2.28  (-. (c6_2 zenon_X15 zenon_X21))
% 2.08/2.28  (c1_2 (a136) (a57))
% 2.08/2.28  ((a30) != zenon_X58)
% 2.08/2.28  ((a51) != zenon_X10)
% 2.08/2.28  ((a95) != zenon_X211)
% 2.08/2.28  ((a49) != zenon_X143)
% 2.08/2.28  (ndr1_1 (a93))
% 2.08/2.28  (c5_2 (a65) (a40))
% 2.08/2.28  (c6_2 (a136) (a57))
% 2.08/2.28  (c7_2 (a39) (a30))
% 2.08/2.28  ((a63) != zenon_X12)
% 2.08/2.28  (c1_2 zenon_X11 (a82))
% 2.08/2.28  ((a49) != zenon_X220)
% 2.08/2.28  ((a130) != zenon_X39)
% 2.08/2.28  (c6_2 (a81) (a82))
% 2.08/2.28  (c8_2 (a47) zenon_X42)
% 2.08/2.28  ((a31) != zenon_X87)
% 2.08/2.28  ((a95) != zenon_X12)
% 2.08/2.28  (zenon_X38 != zenon_X40)
% 2.08/2.28  ((a108) != zenon_X32)
% 2.08/2.28  (c6_2 zenon_X20 (a137))
% 2.08/2.28  ((a82) != zenon_X142)
% 2.08/2.28  (c3_2 (a96) (a30))
% 2.08/2.28  ((a58) != zenon_X196)
% 2.08/2.28  ((a114) != (a130))
% 2.08/2.28  ((a96) != zenon_X24)
% 2.08/2.28  (zenon_X104 != zenon_X82)
% 2.08/2.28  (-. (c2_2 (a121) zenon_X107))
% 2.08/2.28  ((a41) != zenon_X133)
% 2.08/2.28  ((a136) != (a39))
% 2.08/2.28  (zenon_X32 != (a123))
% 2.08/2.28  (-. (c5_2 (a122) (a137)))
% 2.08/2.28  (-. (c4_2 (a18) zenon_X151))
% 2.08/2.28  ((a40) != zenon_X153)
% 2.08/2.28  ((a97) != (a115))
% 2.08/2.28  ((a82) != (a130))
% 2.08/2.28  ((a39) != (a93))
% 2.08/2.28  ((a129) != zenon_X15)
% 2.08/2.28  ((a33) != zenon_X16)
% 2.08/2.28  ((a82) != (a95))
% 2.08/2.28  (-. (c8_2 zenon_X15 (a108)))
% 2.08/2.28  (zenon_X53 != (a49))
% 2.08/2.28  ((a130) != zenon_X37)
% 2.08/2.28  (c6_2 (a96) (a40))
% 2.08/2.28  (c4_2 zenon_X38 (a63))
% 2.08/2.28  ((a30) != zenon_X195)
% 2.08/2.28  ((a115) != zenon_X8)
% 2.08/2.28  (-. (c5_2 zenon_X38 (a40)))
% 2.08/2.28  (-. (c4_2 zenon_X23 zenon_X187))
% 2.08/2.28  (c6_2 (a121) (a95))
% 2.08/2.28  ((a30) != zenon_X111)
% 2.08/2.28  (zenon_X35 != (a49))
% 2.08/2.28  ((a82) != (a115))
% 2.08/2.28  (-. (c5_2 (a68) (a30)))
% 2.08/2.28  (-. (c5_2 zenon_X7 (a58)))
% 2.08/2.28  (c6_2 (a127) (a130))
% 2.08/2.28  (-. (c6_2 (a29) (a137)))
% 2.08/2.28  (-. (c5_0))
% 2.08/2.28  (c7_2 (a39) (a137))
% 2.08/2.28  ((a130) != zenon_X79)
% 2.08/2.28  (c6_2 (a81) (a30))
% 2.08/2.28  (-. (c6_2 zenon_X7 (a97)))
% 2.08/2.28  ((a82) != zenon_X170)
% 2.08/2.28  (c5_2 (a59) zenon_X82)
% 2.08/2.28  (-. (c5_2 (a129) (a49)))
% 2.08/2.28  ((a65) != zenon_X24)
% 2.08/2.28  (zenon_X26 != zenon_X104)
% 2.08/2.28  (c6_2 (a117) (a58))
% 2.08/2.28  ((a81) != (a117))
% 2.08/2.28  (-. (c7_2 (a93) (a123)))
% 2.08/2.28  ((a30) != zenon_X142)
% 2.08/2.28  ((a49) != zenon_X26)
% 2.08/2.28  (-. (c2_2 zenon_X11 (a63)))
% 2.08/2.28  ((a40) != zenon_X35)
% 2.08/2.28  (-. (c5_2 (a65) zenon_X82))
% 2.08/2.28  (-. (c6_2 (a18) (a108)))
% 2.08/2.28  ((a57) != zenon_X8)
% 2.08/2.28  (-. (c6_2 (a104) (a137)))
% 2.08/2.28  (-. (c2_2 zenon_X6 zenon_X172))
% 2.08/2.28  (c6_1 (a18))
% 2.08/2.28  ((a97) != zenon_X160)
% 2.08/2.28  ((a131) != zenon_X26)
% 2.08/2.28  (c1_2 (a39) (a137))
% 2.08/2.28  (zenon_X53 != zenon_X74)
% 2.08/2.28  (zenon_X18 != zenon_X24)
% 2.08/2.28  (-. (c6_2 zenon_X15 (a108)))
% 2.08/2.28  (c5_2 zenon_X11 (a114))
% 2.08/2.28  (c6_2 (a81) (a130))
% 2.08/2.28  ((a41) != (a130))
% 2.08/2.28  ((a82) != zenon_X165)
% 2.08/2.28  (c6_2 (a129) (a82))
% 2.08/2.28  ((a130) != zenon_X168)
% 2.08/2.28  ((a137) != zenon_X95)
% 2.08/2.28  ((a31) != zenon_X29)
% 2.08/2.28  ((a121) != zenon_X24)
% 2.08/2.28  (-. (c2_1 zenon_X0))
% 2.08/2.28  (-. (c2_2 (a47) zenon_X59))
% 2.08/2.28  (c1_2 (a51) (a49))
% 2.08/2.28  ((a95) != zenon_X133)
% 2.08/2.28  (c1_2 (a59) (a123))
% 2.08/2.28  ((a95) != zenon_X124)
% 2.08/2.28  (c8_2 (a39) (a123))
% 2.08/2.28  (-. (c6_1 (a122)))
% 2.08/2.28  (c1_1 zenon_X9)
% 2.08/2.28  (c1_2 (a65) (a40))
% 2.08/2.28  (c6_2 zenon_X6 (a58))
% 2.08/2.28  (c6_2 (a51) (a58))
% 2.08/2.28  (-. (c8_2 (a65) zenon_X151))
% 2.08/2.28  ((a30) != zenon_X95)
% 2.08/2.28  ((a136) != zenon_X3)
% 2.08/2.28  ((a58) != zenon_X153)
% 2.08/2.28  (zenon_X14 != (a130))
% 2.08/2.28  (-. (c5_2 (a93) (a58)))
% 2.08/2.28  ((a82) != (a58))
% 2.08/2.28  ((a29) != (a93))
% 2.08/2.28  ((a30) != zenon_X79)
% 2.08/2.28  (c5_2 (a59) zenon_X29)
% 2.08/2.28  (zenon_X11 != zenon_X3)
% 2.08/2.28  ((a121) != zenon_X6)
% 2.08/2.28  ((a130) != zenon_X123)
% 2.08/2.28  (-. (c2_2 (a39) (a41)))
% 2.08/2.28  (-. (c5_2 (a122) zenon_X78))
% 2.08/2.28  (c5_2 (a59) zenon_X153)
% 2.08/2.28  ((a63) != zenon_X104)
% 2.08/2.28  ((a49) != zenon_X147)
% 2.08/2.28  (-. (c6_2 zenon_X9 (a137)))
% 2.08/2.28  ((a104) != zenon_X15)
% 2.08/2.28  ((a95) != zenon_X8)
% 2.08/2.28  (-. (c4_2 (a136) zenon_X43))
% 2.08/2.28  (c6_2 (a68) (a41))
% 2.08/2.28  ((a63) != zenon_X111)
% 2.08/2.28  (zenon_X38 != (a47))
% 2.08/2.28  (-. (c5_2 zenon_X11 (a40)))
% 2.08/2.28  (-. (c4_2 (a121) zenon_X111))
% 2.08/2.28  (c6_2 zenon_X36 (a137))
% 2.08/2.28  ((a31) != zenon_X12)
% 2.08/2.28  (-. (c5_2 zenon_X7 (a108)))
% 2.08/2.28  ((a30) != zenon_X102)
% 2.08/2.28  (-. (c5_2 (a68) (a49)))
% 2.08/2.28  ((a30) != zenon_X152)
% 2.08/2.28  (c6_2 (a39) (a57))
% 2.08/2.28  (c1_2 (a39) zenon_X72)
% 2.08/2.28  (c8_2 (a47) (a114))
% 2.08/2.28  (c1_2 (a121) (a63))
% 2.08/2.28  (-. (c8_2 (a65) zenon_X86))
% 2.08/2.28  (zenon_X27 != zenon_X30)
% 2.08/2.28  (-. (c6_2 zenon_X27 zenon_X124))
% 2.08/2.28  (-. (c5_2 zenon_X38 (a58)))
% 2.08/2.28  (c7_2 (a39) (a97))
% 2.08/2.28  (zenon_X21 != (a31))
% 2.08/2.28  ((a57) != zenon_X125)
% 2.08/2.28  ((a95) != zenon_X86)
% 2.08/2.28  (c6_1 (a29))
% 2.08/2.28  ((a96) != zenon_X10)
% 2.08/2.28  (c6_2 zenon_X6 (a95))
% 2.08/2.28  (zenon_X53 != zenon_X35)
% 2.08/2.28  ((a40) != zenon_X103)
% 2.08/2.28  (zenon_X23 != (a127))
% 2.08/2.28  (zenon_X38 != zenon_X15)
% 2.08/2.28  (c7_2 (a96) (a97))
% 2.08/2.28  ((a123) != zenon_X72)
% 2.08/2.28  ((a95) != (a41))
% 2.08/2.28  (c8_2 (a136) zenon_X74)
% 2.08/2.28  (-. (c4_2 (a18) zenon_X153))
% 2.08/2.28  ((a58) != zenon_X78)
% 2.08/2.28  ((a51) != zenon_X11)
% 2.08/2.28  (-. (c5_2 zenon_X7 zenon_X188))
% 2.08/2.28  (c6_2 (a39) (a82))
% 2.08/2.28  ((a48) != zenon_X14)
% 2.08/2.28  (-. (c5_2 zenon_X6 zenon_X207))
% 2.08/2.28  (-. (c5_2 (a51) zenon_X26))
% 2.08/2.28  ((a40) != zenon_X51)
% 2.08/2.28  (c6_2 (a136) (a30))
% 2.08/2.28  ((a136) != zenon_X30)
% 2.08/2.28  (zenon_X27 != (a93))
% 2.08/2.28  (-. (c5_2 (a47) (a63)))
% 2.08/2.28  (-. (c3_1 zenon_X23))
% 2.08/2.28  (-. (c8_2 (a39) zenon_X71))
% 2.08/2.28  ((a68) != zenon_X5)
% 2.08/2.28  (c7_2 (a39) (a33))
% 2.08/2.28  (c6_2 (a122) (a33))
% 2.08/2.28  (c8_2 (a39) zenon_X53)
% 2.08/2.28  ((a95) != zenon_X147)
% 2.08/2.28  ((a122) != (a39))
% 2.08/2.28  (ndr1_1 zenon_X36)
% 2.08/2.28  (-. (c7_1 (a51)))
% 2.08/2.28  (-. (c7_2 (a93) zenon_X14))
% 2.08/2.28  (c7_2 (a39) zenon_X53)
% 2.08/2.28  (-. (c5_2 zenon_X20 zenon_X220))
% 2.08/2.28  ((a96) != zenon_X17)
% 2.08/2.28  (zenon_X53 != zenon_X73)
% 2.08/2.28  ((a59) != (a18))
% 2.08/2.28  ((a115) != zenon_X32)
% 2.08/2.28  ((a29) != zenon_X30)
% 2.08/2.28  (c1_1 (a65))
% 2.08/2.28  ((a95) != (a49))
% 2.08/2.28  (c1_2 zenon_X7 (a63))
% 2.08/2.28  (-. (c8_2 (a59) zenon_X86))
% 2.08/2.28  (c6_1 zenon_X10)
% 2.08/2.28  ((a57) != zenon_X180)
% 2.08/2.28  ((a63) != zenon_X96)
% 2.08/2.28  (c4_0)
% 2.08/2.28  (c5_2 (a65) zenon_X26)
% 2.08/2.28  (-. (c6_2 (a39) (a58)))
% 2.08/2.28  (c1_2 (a29) (a108))
% 2.08/2.28  ((a57) != zenon_X68)
% 2.08/2.28  (c7_2 (a39) (a31))
% 2.08/2.28  ((a31) != (a48))
% 2.08/2.28  ((a127) != zenon_X7)
% 2.08/2.28  ((a96) != (a136))
% 2.08/2.28  ((a30) != zenon_X88)
% 2.08/2.28  ((a33) != zenon_X196)
% 2.08/2.28  (zenon_X82 != zenon_X79)
% 2.08/2.28  (zenon_X35 != zenon_X83)
% 2.08/2.28  ((a121) != zenon_X18)
% 2.08/2.28  (-. (c5_2 (a47) zenon_X161))
% 2.08/2.28  (-. (c8_2 (a59) zenon_X26))
% 2.08/2.28  (c7_2 (a47) (a49))
% 2.08/2.28  ((a82) != (a49))
% 2.08/2.28  (c1_2 (a39) (a114))
% 2.08/2.28  ((a97) != zenon_X33)
% 2.08/2.28  (zenon_X26 != (a123))
% 2.08/2.28  ((a57) != zenon_X86)
% 2.08/2.28  ((a57) != zenon_X133)
% 2.08/2.28  (-. (c6_2 (a93) zenon_X95))
% 2.08/2.28  (c5_2 (a59) (a63))
% 2.08/2.28  (c8_2 zenon_X27 (a115))
% 2.08/2.28  ((a68) != zenon_X15)
% 2.08/2.28  ((a130) != zenon_X54)
% 2.08/2.28  (-. (c5_2 (a18) (a49)))
% 2.08/2.28  (c7_2 (a136) zenon_X14)
% 2.08/2.28  (zenon_X38 != zenon_X28)
% 2.08/2.28  (c6_2 zenon_X27 (a82))
% 2.08/2.28  ((a68) != (a122))
% 2.08/2.28  (c1_2 (a29) (a82))
% 2.08/2.28  (-. (c6_2 zenon_X9 (a58)))
% 2.08/2.28  ((a115) != zenon_X34)
% 2.08/2.28  (zenon_X86 != zenon_X79)
% 2.08/2.28  ((a81) != (a39))
% 2.08/2.28  (-. (c7_1 zenon_X40))
% 2.08/2.28  ((a40) != zenon_X113)
% 2.08/2.28  ((a93) != zenon_X3)
% 2.08/2.28  ((a115) != zenon_X143)
% 2.08/2.28  ((a97) != zenon_X188)
% 2.08/2.28  (c5_2 (a59) (a130))
% 2.08/2.28  ((a114) != zenon_X14)
% 2.08/2.28  ((a131) != (a130))
% 2.08/2.28  ((a31) != (a108))
% 2.08/2.28  (c8_2 (a117) (a49))
% 2.08/2.28  (-. (c3_2 (a81) zenon_X65))
% 2.08/2.28  (c7_2 (a39) (a114))
% 2.08/2.28  ((a97) != zenon_X22)
% 2.08/2.28  (zenon_X20 != (a136))
% 2.08/2.28  (c6_2 (a68) zenon_X189)
% 2.08/2.28  ((a95) != zenon_X35)
% 2.08/2.28  ((a47) != (a104))
% 2.08/2.28  (-. (c5_2 (a136) zenon_X88))
% 2.08/2.28  (c8_2 (a29) (a115))
% 2.08/2.28  (c5_2 (a39) (a114))
% 2.08/2.28  (zenon_X42 != zenon_X101)
% 2.08/2.28  ((a47) != zenon_X30)
% 2.08/2.28  (-. (c5_2 (a122) (a40)))
% 2.08/2.28  ((a115) != zenon_X82)
% 2.08/2.28  ((a57) != zenon_X185)
% 2.08/2.28  (zenon_X21 != (a137))
% 2.08/2.28  ((a97) != zenon_X8)
% 2.08/2.28  (-. (c4_1 (a104)))
% 2.08/2.28  (c7_2 (a39) (a108))
% 2.08/2.28  ((a63) != (a123))
% 2.08/2.28  ((a40) != zenon_X84)
% 2.08/2.28  (zenon_X78 != (a49))
% 2.08/2.28  (c6_2 (a39) (a30))
% 2.08/2.28  ((a137) != zenon_X196)
% 2.08/2.28  (zenon_X40 != zenon_X30)
% 2.08/2.28  (zenon_X6 != zenon_X24)
% 2.08/2.28  ((a18) != zenon_X10)
% 2.08/2.28  (c8_2 (a39) (a114))
% 2.08/2.28  (zenon_X30 != zenon_X36)
% 2.08/2.28  ((a81) != zenon_X3)
% 2.08/2.28  ((a58) != (a48))
% 2.08/2.28  ((a18) != (a39))
% 2.08/2.28  (c1_2 (a59) (a97))
% 2.08/2.28  (c8_2 (a47) zenon_X53)
% 2.08/2.28  (-. (c5_2 zenon_X38 (a63)))
% 2.08/2.28  (c8_2 (a122) (a49))
% 2.08/2.28  (-. (c2_2 (a127) (a63)))
% 2.08/2.28  (c1_2 (a18) (a30))
% 2.08/2.28  (c4_1 zenon_X6)
% 2.08/2.28  ((a18) != (a34))
% 2.08/2.28  (-. (c6_2 (a93) (a30)))
% 2.08/2.28  (c6_2 (a127) (a40))
% 2.08/2.28  (c8_2 zenon_X11 (a114))
% 2.08/2.28  (-. (c6_2 (a93) (a31)))
% 2.08/2.28  (zenon_X101 != zenon_X32)
% 2.08/2.28  (c1_2 (a59) (a30))
% 2.08/2.28  ((a40) != zenon_X52)
% 2.08/2.28  ((a81) != (a122))
% 2.08/2.28  ((a51) != (a47))
% 2.08/2.28  ((a122) != zenon_X18)
% 2.08/2.28  ((a137) != zenon_X103)
% 2.08/2.28  ((a30) != zenon_X35)
% 2.08/2.28  ((a29) != zenon_X6)
% 2.08/2.28  (zenon_X20 != (a104))
% 2.08/2.28  (c4_2 (a51) (a31))
% 2.08/2.28  (c1_1 zenon_X20)
% 2.08/2.28  (c5_2 (a59) (a97))
% 2.08/2.28  (c6_2 zenon_X6 (a130))
% 2.08/2.28  (c8_2 (a18) zenon_X147)
% 2.08/2.28  ((a33) != zenon_X35)
% 2.08/2.28  (zenon_X74 != zenon_X32)
% 2.08/2.28  (-. (c5_2 (a122) zenon_X79))
% 2.08/2.28  ((a41) != zenon_X95)
% 2.08/2.28  (c5_1 (a51))
% 2.08/2.28  (zenon_X26 != zenon_X78)
% 2.08/2.28  ((a68) != zenon_X1)
% 2.08/2.28  ((a130) != zenon_X125)
% 2.08/2.28  (zenon_X11 != zenon_X27)
% 2.08/2.28  (zenon_X35 != (a123))
% 2.08/2.28  (-. (c6_1 (a129)))
% 2.08/2.28  (-. (c2_2 zenon_X7 zenon_X128))
% 2.08/2.28  (c6_2 zenon_X20 (a57))
% 2.08/2.28  ((a114) != (a48))
% 2.08/2.28  (zenon_X27 != (a127))
% 2.08/2.28  (-. (c6_1 zenon_X7))
% 2.08/2.28  (zenon_X35 != (a115))
% 2.08/2.28  (zenon_X30 != (a51))
% 2.08/2.28  (ndr1_1 (a18))
% 2.08/2.28  ((a114) != zenon_X100)
% 2.08/2.28  ((a93) != zenon_X15)
% 2.08/2.28  (-. (c7_2 (a93) (a49)))
% 2.08/2.28  ((a18) != zenon_X40)
% 2.08/2.28  (-. (c5_2 (a18) zenon_X153))
% 2.08/2.28  ((a95) != zenon_X46)
% 2.08/2.28  (zenon_X11 != zenon_X15)
% 2.08/2.28  (c8_2 (a136) zenon_X14)
% 2.08/2.28  (c8_2 (a136) zenon_X53)
% 2.08/2.28  (c8_2 (a117) zenon_X83)
% 2.08/2.28  ((a121) != (a29))
% 2.08/2.28  ((a33) != zenon_X69)
% 2.08/2.28  ((a117) != zenon_X24)
% 2.08/2.28  (-. (c5_2 zenon_X38 (a137)))
% 2.08/2.28  (-. (c7_2 (a93) (a114)))
% 2.08/2.28  (-. (c8_2 zenon_X15 (a33)))
% 2.08/2.28  ((a82) != zenon_X48)
% 2.08/2.28  (zenon_X30 != zenon_X28)
% 2.08/2.28  (zenon_X10 != (a47))
% 2.08/2.28  (-. (c5_2 zenon_X23 zenon_X219))
% 2.08/2.28  (c6_2 (a68) (a130))
% 2.08/2.28  ((a40) != zenon_X104)
% 2.08/2.28  (-. (c8_2 zenon_X15 (a82)))
% 2.08/2.28  ((a97) != zenon_X110)
% 2.08/2.28  (zenon_X42 != zenon_X74)
% 2.08/2.28  (c1_2 zenon_X23 (a114))
% 2.08/2.28  (c7_1 (a81))
% 2.08/2.28  ((a82) != zenon_X42)
% 2.08/2.28  ((a121) != (a68))
% 2.08/2.28  (c1_2 (a29) (a137))
% 2.08/2.28  (c1_2 (a18) (a131))
% 2.08/2.28  (c6_2 (a122) (a58))
% 2.08/2.28  (zenon_X40 != (a121))
% 2.08/2.28  ((a117) != (a47))
% 2.08/2.28  ((a95) != zenon_X220)
% 2.08/2.28  (-. (c5_2 (a59) (a31)))
% 2.08/2.28  ((a95) != zenon_X160)
% 2.08/2.28  (zenon_X193 != (a97))
% 2.08/2.28  ((a49) != zenon_X71)
% 2.08/2.28  (zenon_X11 != (a136))
% 2.08/2.28  ((a63) != zenon_X48)
% 2.08/2.28  (c1_2 (a29) (a130))
% 2.08/2.28  (zenon_X29 != zenon_X147)
% 2.08/2.28  (c5_2 (a59) (a33))
% 2.08/2.28  ((a63) != (a30))
% 2.08/2.28  (c4_2 (a81) (a82))
% 2.08/2.28  (-. (c2_2 (a96) (a63)))
% 2.08/2.28  (c6_2 (a81) (a40))
% 2.08/2.28  ((a127) != (a129))
% 2.08/2.28  ((a127) != zenon_X40)
% 2.08/2.28  ((a40) != zenon_X152)
% 2.08/2.28  (-. (c2_2 (a122) zenon_X77))
% 2.08/2.28  (zenon_X23 != (a122))
% 2.08/2.28  ((a95) != zenon_X34)
% 2.08/2.28  ((a40) != (a115))
% 2.08/2.28  ((a108) != zenon_X133)
% 2.08/2.28  (c1_2 (a129) (a131))
% 2.08/2.28  (c5_2 (a59) (a82))
% 2.08/2.28  (zenon_X36 != (a47))
% 2.08/2.28  (zenon_X3 != zenon_X30)
% 2.08/2.28  ((a57) != zenon_X79)
% 2.08/2.28  (zenon_X6 != zenon_X9)
% 2.08/2.28  ((a131) != zenon_X35)
% 2.08/2.28  ((a137) != zenon_X54)
% 2.08/2.28  ((a65) != (a122))
% 2.08/2.28  (zenon_X104 != zenon_X79)
% 2.08/2.28  ((a31) != zenon_X103)
% 2.08/2.28  ((a63) != zenon_X112)
% 2.08/2.28  (c3_1 zenon_X20)
% 2.08/2.28  ((a121) != (a129))
% 2.08/2.28  (zenon_X36 != zenon_X27)
% 2.08/2.28  ((a49) != zenon_X8)
% 2.08/2.28  ((a82) != zenon_X189)
% 2.08/2.28  (zenon_X20 != zenon_X10)
% 2.08/2.28  (-. (c1_2 (a34) zenon_X34))
% 2.08/2.28  (zenon_X3 != zenon_X28)
% 2.08/2.28  (c6_2 (a68) (a97))
% 2.08/2.28  ((a82) != zenon_X69)
% 2.08/2.28  ((a131) != zenon_X82)
% 2.08/2.28  ((a30) != zenon_X37)
% 2.08/2.28  (zenon_X86 != (a97))
% 2.08/2.28  ((a41) != (a97))
% 2.08/2.28  ((a108) != zenon_X8)
% 2.08/2.28  ((a59) != zenon_X3)
% 2.08/2.28  (zenon_X26 != (a58))
% 2.08/2.28  (-. (c2_0))
% 2.08/2.28  (-. (c3_2 (a51) zenon_X131))
% 2.08/2.28  (c8_2 (a136) (a123))
% 2.08/2.28  (c1_2 (a59) (a95))
% 2.08/2.28  (c7_2 (a59) zenon_X22)
% 2.08/2.28  ((a65) != (a129))
% 2.08/2.28  (-. (ndr1_1 zenon_X40))
% 2.08/2.28  ((a130) != zenon_X64)
% 2.08/2.28  (-. (c6_2 (a93) (a41)))
% 2.08/2.28  ((a108) != zenon_X14)
% 2.08/2.28  (zenon_X20 != zenon_X30)
% 2.08/2.28  ((a34) != zenon_X9)
% 2.08/2.28  ((a114) != zenon_X32)
% 2.08/2.28  ((a137) != (a108))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a58)))
% 2.08/2.28  (-. (c5_2 zenon_X7 (a49)))
% 2.08/2.28  ((a30) != zenon_X66)
% 2.08/2.28  ((a95) != zenon_X196)
% 2.08/2.28  ((a137) != zenon_X29)
% 2.08/2.28  (-. (c3_2 (a29) zenon_X68))
% 2.08/2.28  (c5_2 zenon_X23 (a95))
% 2.08/2.28  (zenon_X23 != zenon_X11)
% 2.08/2.28  (c6_2 (a68) zenon_X21)
% 2.08/2.28  ((a137) != zenon_X211)
% 2.08/2.28  (-. (c2_2 (a59) zenon_X80))
% 2.08/2.28  (zenon_X7 != zenon_X18)
% 2.08/2.28  ((a117) != zenon_X30)
% 2.08/2.28  ((a18) != (a121))
% 2.08/2.28  (-. (c8_2 zenon_X15 (a130)))
% 2.08/2.28  (-. (c3_1 zenon_X30))
% 2.08/2.28  ((a82) != (a57))
% 2.08/2.28  (zenon_X36 != zenon_X40)
% 2.08/2.28  (c7_2 (a59) (a137))
% 2.08/2.28  ((a114) != zenon_X101)
% 2.08/2.28  ((a39) != (a47))
% 2.08/2.28  (-. (c5_2 (a18) zenon_X26))
% 2.08/2.28  ((a30) != zenon_X61)
% 2.08/2.28  (c5_2 (a121) (a49))
% 2.08/2.28  ((a57) != zenon_X16)
% 2.08/2.28  (-. (c3_2 (a127) (a58)))
% 2.08/2.28  ((a93) != zenon_X30)
% 2.08/2.28  ((a34) != zenon_X15)
% 2.08/2.28  (c3_2 (a122) (a57))
% 2.08/2.28  (zenon_X20 != zenon_X38)
% 2.08/2.28  (zenon_X26 != zenon_X147)
% 2.08/2.28  (-. (c6_2 zenon_X27 (a30)))
% 2.08/2.28  (c3_2 (a122) (a33))
% 2.08/2.28  ((a48) != (a49))
% 2.08/2.28  (-. (c5_2 (a93) (a31)))
% 2.08/2.28  (c1_2 zenon_X7 (a57))
% 2.08/2.28  (zenon_X21 != zenon_X95)
% 2.08/2.28  ((a65) != zenon_X18)
% 2.08/2.28  (c1_1 (a121))
% 2.08/2.28  ((a49) != zenon_X100)
% 2.08/2.28  (c1_2 (a39) (a57))
% 2.08/2.28  ((a29) != (a129))
% 2.08/2.28  (zenon_X14 != zenon_X101)
% 2.08/2.28  (zenon_X7 != zenon_X28)
% 2.08/2.28  (-. (c2_2 (a122) (a63)))
% 2.08/2.28  (-. (c6_2 (a39) zenon_X21))
% 2.08/2.28  (-. (c3_2 (a51) zenon_X109))
% 2.08/2.28  (-. (c5_2 (a136) (a58)))
% 2.08/2.28  (zenon_X20 != (a29))
% 2.08/2.28  (-. (c5_2 zenon_X11 (a63)))
% 2.08/2.28  ((a82) != (a97))
% 2.08/2.28  ((a58) != (a97))
% 2.08/2.28  (c6_2 zenon_X23 (a57))
% 2.08/2.28  (zenon_X12 != (a97))
% 2.08/2.28  (-. (c6_2 zenon_X11 (a40)))
% 2.08/2.28  (zenon_X104 != zenon_X147)
% 2.08/2.28  (-. (c4_2 (a18) zenon_X26))
% 2.08/2.28  (-. (c2_2 (a47) (a49)))
% 2.08/2.28  (zenon_X118 != (a115))
% 2.08/2.28  ((a129) != zenon_X28)
% 2.08/2.28  (zenon_X36 != zenon_X7)
% 2.08/2.28  (zenon_X23 != zenon_X3)
% 2.08/2.28  ((a96) != zenon_X7)
% 2.08/2.28  ((a57) != zenon_X84)
% 2.08/2.28  (zenon_X7 != (a104))
% 2.08/2.28  ((a57) != zenon_X57)
% 2.08/2.28  (-. (c8_2 zenon_X15 (a137)))
% 2.08/2.28  (-. (c5_2 (a65) zenon_X147))
% 2.08/2.28  (c1_2 (a121) (a30))
% 2.08/2.28  (-. (c5_2 zenon_X38 (a123)))
% 2.08/2.28  ((a121) != (a136))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a57)))
% 2.08/2.28  ((a31) != (a49))
% 2.08/2.28  ((a114) != (a131))
% 2.08/2.28  (c8_2 (a39) zenon_X14)
% 2.08/2.28  (-. (c8_2 (a127) (a115)))
% 2.08/2.28  ((a82) != zenon_X116)
% 2.08/2.28  (-. (c5_2 (a65) (a49)))
% 2.08/2.28  (-. (c6_2 zenon_X7 zenon_X133))
% 2.08/2.28  (c1_2 zenon_X23 (a57))
% 2.08/2.28  ((a30) != (a131))
% 2.08/2.28  (zenon_X6 != zenon_X30)
% 2.08/2.28  ((a39) != zenon_X24)
% 2.08/2.28  ((a95) != zenon_X33)
% 2.08/2.28  (zenon_X23 != (a47))
% 2.08/2.28  (zenon_X82 != zenon_X147)
% 2.08/2.28  (-. (c5_2 (a18) zenon_X79))
% 2.08/2.28  ((a121) != (a81))
% 2.08/2.28  ((a122) != zenon_X17)
% 2.08/2.28  ((a30) != zenon_X100)
% 2.08/2.28  (c4_2 (a65) (a115))
% 2.08/2.28  (-. (c4_2 (a51) zenon_X110))
% 2.08/2.28  (c1_2 zenon_X7 (a95))
% 2.08/2.28  (-. (c8_2 (a34) zenon_X35))
% 2.08/2.28  (c8_2 (a29) (a123))
% 2.08/2.28  (-. (c3_1 zenon_X15))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a33)))
% 2.08/2.28  (-. (c6_2 (a18) (a82)))
% 2.08/2.28  (c6_2 (a96) (a137))
% 2.08/2.28  (-. (c5_2 (a96) (a97)))
% 2.08/2.28  (-. (c2_2 (a136) zenon_X62))
% 2.08/2.28  (-. (c5_2 (a39) (a115)))
% 2.08/2.28  (-. (c5_2 zenon_X38 (a95)))
% 2.08/2.28  ((a63) != zenon_X39)
% 2.08/2.28  ((a137) != zenon_X111)
% 2.08/2.28  (-. (c6_1 zenon_X6))
% 2.08/2.28  (c1_2 (a65) (a114))
% 2.08/2.28  ((a29) != zenon_X28)
% 2.08/2.28  (c1_2 (a18) (a114))
% 2.08/2.28  (-. (c5_1 (a104)))
% 2.08/2.28  (zenon_X3 != zenon_X15)
% 2.08/2.28  (-. (c6_1 zenon_X20))
% 2.08/2.28  ((a58) != zenon_X142)
% 2.08/2.28  ((a137) != zenon_X87)
% 2.08/2.28  (ndr1_1 zenon_X23)
% 2.08/2.28  (c8_2 (a29) zenon_X42)
% 2.08/2.28  (zenon_X3 != (a121))
% 2.08/2.28  ((a68) != (a39))
% 2.08/2.28  ((a95) != zenon_X87)
% 2.08/2.28  (c1_2 (a59) (a114))
% 2.08/2.28  ((a30) != zenon_X114)
% 2.08/2.28  ((a97) != zenon_X14)
% 2.08/2.28  (c6_2 (a121) (a137))
% 2.08/2.28  (c1_2 (a18) (a82))
% 2.08/2.28  (-. (c3_2 (a51) (a58)))
% 2.08/2.28  (c5_2 (a59) (a57))
% 2.08/2.28  (c3_1 (a117))
% 2.08/2.28  (-. (c5_2 (a117) (a63)))
% 2.08/2.28  (c4_1 zenon_X20)
% 2.08/2.28  (zenon_X36 != zenon_X15)
% 2.08/2.28  ((a115) != zenon_X22)
% 2.08/2.28  (zenon_X20 != (a51))
% 2.08/2.28  ((a136) != zenon_X15)
% 2.08/2.28  ((a63) != zenon_X187)
% 2.08/2.28  (-. (c5_2 zenon_X38 (a31)))
% 2.08/2.28  (c6_2 (a51) (a57))
% 2.08/2.28  ((a59) != zenon_X20)
% 2.08/2.28  (c6_2 zenon_X23 (a137))
% 2.08/2.28  (-. (c3_2 zenon_X7 (a58)))
% 2.08/2.28  (c6_2 (a68) zenon_X87)
% 2.08/2.28  (-. (c6_2 (a29) zenon_X37))
% 2.08/2.28  (c6_2 (a65) (a95))
% 2.08/2.28  ((a108) != zenon_X123)
% 2.08/2.28  ((a65) != zenon_X1)
% 2.08/2.28  (c1_2 (a122) (a33))
% 2.08/2.28  ((a57) != zenon_X60)
% 2.08/2.28  (c6_2 (a96) (a58))
% 2.08/2.28  (c8_2 (a47) (a49))
% 2.08/2.28  ((a40) != zenon_X133)
% 2.08/2.28  (zenon_X42 != (a123))
% 2.08/2.28  ((a95) != zenon_X16)
% 2.08/2.28  (-. (c5_2 (a39) (a97)))
% 2.08/2.28  ((a121) != zenon_X27)
% 2.08/2.28  ((a121) != (a117))
% 2.08/2.28  ((a117) != zenon_X18)
% 2.08/2.28  ((a137) != zenon_X110)
% 2.08/2.28  (zenon_X14 != zenon_X72)
% 2.08/2.28  (zenon_X10 != (a59))
% 2.08/2.28  ((a41) != zenon_X147)
% 2.08/2.28  ((a122) != (a129))
% 2.08/2.28  (-. (c5_2 zenon_X7 (a30)))
% 2.08/2.28  ((a117) != (a39))
% 2.08/2.28  (c7_2 (a136) (a82))
% 2.08/2.28  (zenon_X36 != (a104))
% 2.08/2.28  (zenon_X40 != zenon_X24)
% 2.08/2.28  ((a95) != zenon_X29)
% 2.08/2.28  (zenon_X20 != zenon_X36)
% 2.08/2.28  ((a117) != (a122))
% 2.08/2.28  (c6_2 (a96) (a130))
% 2.08/2.28  ((a82) != zenon_X75)
% 2.08/2.28  ((a137) != (a33))
% 2.08/2.28  (-. (c5_2 (a96) (a63)))
% 2.08/2.28  (zenon_X38 != zenon_X3)
% 2.08/2.28  (-. (c5_2 zenon_X38 (a97)))
% 2.08/2.28  ((a108) != (a41))
% 2.08/2.28  ((a114) != zenon_X35)
% 2.08/2.28  ((a130) != zenon_X95)
% 2.08/2.28  ((a81) != zenon_X15)
% 2.08/2.28  (-. (c3_2 (a122) (a123)))
% 2.08/2.28  ((a49) != zenon_X83)
% 2.08/2.28  ((a65) != zenon_X3)
% 2.08/2.28  ((a96) != zenon_X3)
% 2.08/2.28  ((a40) != (a33))
% 2.08/2.28  (c1_2 (a96) (a40))
% 2.08/2.28  ((a58) != (a41))
% 2.08/2.28  ((a58) != zenon_X86)
% 2.08/2.28  (zenon_X14 != zenon_X71)
% 2.08/2.28  ((a57) != zenon_X56)
% 2.08/2.28  (c8_2 zenon_X38 (a115))
% 2.08/2.28  (-. (c6_2 zenon_X15 (a63)))
% 2.08/2.28  (-. (c3_2 zenon_X6 zenon_X166))
% 2.08/2.28  ((a63) != (a97))
% 2.08/2.28  (-. (c5_2 (a68) (a63)))
% 2.08/2.28  (-. (c4_2 zenon_X36 zenon_X192))
% 2.08/2.28  ((a136) != zenon_X24)
% 2.08/2.28  (-. (c6_2 (a29) (a95)))
% 2.08/2.28  (zenon_X6 != zenon_X11)
% 2.08/2.28  ((a96) != (a29))
% 2.08/2.28  (-. (c6_2 (a129) (a130)))
% 2.08/2.28  (-. (c5_2 (a47) (a58)))
% 2.08/2.28  (c6_2 (a129) (a58))
% 2.08/2.28  (zenon_X30 != (a121))
% 2.08/2.28  ((a31) != zenon_X8)
% 2.08/2.28  (zenon_X36 != zenon_X38)
% 2.08/2.28  ((a130) != zenon_X108)
% 2.08/2.28  (c1_2 (a59) (a131))
% 2.08/2.28  (zenon_X6 != zenon_X18)
% 2.08/2.28  (-. (c4_1 (a59)))
% 2.08/2.28  ((a121) != (a96))
% 2.08/2.28  (-. (c3_2 (a117) (a58)))
% 2.08/2.28  (c7_2 (a136) (a131))
% 2.08/2.28  ((a63) != zenon_X37)
% 2.08/2.28  (-. (c8_2 (a59) zenon_X151))
% 2.08/2.28  (zenon_X53 != zenon_X71)
% 2.08/2.28  (zenon_X26 != (a31))
% 2.08/2.28  (zenon_X104 != zenon_X153)
% 2.08/2.28  (zenon_X23 != zenon_X18)
% 2.08/2.28  (c4_1 zenon_X9)
% 2.08/2.28  (c6_2 zenon_X11 (a57))
% 2.08/2.28  ((a137) != zenon_X142)
% 2.08/2.28  ((a58) != zenon_X29)
% 2.08/2.28  (c5_2 (a127) (a95))
% 2.08/2.28  (-. (c2_2 (a127) zenon_X85))
% 2.08/2.28  (c8_2 zenon_X11 (a115))
% 2.08/2.28  ((a81) != zenon_X9)
% 2.08/2.28  (-. (c6_2 zenon_X7 (a41)))
% 2.08/2.28  ((a65) != (a104))
% 2.08/2.28  (zenon_X26 != zenon_X82)
% 2.08/2.28  (c4_2 (a121) (a63))
% 2.08/2.28  ((a40) != zenon_X55)
% 2.08/2.28  (-. (c8_2 (a39) zenon_X101))
% 2.08/2.28  ((a65) != zenon_X27)
% 2.08/2.28  (c7_2 (a59) (a40))
% 2.08/2.28  ((a121) != zenon_X15)
% 2.08/2.28  ((a63) != (a48))
% 2.08/2.28  ((a81) != zenon_X6)
% 2.08/2.28  (zenon_X22 != (a137))
% 2.08/2.28  (c1_1 zenon_X6)
% 2.08/2.28  (ndr1_1 (a59))
% 2.08/2.28  (zenon_X23 != (a129))
% 2.08/2.28  (zenon_X20 != zenon_X15)
% 2.08/2.28  (zenon_X21 != (a95))
% 2.08/2.28  (c6_2 (a122) (a30))
% 2.08/2.28  ((a30) != (a123))
% 2.08/2.28  (c3_2 (a117) (a57))
% 2.08/2.28  (zenon_X33 != (a115))
% 2.08/2.28  ((a30) != zenon_X189)
% 2.08/2.28  ((a57) != (a108))
% 2.08/2.28  (c6_2 zenon_X11 (a95))
% 2.08/2.28  (-. (c6_2 (a47) (a30)))
% 2.08/2.28  (c6_2 (a68) zenon_X37)
% 2.08/2.28  (c6_2 zenon_X27 (a137))
% 2.08/2.28  ((a137) != zenon_X153)
% 2.08/2.28  (c5_2 (a47) (a40))
% 2.08/2.28  (-. (c1_1 (a93)))
% 2.08/2.28  (zenon_X78 != (a115))
% 2.08/2.28  ((a40) != (a97))
% 2.08/2.28  ((a58) != zenon_X12)
% 2.08/2.28  ((a40) != zenon_X8)
% 2.08/2.28  (-. (c6_2 zenon_X15 zenon_X16))
% 2.08/2.28  ((a30) != zenon_X220)
% 2.08/2.28  (-. (c7_2 (a121) (a108)))
% 2.08/2.28  (-. (c7_2 (a93) zenon_X83))
% 2.08/2.28  ((a95) != zenon_X123)
% 2.08/2.28  (c1_2 (a39) zenon_X73)
% 2.08/2.28  ((a65) != zenon_X38)
% 2.08/2.28  ((a33) != zenon_X82)
% 2.08/2.28  (c4_2 (a122) (a33))
% 2.08/2.28  ((a82) != zenon_X197)
% 2.08/2.28  ((a115) != zenon_X111)
% 2.08/2.28  (zenon_X42 != zenon_X33)
% 2.08/2.28  ((a123) != (a97))
% 2.08/2.28  ((a130) != zenon_X86)
% 2.08/2.28  (-. (c4_2 (a93) (a30)))
% 2.08/2.28  ((a123) != zenon_X73)
% 2.08/2.28  ((a130) != zenon_X131)
% 2.08/2.28  (zenon_X53 != zenon_X42)
% 2.08/2.28  ((a82) != zenon_X12)
% 2.08/2.28  ((a30) != zenon_X39)
% 2.08/2.28  ((a18) != zenon_X9)
% 2.08/2.28  ((a31) != zenon_X78)
% 2.08/2.28  ((a18) != zenon_X28)
% 2.08/2.28  ((a31) != zenon_X86)
% 2.08/2.28  (zenon_X53 != (a115))
% 2.08/2.28  (c6_2 (a68) zenon_X12)
% 2.08/2.28  ((a130) != zenon_X68)
% 2.08/2.28  (zenon_X23 != (a18))
% 2.08/2.28  (-. (c5_2 (a129) (a97)))
% 2.08/2.28  ((a108) != zenon_X124)
% 2.08/2.28  ((a114) != (a40))
% 2.08/2.28  ((a95) != zenon_X153)
% 2.08/2.28  ((a137) != zenon_X124)
% 2.08/2.28  ((a30) != zenon_X62)
% 2.08/2.28  ((a63) != zenon_X35)
% 2.08/2.28  (c8_2 (a29) zenon_X32)
% 2.08/2.28  (-. (c6_1 zenon_X23))
% 2.08/2.28  ((a95) != zenon_X13)
% 2.08/2.28  (-. (c2_2 (a129) (a63)))
% 2.08/2.28  (c3_1 (a129))
% 2.08/2.28  (zenon_X18 != zenon_X9)
% 2.08/2.28  (-. (c3_2 (a65) zenon_X94))
% 2.08/2.28  ((a40) != zenon_X89)
% 2.08/2.28  (-. (c6_1 (a68)))
% 2.08/2.28  (c4_2 (a65) (a49))
% 2.08/2.28  (-. (c5_2 zenon_X7 (a63)))
% 2.08/2.28  (zenon_X7 != (a51))
% 2.08/2.28  (-. (c5_2 zenon_X38 zenon_X147))
% 2.08/2.28  (c1_1 (a117))
% 2.08/2.28  ((a137) != zenon_X63)
% 2.08/2.28  ((a130) != zenon_X65)
% 2.08/2.28  (c4_2 (a96) (a63))
% 2.08/2.28  ((a33) != zenon_X147)
% 2.08/2.28  (c6_2 zenon_X7 (a33))
% 2.08/2.28  (zenon_X35 != zenon_X14)
% 2.08/2.28  (-. (c2_1 zenon_X15))
% 2.08/2.28  ((a123) != zenon_X82)
% 2.08/2.28  ((a95) != zenon_X152)
% 2.08/2.28  (-. (c5_2 zenon_X36 (a63)))
% 2.08/2.28  (zenon_X2 != (a115))
% 2.08/2.28  (zenon_X23 != (a117))
% 2.08/2.28  (c1_2 zenon_X7 (a108))
% 2.08/2.28  (c6_1 (a59))
% 2.08/2.28  ((a31) != (a97))
% 2.08/2.28  ((a41) != (a115))
% 2.08/2.28  ((a136) != (a122))
% 2.08/2.28  ((a33) != zenon_X45)
% 2.08/2.28  (c7_2 (a136) zenon_X71)
% 2.08/2.28  (-. (c5_2 (a136) (a97)))
% 2.08/2.28  (c1_2 (a59) (a82))
% 2.08/2.28  (c3_1 zenon_X27)
% 2.08/2.28  (-. (c6_2 zenon_X11 (a130)))
% 2.08/2.28  ((a30) != zenon_X134)
% 2.08/2.28  (c6_2 (a68) (a108))
% 2.08/2.28  (c1_2 (a29) (a31))
% 2.08/2.28  (zenon_X20 != zenon_X40)
% 2.08/2.28  ((a93) != (a104))
% 2.08/2.28  ((a136) != zenon_X36)
% 2.08/2.28  (c7_2 (a136) zenon_X42)
% 2.08/2.28  (-. (c2_2 (a121) (a63)))
% 2.08/2.28  (c3_2 (a136) (a137))
% 2.08/2.28  (c8_2 (a47) zenon_X35)
% 2.08/2.28  ((a81) != (a136))
% 2.08/2.28  ((a127) != zenon_X6)
% 2.08/2.28  (c1_2 (a121) (a123))
% 2.08/2.28  ((a129) != (a47))
% 2.08/2.28  (-. (c5_2 zenon_X11 (a57)))
% 2.08/2.28  (c6_2 (a129) (a108))
% 2.08/2.28  (-. (c5_2 (a122) (a130)))
% 2.08/2.28  (zenon_X9 != (a104))
% 2.08/2.28  ((a30) != zenon_X125)
% 2.08/2.28  (zenon_X27 != (a104))
% 2.08/2.28  ((a30) != zenon_X87)
% 2.08/2.28  (-. (c4_2 (a93) (a95)))
% 2.08/2.28  (-. (c7_2 (a47) (a108)))
% 2.08/2.28  ((a40) != zenon_X12)
% 2.08/2.28  (zenon_X7 != (a129))
% 2.08/2.28  (zenon_X27 != (a68))
% 2.08/2.28  ((a127) != zenon_X24)
% 2.08/2.28  ((a49) != zenon_X70)
% 2.08/2.28  (c4_2 (a65) zenon_X82)
% 2.08/2.28  ((a63) != zenon_X86)
% 2.08/2.28  ((a137) != zenon_X91)
% 2.08/2.28  ((a58) != (a130))
% 2.08/2.28  ((a33) != zenon_X64)
% 2.08/2.28  (zenon_X22 != zenon_X147)
% 2.08/2.28  ((a39) != zenon_X30)
% 2.08/2.28  (c1_2 (a39) zenon_X70)
% 2.08/2.28  (-. (c6_1 (a96)))
% 2.08/2.28  ((a40) != zenon_X56)
% 2.08/2.28  ((a114) != zenon_X34)
% 2.08/2.28  (-. (c2_2 (a129) zenon_X76))
% 2.08/2.28  ((a34) != zenon_X24)
% 2.08/2.28  (zenon_X36 != (a39))
% 2.08/2.28  (zenon_X11 != zenon_X24)
% 2.08/2.28  ((a137) != zenon_X12)
% 2.08/2.28  ((a49) != zenon_X101)
% 2.08/2.28  (-. (c2_2 (a39) zenon_X60))
% 2.08/2.28  (-. (c6_2 (a39) zenon_X87))
% 2.08/2.28  ((a65) != (a29))
% 2.08/2.28  ((a31) != zenon_X104)
% 2.08/2.28  ((a136) != (a127))
% 2.08/2.28  (-. (c6_2 zenon_X23 zenon_X123))
% 2.08/2.28  (c5_2 (a29) (a82))
% 2.08/2.28  (c8_2 (a93) zenon_X32)
% 2.08/2.28  (c8_2 (a93) zenon_X35)
% 2.08/2.28  (-. (c5_2 (a18) (a30)))
% 2.08/2.28  ((a95) != zenon_X112)
% 2.08/2.28  (c5_2 zenon_X27 (a95))
% 2.08/2.28  ((a108) != zenon_X16)
% 2.08/2.28  (c5_2 (a65) (a33))
% 2.08/2.28  (-. (c3_2 zenon_X36 (a58)))
% 2.08/2.28  (-. (c6_2 zenon_X27 (a40)))
% 2.08/2.28  ((a117) != (a51))
% 2.08/2.28  (-. (c5_2 (a51) (a108)))
% 2.08/2.28  (zenon_X6 != (a47))
% 2.08/2.28  (zenon_X83 != zenon_X32)
% 2.08/2.28  ((a82) != zenon_X185)
% 2.08/2.28  ((a123) != zenon_X147)
% 2.08/2.28  ((a49) != zenon_X32)
% 2.08/2.28  (-. (c3_2 zenon_X20 zenon_X155))
% 2.08/2.28  (c1_2 zenon_X36 (a57))
% 2.08/2.28  ((a137) != zenon_X66)
% 2.08/2.28  (zenon_X38 != zenon_X30)
% 2.08/2.28  (-. (c2_1 zenon_X3))
% 2.08/2.28  (zenon_X15 != zenon_X28)
% 2.08/2.28  (zenon_X29 != (a115))
% 2.08/2.28  (c6_2 zenon_X20 (a95))
% 2.08/2.28  (c8_2 (a93) (a108))
% 2.08/2.28  ((a117) != zenon_X10)
% 2.08/2.28  (-. (c7_1 zenon_X24))
% 2.08/2.28  (c6_2 (a68) zenon_X16)
% 2.08/2.28  (zenon_X23 != zenon_X40)
% 2.08/2.28  ((a136) != zenon_X38)
% 2.08/2.28  (-. (c2_2 (a93) zenon_X102))
% 2.08/2.28  ((a82) != zenon_X158)
% 2.08/2.28  (c5_2 (a47) (a82))
% 2.08/2.28  ((a97) != zenon_X79)
% 2.08/2.28  (-. (c5_2 (a51) zenon_X143))
% 2.08/2.28  (-. (c4_2 (a18) zenon_X22))
% 2.08/2.28  (-. (c2_2 (a65) zenon_X93))
% 2.08/2.28  ((a57) != zenon_X94)
% 2.08/2.28  ((a57) != zenon_X165)
% 2.08/2.28  (c6_2 zenon_X7 (a108))
% 2.08/2.28  ((a47) != zenon_X18)
% 2.08/2.28  (-. (c6_2 (a47) (a82)))
% 2.08/2.28  ((a57) != zenon_X48)
% 2.08/2.28  (zenon_X14 != (a123))
% 2.08/2.28  (c4_2 (a39) (a30))
% 2.08/2.28  (c3_2 (a39) (a40))
% 2.08/2.28  (c5_2 (a65) (a137))
% 2.08/2.28  (-. (c6_1 (a136)))
% 2.08/2.28  ((a51) != zenon_X36)
% 2.08/2.28  (-. (c3_2 (a129) (a58)))
% 2.08/2.28  ((a59) != (a81))
% 2.08/2.28  (c6_2 (a68) zenon_X95)
% 2.08/2.28  (zenon_X10 != (a65))
% 2.08/2.28  (c5_2 (a29) (a95))
% 2.08/2.28  ((a82) != zenon_X54)
% 2.08/2.28  ((a82) != zenon_X152)
% 2.08/2.28  (-. (c4_1 zenon_X24))
% 2.08/2.28  (zenon_X42 != (a115))
% 2.08/2.28  (c1_2 (a96) (a95))
% 2.08/2.28  (-. (c6_2 (a93) (a95)))
% 2.08/2.28  (c6_2 (a136) (a58))
% 2.08/2.28  (c8_2 (a104) (a82))
% 2.08/2.28  (zenon_X10 != (a129))
% 2.08/2.28  (zenon_X20 != (a39))
% 2.08/2.28  ((a58) != zenon_X39)
% 2.08/2.28  ((a108) != (a48))
% 2.08/2.28  ((a122) != (a34))
% 2.08/2.28  (-. (c5_2 (a18) zenon_X82))
% 2.08/2.28  (c1_2 (a121) (a115))
% 2.08/2.28  ((a40) != zenon_X39)
% 2.08/2.28  (-. (c8_2 (a59) zenon_X29))
% 2.08/2.28  (-. (c5_2 (a59) zenon_X22))
% 2.08/2.28  ((a114) != zenon_X74)
% 2.08/2.28  (zenon_X26 != zenon_X86)
% 2.08/2.28  (-. (c4_2 (a29) zenon_X49))
% 2.08/2.28  ((a97) != zenon_X39)
% 2.08/2.28  (zenon_X27 != (a122))
% 2.08/2.28  (c4_2 (a129) (a63))
% 2.08/2.28  ((a95) != zenon_X49)
% 2.08/2.28  ((a130) != zenon_X134)
% 2.08/2.28  (c8_2 (a129) (a97))
% 2.08/2.28  ((a121) != zenon_X10)
% 2.08/2.28  (c8_2 (a29) zenon_X35)
% 2.08/2.28  (zenon_X132 != (a115))
% 2.08/2.28  (c3_1 zenon_X7)
% 2.08/2.28  ((a59) != zenon_X11)
% 2.08/2.28  (zenon_X23 != (a96))
% 2.08/2.28  (c1_2 (a129) (a63))
% 2.08/2.28  (-. (c6_2 zenon_X7 zenon_X16))
% 2.08/2.28  ((a127) != zenon_X5)
% 2.08/2.28  (zenon_X11 != (a39))
% 2.08/2.28  ((a137) != zenon_X117)
% 2.08/2.28  (zenon_X11 != zenon_X28)
% 2.08/2.28  ((a40) != zenon_X88)
% 2.08/2.29  (c6_2 (a121) (a82))
% 2.08/2.29  (c8_1 (a122))
% 2.08/2.29  ((a82) != zenon_X49)
% 2.08/2.29  ((a137) != zenon_X37)
% 2.08/2.29  (zenon_X10 != (a122))
% 2.08/2.29  ((a29) != (a47))
% 2.08/2.29  (c8_2 zenon_X23 zenon_X132)
% 2.08/2.29  (-. (c5_2 (a121) (a108)))
% 2.08/2.29  (-. (c6_2 (a29) (a40)))
% 2.08/2.29  ((a29) != zenon_X24)
% 2.08/2.29  ((a57) != (a48))
% 2.08/2.29  (c1_2 (a59) (a63))
% 2.08/2.29  (c1_2 (a59) (a58))
% 2.08/2.29  (-. (c5_2 zenon_X11 zenon_X79))
% 2.08/2.29  (zenon_X36 != zenon_X23)
% 2.08/2.29  ((a51) != zenon_X9)
% 2.08/2.29  ((a122) != zenon_X5)
% 2.08/2.29  (zenon_X11 != (a117))
% 2.08/2.29  ((a29) != zenon_X18)
% 2.08/2.29  ((a96) != zenon_X28)
% 2.08/2.29  (-. (c6_1 (a47)))
% 2.08/2.29  (-. (c6_2 zenon_X27 (a108)))
% 2.08/2.29  (c6_2 (a136) (a82))
% 2.08/2.29  (c5_2 (a47) (a137))
% 2.08/2.29  (c8_2 (a129) zenon_X42)
% 2.08/2.29  (-. (c8_1 zenon_X5))
% 2.08/2.29  (-. (c6_2 zenon_X27 (a130)))
% 2.08/2.29  (c5_1 (a65))
% 2.08/2.29  ((a30) != zenon_X50)
% 2.08/2.29  ((a81) != zenon_X10)
% 2.08/2.29  ((a51) != zenon_X27)
% 2.08/2.29  (c3_2 (a129) (a30))
% 2.08/2.29  (zenon_X151 != zenon_X26)
% 2.08/2.29  ((a136) != zenon_X10)
% 2.08/2.29  ((a68) != zenon_X3)
% 2.08/2.29  (-. (c1_1 (a29)))
% 2.08/2.29  (-. (c5_2 (a68) (a58)))
% 2.08/2.29  (zenon_X10 != zenon_X11)
% 2.08/2.29  (-. (c6_2 zenon_X15 (a40)))
% 2.08/2.29  (zenon_X22 != zenon_X39)
% 2.08/2.29  ((a137) != zenon_X79)
% 2.08/2.29  ((a129) != zenon_X38)
% 2.08/2.29  (c5_2 (a29) (a114))
% 2.08/2.29  (c8_2 (a129) (a123))
% 2.08/2.29  (-. (c5_1 zenon_X1))
% 2.08/2.29  (c5_2 (a51) (a95))
% 2.08/2.29  (c1_2 (a93) (a114))
% 2.08/2.29  (zenon_X20 != zenon_X6)
% 2.08/2.29  ((a33) != zenon_X145)
% 2.08/2.29  (c1_2 (a121) (a49))
% 2.08/2.29  (c1_2 zenon_X27 (a58))
% 2.08/2.29  (-. (c4_1 zenon_X11))
% 2.08/2.29  (c7_2 (a136) zenon_X83)
% 2.08/2.29  (-. (c3_2 (a121) (a58)))
% 2.08/2.29  (-. (c6_2 (a104) (a57)))
% 2.08/2.29  (-. (c8_2 (a39) zenon_X74))
% 2.08/2.29  ((a57) != zenon_X50)
% 2.08/2.29  ((a97) != zenon_X2)
% 2.08/2.29  ((a30) != zenon_X48)
% 2.08/2.29  (zenon_X42 != zenon_X71)
% 2.08/2.29  (c5_2 (a121) (a30))
% 2.08/2.29  ((a65) != zenon_X15)
% 2.08/2.29  ((a121) != (a39))
% 2.08/2.29  (c8_2 (a18) zenon_X26)
% 2.08/2.29  (-. (c5_2 zenon_X36 (a58)))
% 2.08/2.29  ((a137) != zenon_X16)
% 2.08/2.29  ((a97) != zenon_X72)
% 2.08/2.29  ((a117) != zenon_X15)
% 2.08/2.29  (zenon_X72 != (a130))
% 2.08/2.29  (zenon_X71 != (a115))
% 2.08/2.29  (-. (c5_2 (a81) (a63)))
% 2.08/2.29  ((a108) != (a130))
% 2.08/2.29  (c6_2 zenon_X23 (a130))
% 2.08/2.29  (-. (c2_1 (a93)))
% 2.08/2.29  (zenon_X20 != (a117))
% 2.08/2.29  (zenon_X23 != (a136))
% 2.08/2.29  (c1_2 (a59) (a130))
% 2.08/2.29  (c3_2 (a81) (a30))
% 2.08/2.29  (c1_1 (a34))
% 2.08/2.29  (-. (c5_2 (a122) (a95)))
% 2.08/2.29  (c2_1 (a96))
% 2.08/2.29  ((a131) != zenon_X34)
% 2.08/2.29  ((a130) != zenon_X50)
% 2.08/2.29  (c6_2 (a127) (a82))
% 2.08/2.29  ((a30) != zenon_X160)
% 2.08/2.29  ((a57) != zenon_X22)
% 2.08/2.29  ((a33) != zenon_X125)
% 2.08/2.29  ((a82) != zenon_X35)
% 2.08/2.29  (zenon_X72 != (a115))
% 2.08/2.29  ((a114) != (a115))
% 2.08/2.29  ((a30) != zenon_X147)
% 2.08/2.29  ((a137) != zenon_X96)
% 2.08/2.29  (c5_2 (a96) (a95))
% 2.08/2.29  ((a137) != (a41))
% 2.08/2.29  (c7_2 (a136) zenon_X72)
% 2.08/2.29  ((a57) != zenon_X51)
% 2.08/2.29  ((a49) != zenon_X82)
% 2.08/2.29  ((a30) != zenon_X97)
% 2.08/2.29  ((a49) != zenon_X160)
% 2.08/2.29  (c3_2 (a129) (a130))
% 2.08/2.29  ((a114) != zenon_X72)
% 2.08/2.29  (c1_2 (a136) (a63))
% 2.08/2.29  ((a122) != zenon_X38)
% 2.08/2.29  ((a114) != zenon_X86)
% 2.08/2.29  (-. (c5_2 zenon_X36 zenon_X222))
% 2.08/2.29  (c1_2 (a129) (a82))
% 2.08/2.29  ((a63) != zenon_X13)
% 2.08/2.29  (c7_2 (a136) zenon_X70)
% 2.08/2.29  (-. (c3_2 zenon_X38 (a58)))
% 2.08/2.29  (c7_2 (a39) (a40))
% 2.08/2.29  (-. (c5_2 (a129) (a95)))
% 2.08/2.29  (-. (c5_2 zenon_X11 (a30)))
% 2.08/2.29  (c8_2 (a93) (a31))
% 2.08/2.29  ((a82) != zenon_X21)
% 2.08/2.29  (c1_2 (a18) (a137))
% 2.08/2.29  (-. (c2_1 zenon_X9))
% 2.08/2.29  (c8_2 (a122) zenon_X53)
% 2.08/2.29  ((a51) != zenon_X1)
% 2.08/2.29  (zenon_X104 != (a49))
% 2.08/2.29  (zenon_X3 != (a104))
% 2.08/2.29  (c1_2 (a65) (a58))
% 2.08/2.29  ((a95) != zenon_X104)
% 2.08/2.29  (-. (c5_2 zenon_X20 (a97)))
% 2.08/2.29  (c6_2 (a59) (a95))
% 2.08/2.29  ((a40) != zenon_X29)
% 2.08/2.29  ((a59) != (a65))
% 2.08/2.29  ((a82) != (a137))
% 2.08/2.29  (zenon_X7 != (a122))
% 2.08/2.29  ((a82) != zenon_X82)
% 2.08/2.29  ((a95) != zenon_X219)
% 2.08/2.29  ((a81) != (a93))
% 2.08/2.29  ((a123) != zenon_X70)
% 2.08/2.29  ((a131) != (a123))
% 2.08/2.29  ((a121) != (a122))
% 2.08/2.29  (ndr1_1 (a51))
% 2.08/2.29  (c6_2 zenon_X6 (a57))
% 2.08/2.29  (-. (c3_2 (a65) zenon_X99))
% 2.08/2.29  ((a68) != (a93))
% 2.08/2.29  ((a114) != zenon_X8)
% 2.08/2.29  ((a63) != zenon_X110)
% 2.08/2.29  (c1_2 (a18) (a31))
% 2.08/2.29  (zenon_X11 != zenon_X30)
% 2.08/2.29  (c4_2 (a51) (a137))
% 2.08/2.29  (c6_2 (a136) (a40))
% 2.08/2.29  ((a58) != zenon_X79)
% 2.08/2.29  (c5_2 (a121) (a95))
% 2.08/2.29  (c1_2 (a51) (a123))
% 2.08/2.29  ((a57) != zenon_X99)
% 2.08/2.29  (-. (c6_2 (a93) (a82)))
% 2.08/2.29  ((a95) != zenon_X119)
% 2.08/2.29  ((a97) != zenon_X104)
% 2.08/2.29  ((a93) != zenon_X40)
% 2.08/2.29  (c3_2 (a93) (a30))
% 2.08/2.29  (-. (c1_2 (a122) (a123)))
% 2.08/2.29  ((a48) != (a130))
% 2.08/2.29  ((a108) != zenon_X142)
% 2.08/2.29  (ndr1_1 zenon_X27)
% 2.08/2.29  (zenon_X38 != zenon_X10)
% 2.08/2.29  (zenon_X86 != (a115))
% 2.08/2.29  (zenon_X42 != zenon_X70)
% 2.08/2.29  ((a40) != zenon_X91)
% 2.08/2.29  (-. (c5_2 zenon_X27 (a58)))
% 2.08/2.29  ((a59) != zenon_X18)
% 2.08/2.29  ((a18) != (a127))
% 2.08/2.29  (-. (c4_1 zenon_X15))
% 2.08/2.29  ((a136) != (a129))
% 2.08/2.29  (c7_0)
% 2.08/2.29  ((a127) != zenon_X15)
% 2.08/2.29  (-. (c2_1 zenon_X40))
% 2.08/2.29  ((a40) != zenon_X16)
% 2.08/2.29  (c4_2 (a29) (a57))
% 2.08/2.29  (c3_2 (a122) (a30))
% 2.08/2.29  (c7_1 (a122))
% 2.08/2.29  ((a57) != zenon_X197)
% 2.08/2.29  (zenon_X153 != (a49))
% 2.08/2.29  ((a41) != zenon_X82)
% 2.08/2.29  (c2_2 (a29) (a30))
% 2.08/2.29  (zenon_X6 != (a34))
% 2.08/2.29  ((a123) != zenon_X83)
% 2.08/2.29  ((a30) != zenon_X80)
% 2.08/2.29  ((a57) != zenon_X26)
% 2.08/2.29  ((a108) != zenon_X91)
% 2.08/2.29  (zenon_X7 != (a47))
% 2.08/2.29  (zenon_X6 != zenon_X3)
% 2.08/2.29  (-. (c5_2 (a117) (a137)))
% 2.08/2.29  (c8_2 (a18) zenon_X151)
% 2.08/2.29  ((a40) != zenon_X161)
% 2.08/2.29  ((a96) != (a129))
% 2.08/2.29  ((a30) != zenon_X136)
% 2.08/2.29  ((a30) != zenon_X110)
% 2.08/2.29  ((a30) != zenon_X143)
% 2.08/2.29  (c1_1 (a59))
% 2.08/2.29  ((a137) != zenon_X195)
% 2.08/2.29  ((a63) != zenon_X21)
% 2.08/2.29  (-. (c3_2 (a96) (a115)))
% 2.08/2.29  (c6_2 (a29) (a57))
% 2.08/2.29  ((a108) != zenon_X95)
% 2.08/2.29  ((a68) != zenon_X0)
% 2.08/2.29  ((a122) != zenon_X30)
% 2.08/2.29  (c6_2 (a68) (a95))
% 2.08/2.29  ((a114) != zenon_X219)
% 2.08/2.29  (c1_1 zenon_X7)
% 2.08/2.29  (zenon_X39 != zenon_X153)
% 2.08/2.29  (-. (c6_2 (a93) (a108)))
% 2.08/2.29  (c6_2 (a121) (a108))
% 2.08/2.29  ((a117) != zenon_X17)
% 2.08/2.29  (-. (c1_1 zenon_X11))
% 2.08/2.29  (-. (c3_2 zenon_X6 zenon_X168))
% 2.08/2.29  ((a40) != zenon_X69)
% 2.08/2.29  (c8_1 (a96))
% 2.08/2.29  ((a30) != zenon_X67)
% 2.08/2.29  (zenon_X21 != zenon_X189)
% 2.08/2.29  ((a137) != (a49))
% 2.08/2.29  ((a40) != zenon_X64)
% 2.08/2.29  ((a123) != (a41))
% 2.08/2.29  (-. (c1_1 zenon_X15))
% 2.08/2.29  (zenon_X9 != (a59))
% 2.08/2.29  ((a130) != zenon_X22)
% 2.08/2.29  (-. (c5_2 zenon_X20 (a30)))
% 2.08/2.29  (c7_2 (a39) (a131))
% 2.08/2.29  (zenon_X11 != (a29))
% 2.08/2.29  ((a63) != (a108))
% 2.08/2.29  ((a33) != zenon_X195)
% 2.08/2.29  (c6_2 (a68) zenon_X193)
% 2.08/2.29  ((a40) != zenon_X142)
% 2.08/2.29  ((a127) != zenon_X30)
% 2.08/2.29  ((a30) != zenon_X54)
% 2.08/2.29  ((a82) != zenon_X123)
% 2.08/2.29  (c4_2 (a51) (a30))
% 2.08/2.29  ((a63) != (a58))
% 2.08/2.29  (c5_2 (a59) (a41))
% 2.08/2.29  (c4_2 (a51) (a130))
% 2.08/2.29  (c5_2 (a93) (a114))
% 2.08/2.29  (c8_2 (a47) (a48))
% 2.08/2.29  ((a130) != (a40))
% 2.08/2.29  (-. (c5_2 (a93) (a108)))
% 2.08/2.29  (c8_2 zenon_X23 (a123))
% 2.08/2.29  ((a30) != zenon_X2)
% 2.08/2.29  (c1_2 (a51) (a30))
% 2.08/2.29  ((a63) != zenon_X195)
% 2.08/2.29  (zenon_X86 != (a30))
% 2.08/2.29  (-. (c7_2 (a93) zenon_X53))
% 2.08/2.29  ((a82) != zenon_X52)
% 2.08/2.29  (-. (c8_2 (a39) zenon_X8))
% 2.08/2.29  (-. (c8_2 zenon_X15 (a58)))
% 2.08/2.29  (zenon_X18 != zenon_X28)
% 2.08/2.29  (-. (c5_2 (a136) (a95)))
% 2.08/2.29  (zenon_X40 != zenon_X28)
% 2.08/2.29  (-. (c5_2 zenon_X11 (a97)))
% 2.08/2.29  (-. (c2_1 (a104)))
% 2.08/2.29  ((a81) != (a104))
% 2.08/2.29  (-. (c6_2 (a104) (a40)))
% 2.08/2.29  (c5_2 (a59) (a30))
% 2.08/2.29  ((a131) != (a31))
% 2.08/2.29  (c1_2 zenon_X23 (a82))
% 2.08/2.29  ((a93) != (a51))
% 2.08/2.29  (-. (c5_2 (a39) zenon_X86))
% 2.08/2.29  (c1_2 (a47) (a108))
% 2.08/2.29  (c5_2 (a59) zenon_X151)
% 2.08/2.29  ((a114) != zenon_X103)
% 2.08/2.29  ((a137) != zenon_X170)
% 2.08/2.29  (-. (c1_1 zenon_X28))
% 2.08/2.29  (zenon_X21 != zenon_X193)
% 2.08/2.29  ((a131) != zenon_X8)
% 2.08/2.29  ((a129) != (a39))
% 2.08/2.29  (-. (c3_2 (a47) zenon_X66))
% 2.08/2.29  (zenon_X71 != (a123))
% 2.08/2.29  (-. (c2_2 (a47) (a48)))
% 2.08/2.29  ((a131) != zenon_X32)
% 2.08/2.29  ((a30) != zenon_X55)
% 2.08/2.29  (ndr1_1 (a129))
% 2.08/2.29  (zenon_X39 != zenon_X82)
% 2.08/2.29  (zenon_X27 != (a96))
% 2.08/2.29  ((a129) != zenon_X24)
% 2.08/2.29  (c6_2 zenon_X7 (a57))
% 2.08/2.29  (ndr1_0)
% 2.08/2.29  (-. (c6_2 zenon_X7 (a31)))
% 2.08/2.29  ((a40) != zenon_X54)
% 2.08/2.29  ((a51) != (a104))
% 2.08/2.29  (c1_1 (a136))
% 2.08/2.29  (c6_2 zenon_X27 (a95))
% 2.08/2.29  (c3_1 (a59))
% 2.08/2.29  ((a81) != zenon_X11)
% 2.08/2.29  (-. (c5_2 zenon_X11 (a137)))
% 2.08/2.29  (-. (c3_2 (a122) (a58)))
% 2.08/2.29  ((a57) != (a115))
% 2.08/2.29  ((a30) != zenon_X12)
% 2.08/2.29  (c8_2 (a117) zenon_X35)
% 2.08/2.29  (-. (c6_2 zenon_X9 (a40)))
% 2.08/2.29  ((a97) != zenon_X74)
% 2.08/2.29  ((a40) != zenon_X66)
% 2.08/2.29  ((a57) != (a49))
% 2.08/2.29  ((a57) != zenon_X64)
% 2.08/2.29  (c8_2 (a122) zenon_X42)
% 2.08/2.29  ((a95) != zenon_X78)
% 2.08/2.29  (zenon_X21 != zenon_X16)
% 2.08/2.29  ((a57) != zenon_X93)
% 2.08/2.29  (c8_2 zenon_X27 (a130))
% 2.08/2.29  (c6_1 zenon_X15)
% 2.08/2.29  ((a29) != (a39))
% 2.08/2.29  ((a130) != zenon_X124)
% 2.08/2.29  ((a137) != zenon_X84)
% 2.08/2.29  ((a33) != zenon_X133)
% 2.08/2.29  ((a31) != zenon_X37)
% 2.08/2.29  (c6_2 (a81) (a58))
% 2.08/2.29  ((a30) != (a97))
% 2.08/2.29  (c6_2 (a51) (a95))
% 2.08/2.29  (-. (c2_1 zenon_X30))
% 2.08/2.29  ((a136) != (a117))
% 2.08/2.29  (-. (c8_2 (a59) zenon_X147))
% 2.08/2.29  (c6_2 zenon_X23 (a82))
% 2.08/2.29  (-. (ndr1_1 zenon_X10))
% 2.08/2.29  ((a130) != zenon_X67)
% 2.08/2.29  (-. (c5_2 (a68) (a97)))
% 2.08/2.29  (zenon_X104 != (a115))
% 2.08/2.29  ((a114) != (a49))
% 2.08/2.29  ((a127) != (a117))
% 2.08/2.29  ((a30) != zenon_X82)
% 2.08/2.29  (c8_2 (a104) (a130))
% 2.08/2.29  (c1_2 (a136) (a130))
% 2.08/2.29  (zenon_X26 != (a95))
% 2.08/2.29  ((a33) != (a115))
% 2.08/2.29  ((a30) != (a108))
% 2.08/2.29  ((a137) != zenon_X88)
% 2.08/2.29  ((a40) != zenon_X79)
% 2.08/2.29  ((a65) != zenon_X11)
% 2.08/2.29  (-. (c6_2 (a104) (a82)))
% 2.08/2.29  (zenon_X18 != zenon_X15)
% 2.08/2.29  (-. (c5_2 zenon_X38 zenon_X39))
% 2.08/2.29  ((a40) != zenon_X67)
% 2.08/2.29  ((a29) != zenon_X38)
% 2.08/2.29  ((a58) != zenon_X123)
% 2.08/2.29  ((a130) != zenon_X197)
% 2.08/2.29  (c7_1 zenon_X20)
% 2.08/2.29  (zenon_X23 != zenon_X27)
% 2.08/2.29  (c6_2 (a51) (a108))
% 2.08/2.29  (-. (c7_2 (a93) zenon_X70))
% 2.08/2.29  ((a41) != zenon_X16)
% 2.08/2.29  (c8_2 (a93) (a63))
% 2.08/2.29  ((a40) != zenon_X189)
% 2.08/2.29  (-. (c5_2 zenon_X23 (a63)))
% 2.08/2.29  (zenon_X23 != (a39))
% 2.08/2.29  ((a30) != zenon_X121)
% 2.08/2.29  (-. (c7_2 zenon_X36 (a108)))
% 2.08/2.29  (c5_2 (a59) (a49))
% 2.08/2.29  (-. (ndr1_1 zenon_X18))
% 2.08/2.29  (c5_2 (a59) (a58))
% 2.08/2.29  (zenon_X3 != (a51))
% 2.08/2.29  (zenon_X10 != zenon_X27)
% 2.08/2.29  (c4_1 (a136))
% 2.08/2.29  (c5_2 (a65) zenon_X29)
% 2.08/2.29  (-. (c7_2 (a93) (a131)))
% 2.08/2.29  (c2_2 (a59) (a57))
% 2.08/2.29  (c6_2 (a81) (a137))
% 2.08/2.29  (-. (c5_2 (a117) (a30)))
% 2.08/2.29  (c4_2 zenon_X11 (a63))
% 2.08/2.29  (zenon_X7 != zenon_X10)
% 2.08/2.29  (-. (c6_2 zenon_X23 (a58)))
% 2.08/2.29  (-. (c4_2 zenon_X27 zenon_X112))
% 2.08/2.29  ((a82) != zenon_X183)
% 2.08/2.29  (-. (c6_2 (a47) zenon_X21))
% 2.08/2.29  (c6_2 (a96) (a30))
% 2.08/2.29  ((a49) != zenon_X121)
% 2.08/2.29  (-. (c6_1 (a121)))
% 2.08/2.29  ((a18) != zenon_X24)
% 2.08/2.29  (c4_2 zenon_X7 (a63))
% 2.08/2.29  (c8_2 (a93) zenon_X42)
% 2.08/2.29  (zenon_X23 != (a104))
% 2.08/2.29  (-. (c2_2 (a51) zenon_X106))
% 2.08/2.29  (-. (c6_2 (a93) (a40)))
% 2.08/2.29  (zenon_X6 != zenon_X28)
% 2.08/2.29  ((a59) != zenon_X27)
% 2.08/2.29  (zenon_X10 != (a93))
% 2.08/2.29  (c8_2 (a29) zenon_X53)
% 2.08/2.29  (-. (c5_2 (a39) zenon_X82))
% 2.08/2.29  ((a114) != zenon_X104)
% 2.08/2.29  (zenon_X72 != zenon_X32)
% 2.08/2.29  (-. (c3_2 zenon_X15 zenon_X210))
% 2.08/2.29  ((a63) != (a41))
% 2.08/2.29  (c1_2 (a18) (a108))
% 2.08/2.29  (zenon_X104 != zenon_X8)
% 2.08/2.29  (ndr1_1 (a96))
% 2.08/2.29  (c7_1 zenon_X11)
% 2.08/2.29  ((a63) != zenon_X82)
% 2.08/2.29  ((a82) != zenon_X87)
% 2.08/2.29  ((a30) != zenon_X89)
% 2.08/2.29  ((a130) != zenon_X34)
% 2.08/2.29  ((a108) != (a49))
% 2.08/2.29  (zenon_X26 != zenon_X153)
% 2.08/2.29  (-. (c3_2 zenon_X38 zenon_X224))
% 2.08/2.29  ((a93) != zenon_X18)
% 2.08/2.29  ((a30) != zenon_X57)
% 2.08/2.29  ((a130) != zenon_X117)
% 2.08/2.29  (zenon_X38 != (a34))
% 2.08/2.29  (c5_2 (a68) (a95))
% 2.08/2.29  (zenon_X20 != zenon_X23)
% 2.08/2.29  (zenon_X151 != (a137))
% 2.08/2.29  ((a63) != zenon_X153)
% 2.08/2.29  (c3_2 (a59) (a57))
% 2.08/2.29  ((a108) != zenon_X12)
% 2.08/2.29  (c8_2 zenon_X27 zenon_X105)
% 2.08/2.29  (-. (c3_2 zenon_X27 zenon_X183))
% 2.08/2.29  ((a33) != (a97))
% 2.08/2.29  (c1_2 (a47) (a63))
% 2.08/2.29  (zenon_X83 != (a115))
% 2.08/2.29  (c8_2 (a129) (a115))
% 2.08/2.29  ((a131) != zenon_X195)
% 2.08/2.29  (-. (c3_2 zenon_X36 zenon_X180))
% 2.08/2.29  (-. (c3_2 zenon_X23 zenon_X185))
% 2.08/2.29  (zenon_X11 != zenon_X9)
% 2.08/2.29  ((a114) != (a63))
% 2.08/2.29  (zenon_X22 != (a40))
% 2.08/2.29  (c7_1 (a18))
% 2.08/2.29  (-. (c4_1 zenon_X30))
% 2.08/2.29  ((a130) != zenon_X133)
% 2.08/2.29  ((a40) != zenon_X110)
% 2.08/2.29  ((a49) != zenon_X74)
% 2.08/2.29  (zenon_X27 != zenon_X3)
% 2.08/2.29  ((a108) != zenon_X35)
% 2.08/2.29  (c1_2 (a29) (a41))
% 2.08/2.29  ((a63) != zenon_X32)
% 2.08/2.29  (-. (c3_2 (a47) zenon_X56))
% 2.08/2.29  ((a57) != zenon_X168)
% 2.08/2.29  ((a82) != zenon_X44)
% 2.08/2.29  ((a114) != zenon_X82)
% 2.08/2.29  ((a57) != zenon_X195)
% 2.08/2.29  (-. (c6_2 (a18) (a137)))
% 2.08/2.29  ((a130) != zenon_X142)
% 2.08/2.29  (-. (c5_2 (a59) (a40)))
% 2.08/2.29  (-. (c3_2 (a96) zenon_X75))
% 2.08/2.29  ((a30) != (a40))
% 2.08/2.29  (c1_2 (a65) (a95))
% 2.08/2.29  ((a97) != zenon_X83)
% 2.08/2.29  (zenon_X151 != (a49))
% 2.08/2.29  ((a96) != (a104))
% 2.08/2.29  (zenon_X7 != (a18))
% 2.08/2.29  ((a31) != zenon_X110)
% 2.08/2.29  (c5_2 (a65) (a58))
% 2.08/2.29  (zenon_X14 != (a115))
% 2.08/2.29  ((a63) != zenon_X34)
% 2.08/2.29  (zenon_X32 != zenon_X8)
% 2.08/2.29  (c6_2 zenon_X7 (a30))
% 2.08/2.29  (-. (c5_2 zenon_X20 (a49)))
% 2.08/2.29  (-. (c7_1 (a104)))
% 2.08/2.29  ((a121) != zenon_X7)
% 2.08/2.29  ((a82) != zenon_X108)
% 2.08/2.29  ((a114) != (a58))
% 2.08/2.29  (-. (c5_2 zenon_X11 zenon_X26))
% 2.08/2.29  (-. (c5_2 (a121) zenon_X136))
% 2.08/2.29  (c6_1 zenon_X3)
% 2.08/2.29  (c7_1 zenon_X7)
% 2.08/2.29  ((a137) != zenon_X68)
% 2.08/2.29  ((a97) != zenon_X100)
% 2.08/2.29  ((a31) != (a115))
% 2.08/2.29  (-. (c7_2 (a65) (a57)))
% 2.08/2.29  ((a117) != zenon_X36)
% 2.08/2.29  ((a31) != zenon_X79)
% 2.08/2.29  ((a65) != (a34))
% 2.08/2.29  (zenon_X153 != zenon_X147)
% 2.08/2.29  (-. (c7_2 zenon_X38 (a108)))
% 2.08/2.29  ((a48) != zenon_X35)
% 2.08/2.29  (zenon_X10 != (a39))
% 2.08/2.29  ((a123) != zenon_X111)
% 2.08/2.29  (c1_1 zenon_X38)
% 2.08/2.29  ((a40) != zenon_X111)
% 2.08/2.29  (c5_2 (a65) (a108))
% 2.08/2.29  ((a65) != zenon_X28)
% 2.08/2.29  (zenon_X23 != zenon_X38)
% 2.08/2.29  (-. (c3_1 (a29)))
% 2.08/2.29  ((a97) != zenon_X207)
% 2.08/2.29  ((a93) != zenon_X6)
% 2.08/2.29  (c8_2 (a117) zenon_X32)
% 2.08/2.29  (-. (c6_1 zenon_X28))
% 2.08/2.29  (-. (c2_2 zenon_X36 zenon_X184))
% 2.08/2.29  (zenon_X73 != zenon_X32)
% 2.08/2.29  ((a58) != zenon_X100)
% 2.08/2.29  (c8_2 (a93) zenon_X14)
% 2.08/2.29  (-. (c3_2 zenon_X20 (a58)))
% 2.08/2.29  (-. (c5_2 (a51) (a58)))
% 2.08/2.29  (zenon_X26 != (a41))
% 2.08/2.29  (c1_2 (a29) (a40))
% 2.08/2.29  (-. (c2_2 (a117) (a63)))
% 2.08/2.29  ((a81) != zenon_X27)
% 2.08/2.29  (-. (c6_2 zenon_X9 zenon_X193))
% 2.08/2.29  ((a123) != zenon_X100)
% 2.08/2.29  ((a33) != zenon_X32)
% 2.08/2.29  (-. (c5_2 (a39) zenon_X79))
% 2.08/2.29  ((a108) != zenon_X37)
% 2.08/2.29  (c6_2 zenon_X11 (a82))
% 2.08/2.29  ((a95) != zenon_X142)
% 2.08/2.29  ((a49) != zenon_X33)
% 2.08/2.29  (-. (c8_2 (a39) zenon_X70))
% 2.08/2.29  (c1_2 (a18) (a33))
% 2.08/2.29  (ndr1_1 (a136))
% 2.08/2.29  ((a95) != zenon_X48)
% 2.08/2.29  (c3_1 (a47))
% 2.08/2.29  ((a108) != (a131))
% 2.08/2.29  ((a82) != zenon_X64)
% 2.08/2.29  ((a57) != zenon_X77)
% 2.08/2.29  (zenon_X6 != zenon_X38)
% 2.08/2.29  (c1_2 (a59) (a57))
% 2.08/2.29  (zenon_X35 != (a97))
% 2.08/2.29  ((a29) != zenon_X40)
% 2.08/2.29  (c1_2 (a96) (a137))
% 2.08/2.29  (c3_1 (a122))
% 2.08/2.29  (zenon_X105 != (a115))
% 2.08/2.29  (zenon_X36 != (a29))
% 2.08/2.29  ((a39) != zenon_X6)
% 2.08/2.29  ((a130) != zenon_X88)
% 2.08/2.29  (-. (c6_2 (a93) zenon_X12))
% 2.08/2.29  (-. (c5_2 (a129) (a63)))
% 2.08/2.29  ((a49) != (a97))
% 2.08/2.29  (zenon_X6 != zenon_X36)
% 2.08/2.29  (zenon_X226 != (a115))
% 2.08/2.29  (zenon_X79 != zenon_X147)
% 2.08/2.29  (c1_2 (a47) (a30))
% 2.08/2.29  (-. (c2_2 zenon_X7 (a63)))
% 2.08/2.29  ((a68) != (a136))
% 2.08/2.29  ((a130) != zenon_X89)
% 2.08/2.29  ((a33) != zenon_X123)
% 2.08/2.29  (zenon_X9 != zenon_X30)
% 2.08/2.29  (c5_2 (a65) (a82))
% 2.08/2.29  (-. (c6_2 zenon_X15 (a95)))
% 2.08/2.29  ((a122) != (a93))
% 2.08/2.29  (zenon_X79 != (a115))
% 2.08/2.29  ((a57) != zenon_X153)
% 2.08/2.29  (c8_2 (a18) zenon_X82)
% 2.08/2.29  ((a30) != zenon_X113)
% 2.08/2.29  (zenon_X10 != (a29))
% 2.08/2.29  (-. (c4_2 (a18) zenon_X86))
% 2.08/2.29  (-. (c5_2 (a81) (a49)))
% 2.08/2.29  ((a81) != (a51))
% 2.08/2.29  (-. (ndr1_1 (a34)))
% 2.08/2.29  (c1_2 (a18) (a115))
% 2.08/2.29  (-. (c3_2 (a121) zenon_X134))
% 2.08/2.29  ((a95) != zenon_X14)
% 2.08/2.29  ((a58) != zenon_X147)
% 2.08/2.29  ((a58) != zenon_X195)
% 2.08/2.29  (c6_2 (a68) (a40))
% 2.08/2.29  ((a121) != zenon_X1)
% 2.08/2.29  ((a41) != zenon_X8)
% 2.08/2.29  ((a30) != zenon_X49)
% 2.08/2.29  (zenon_X22 != (a58))
% 2.08/2.29  (c5_2 (a122) (a123))
% 2.08/2.29  (-. (c6_2 (a47) (a31)))
% 2.08/2.29  (c7_2 (a59) zenon_X79)
% 2.08/2.29  (c4_2 (a51) (a40))
% 2.08/2.29  ((a96) != zenon_X40)
% 2.08/2.29  ((a97) != zenon_X82)
% 2.08/2.29  ((a30) != zenon_X123)
% 2.08/2.29  (c8_2 (a136) zenon_X42)
% 2.08/2.29  (-. (c2_1 zenon_X38))
% 2.08/2.29  (zenon_X53 != (a130))
% 2.08/2.29  (c8_2 (a136) (a114))
% 2.08/2.29  ((a57) != zenon_X104)
% 2.08/2.29  ((a57) != zenon_X149)
% 2.08/2.29  ((a63) != zenon_X192)
% 2.08/2.29  (c6_2 (a68) zenon_X133)
% 2.08/2.29  ((a30) != zenon_X158)
% 2.08/2.29  (-. (c5_2 (a122) (a30)))
% 2.08/2.29  (-. (c6_2 (a18) zenon_X152))
% 2.08/2.29  (c3_2 (a47) (a30))
% 2.08/2.29  (zenon_X7 != (a93))
% 2.08/2.29  (c6_1 zenon_X24)
% 2.08/2.29  ((a82) != zenon_X147)
% 2.08/2.29  (zenon_X39 != (a115))
% 2.08/2.29  (zenon_X11 != zenon_X38)
% 2.08/2.29  (ndr1_1 (a47))
% 2.08/2.29  (zenon_X27 != zenon_X18)
% 2.08/2.29  (-. (c3_2 (a68) (a115)))
% 2.08/2.29  (c1_2 zenon_X7 (a33))
% 2.08/2.29  (-. (c4_2 (a39) (a40)))
% 2.08/2.29  (zenon_X20 != zenon_X24)
% 2.08/2.29  (c4_1 (a96))
% 2.08/2.29  ((a108) != zenon_X82)
% 2.08/2.29  (zenon_X26 != (a40))
% 2.08/2.29  (c8_2 (a104) (a95))
% 2.08/2.29  (zenon_X36 != zenon_X28)
% 2.08/2.29  (zenon_X10 != zenon_X30)
% 2.08/2.29  (c1_2 (a39) (a41))
% 2.08/2.29  ((a121) != (a127))
% 2.08/2.29  ((a137) != zenon_X56)
% 2.08/2.29  (c1_2 zenon_X20 (a95))
% 2.08/2.29  ((a33) != zenon_X21)
% 2.08/2.29  (c5_1 (a136))
% 2.08/2.29  (-. (c6_1 zenon_X11))
% 2.08/2.29  (c6_2 (a96) (a57))
% 2.08/2.29  (c6_2 (a121) (a57))
% 2.08/2.29  ((a130) != zenon_X161)
% 2.08/2.29  (zenon_X21 != zenon_X133)
% 2.08/2.29  ((a136) != (a93))
% 2.08/2.29  (zenon_X18 != zenon_X30)
% 2.08/2.29  ((a131) != (a137))
% 2.08/2.29  ((a31) != zenon_X133)
% 2.08/2.29  ((a59) != (a127))
% 2.08/2.29  (-. (c3_2 (a39) zenon_X67))
% 2.08/2.29  ((a31) != zenon_X96)
% 2.08/2.29  ((a30) != zenon_X56)
% 2.08/2.29  (c4_2 (a39) (a57))
% 2.08/2.29  ((a127) != (a34))
% 2.08/2.29  ((a97) != zenon_X101)
% 2.08/2.29  (-. (c3_2 (a68) (a58)))
% 2.08/2.29  ((a95) != zenon_X120)
% 2.08/2.29  ((a65) != (a136))
% 2.08/2.29  ((a59) != zenon_X6)
% 2.08/2.29  (-. (c6_1 (a127)))
% 2.08/2.29  (c6_2 (a96) (a95))
% 2.08/2.29  ((a130) != zenon_X75)
% 2.08/2.29  (c8_2 (a129) (a49))
% 2.08/2.29  ((a57) != zenon_X123)
% 2.08/2.29  ((a129) != zenon_X30)
% 2.08/2.29  (-. (c2_2 (a117) zenon_X81))
% 2.08/2.29  ((a33) != zenon_X26)
% 2.08/2.29  ((a121) != zenon_X36)
% 2.08/2.29  (c3_2 (a39) (a57))
% 2.08/2.29  (c3_1 (a121))
% 2.08/2.29  (c1_2 (a18) (a49))
% 2.08/2.29  (-. (c7_2 zenon_X7 (a108)))
% 2.08/2.29  (-. (c6_2 zenon_X9 (a108)))
% 2.08/2.29  (zenon_X10 != zenon_X24)
% 2.08/2.29  ((a81) != (a129))
% 2.08/2.29  ((a57) != (a31))
% 2.08/2.29  ((a136) != zenon_X18)
% 2.08/2.29  ((a47) != zenon_X24)
% 2.08/2.29  ((a130) != (a123))
% 2.08/2.29  (c6_2 (a122) (a130))
% 2.08/2.29  (zenon_X23 != (a93))
% 2.08/2.29  ((a59) != (a34))
% 2.08/2.29  ((a30) != zenon_X196)
% 2.08/2.29  (-. (c4_1 (a93)))
% 2.08/2.29  (-. (c6_2 (a104) (a33)))
% 2.08/2.29  ((a40) != zenon_X68)
% 2.08/2.29  (zenon_X53 != zenon_X32)
% 2.08/2.29  (c1_1 zenon_X23)
% 2.08/2.29  (-. (c7_1 zenon_X3))
% 2.08/2.29  ((a49) != zenon_X120)
% 2.08/2.29  (-. (c1_1 (a122)))
% 2.08/2.29  (-. (c7_2 (a121) zenon_X2))
% 2.08/2.29  ((a95) != (a40))
% 2.08/2.29  ((a31) != zenon_X196)
% 2.08/2.29  (zenon_X153 != (a30))
% 2.08/2.29  ((a49) != zenon_X188)
% 2.08/2.29  (c1_2 (a39) zenon_X83)
% 2.08/2.29  (zenon_X53 != zenon_X101)
% 2.08/2.29  (c8_2 (a29) zenon_X14)
% 2.08/2.29  ((a82) != zenon_X47)
% 2.08/2.29  ((a93) != zenon_X24)
% 2.08/2.29  ((a108) != zenon_X103)
% 2.08/2.29  (c5_2 (a81) (a95))
% 2.08/2.29  (-. (c5_2 (a93) (a130)))
% 2.08/2.29  ((a29) != (a51))
% 2.08/2.29  (c5_1 (a121))
% 2.08/2.29  (c8_2 (a18) (a30))
% 2.08/2.29  ((a33) != zenon_X22)
% 2.08/2.29  ((a136) != zenon_X1)
% 2.08/2.29  ((a40) != (a41))
% 2.08/2.29  (c1_2 (a29) (a30))
% 2.08/2.29  ((a59) != zenon_X28)
% 2.08/2.29  (c3_1 (a81))
% 2.08/2.29  ((a130) != zenon_X56)
% 2.08/2.29  (zenon_X20 != (a93))
% 2.08/2.29  ((a40) != zenon_X65)
% 2.08/2.29  (zenon_X10 != zenon_X36)
% 2.08/2.29  ((a57) != (a130))
% 2.08/2.29  (-. (c5_2 zenon_X38 (a115)))
% 2.08/2.29  (-. (c5_2 zenon_X11 zenon_X104))
% 2.08/2.29  ((a18) != (a51))
% 2.08/2.29  (c7_2 (a39) zenon_X14)
% 2.08/2.29  (-. (c3_1 (a18)))
% 2.08/2.29  ((a65) != (a117))
% 2.08/2.29  (-. (c5_2 (a39) zenon_X147))
% 2.08/2.29  (c5_2 (a59) (a95))
% 2.08/2.29  (-. (c2_2 (a81) zenon_X58))
% 2.08/2.29  (c8_2 (a104) (a131))
% 2.08/2.29  ((a57) != zenon_X155)
% 2.08/2.29  (-. (c5_2 (a18) (a97)))
% 2.08/2.29  (zenon_X11 != (a47))
% 2.08/2.29  (c5_2 (a59) (a123))
% 2.08/2.29  (c8_2 (a93) (a123))
% 2.08/2.29  ((a65) != zenon_X23)
% 2.08/2.29  (c6_2 zenon_X6 (a108))
% 2.08/2.29  (-. (c2_1 zenon_X10))
% 2.08/2.29  ((a30) != (a33))
% 2.08/2.29  (c7_2 (a136) (a115))
% 2.08/2.29  ((a123) != zenon_X79)
% 2.08/2.29  (zenon_X151 != (a40))
% 2.08/2.29  (-. (c5_2 zenon_X11 zenon_X8))
% 2.08/2.29  ((a130) != zenon_X91)
% 2.08/2.29  (c5_2 (a65) (a131))
% 2.08/2.29  (-. (c5_2 (a29) zenon_X91))
% 2.08/2.29  ((a31) != zenon_X111)
% 2.08/2.29  ((a95) != zenon_X88)
% 2.08/2.29  ((a18) != (a122))
% 2.08/2.29  (c8_2 (a136) zenon_X32)
% 2.08/2.29  ((a41) != zenon_X79)
% 2.08/2.29  (-. (c3_1 zenon_X11))
% 2.08/2.29  ((a95) != zenon_X82)
% 2.08/2.29  (-. (c8_1 zenon_X28))
% 2.08/2.29  (c6_2 (a96) (a82))
% 2.08/2.29  (-. (c7_1 zenon_X30))
% 2.08/2.29  (c7_1 zenon_X27)
% 2.08/2.29  (c6_2 (a129) (a30))
% 2.08/2.29  (c5_2 zenon_X11 (a95))
% 2.08/2.29  ((a121) != zenon_X20)
% 2.08/2.29  (-. (c5_2 zenon_X11 (a123)))
% 2.08/2.29  (c1_2 (a18) zenon_X39)
% 2.08/2.29  ((a65) != (a93))
% 2.08/2.29  (-. (c4_1 (a65)))
% 2.08/2.29  (-. (c7_2 (a121) zenon_X42))
% 2.08/2.29  ((a108) != zenon_X33)
% 2.08/2.29  ((a30) != (a41))
% 2.08/2.29  (c1_2 (a65) (a63))
% 2.08/2.29  ((a58) != zenon_X124)
% 2.08/2.29  ((a30) != zenon_X108)
% 2.08/2.29  ((a30) != zenon_X16)
% 2.08/2.29  (-. (c7_1 zenon_X6))
% 2.08/2.29  (-. (c5_2 zenon_X38 (a30)))
% 2.08/2.29  ((a57) != zenon_X54)
% 2.08/2.29  ((a31) != zenon_X153)
% 2.08/2.29  (zenon_X23 != zenon_X28)
% 2.08/2.29  ((a93) != (a47))
% 2.08/2.29  ((a121) != zenon_X28)
% 2.08/2.29  (zenon_X20 != (a18))
% 2.08/2.29  (c1_2 zenon_X27 (a63))
% 2.08/2.29  ((a123) != zenon_X110)
% 2.08/2.29  ((a127) != (a29))
% 2.08/2.29  (-. (c8_1 zenon_X36))
% 2.08/2.29  (c5_2 zenon_X36 (a95))
% 2.08/2.29  ((a65) != zenon_X6)
% 2.08/2.29  (c4_1 (a127))
% 2.08/2.29  (-. (c6_1 (a117)))
% 2.08/2.29  (c1_2 (a129) (a137))
% 2.08/2.29  ((a63) != zenon_X44)
% 2.08/2.29  ((a130) != zenon_X12)
% 2.08/2.29  ((a82) != zenon_X67)
% 2.08/2.29  (-. (c3_2 (a39) zenon_X50))
% 2.08/2.29  (c5_2 (a18) (a95))
% 2.08/2.29  (zenon_X11 != (a122))
% 2.08/2.29  (c6_2 (a18) (a95))
% 2.08/2.29  (-. (c2_1 zenon_X28))
% 2.08/2.29  (c6_2 (a136) (a130))
% 2.08/2.29  (-. (c3_2 (a96) (a58)))
% 2.08/2.29  (-. (c5_2 zenon_X11 (a115)))
% 2.08/2.29  (-. (c5_2 zenon_X36 (a108)))
% 2.08/2.29  (-. (c5_2 (a117) (a49)))
% 2.08/2.29  (c6_1 zenon_X30)
% 2.08/2.29  (zenon_X20 != (a34))
% 2.08/2.29  (zenon_X26 != (a63))
% 2.08/2.29  (c5_2 (a65) (a123))
% 2.08/2.29  (c6_2 zenon_X38 (a58))
% 2.08/2.29  (-. (c5_2 (a51) zenon_X147))
% 2.08/2.29  ((a131) != zenon_X79)
% 2.08/2.29  ((a121) != zenon_X38)
% 2.08/2.29  ((a34) != (a104))
% 2.08/2.29  (c6_2 zenon_X36 (a58))
% 2.08/2.29  (c7_1 (a127))
% 2.08/2.29  ((a82) != zenon_X145)
% 2.08/2.29  (c4_1 (a81))
% 2.08/2.29  ((a18) != (a104))
% 2.08/2.29  ((a31) != zenon_X91)
% 2.08/2.29  ((a96) != (a117))
% 2.08/2.29  (c1_2 (a136) (a137))
% 2.08/2.29  ((a82) != zenon_X26)
% 2.08/2.29  (-. (c5_2 zenon_X38 zenon_X82))
% 2.08/2.29  ((a117) != (a104))
% 2.08/2.29  (-. (c3_2 (a117) (a115)))
% 2.08/2.29  (zenon_X26 != zenon_X39)
% 2.08/2.29  (c4_2 (a68) (a63))
% 2.08/2.29  (c8_2 (a136) (a97))
% 2.08/2.29  ((a51) != (a127))
% 2.08/2.29  ((a82) != zenon_X43)
% 2.08/2.29  ((a68) != (a129))
% 2.08/2.29  ((a129) != zenon_X3)
% 2.08/2.29  ((a30) != zenon_X59)
% 2.08/2.29  ((a58) != zenon_X32)
% 2.08/2.29  (c1_2 (a51) (a130))
% 2.08/2.29  ((a47) != zenon_X3)
% 2.08/2.29  (-. (c8_1 zenon_X11))
% 2.08/2.29  ((a30) != (a82))
% 2.08/2.29  ((a31) != zenon_X193)
% 2.08/2.29  (-. (c7_2 (a93) zenon_X8))
% 2.08/2.29  ((a123) != (a108))
% 2.08/2.29  (-. (c6_1 zenon_X9))
% 2.08/2.29  ((a82) != zenon_X32)
% 2.08/2.29  (-. (c2_1 (a129)))
% 2.08/2.29  (c1_1 (a51))
% 2.08/2.29  ((a33) != zenon_X8)
% 2.08/2.29  ((a18) != (a117))
% 2.08/2.29  (c1_2 (a39) (a63))
% 2.08/2.29  (c1_2 (a39) (a95))
% 2.08/2.29  ((a114) != zenon_X83)
% 2.08/2.29  ((a97) != zenon_X26)
% 2.08/2.29  ((a95) != zenon_X143)
% 2.08/2.29  (c1_1 (a127))
% 2.08/2.29  (c4_2 (a47) (a63))
% 2.08/2.29  (c1_2 (a51) (a57))
% 2.08/2.29  (c1_2 (a39) zenon_X32)
% 2.08/2.29  ((a137) != zenon_X67)
% 2.08/2.29  (-. (c8_2 zenon_X15 (a30)))
% 2.08/2.29  (c1_2 (a18) (a97))
% 2.08/2.29  ((a57) != (a41))
% 2.08/2.29  (c1_2 (a29) (a57))
% 2.08/2.29  (c8_2 (a81) (a82))
% 2.08/2.29  (-. (c5_2 (a129) (a108)))
% 2.08/2.29  ((a63) != zenon_X196)
% 2.08/2.29  (zenon_X9 != zenon_X27)
% 2.08/2.29  (-. (c5_2 zenon_X7 (a97)))
% 2.08/2.29  (c1_1 (a96))
% 2.08/2.29  ((a136) != (a51))
% 2.08/2.29  (-. (c7_2 (a93) (a115)))
% 2.08/2.29  (zenon_X78 != zenon_X147)
% 2.08/2.29  ((a57) != zenon_X139)
% 2.08/2.29  ((a96) != zenon_X30)
% 2.08/2.29  (-. (c5_2 (a51) zenon_X22))
% 2.08/2.29  (c5_2 (a29) (a41))
% 2.08/2.29  (zenon_X21 != zenon_X87)
% 2.08/2.29  ((a58) != (a49))
% 2.08/2.29  (-. (c3_2 (a29) zenon_X114))
% 2.08/2.29  (c8_2 (a104) (a137))
% 2.08/2.29  ((a82) != zenon_X139)
% 2.08/2.29  (c8_2 (a39) zenon_X35)
% 2.08/2.29  (-. (c7_2 (a129) (a108)))
% 2.08/2.29  (zenon_X42 != zenon_X83)
% 2.08/2.29  (zenon_X6 != zenon_X27)
% 2.08/2.29  ((a57) != zenon_X67)
% 2.08/2.29  (zenon_X38 != (a104))
% 2.08/2.29  ((a63) != zenon_X43)
% 2.08/2.29  (c1_2 (a81) (a95))
% 2.08/2.29  (-. (c2_2 (a18) zenon_X150))
% 2.08/2.29  (zenon_X9 != (a39))
% 2.08/2.29  (c1_1 (a68))
% 2.08/2.29  (c7_2 (a39) (a48))
% 2.08/2.29  (c6_2 zenon_X36 (a82))
% 2.08/2.29  (-. (c5_2 (a39) (a108)))
% 2.08/2.29  ((a40) != zenon_X32)
% 2.08/2.29  ((a30) != zenon_X32)
% 2.08/2.29  ((a97) != zenon_X88)
% 2.08/2.29  (zenon_X20 != zenon_X18)
% 2.08/2.29  (c1_2 (a129) (a95))
% 2.08/2.29  ((a58) != zenon_X91)
% 2.08/2.29  (-. (c5_2 (a136) (a63)))
% 2.08/2.29  ((a41) != zenon_X196)
% 2.08/2.29  ((a81) != zenon_X40)
% 2.08/2.29  (zenon_X11 != (a34))
% 2.08/2.29  ((a30) != zenon_X124)
% 2.08/2.29  ((a95) != (a48))
% 2.08/2.29  ((a114) != (a97))
% 2.08/2.29  (c6_2 (a68) (a82))
% 2.08/2.29  ((a127) != zenon_X18)
% 2.08/2.29  (-. (c5_2 (a81) (a30)))
% 2.08/2.29  (zenon_X35 != zenon_X32)
% 2.08/2.29  ((a31) != zenon_X147)
% 2.08/2.29  (-. (c6_2 (a93) (a58)))
% 2.08/2.29  (c6_2 (a47) (a57))
% 2.08/2.29  ((a137) != zenon_X108)
% 2.08/2.29  ((a49) != (a131))
% 2.08/2.29  ((a31) != (a137))
% 2.08/2.29  (c6_2 zenon_X38 (a108))
% 2.08/2.29  ((a121) != (a93))
% 2.08/2.29  (-. (c5_2 (a129) zenon_X100))
% 2.08/2.29  ((a29) != zenon_X7)
% 2.08/2.29  ((a82) != zenon_X95)
% 2.08/2.29  ((a127) != (a122))
% 2.08/2.29  (-. (c3_2 (a122) (a115)))
% 2.08/2.29  (-. (c5_2 (a136) (a49)))
% 2.08/2.29  ((a95) != (a115))
% 2.08/2.29  (zenon_X14 != zenon_X74)
% 2.08/2.29  (c7_2 (a136) (a130))
% 2.08/2.29  (-. (c3_2 zenon_X6 (a58)))
% 2.08/2.29  (-. (c7_2 (a129) (a131)))
% 2.08/2.29  (-. (c5_2 zenon_X11 (a58)))
% 2.08/2.29  (zenon_X10 != zenon_X28)
% 2.08/2.29  (c6_2 (a39) (a41))
% 2.08/2.29  ((a137) != zenon_X64)
% 2.08/2.29  (-. (c5_2 (a59) (a115)))
% 2.08/2.29  (zenon_X86 != (a49))
% 2.08/2.29  (c1_2 (a122) (a82))
% 2.08/2.29  (-. (c7_1 zenon_X38))
% 2.08/2.29  (-. (c4_2 (a39) zenon_X48))
% 2.08/2.29  (-. (c2_2 (a68) zenon_X98))
% 2.08/2.29  (zenon_X27 != (a18))
% 2.08/2.29  (zenon_X29 != (a30))
% 2.08/2.29  (c1_2 (a59) (a49))
% 2.08/2.29  (-. (c4_2 zenon_X7 zenon_X145))
% 2.08/2.29  ((a29) != (a136))
% 2.08/2.29  ((a95) != zenon_X100)
% 2.08/2.29  ((a40) != zenon_X63)
% 2.08/2.29  ((a123) != zenon_X39)
% 2.08/2.29  ((a97) != zenon_X121)
% 2.08/2.29  (-. (c3_2 (a121) zenon_X108))
% 2.08/2.29  (-. (c3_1 zenon_X40))
% 2.08/2.29  ((a30) != zenon_X63)
% 2.08/2.29  (zenon_X7 != zenon_X24)
% 2.08/2.29  (zenon_X36 != zenon_X3)
% 2.08/2.29  ((a121) != zenon_X11)
% 2.08/2.29  ((a30) != zenon_X161)
% 2.08/2.29  (c5_2 (a65) (a130))
% 2.08/2.29  ((a137) != zenon_X134)
% 2.08/2.29  (c3_2 (a59) (a30))
% 2.08/2.29  ((a57) != zenon_X87)
% 2.08/2.29  ((a31) != zenon_X189)
% 2.08/2.29  (ndr1_1 (a39))
% 2.08/2.29  (c8_1 (a117))
% 2.08/2.29  (zenon_X11 != zenon_X40)
% 2.08/2.29  (c5_2 (a29) (a130))
% 2.08/2.29  ((a97) != zenon_X147)
% 2.08/2.29  (c6_2 (a47) (a58))
% 2.08/2.29  (zenon_X153 != zenon_X79)
% 2.08/2.29  ((a137) != zenon_X39)
% 2.08/2.29  (c7_2 (a39) (a58))
% 2.08/2.29  ((a96) != zenon_X36)
% 2.08/2.29  ((a127) != (a104))
% 2.08/2.29  ((a117) != (a34))
% 2.08/2.29  (c4_1 zenon_X10)
% 2.08/2.29  (-. (c6_2 zenon_X11 (a58)))
% 2.08/2.29  (-. (c6_2 zenon_X9 (a95)))
% 2.08/2.29  (-. (c8_2 zenon_X15 (a57)))
% 2.08/2.29  ((a49) != zenon_X207)
% 2.08/2.29  (-. (c5_2 (a93) (a95)))
% 2.08/2.29  ((a137) != zenon_X8)
% 2.08/2.29  (zenon_X74 != (a115))
% 2.08/2.29  (c4_2 (a51) (a97))
% 2.08/2.29  (zenon_X21 != zenon_X37)
% 2.08/2.29  ((a59) != (a51))
% 2.08/2.29  (c8_2 (a136) zenon_X35)
% 2.08/2.29  ((a82) != zenon_X117)
% 2.08/2.29  ((a137) != zenon_X55)
% 2.08/2.29  (-. (c1_2 (a47) (a48)))
% 2.08/2.29  (zenon_X151 != zenon_X82)
% 2.08/2.29  (zenon_X74 != zenon_X35)
% 2.08/2.29  (-. (c2_2 zenon_X27 zenon_X162))
% 2.08/2.29  (c7_1 (a96))
% 2.08/2.29  (-. (c5_2 zenon_X38 zenon_X22))
% 2.08/2.29  ((a123) != (a95))
% 2.08/2.29  ((a57) != zenon_X81)
% 2.08/2.29  (c1_2 (a121) (a31))
% 2.08/2.29  (c5_2 (a29) (a58))
% 2.08/2.29  ((a96) != zenon_X18)
% 2.08/2.29  (c6_1 zenon_X40)
% 2.08/2.29  ((a130) != zenon_X63)
% 2.08/2.29  ((a65) != zenon_X7)
% 2.08/2.29  (zenon_X38 != zenon_X9)
% 2.08/2.29  ((a131) != zenon_X22)
% 2.08/2.29  (zenon_X6 != (a18))
% 2.08/2.29  (zenon_X7 != (a39))
% 2.08/2.29  (-. (c3_1 (a39)))
% 2.08/2.29  (-. (c4_1 (a29)))
% 2.08/2.29  (c6_2 zenon_X20 (a33))
% 2.08/2.29  (c3_2 (a29) (a57))
% 2.08/2.29  (-. (c7_2 (a59) (a57)))
% 2.08/2.29  (zenon_X105 != (a123))
% 2.08/2.29  (c6_2 zenon_X7 (a58))
% 2.08/2.29  (zenon_X26 != zenon_X29)
% 2.08/2.29  (c3_2 (a96) (a57))
% 2.08/2.29  ((a65) != (a81))
% 2.08/2.29  (zenon_X23 != zenon_X24)
% 2.08/2.29  ((a59) != zenon_X7)
% 2.08/2.29  (zenon_X9 != (a93))
% 2.08/2.29  ((a40) != zenon_X100)
% 2.08/2.29  ((a82) != zenon_X155)
% 2.08/2.29  (zenon_X70 != zenon_X32)
% 2.08/2.29  (zenon_X153 != (a97))
% 2.08/2.29  (c8_2 (a47) (a97))
% 2.08/2.29  (-. (c6_2 (a104) (a30)))
% 2.08/2.29  (zenon_X27 != zenon_X28)
% 2.08/2.29  (c8_2 (a47) (a115))
% 2.08/2.29  ((a57) != zenon_X35)
% 2.08/2.29  ((a65) != (a68))
% 2.08/2.29  ((a127) != zenon_X38)
% 2.08/2.29  (-. (c6_2 zenon_X27 (a57)))
% 2.08/2.29  (c6_2 (a68) (a31))
% 2.08/2.29  (-. (c5_2 (a117) (a58)))
% 2.08/2.29  (c1_2 (a68) (a95))
% 2.08/2.29  (c5_2 (a65) zenon_X39)
% 2.08/2.29  ((a95) != zenon_X91)
% 2.08/2.29  (zenon_X153 != zenon_X82)
% 2.08/2.29  (ndr1_1 zenon_X20)
% 2.08/2.29  ((a137) != (a130))
% 2.08/2.29  (c8_2 (a47) zenon_X32)
% 2.08/2.29  ((a58) != zenon_X82)
% 2.08/2.29  ((a95) != zenon_X195)
% 2.08/2.29  ((a82) != zenon_X196)
% 2.08/2.29  ((a137) != (a97))
% 2.08/2.29  (c1_2 (a59) zenon_X39)
% 2.08/2.29  (-. (c5_2 (a51) zenon_X79))
% 2.08/2.29  (zenon_X78 != (a30))
% 2.08/2.29  ((a40) != zenon_X50)
% 2.08/2.29  (c5_2 (a65) zenon_X79)
% 2.08/2.29  (zenon_X83 != (a130))
% 2.08/2.29  (zenon_X22 != (a41))
% 2.08/2.29  (zenon_X132 != (a123))
% 2.08/2.29  (c1_2 (a65) zenon_X104)
% 2.08/2.29  (c8_2 (a93) (a58))
% 2.08/2.29  ((a131) != (a115))
% 2.08/2.29  (zenon_X42 != zenon_X32)
% 2.08/2.29  ((a137) != (a115))
% 2.08/2.29  ((a117) != zenon_X6)
% 2.08/2.29  (c6_2 (a127) (a57))
% 2.08/2.29  ((a95) != zenon_X47)
% 2.08/2.29  ((a129) != zenon_X18)
% 2.08/2.29  (-. (c3_2 (a129) zenon_X63))
% 2.08/2.29  (-. (c3_2 (a29) zenon_X51))
% 2.08/2.29  (-. (c6_2 zenon_X7 (a40)))
% 2.08/2.29  (c5_2 (a39) (a137))
% 2.08/2.29  ((a137) != (a58))
% 2.08/2.29  (-. (c5_2 (a18) zenon_X147))
% 2.08/2.29  (zenon_X71 != zenon_X35)
% 2.08/2.29  ((a96) != (a47))
% 2.08/2.29  ((a40) != zenon_X123)
% 2.08/2.29  ((a30) != (a115))
% 2.08/2.29  (c1_2 zenon_X6 (a95))
% 2.08/2.29  ((a130) != (a33))
% 2.08/2.29  ((a130) != zenon_X51)
% 2.08/2.29  (zenon_X27 != zenon_X40)
% 2.08/2.29  (c1_2 (a65) (a137))
% 2.08/2.29  (zenon_X73 != (a130))
% 2.08/2.29  ((a58) != zenon_X37)
% 2.08/2.29  ((a30) != zenon_X133)
% 2.08/2.29  (-. (c8_2 zenon_X15 zenon_X195))
% 2.08/2.29  ((a114) != (a108))
% 2.08/2.29  (-. (c5_2 zenon_X38 (a49)))
% 2.08/2.29  ((a137) != zenon_X193)
% 2.08/2.29  ((a108) != zenon_X193)
% 2.08/2.29  ((a51) != (a34))
% 2.08/2.29  ((a127) != (a39))
% 2.08/2.29  ((a97) != zenon_X111)
% 2.08/2.29  ((a82) != zenon_X125)
% 2.08/2.29  (c8_2 zenon_X23 (a114))
% 2.08/2.29  ((a58) != zenon_X133)
% 2.08/2.29  ((a58) != zenon_X197)
% 2.08/2.29  ((a57) != zenon_X82)
% 2.08/2.29  ((a81) != zenon_X38)
% 2.08/2.29  (-. (c1_2 (a96) (a97)))
% 2.08/2.29  (-. (ndr1_1 zenon_X3))
% 2.08/2.29  (-. (c2_1 (a47)))
% 2.08/2.29  ((a63) != (a137))
% 2.08/2.29  (-. (c5_2 zenon_X11 zenon_X153))
% 2.08/2.29  ((a81) != zenon_X23)
% 2.08/2.29  ((a82) != (a108))
% 2.08/2.29  (c8_2 (a104) (a63))
% 2.08/2.29  (zenon_X11 != (a93))
% 2.08/2.29  (-. (c5_2 (a129) (a58)))
% 2.08/2.29  ((a49) != zenon_X211)
% 2.08/2.29  (c1_2 (a59) (a33))
% 2.08/2.29  (zenon_X14 != zenon_X73)
% 2.08/2.29  (-. (c3_2 (a39) zenon_X113))
% 2.08/2.29  ((a117) != (a129))
% 2.08/2.29  (c4_2 (a81) (a63))
% 2.08/2.29  ((a63) != zenon_X47)
% 2.08/2.29  (-. (c6_1 zenon_X36))
% 2.08/2.29  ((a81) != zenon_X7)
% 2.08/2.29  ((a114) != zenon_X71)
% 2.08/2.29  (-. (c6_2 (a47) (a137)))
% 2.08/2.29  (-. (c7_2 (a51) (a108)))
% 2.08/2.29  (-. (c8_0))
% 2.08/2.29  (-. (c5_2 (a121) (a63)))
% 2.08/2.29  ((a123) != zenon_X86)
% 2.08/2.29  (-. (c8_2 (a117) (a115)))
% 2.08/2.29  ((a136) != zenon_X6)
% 2.08/2.29  (zenon_X7 != zenon_X27)
% 2.08/2.29  ((a57) != zenon_X124)
% 2.08/2.29  (c1_2 (a96) (a63))
% 2.08/2.29  (c1_1 zenon_X3)
% 2.08/2.29  (c4_1 zenon_X38)
% 2.08/2.29  (zenon_X7 != zenon_X38)
% 2.08/2.29  (c1_2 (a18) (a58))
% 2.08/2.29  (c1_2 (a129) (a130))
% 2.08/2.29  ((a82) != (a123))
% 2.08/2.29  (c8_2 zenon_X11 zenon_X118)
% 2.08/2.29  (c7_2 (a136) zenon_X33)
% 2.08/2.29  (zenon_X7 != zenon_X3)
% 2.08/2.29  (-. (c5_2 (a129) (a31)))
% 2.08/2.29  (-. (c3_2 (a122) zenon_X64))
% 2.08/2.29  (ndr1_1 (a65))
% 2.08/2.29  ((a137) != zenon_X78)
% 2.08/2.29  (c8_2 (a117) zenon_X42)
% 2.08/2.29  (c1_2 zenon_X36 (a63))
% 2.08/2.29  ((a41) != (a48))
% 2.08/2.29  ((a51) != (a129))
% 2.08/2.29  (c5_2 (a65) (a57))
% 2.08/2.29  (c4_2 (a51) (a95))
% 2.08/2.29  ((a122) != zenon_X28)
% 2.08/2.29  (c6_2 (a121) (a58))
% 2.08/2.29  (-. (c3_2 (a136) zenon_X52))
% 2.08/2.29  (c8_2 (a129) zenon_X32)
% 2.08/2.29  (c3_2 (a81) (a82))
% 2.08/2.29  (-. (c6_2 (a104) (a95)))
% 2.08/2.29  (-. (c5_2 (a96) (a49)))
% 2.08/2.29  (-. (c7_2 (a93) zenon_X74))
% 2.08/2.29  ((a40) != zenon_X82)
% 2.08/2.29  (-. (c6_2 (a47) (a95)))
% 2.08/2.29  ((a33) != (a58))
% 2.08/2.29  (-. (c7_2 (a93) (a48)))
% 2.08/2.29  ((a31) != (a82))
% 2.08/2.29  (zenon_X39 != zenon_X147)
% 2.08/2.29  (ndr1_1 (a117))
% 2.08/2.29  (c1_2 zenon_X27 (a82))
% 2.08/2.29  ((a65) != zenon_X40)
% 2.08/2.29  ((a123) != zenon_X88)
% 2.08/2.29  ((a65) != zenon_X36)
% 2.08/2.29  ((a81) != zenon_X24)
% 2.08/2.29  (-. (c6_2 zenon_X15 (a31)))
% 2.08/2.29  ((a108) != zenon_X147)
% 2.08/2.29  ((a96) != zenon_X0)
% 2.08/2.29  (c8_2 (a18) (a49))
% 2.08/2.29  ((a63) != zenon_X79)
% 2.08/2.29  (c8_2 (a104) (a33))
% 2.08/2.29  (c5_2 (a65) zenon_X104)
% 2.08/2.29  (-. (c8_2 (a122) (a115)))
% 2.08/2.29  (zenon_X6 != zenon_X15)
% 2.08/2.29  ((a95) != zenon_X37)
% 2.08/2.29  ((a63) != (a31))
% 2.08/2.29  (-. (c6_2 (a18) (a30)))
% 2.08/2.29  (-. (c7_1 zenon_X9))
% 2.08/2.29  (c8_2 (a18) (a114))
% 2.08/2.29  (zenon_X39 != zenon_X8)
% 2.08/2.29  (-. (c8_2 (a129) (a130)))
% 2.08/2.29  (c5_2 (a59) zenon_X86)
% 2.08/2.29  (c7_1 (a65))
% 2.08/2.29  ((a82) != zenon_X84)
% 2.08/2.29  ((a63) != (a95))
% 2.08/2.29  ((a96) != zenon_X15)
% 2.08/2.29  (zenon_X16 != (a97))
% 2.08/2.29  (c6_2 zenon_X7 (a95))
% 2.08/2.29  ((a137) != zenon_X75)
% 2.08/2.29  ((a31) != zenon_X82)
% 2.08/2.29  (c5_2 zenon_X20 (a95))
% 2.08/2.29  (zenon_X9 != (a65))
% 2.08/2.29  (c5_2 (a59) (a108))
% 2.08/2.29  (c7_2 (a34) (a95))
% 2.08/2.29  ((a121) != zenon_X23)
% 2.08/2.29  ((a108) != zenon_X153)
% 2.08/2.29  ((a130) != (a97))
% 2.08/2.29  (-. (c8_2 (a65) zenon_X26))
% 2.08/2.29  (c1_2 (a127) (a95))
% 2.08/2.29  ((a58) != (a108))
% 2.08/2.29  ((a127) != zenon_X10)
% 2.08/2.29  (zenon_X9 != zenon_X36)
% 2.08/2.29  ((a97) != zenon_X143)
% 2.08/2.29  (zenon_X23 != (a29))
% 2.08/2.29  ((a108) != (a95))
% 2.08/2.29  (c3_1 (a68))
% 2.08/2.29  (c1_2 (a136) (a82))
% 2.08/2.29  (c3_1 (a51))
% 2.08/2.29  ((a57) != zenon_X85)
% 2.08/2.29  ((a137) != zenon_X161)
% 2.08/2.29  (c8_2 (a122) zenon_X14)
% 2.08/2.29  ((a68) != zenon_X6)
% 2.08/2.29  (-. (c3_2 (a93) zenon_X115))
% 2.08/2.29  (c7_2 (a39) (a57))
% 2.08/2.29  (-. (c2_1 zenon_X24))
% 2.08/2.29  ((a30) != zenon_X52)
% 2.08/2.29  ((a58) != (a123))
% 2.08/2.29  (-. (c5_2 (a122) zenon_X147))
% 2.08/2.29  (ndr1_1 (a127))
% 2.08/2.29  (c1_2 zenon_X23 (a30))
% 2.08/2.29  ((a114) != zenon_X70)
% 2.08/2.29  ((a31) != (a41))
% 2.08/2.29  ((a30) != zenon_X60)
% 2.08/2.29  (-. (c5_2 (a59) zenon_X79))
% 2.08/2.29  (-. (c6_2 (a39) (a31)))
% 2.08/2.29  (c1_2 zenon_X7 (a130))
% 2.08/2.29  (c1_2 (a47) (a95))
% 2.08/2.29  (-. (c4_2 (a18) zenon_X147))
% 2.08/2.29  ((a29) != (a34))
% 2.08/2.29  ((a57) != zenon_X152)
% 2.08/2.29  (c8_2 (a29) (a49))
% 2.08/2.29  ((a40) != zenon_X197)
% 2.08/2.29  (c1_2 (a39) zenon_X8)
% 2.08/2.29  ((a117) != zenon_X3)
% 2.08/2.29  (c6_2 zenon_X36 (a130))
% 2.08/2.29  ((a33) != zenon_X43)
% 2.08/2.29  ((a51) != zenon_X15)
% 2.08/2.29  ((a137) != zenon_X189)
% 2.08/2.29  (-. (c7_2 (a117) (a115)))
% 2.08/2.29  ((a82) != zenon_X22)
% 2.08/2.29  (c1_2 (a65) (a108))
% 2.08/2.29  ((a81) != (a29))
% 2.08/2.29  (c6_2 zenon_X36 (a57))
% 2.08/2.29  ((a59) != (a29))
% 2.08/2.29  (-. (c6_1 (a51)))
% 2.08/2.29  (c8_1 (a68))
% 2.08/2.29  (c6_1 (a39))
% 2.08/2.29  (-. (c1_1 (a104)))
% 2.08/2.29  (c8_2 (a117) (a97))
% 2.08/2.29  ((a123) != zenon_X78)
% 2.08/2.29  (c8_2 (a93) (a82))
% 2.08/2.29  ((a137) != zenon_X32)
% 2.08/2.29  ((a96) != zenon_X6)
% 2.08/2.29  (c1_2 (a65) zenon_X39)
% 2.08/2.29  (c8_2 (a104) (a58))
% 2.08/2.29  (zenon_X10 != (a104))
% 2.08/2.29  (c1_1 zenon_X10)
% 2.08/2.29  ((a30) != zenon_X14)
% 2.08/2.29  ((a108) != zenon_X86)
% 2.08/2.29  ((a57) != zenon_X113)
% 2.08/2.29  (-. (c2_2 zenon_X20 (a63)))
% 2.08/2.29  ((a137) != zenon_X104)
% 2.08/2.29  (-. (c5_2 (a122) (a31)))
% 2.08/2.29  ((a30) != zenon_X64)
% 2.08/2.29  (c8_2 (a39) (a115))
% 2.08/2.29  (-. (c7_1 zenon_X10))
% 2.08/2.29  (c6_2 (a51) (a130))
% 2.08/2.29  (-. (c4_2 (a18) zenon_X78))
% 2.08/2.29  (zenon_X20 != zenon_X3)
% 2.08/2.29  (zenon_X151 != zenon_X22)
% 2.08/2.29  (c1_2 (a18) (a41))
% 2.08/2.29  (-. (c8_2 (a65) zenon_X153))
% 2.08/2.29  ((a137) != zenon_X82)
% 2.08/2.29  ((a59) != (a121))
% 2.08/2.29  (c6_2 (a122) (a57))
% 2.08/2.29  ((a95) != zenon_X44)
% 2.08/2.29  (zenon_X35 != (a130))
% 2.08/2.29  (c1_2 (a96) (a30))
% 2.08/2.29  (-. (c6_2 zenon_X15 (a41)))
% 2.08/2.29  (c1_2 (a39) (a40))
% 2.08/2.29  (-. (c5_2 zenon_X38 zenon_X79))
% 2.08/2.29  (-. (c3_2 zenon_X11 zenon_X139))
% 2.08/2.29  (zenon_X71 != zenon_X32)
% 2.08/2.29  ((a97) != (a108))
% 2.08/2.29  ((a30) != zenon_X21)
% 2.08/2.29  (-. (c7_2 (a93) zenon_X73))
% 2.08/2.29  ((a68) != zenon_X9)
% 2.08/2.29  (zenon_X53 != zenon_X83)
% 2.08/2.29  (zenon_X42 != zenon_X72)
% 2.08/2.29  (c4_1 (a117))
% 2.08/2.29  (-. (c1_1 zenon_X30))
% 2.08/2.29  ((a57) != zenon_X134)
% 2.08/2.29  (-. (c5_2 zenon_X11 zenon_X147))
% 2.08/2.29  ((a108) != zenon_X152)
% 2.08/2.29  (c2_1 (a68))
% 2.08/2.29  ((a49) != zenon_X110)
% 2.08/2.29  ((a59) != (a96))
% 2.08/2.29  (-. (c6_2 zenon_X9 (a31)))
% 2.08/2.29  ((a30) != zenon_X84)
% 2.08/2.29  ((a96) != zenon_X9)
% 2.08/2.29  ((a81) != (a47))
% 2.08/2.29  ((a82) != zenon_X124)
% 2.08/2.29  ((a18) != (a81))
% 2.08/2.29  (zenon_X20 != zenon_X9)
% 2.08/2.29  (-. (c7_2 (a93) zenon_X32))
% 2.08/2.29  ((a137) != zenon_X51)
% 2.08/2.29  (zenon_X70 != (a115))
% 2.08/2.29  (c4_2 (a51) (a49))
% 2.08/2.29  ((a123) != zenon_X104)
% 2.08/2.29  (c4_2 (a65) zenon_X147)
% 2.08/2.29  ((a30) != zenon_X76)
% 2.08/2.29  ((a57) != zenon_X142)
% 2.08/2.29  (zenon_X7 != zenon_X6)
% 2.08/2.29  (zenon_X53 != zenon_X70)
% 2.08/2.29  ((a29) != (a122))
% 2.08/2.29  ((a130) != zenon_X16)
% 2.08/2.29  (c5_2 (a65) zenon_X86)
% 2.08/2.29  (c1_2 (a65) (a131))
% 2.08/2.29  ((a82) != zenon_X56)
% 2.08/2.29  (-. (c3_2 (a47) (a58)))
% 2.08/2.29  ((a41) != zenon_X12)
% 2.08/2.29  ((a41) != zenon_X32)
% 2.08/2.29  (-. (c3_2 (a18) zenon_X149))
% 2.08/2.29  ((a30) != zenon_X22)
% 2.08/2.29  ((a57) != zenon_X61)
% 2.08/2.29  (c1_2 (a51) (a115))
% 2.08/2.29  ((a57) != zenon_X109)
% 2.08/2.29  (c7_2 (a39) zenon_X42)
% 2.08/2.29  ((a57) != zenon_X131)
% 2.08/2.29  (c6_0)
% 2.08/2.29  ((a137) != zenon_X35)
% 2.08/2.29  (c1_2 (a65) (a82))
% 2.08/2.29  (-. (c4_2 (a47) zenon_X47))
% 2.08/2.29  (c1_2 (a29) (a114))
% 2.08/2.29  (-. (c5_2 zenon_X11 (a31)))
% 2.08/2.29  (c8_2 (a129) zenon_X70)
% 2.08/2.29  (zenon_X78 != zenon_X22)
% 2.08/2.29  (c8_2 (a117) zenon_X53)
% 2.08/2.29  (zenon_X53 != zenon_X8)
% 2.08/2.29  ((a93) != zenon_X28)
% 2.08/2.29  (c4_2 (a122) (a63))
% 2.08/2.29  (c7_2 (a136) zenon_X73)
% 2.08/2.29  (zenon_X22 != zenon_X29)
% 2.08/2.29  ((a49) != zenon_X79)
% 2.08/2.29  (c1_2 (a39) zenon_X71)
% 2.08/2.29  ((a131) != zenon_X197)
% 2.08/2.29  ((a114) != zenon_X79)
% 2.08/2.29  (c1_2 (a51) (a97))
% 2.08/2.29  (c5_2 (a121) (a115))
% 2.08/2.29  (-. (c5_2 zenon_X11 (a49)))
% 2.08/2.29  (-. (c5_2 zenon_X11 (a108)))
% 2.08/2.29  ((a95) != zenon_X111)
% 2.08/2.29  (-. (c5_2 (a127) (a63)))
% 2.08/2.29  ((a58) != zenon_X152)
% 2.08/2.29  ((a82) != zenon_X45)
% 2.08/2.29  (c8_2 (a117) (a114))
% 2.08/2.29  (zenon_X151 != (a115))
% 2.08/2.29  (c4_1 (a68))
% 2.08/2.29  (c8_2 (a122) zenon_X71)
% 2.08/2.29  (c1_2 (a121) (a130))
% 2.08/2.29  (-. (c6_2 (a18) (a130)))
% 2.08/2.29  ((a131) != (a40))
% 2.08/2.29  (zenon_X26 != (a108))
% 2.08/2.29  (c7_1 (a68))
% 2.08/2.29  ((a68) != zenon_X38)
% 2.08/2.29  ((a82) != zenon_X96)
% 2.08/2.29  ((a95) != zenon_X197)
% 2.08/2.29  ((a59) != (a129))
% 2.08/2.29  (-. (c6_2 (a29) zenon_X96))
% 2.08/2.29  ((a57) != (a58))
% 2.08/2.29  ((a30) != zenon_X51)
% 2.08/2.29  ((a130) != zenon_X84)
% 2.08/2.29  (c3_2 (a127) (a57))
% 2.08/2.29  ((a114) != zenon_X147)
% 2.08/2.29  (-. (c6_2 (a104) zenon_X196))
% 2.08/2.29  (-. (c2_2 (a96) zenon_X57))
% 2.08/2.29  ((a68) != (a51))
% 2.08/2.29  ((a82) != (a33))
% 2.08/2.29  ((a68) != zenon_X18)
% 2.08/2.29  (c7_1 (a59))
% 2.08/2.29  (-. (ndr1_1 zenon_X9))
% 2.08/2.29  (c1_2 (a65) (a41))
% 2.08/2.29  (-. (c2_2 zenon_X23 (a63)))
% 2.08/2.29  (c8_2 (a39) (a49))
% 2.08/2.29  ((a30) != zenon_X68)
% 2.08/2.29  ((a33) != (a31))
% 2.08/2.29  ((a136) != zenon_X27)
% 2.08/2.29  ((a130) != zenon_X52)
% 2.08/2.29  ((a51) != zenon_X18)
% 2.08/2.29  (-. (c5_2 (a122) (a97)))
% 2.08/2.29  ((a108) != zenon_X100)
% 2.08/2.29  (zenon_X35 != zenon_X8)
% 2.08/2.29  (-. (c7_2 (a93) zenon_X35))
% 2.08/2.29  ((a95) != zenon_X95)
% 2.08/2.29  (-. (c3_2 (a136) (a58)))
% 2.08/2.29  (zenon_X3 != zenon_X9)
% 2.08/2.29  ((a57) != zenon_X65)
% 2.08/2.29  ((a63) != zenon_X197)
% 2.08/2.29  (c8_2 (a122) (a97))
% 2.08/2.29  ((a18) != (a129))
% 2.08/2.29  ((a63) != (a82))
% 2.08/2.29  ((a34) != zenon_X28)
% 2.08/2.29  (c1_2 (a18) (a130))
% 2.08/2.29  ((a97) != zenon_X120)
% 2.08/2.29  (c7_2 (a39) (a115))
% 2.08/2.29  ((a59) != (a117))
% 2.08/2.29  (c8_2 (a93) zenon_X53)
% 2.08/2.29  ((a95) != zenon_X222)
% 2.08/2.29  (zenon_X42 != zenon_X2)
% 2.08/2.29  (c6_2 (a68) (a137))
% 2.08/2.29  (-. (c5_2 (a93) (a137)))
% 2.08/2.29  ((a96) != (a34))
% 2.08/2.29  ((a114) != (a123))
% 2.08/2.29  (c1_2 zenon_X7 (a30))
% 2.08/2.29  (c7_1 (a93))
% 2.08/2.29  (-. (c8_2 (a65) zenon_X79))
% 2.08/2.29  (c3_1 (a65))
% 2.08/2.29  ((a137) != zenon_X100)
% 2.08/2.29  (zenon_X24 != zenon_X28)
% 2.08/2.29  (zenon_X101 != (a130))
% 2.08/2.29  (-. (c1_2 (a104) zenon_X8))
% 2.08/2.29  (c5_2 (a47) (a30))
% 2.08/2.29  (-. (c3_1 zenon_X10))
% 2.08/2.29  (-. (c5_2 zenon_X20 (a63)))
% 2.08/2.29  (c6_1 (a65))
% 2.08/2.29  ((a121) != zenon_X9)
% 2.08/2.29  ((a82) != zenon_X66)
% 2.08/2.29  ((a137) != (a95))
% 2.08/2.29  ((a137) != zenon_X52)
% 2.08/2.29  (c6_2 zenon_X27 (a58))
% 2.08/2.29  ((a57) != zenon_X80)
% 2.08/2.29  (zenon_X18 != zenon_X36)
% 2.08/2.29  (c1_2 (a136) (a30))
% 2.08/2.29  (zenon_X26 != (a115))
% 2.08/2.29  (c1_2 (a117) (a115))
% 2.08/2.29  (zenon_X40 != (a51))
% 2.08/2.29  (c3_1 (a127))
% 2.08/2.29  (-. (c5_1 (a127)))
% 2.08/2.29  ((a97) != zenon_X211)
% 2.08/2.29  (-. (c6_2 zenon_X11 (a30)))
% 2.08/2.29  (-. (c7_2 (a93) (a97)))
% 2.08/2.29  (c3_2 zenon_X20 (a57))
% 2.08/2.29  (c4_2 (a136) (a63))
% 2.08/2.29  (c1_2 (a18) (a57))
% 2.08/2.29  (c7_2 (a136) zenon_X8)
% 2.08/2.29  (zenon_X42 != (a108))
% 2.08/2.29  ((a40) != zenon_X193)
% 2.08/2.29  (-. (c5_2 (a39) (a58)))
% 2.08/2.29  *)
% 2.08/2.29  (* NO-PROOF *)
% 2.08/2.29  % SZS status GaveUp
% 2.08/2.29  Number of rewrites on terms: 0
% 2.08/2.29  Number of rewrites on props: 0
% 2.08/2.29  nodes searched: 72952
% 2.08/2.29  max branch formulas: 5529
% 2.08/2.29  proof nodes created: 1565
% 2.08/2.29  formulas created: 71619
% 2.08/2.29  
%------------------------------------------------------------------------------