ZenonModulo---0.5.0.UNK-Non.f

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

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

% Result   : Unknown 1.06s 1.22s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13  % Problem  : SYN422+1 : TPTP v8.2.0. Released v2.1.0.
% 0.13/0.13  % Command  : run_zenon_modulo %d %s
% 0.14/0.34  % Computer : n013.cluster.edu
% 0.14/0.34  % Model    : x86_64 x86_64
% 0.14/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34  % Memory   : 8042.1875MB
% 0.14/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34  % CPULimit : 300
% 0.14/0.34  % WCLimit  : 300
% 0.14/0.34  % DateTime : Sun Jun 23 23:41:09 EDT 2024
% 0.14/0.34  % CPUTime  : 
% 1.06/1.21  Zenon error: exhausted search space without finding a proof
% 1.06/1.21  (* Current branch:
% 1.06/1.21  (c2_2 (a622) (a623))
% 1.06/1.21  (-. (c4_2 (a628) (a657)))
% 1.06/1.21  ((a730) != (a731))
% 1.06/1.21  (-. (c4_2 zenon_X23 zenon_X24))
% 1.06/1.21  ((a732) != zenon_X58)
% 1.06/1.21  ((a656) != (a669))
% 1.06/1.21  ((a731) != zenon_X55)
% 1.06/1.21  ((a710) != (a677))
% 1.06/1.21  (zenon_X42 != zenon_X46)
% 1.06/1.21  (zenon_X16 != zenon_X56)
% 1.06/1.21  (zenon_X16 != (a629))
% 1.06/1.21  (zenon_X43 != (a664))
% 1.06/1.21  ((a623) != zenon_X29)
% 1.06/1.21  (c10_2 zenon_X9 (a623))
% 1.06/1.21  (-. (c5_1 (a639)))
% 1.06/1.21  (c4_2 (a618) (a640))
% 1.06/1.21  (-. (c1_2 (a737) zenon_X29))
% 1.06/1.21  (-. (c5_1 (a670)))
% 1.06/1.21  ((a732) != zenon_X42)
% 1.06/1.21  (zenon_X25 != (a709))
% 1.06/1.21  (-. (c3_2 zenon_X7 (a732)))
% 1.06/1.21  (c7_2 (a690) (a754))
% 1.06/1.21  (zenon_X38 != (a677))
% 1.06/1.21  ((a754) != (a677))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a626)))
% 1.06/1.21  (c9_2 (a737) (a731))
% 1.06/1.21  ((a625) != zenon_X2)
% 1.06/1.21  ((a732) != zenon_X80)
% 1.06/1.21  ((a714) != zenon_X48)
% 1.06/1.21  ((a626) != zenon_X52)
% 1.06/1.21  (-. (c2_1 (a709)))
% 1.06/1.21  (-. (c3_2 zenon_X7 zenon_X8))
% 1.06/1.21  (zenon_X20 != (a737))
% 1.06/1.21  ((a657) != zenon_X50)
% 1.06/1.21  (c8_2 (a618) (a629))
% 1.06/1.21  ((a690) != (a737))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a623)))
% 1.06/1.21  (-. (c2_1 (a670)))
% 1.06/1.21  ((a755) != zenon_X2)
% 1.06/1.21  (-. (c3_2 zenon_X7 zenon_X42))
% 1.06/1.21  (-. (c1_2 (a737) (a662)))
% 1.06/1.21  (c8_2 (a618) (a657))
% 1.06/1.21  (zenon_X58 != zenon_X49)
% 1.06/1.21  (c7_2 (a708) zenon_X58)
% 1.06/1.21  ((a623) != zenon_X12)
% 1.06/1.21  (-. (c4_2 (a729) zenon_X53))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X1))
% 1.06/1.21  ((a737) != (a658))
% 1.06/1.21  (c1_2 (a669) (a640))
% 1.06/1.21  (-. (c4_2 (a729) zenon_X49))
% 1.06/1.21  (c8_2 (a753) (a738))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X19))
% 1.06/1.21  ((a670) != (a628))
% 1.06/1.21  ((a670) != zenon_X7)
% 1.06/1.21  (-. (c4_2 zenon_X23 (a738)))
% 1.06/1.21  ((a657) != zenon_X53)
% 1.06/1.21  (-. (c4_2 zenon_X25 (a744)))
% 1.06/1.21  ((a744) != zenon_X55)
% 1.06/1.21  ((a709) != (a625))
% 1.06/1.21  (-. (c4_2 (a658) (a629)))
% 1.06/1.21  (c9_1 (a618))
% 1.06/1.21  ((a690) != (a755))
% 1.06/1.21  ((a755) != (a625))
% 1.06/1.21  (-. (c6_1 (a670)))
% 1.06/1.21  ((a618) != zenon_X2)
% 1.06/1.21  (c7_2 zenon_X7 (a732))
% 1.06/1.21  (ndr1_1 (a670))
% 1.06/1.21  ((a731) != (a662))
% 1.06/1.21  ((a738) != zenon_X58)
% 1.06/1.21  ((a744) != (a710))
% 1.06/1.21  (-. (c4_2 (a737) (a623)))
% 1.06/1.21  (-. (c4_2 (a625) zenon_X65))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a754)))
% 1.06/1.21  (zenon_X16 != zenon_X72)
% 1.06/1.21  (zenon_X20 != (a622))
% 1.06/1.21  (-. (c4_2 (a628) zenon_X8))
% 1.06/1.21  (-. (c3_2 (a729) (a677)))
% 1.06/1.21  (c8_2 (a753) (a664))
% 1.06/1.21  (-. (c4_2 (a628) (a626)))
% 1.06/1.21  ((a732) != (a744))
% 1.06/1.21  (-. (c3_2 zenon_X7 (a626)))
% 1.06/1.21  (c7_2 (a701) (a732))
% 1.06/1.21  ((a662) != (a714))
% 1.06/1.21  ((a732) != zenon_X52)
% 1.06/1.21  (c1_1 (a656))
% 1.06/1.21  ((a669) != zenon_X28)
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X43))
% 1.06/1.21  (c8_2 (a618) zenon_X10)
% 1.06/1.21  ((a754) != zenon_X26)
% 1.06/1.21  ((a629) != zenon_X60)
% 1.06/1.21  ((a657) != (a662))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X54))
% 1.06/1.21  (-. (c4_2 (a658) (a731)))
% 1.06/1.21  ((a744) != zenon_X1)
% 1.06/1.21  ((a731) != (a691))
% 1.06/1.21  ((a730) != (a629))
% 1.06/1.21  ((a629) != zenon_X48)
% 1.06/1.21  (-. (c3_2 (a669) zenon_X8))
% 1.06/1.21  ((a657) != (a629))
% 1.06/1.21  ((a662) != zenon_X1)
% 1.06/1.21  (zenon_X11 != (a731))
% 1.06/1.21  (c9_2 (a737) (a738))
% 1.06/1.21  (-. (c4_2 (a628) (a738)))
% 1.06/1.21  ((a744) != zenon_X11)
% 1.06/1.21  (c5_2 (a669) zenon_X8)
% 1.06/1.21  ((a738) != (a691))
% 1.06/1.21  (zenon_X20 != (a669))
% 1.06/1.21  (-. (c3_2 (a622) (a744)))
% 1.06/1.21  (c4_2 (a622) (a732))
% 1.06/1.21  (zenon_X23 != zenon_X2)
% 1.06/1.21  ((a731) != zenon_X38)
% 1.06/1.21  (zenon_X42 != zenon_X48)
% 1.06/1.21  (c4_2 (a669) zenon_X72)
% 1.06/1.21  (-. (c4_2 zenon_X25 (a657)))
% 1.06/1.21  (c10_2 (a669) zenon_X11)
% 1.06/1.21  (-. (c3_2 zenon_X4 (a640)))
% 1.06/1.21  ((a623) != zenon_X27)
% 1.06/1.21  (zenon_X12 != zenon_X46)
% 1.06/1.21  ((a662) != zenon_X42)
% 1.06/1.21  (-. (c3_2 zenon_X7 zenon_X48))
% 1.06/1.21  ((a658) != (a670))
% 1.06/1.21  (-. (c3_2 (a639) zenon_X70))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X42))
% 1.06/1.21  (zenon_X10 != zenon_X26)
% 1.06/1.21  ((a623) != zenon_X44)
% 1.06/1.21  (-. (c3_2 (a639) (a657)))
% 1.06/1.21  (-. (c3_2 (a729) zenon_X49))
% 1.06/1.21  (-. (c3_2 (a628) (a744)))
% 1.06/1.21  (-. (c4_2 (a625) (a629)))
% 1.06/1.21  (zenon_X20 != (a628))
% 1.06/1.21  ((a702) != zenon_X79)
% 1.06/1.21  (zenon_X1 != (a677))
% 1.06/1.21  ((a702) != zenon_X46)
% 1.06/1.21  (c9_1 (a737))
% 1.06/1.21  ((a629) != (a691))
% 1.06/1.21  ((a629) != zenon_X54)
% 1.06/1.21  (-. (c3_2 (a729) (a732)))
% 1.06/1.21  (-. (c7_2 (a755) zenon_X0))
% 1.06/1.21  ((a626) != (a714))
% 1.06/1.21  (zenon_X40 != zenon_X8)
% 1.06/1.21  (c7_2 (a690) (a629))
% 1.06/1.21  ((a753) != (a701))
% 1.06/1.21  ((a744) != zenon_X26)
% 1.06/1.21  (c4_2 (a669) (a731))
% 1.06/1.21  (zenon_X48 != zenon_X39)
% 1.06/1.21  ((a623) != zenon_X53)
% 1.06/1.21  (c7_2 (a690) zenon_X10)
% 1.06/1.21  (-. (c3_2 (a625) (a744)))
% 1.06/1.21  (c3_2 (a669) zenon_X52)
% 1.06/1.21  ((a702) != zenon_X11)
% 1.06/1.21  (-. (c4_2 (a628) (a664)))
% 1.06/1.21  ((a737) != (a656))
% 1.06/1.21  (zenon_X55 != zenon_X79)
% 1.06/1.21  (-. (c3_2 (a701) (a738)))
% 1.06/1.21  ((a618) != (a670))
% 1.06/1.21  ((a732) != zenon_X44)
% 1.06/1.21  (-. (c4_2 (a618) zenon_X48))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a662)))
% 1.06/1.21  ((a657) != zenon_X39)
% 1.06/1.21  ((a626) != zenon_X49)
% 1.06/1.21  (zenon_X10 != zenon_X56)
% 1.06/1.21  ((a690) != (a625))
% 1.06/1.21  (-. (c3_2 (a628) (a702)))
% 1.06/1.21  ((a628) != (a721))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X53))
% 1.06/1.21  ((a738) != (a664))
% 1.06/1.21  (c10_2 zenon_X9 (a664))
% 1.06/1.21  (c10_2 zenon_X9 (a657))
% 1.06/1.21  (zenon_X58 != zenon_X39)
% 1.06/1.21  ((a664) != (a677))
% 1.06/1.21  (c8_2 (a618) (a754))
% 1.06/1.21  (zenon_X16 != zenon_X39)
% 1.06/1.21  ((a662) != (a640))
% 1.06/1.21  ((a628) != (a625))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a629)))
% 1.06/1.21  (c4_2 (a669) zenon_X40)
% 1.06/1.21  (c8_2 (a753) (a754))
% 1.06/1.21  (c9_1 (a625))
% 1.06/1.21  (-. (c3_2 (a701) zenon_X53))
% 1.06/1.21  (-. (c6_1 zenon_X6))
% 1.06/1.21  ((a664) != zenon_X46)
% 1.06/1.21  ((a737) != zenon_X4)
% 1.06/1.21  ((a744) != zenon_X60)
% 1.06/1.21  (-. (c4_2 (a737) (a677)))
% 1.06/1.21  ((a744) != zenon_X51)
% 1.06/1.21  (c2_1 (a622))
% 1.06/1.21  ((a730) != zenon_X60)
% 1.06/1.21  ((a701) != (a639))
% 1.06/1.21  (-. (c7_2 (a755) (a738)))
% 1.06/1.21  (c4_2 (a669) (a732))
% 1.06/1.21  ((a664) != (a691))
% 1.06/1.21  (-. (c3_2 (a639) zenon_X40))
% 1.06/1.21  (zenon_X82 != (a662))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X79))
% 1.06/1.21  (-. (c4_2 (a729) zenon_X40))
% 1.06/1.21  (-. (c1_2 zenon_X28 (a738)))
% 1.06/1.21  (zenon_X23 != zenon_X4)
% 1.06/1.21  (-. (c5_2 (a628) (a629)))
% 1.06/1.21  ((a629) != (a714))
% 1.06/1.21  (-. (c3_2 zenon_X7 zenon_X19))
% 1.06/1.21  (-. (c3_1 (a670)))
% 1.06/1.21  (c4_2 (a618) (a754))
% 1.06/1.21  (-. (c8_1 (a656)))
% 1.06/1.21  ((a709) != (a656))
% 1.06/1.21  ((a626) != (a677))
% 1.06/1.21  (c3_2 (a658) (a731))
% 1.06/1.21  ((a626) != (a657))
% 1.06/1.21  (-. (c4_2 (a755) zenon_X75))
% 1.06/1.21  (-. (c1_2 (a622) zenon_X15))
% 1.06/1.21  (-. (c4_2 (a737) zenon_X48))
% 1.06/1.21  (-. (c4_2 (a729) zenon_X48))
% 1.06/1.21  ((a732) != (a623))
% 1.06/1.21  (c7_2 (a708) (a730))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X51))
% 1.06/1.21  ((a662) != zenon_X48)
% 1.06/1.21  (-. (c10_2 (a690) (a691)))
% 1.06/1.21  ((a709) != zenon_X7)
% 1.06/1.21  (-. (c4_2 (a729) (a662)))
% 1.06/1.21  (c1_2 (a669) (a754))
% 1.06/1.21  ((a732) != zenon_X62)
% 1.06/1.21  ((a623) != zenon_X63)
% 1.06/1.21  (-. (c4_2 (a690) zenon_X46))
% 1.06/1.21  (-. (c3_2 (a628) (a732)))
% 1.06/1.21  (-. (c4_2 zenon_X20 zenon_X78))
% 1.06/1.21  (-. (c5_2 (a708) zenon_X39))
% 1.06/1.21  (zenon_X55 != zenon_X66)
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X38))
% 1.06/1.21  (-. (c8_1 (a737)))
% 1.06/1.21  ((a731) != zenon_X53)
% 1.06/1.21  ((a670) != zenon_X4)
% 1.06/1.21  (c9_1 zenon_X23)
% 1.06/1.21  (-. (c7_2 (a755) (a662)))
% 1.06/1.21  ((a744) != zenon_X61)
% 1.06/1.21  ((a664) != zenon_X54)
% 1.06/1.21  ((a625) != zenon_X21)
% 1.06/1.21  ((a732) != zenon_X26)
% 1.06/1.21  (-. (c4_2 (a656) (a662)))
% 1.06/1.21  (-. (c3_2 (a622) (a662)))
% 1.06/1.21  ((a622) != (a669))
% 1.06/1.21  (c1_2 (a669) zenon_X43)
% 1.06/1.21  ((a618) != (a755))
% 1.06/1.21  (-. (c3_2 (a628) zenon_X48))
% 1.06/1.21  (c7_2 (a708) (a738))
% 1.06/1.21  (zenon_X70 != zenon_X72)
% 1.06/1.21  (-. (c9_2 (a729) (a730)))
% 1.06/1.21  (c9_1 (a701))
% 1.06/1.21  (c7_2 (a618) zenon_X10)
% 1.06/1.21  (zenon_X17 != (a755))
% 1.06/1.21  ((a744) != zenon_X39)
% 1.06/1.21  (-. (c2_1 (a755)))
% 1.06/1.21  (c7_2 zenon_X21 (a732))
% 1.06/1.21  (zenon_X20 != (a753))
% 1.06/1.21  ((a626) != zenon_X19)
% 1.06/1.21  ((a618) != zenon_X4)
% 1.06/1.21  (zenon_X16 != (a640))
% 1.06/1.21  (-. (c9_1 (a755)))
% 1.06/1.21  (c8_2 (a753) (a702))
% 1.06/1.21  (c7_2 (a628) (a732))
% 1.06/1.21  (c7_2 (a708) zenon_X70)
% 1.06/1.21  ((a754) != zenon_X79)
% 1.06/1.21  (c4_1 (a622))
% 1.06/1.21  (c4_2 (a669) zenon_X19)
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X48))
% 1.06/1.21  (-. (c4_2 (a658) zenon_X16))
% 1.06/1.21  (zenon_X24 != zenon_X56)
% 1.06/1.21  ((a626) != zenon_X15)
% 1.06/1.21  (-. (c1_2 (a622) (a664)))
% 1.06/1.21  ((a754) != zenon_X66)
% 1.06/1.21  (zenon_X29 != zenon_X57)
% 1.06/1.21  (-. (c4_2 (a628) zenon_X46))
% 1.06/1.21  (-. (c3_2 (a656) (a629)))
% 1.06/1.21  (c10_2 (a669) zenon_X41)
% 1.06/1.21  (-. (c3_2 (a622) zenon_X10))
% 1.06/1.21  (c4_2 (a669) (a657))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X42))
% 1.06/1.21  (c7_2 (a690) (a640))
% 1.06/1.21  (c4_2 (a669) zenon_X55)
% 1.06/1.21  (zenon_X16 != zenon_X79)
% 1.06/1.21  ((a738) != zenon_X1)
% 1.06/1.21  (zenon_X20 != zenon_X2)
% 1.06/1.21  ((a744) != zenon_X64)
% 1.06/1.21  (-. (c6_2 (a709) (a710)))
% 1.06/1.21  (-. (c4_2 (a690) (a664)))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a657)))
% 1.06/1.21  (-. (c3_2 zenon_X2 (a677)))
% 1.06/1.21  ((a701) != (a669))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X40))
% 1.06/1.21  (zenon_X16 != zenon_X8)
% 1.06/1.21  (-. (c9_1 (a729)))
% 1.06/1.21  ((a640) != (a732))
% 1.06/1.21  (ndr1_1 (a729))
% 1.06/1.21  (zenon_X25 != (a670))
% 1.06/1.21  (-. (c3_2 (a701) zenon_X66))
% 1.06/1.21  ((a623) != (a714))
% 1.06/1.21  (-. (c3_2 (a656) (a626)))
% 1.06/1.21  ((a629) != zenon_X56)
% 1.06/1.21  (c8_2 (a753) (a732))
% 1.06/1.21  (-. (c3_2 (a701) (a662)))
% 1.06/1.21  (c7_2 (a690) zenon_X82)
% 1.06/1.21  (c2_1 (a690))
% 1.06/1.21  (zenon_X82 != zenon_X56)
% 1.06/1.21  ((a662) != zenon_X26)
% 1.06/1.21  (-. (c3_2 zenon_X2 zenon_X70))
% 1.06/1.21  ((a664) != zenon_X38)
% 1.06/1.21  ((a731) != zenon_X49)
% 1.06/1.21  ((a656) != zenon_X7)
% 1.06/1.21  (c9_2 (a618) (a731))
% 1.06/1.21  ((a664) != (a702))
% 1.06/1.21  (-. (c3_2 (a639) (a640)))
% 1.06/1.21  (zenon_X48 != zenon_X54)
% 1.06/1.21  (-. (c4_2 (a729) zenon_X1))
% 1.06/1.21  (-. (c4_2 (a625) (a738)))
% 1.06/1.21  (c3_2 (a669) (a626))
% 1.06/1.21  (c7_2 (a670) (a714))
% 1.06/1.21  ((a755) != zenon_X4)
% 1.06/1.21  ((a744) != zenon_X0)
% 1.06/1.21  ((a738) != (a640))
% 1.06/1.21  (-. (c3_2 (a622) (a702)))
% 1.06/1.21  ((a690) != zenon_X7)
% 1.06/1.21  (-. (c3_2 (a625) zenon_X16))
% 1.06/1.21  ((a754) != (a731))
% 1.06/1.21  (-. (c1_2 (a622) (a629)))
% 1.06/1.21  (zenon_X41 != (a626))
% 1.06/1.21  (-. (c3_2 (a737) (a744)))
% 1.06/1.21  (c7_2 (a618) (a640))
% 1.06/1.21  ((a744) != zenon_X56)
% 1.06/1.21  (-. (c5_2 (a708) zenon_X56))
% 1.06/1.21  (-. (c4_2 (a729) (a657)))
% 1.06/1.21  ((a664) != zenon_X58)
% 1.06/1.21  ((a744) != zenon_X66)
% 1.06/1.21  ((a623) != zenon_X79)
% 1.06/1.21  (zenon_X20 != zenon_X23)
% 1.06/1.21  ((a690) != (a669))
% 1.06/1.21  ((a618) != zenon_X23)
% 1.06/1.21  (-. (c3_2 (a639) (a626)))
% 1.06/1.21  (zenon_X58 != zenon_X66)
% 1.06/1.21  (-. (c10_2 (a618) zenon_X15))
% 1.06/1.21  (-. (c3_2 (a639) (a744)))
% 1.06/1.21  (c3_0)
% 1.06/1.21  ((a656) != zenon_X23)
% 1.06/1.21  (-. (c3_2 (a639) zenon_X8))
% 1.06/1.21  (c3_2 (a709) (a714))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X11))
% 1.06/1.21  ((a702) != zenon_X66)
% 1.06/1.21  ((a640) != zenon_X66)
% 1.06/1.21  (-. (c3_2 zenon_X2 zenon_X52))
% 1.06/1.21  (-. (c4_2 zenon_X23 zenon_X56))
% 1.06/1.21  (zenon_X19 != zenon_X66)
% 1.06/1.21  (-. (c3_2 (a639) (a623)))
% 1.06/1.21  (c9_1 zenon_X20)
% 1.06/1.21  (zenon_X52 != zenon_X8)
% 1.06/1.21  (-. (c4_2 (a656) (a738)))
% 1.06/1.21  (zenon_X48 != (a738))
% 1.06/1.21  ((a702) != zenon_X15)
% 1.06/1.21  (-. (c3_2 zenon_X2 zenon_X66))
% 1.06/1.21  ((a628) != zenon_X23)
% 1.06/1.21  (-. (c4_2 (a737) zenon_X66))
% 1.06/1.21  (-. (c4_2 (a622) (a662)))
% 1.06/1.21  (-. (c3_2 (a628) (a731)))
% 1.06/1.21  ((a618) != (a729))
% 1.06/1.21  (-. (c4_2 zenon_X23 zenon_X82))
% 1.06/1.21  (-. (c3_2 zenon_X7 zenon_X51))
% 1.06/1.21  (zenon_X7 != (a639))
% 1.06/1.21  (zenon_X72 != (a640))
% 1.06/1.21  ((a640) != (a664))
% 1.06/1.21  (c1_0)
% 1.06/1.21  (c6_2 (a669) (a754))
% 1.06/1.21  ((a618) != (a639))
% 1.06/1.21  (-. (c3_2 (a753) (a732)))
% 1.06/1.21  (-. (c3_2 (a753) zenon_X1))
% 1.06/1.21  ((a755) != (a622))
% 1.06/1.21  (c4_2 (a669) zenon_X79)
% 1.06/1.21  ((a662) != zenon_X52)
% 1.06/1.21  (-. (c4_2 (a618) zenon_X79))
% 1.06/1.21  ((a626) != zenon_X58)
% 1.06/1.21  (-. (c4_2 (a701) (a738)))
% 1.06/1.21  ((a656) != (a721))
% 1.06/1.21  (-. (c4_2 (a737) zenon_X53))
% 1.06/1.21  (zenon_X20 != (a755))
% 1.06/1.21  ((a753) != zenon_X7)
% 1.06/1.21  (zenon_X58 != zenon_X42)
% 1.06/1.21  (-. (c4_2 zenon_X23 (a731)))
% 1.06/1.21  (c7_2 (a656) (a732))
% 1.06/1.21  (c8_2 (a618) (a626))
% 1.06/1.21  ((a623) != zenon_X58)
% 1.06/1.21  ((a754) != zenon_X58)
% 1.06/1.21  ((a657) != zenon_X82)
% 1.06/1.21  ((a626) != zenon_X46)
% 1.06/1.21  (zenon_X1 != zenon_X79)
% 1.06/1.21  ((a677) != zenon_X15)
% 1.06/1.21  ((a618) != (a709))
% 1.06/1.21  (c4_2 (a690) zenon_X82)
% 1.06/1.21  ((a709) != (a628))
% 1.06/1.21  (-. (c3_2 (a628) (a657)))
% 1.06/1.21  (-. (c3_2 (a622) zenon_X58))
% 1.06/1.21  ((a732) != zenon_X64)
% 1.06/1.21  ((a662) != zenon_X40)
% 1.06/1.21  (c7_2 (a690) (a702))
% 1.06/1.21  (c9_1 (a658))
% 1.06/1.21  (-. (c3_2 (a622) zenon_X66))
% 1.06/1.21  ((a731) != zenon_X82)
% 1.06/1.21  ((a730) != zenon_X42)
% 1.06/1.21  (-. (c4_2 (a628) zenon_X53))
% 1.06/1.21  (c9_1 (a670))
% 1.06/1.21  ((a664) != zenon_X60)
% 1.06/1.21  (c8_2 (a753) (a677))
% 1.06/1.21  (-. (c4_2 (a618) (a629)))
% 1.06/1.21  (-. (c1_2 (a669) (a732)))
% 1.06/1.21  ((a755) != zenon_X21)
% 1.06/1.21  (zenon_X58 != zenon_X72)
% 1.06/1.21  ((a731) != zenon_X60)
% 1.06/1.21  ((a670) != (a656))
% 1.06/1.21  ((a628) != (a639))
% 1.06/1.21  ((a623) != zenon_X40)
% 1.06/1.21  (zenon_X15 != (a623))
% 1.06/1.21  ((a662) != (a738))
% 1.06/1.21  ((a730) != zenon_X46)
% 1.06/1.21  (zenon_X39 != zenon_X8)
% 1.06/1.21  ((a738) != zenon_X64)
% 1.06/1.21  ((a709) != (a755))
% 1.06/1.21  (-. (c4_1 (a737)))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X58))
% 1.06/1.21  (-. (c7_2 (a755) (a623)))
% 1.06/1.21  (zenon_X25 != (a658))
% 1.06/1.21  ((a737) != (a729))
% 1.06/1.21  ((a625) != (a622))
% 1.06/1.21  (c5_2 (a701) (a702))
% 1.06/1.21  ((a626) != zenon_X42)
% 1.06/1.21  ((a664) != zenon_X16)
% 1.06/1.21  (-. (c3_2 (a628) zenon_X58))
% 1.06/1.21  (-. (c3_2 (a737) zenon_X70))
% 1.06/1.21  (-. (c3_2 zenon_X7 zenon_X16))
% 1.06/1.21  (c1_2 (a669) (a662))
% 1.06/1.21  ((a677) != (a662))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a738)))
% 1.06/1.21  ((a626) != (a710))
% 1.06/1.21  (-. (c8_1 (a618)))
% 1.06/1.21  (-. (c3_2 zenon_X21 (a677)))
% 1.06/1.21  (c3_2 (a669) (a754))
% 1.06/1.21  (ndr1_1 zenon_X17)
% 1.06/1.21  (-. (c4_2 (a737) zenon_X82))
% 1.06/1.21  (-. (c1_2 (a669) (a664)))
% 1.06/1.21  (-. (c4_2 (a628) (a702)))
% 1.06/1.21  ((a755) != (a669))
% 1.06/1.21  (c3_2 (a669) zenon_X54)
% 1.06/1.21  ((a657) != zenon_X26)
% 1.06/1.21  ((a618) != (a628))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X19))
% 1.06/1.21  ((a732) != zenon_X49)
% 1.06/1.21  ((a709) != (a639))
% 1.06/1.21  ((a731) != (a738))
% 1.06/1.21  (c7_2 (a708) (a744))
% 1.06/1.21  (c4_2 (a669) zenon_X52)
% 1.06/1.21  (zenon_X16 != zenon_X48)
% 1.06/1.21  ((a618) != (a656))
% 1.06/1.21  ((a629) != zenon_X19)
% 1.06/1.21  (-. (c3_2 (a737) zenon_X48))
% 1.06/1.21  (c4_2 (a618) (a623))
% 1.06/1.21  (zenon_X12 != zenon_X19)
% 1.06/1.21  ((a623) != zenon_X46)
% 1.06/1.21  (c5_2 (a701) zenon_X10)
% 1.06/1.21  (zenon_X70 != (a677))
% 1.06/1.21  (-. (c3_2 (a753) zenon_X8))
% 1.06/1.21  (-. (c3_2 (a622) (a657)))
% 1.06/1.21  (-. (c4_2 (a729) zenon_X42))
% 1.06/1.21  (c3_2 (a669) zenon_X19)
% 1.06/1.21  ((a664) != zenon_X42)
% 1.06/1.21  (-. (c3_2 (a656) zenon_X48))
% 1.06/1.21  (-. (c8_1 (a639)))
% 1.06/1.21  (-. (c3_2 (a753) zenon_X16))
% 1.06/1.21  ((a690) != (a729))
% 1.06/1.21  ((a738) != zenon_X61)
% 1.06/1.21  (c10_2 zenon_X18 (a662))
% 1.06/1.21  ((a625) != (a669))
% 1.06/1.21  (zenon_X29 != (a629))
% 1.06/1.21  ((a677) != zenon_X26)
% 1.06/1.21  (c4_1 (a721))
% 1.06/1.21  (zenon_X42 != zenon_X66)
% 1.06/1.21  ((a669) != zenon_X21)
% 1.06/1.21  ((a622) != zenon_X4)
% 1.06/1.21  (-. (c3_2 (a737) zenon_X16))
% 1.06/1.21  (-. (c4_2 (a628) zenon_X12))
% 1.06/1.21  (-. (c3_2 (a656) zenon_X8))
% 1.06/1.21  (zenon_X20 != zenon_X21)
% 1.06/1.21  (ndr1_1 (a625))
% 1.06/1.21  (zenon_X58 != zenon_X53)
% 1.06/1.21  (-. (c3_2 (a753) zenon_X79))
% 1.06/1.21  ((a664) != zenon_X51)
% 1.06/1.21  ((a662) != zenon_X49)
% 1.06/1.21  (zenon_X56 != (a664))
% 1.06/1.21  (-. (c4_2 (a658) zenon_X79))
% 1.06/1.21  ((a628) != zenon_X4)
% 1.06/1.21  ((a754) != (a691))
% 1.06/1.21  ((a623) != zenon_X11)
% 1.06/1.21  ((a640) != zenon_X46)
% 1.06/1.21  ((a732) != (a731))
% 1.06/1.21  (c9_2 zenon_X23 (a731))
% 1.06/1.21  (-. (c4_2 (a737) (a662)))
% 1.06/1.21  (-. (c3_2 (a753) (a677)))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X12))
% 1.06/1.21  (-. (c4_2 zenon_X25 (a662)))
% 1.06/1.21  ((a702) != (a662))
% 1.06/1.21  (-. (c3_2 (a753) (a657)))
% 1.06/1.21  (c3_2 zenon_X20 (a714))
% 1.06/1.21  (c7_2 (a708) (a731))
% 1.06/1.21  (c2_2 zenon_X14 (a677))
% 1.06/1.21  ((a657) != (a677))
% 1.06/1.21  ((a629) != (a732))
% 1.06/1.21  (-. (c1_2 zenon_X28 zenon_X29))
% 1.06/1.21  (zenon_X49 != zenon_X66)
% 1.06/1.21  (c3_2 (a690) (a731))
% 1.06/1.21  (c3_2 (a628) (a629))
% 1.06/1.21  (c4_2 (a690) zenon_X19)
% 1.06/1.21  (c4_2 (a701) (a732))
% 1.06/1.21  (-. (c1_2 zenon_X9 zenon_X1))
% 1.06/1.21  (zenon_X70 != zenon_X79)
% 1.06/1.21  (c10_2 (a669) (a640))
% 1.06/1.21  (-. (c3_2 (a701) zenon_X8))
% 1.06/1.21  (-. (c3_2 (a625) (a732)))
% 1.06/1.21  (c10_2 zenon_X9 (a640))
% 1.06/1.21  (zenon_X24 != zenon_X82)
% 1.06/1.21  (-. (c3_2 (a625) zenon_X66))
% 1.06/1.21  (-. (c3_2 zenon_X21 zenon_X40))
% 1.06/1.21  (c8_2 (a618) (a738))
% 1.06/1.22  (zenon_X24 != zenon_X46)
% 1.06/1.22  ((a709) != zenon_X2)
% 1.06/1.22  (-. (c3_2 (a625) (a657)))
% 1.06/1.22  (c2_2 zenon_X17 (a664))
% 1.06/1.22  (c4_2 (a690) zenon_X24)
% 1.06/1.22  (c7_2 (a709) (a714))
% 1.06/1.22  ((a626) != zenon_X12)
% 1.06/1.22  (-. (c3_2 (a639) zenon_X10))
% 1.06/1.22  (c6_2 zenon_X3 (a744))
% 1.06/1.22  (-. (c7_1 (a755)))
% 1.06/1.22  (c4_2 (a690) zenon_X10)
% 1.06/1.22  (c6_2 (a669) zenon_X44)
% 1.06/1.22  (zenon_X10 != zenon_X44)
% 1.06/1.22  (c1_2 (a669) zenon_X15)
% 1.06/1.22  ((a629) != zenon_X40)
% 1.06/1.22  (-. (c1_2 (a622) (a732)))
% 1.06/1.22  ((a754) != zenon_X27)
% 1.06/1.22  ((a714) != zenon_X60)
% 1.06/1.22  ((a664) != zenon_X79)
% 1.06/1.22  (-. (c5_1 (a708)))
% 1.06/1.22  ((a623) != zenon_X19)
% 1.06/1.22  ((a669) != zenon_X18)
% 1.06/1.22  ((a732) != zenon_X46)
% 1.06/1.22  (c2_2 (a690) (a664))
% 1.06/1.22  (-. (c1_2 zenon_X28 zenon_X15))
% 1.06/1.22  (-. (c3_2 (a625) (a662)))
% 1.06/1.22  (-. (c3_2 (a639) (a662)))
% 1.06/1.22  (-. (c3_2 (a737) (a677)))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X8))
% 1.06/1.22  ((a731) != zenon_X1)
% 1.06/1.22  (zenon_X1 != zenon_X8)
% 1.06/1.22  (-. (c3_2 (a628) zenon_X8))
% 1.06/1.22  ((a657) != (a710))
% 1.06/1.22  ((a662) != zenon_X63)
% 1.06/1.22  ((a658) != (a729))
% 1.06/1.22  (-. (c4_2 (a658) (a738)))
% 1.06/1.22  ((a744) != (a626))
% 1.06/1.22  ((a662) != zenon_X41)
% 1.06/1.22  (-. (c3_2 (a729) zenon_X53))
% 1.06/1.22  (-. (c5_2 (a690) (a691)))
% 1.06/1.22  ((a701) != zenon_X2)
% 1.06/1.22  (c7_2 (a618) (a662))
% 1.06/1.22  (-. (c8_1 (a658)))
% 1.06/1.22  ((a738) != zenon_X66)
% 1.06/1.22  (-. (c4_2 (a658) (a744)))
% 1.06/1.22  (c6_2 (a669) (a664))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X56))
% 1.06/1.22  (-. (c8_1 (a622)))
% 1.06/1.22  (c3_2 (a669) zenon_X1)
% 1.06/1.22  (-. (c3_2 (a656) zenon_X58))
% 1.06/1.22  (zenon_X10 != zenon_X60)
% 1.06/1.22  ((a657) != zenon_X51)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X55))
% 1.06/1.22  (c3_2 (a669) (a629))
% 1.06/1.22  (-. (c3_2 (a628) zenon_X66))
% 1.06/1.22  ((a670) != (a622))
% 1.06/1.22  (zenon_X72 != zenon_X79)
% 1.06/1.22  (-. (c1_2 (a669) (a731)))
% 1.06/1.22  (zenon_X24 != (a738))
% 1.06/1.22  (zenon_X22 != (a670))
% 1.06/1.22  (zenon_X20 != (a709))
% 1.06/1.22  (zenon_X10 != (a677))
% 1.06/1.22  ((a677) != (a702))
% 1.06/1.22  (zenon_X25 != zenon_X7)
% 1.06/1.22  (zenon_X72 != zenon_X53)
% 1.06/1.22  ((a702) != zenon_X42)
% 1.06/1.22  ((a737) != (a701))
% 1.06/1.22  (zenon_X72 != zenon_X60)
% 1.06/1.22  ((a714) != zenon_X1)
% 1.06/1.22  ((a657) != zenon_X46)
% 1.06/1.22  (-. (c4_2 zenon_X25 zenon_X46))
% 1.06/1.22  ((a701) != zenon_X23)
% 1.06/1.22  (c8_2 (a618) (a640))
% 1.06/1.22  ((a626) != (a731))
% 1.06/1.22  ((a640) != zenon_X8)
% 1.06/1.22  (-. (c3_2 (a656) zenon_X66))
% 1.06/1.22  (c3_1 zenon_X22)
% 1.06/1.22  (-. (c7_2 (a755) (a744)))
% 1.06/1.22  (zenon_X58 != zenon_X51)
% 1.06/1.22  ((a662) != zenon_X0)
% 1.06/1.22  (-. (c3_2 (a622) (a664)))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X51))
% 1.06/1.22  (c6_2 (a669) (a677))
% 1.06/1.22  (c2_1 zenon_X21)
% 1.06/1.22  ((a629) != zenon_X50)
% 1.06/1.22  (-. (c3_2 zenon_X7 (a657)))
% 1.06/1.22  (c9_2 (a658) (a731))
% 1.06/1.22  (-. (c4_2 (a628) zenon_X66))
% 1.06/1.22  (ndr1_1 (a701))
% 1.06/1.22  (-. (c4_2 (a618) zenon_X42))
% 1.06/1.22  ((a662) != zenon_X55)
% 1.06/1.22  (-. (c6_2 (a690) zenon_X55))
% 1.06/1.22  (c3_2 (a669) zenon_X51)
% 1.06/1.22  (-. (c4_2 (a729) (a629)))
% 1.06/1.22  ((a744) != zenon_X52)
% 1.06/1.22  ((a737) != zenon_X23)
% 1.06/1.22  (zenon_X7 != (a729))
% 1.06/1.22  (zenon_X25 != (a755))
% 1.06/1.22  ((a738) != zenon_X62)
% 1.06/1.22  ((a744) != zenon_X40)
% 1.06/1.22  ((a670) != zenon_X21)
% 1.06/1.22  (-. (c5_1 (a721)))
% 1.06/1.22  (zenon_X72 != zenon_X66)
% 1.06/1.22  (zenon_X40 != (a677))
% 1.06/1.22  (zenon_X10 != zenon_X40)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X54))
% 1.06/1.22  ((a738) != zenon_X56)
% 1.06/1.22  (-. (c3_2 (a753) zenon_X48))
% 1.06/1.22  (-. (c3_2 (a628) zenon_X10))
% 1.06/1.22  ((a626) != zenon_X38)
% 1.06/1.22  (c3_2 (a669) (a738))
% 1.06/1.22  (zenon_X27 != zenon_X57)
% 1.06/1.22  ((a744) != zenon_X62)
% 1.06/1.22  (zenon_X25 != (a628))
% 1.06/1.22  (-. (c4_2 (a729) (a738)))
% 1.06/1.22  ((a629) != zenon_X39)
% 1.06/1.22  (-. (c4_2 (a628) (a731)))
% 1.06/1.22  (c10_2 (a669) (a702))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X53))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X72))
% 1.06/1.22  (c7_0)
% 1.06/1.22  (zenon_X16 != zenon_X40)
% 1.06/1.22  ((a731) != zenon_X27)
% 1.06/1.22  (-. (c4_2 (a622) (a738)))
% 1.06/1.22  ((a677) != zenon_X60)
% 1.06/1.22  (-. (c7_2 (a755) (a664)))
% 1.06/1.22  (zenon_X15 != zenon_X43)
% 1.06/1.22  ((a623) != (a754))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X79))
% 1.06/1.22  (-. (c3_2 (a701) (a629)))
% 1.06/1.22  (-. (c6_1 zenon_X20))
% 1.06/1.22  (c3_2 (a669) zenon_X72)
% 1.06/1.22  ((a657) != zenon_X49)
% 1.06/1.22  (-. (c4_2 (a656) (a623)))
% 1.06/1.22  (-. (c3_2 (a753) zenon_X66))
% 1.06/1.22  ((a714) != zenon_X79)
% 1.06/1.22  (-. (c4_2 zenon_X23 (a657)))
% 1.06/1.22  (zenon_X15 != zenon_X10)
% 1.06/1.22  (-. (c1_2 (a669) zenon_X57))
% 1.06/1.22  (zenon_X79 != zenon_X53)
% 1.06/1.22  (c4_2 (a737) (a731))
% 1.06/1.22  (zenon_X43 != (a657))
% 1.06/1.22  ((a623) != (a629))
% 1.06/1.22  (-. (c2_1 (a753)))
% 1.06/1.22  ((a702) != zenon_X57)
% 1.06/1.22  ((a629) != zenon_X15)
% 1.06/1.22  (-. (c3_2 (a625) (a702)))
% 1.06/1.22  (-. (c3_2 (a618) zenon_X68))
% 1.06/1.22  ((a738) != zenon_X0)
% 1.06/1.22  ((a731) != zenon_X56)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X58))
% 1.06/1.22  ((a690) != zenon_X2)
% 1.06/1.22  (zenon_X15 != zenon_X27)
% 1.06/1.22  ((a753) != (a622))
% 1.06/1.22  (-. (c3_2 (a628) (a623)))
% 1.06/1.22  (c10_2 (a669) (a662))
% 1.06/1.22  ((a623) != zenon_X48)
% 1.06/1.22  ((a732) != zenon_X40)
% 1.06/1.22  (-. (c3_2 zenon_X7 (a629)))
% 1.06/1.22  (c4_2 zenon_X21 (a732))
% 1.06/1.22  ((a670) != (a709))
% 1.06/1.22  ((a664) != zenon_X57)
% 1.06/1.22  (-. (c5_2 (a708) zenon_X66))
% 1.06/1.22  (c1_2 (a669) (a623))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a664)))
% 1.06/1.22  ((a656) != (a729))
% 1.06/1.22  ((a702) != zenon_X19)
% 1.06/1.22  (-. (c4_2 zenon_X23 zenon_X12))
% 1.06/1.22  (-. (c5_1 zenon_X2))
% 1.06/1.22  (-. (c3_2 (a656) zenon_X10))
% 1.06/1.22  (-. (c3_2 (a639) zenon_X66))
% 1.06/1.22  (-. (c7_2 (a755) (a714)))
% 1.06/1.22  (c1_2 (a669) zenon_X11)
% 1.06/1.22  (zenon_X56 != (a677))
% 1.06/1.22  (zenon_X25 != (a639))
% 1.06/1.22  (-. (c3_2 (a639) zenon_X53))
% 1.06/1.22  (-. (c4_2 (a658) (a657)))
% 1.06/1.22  (-. (c3_2 (a753) (a626)))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X60))
% 1.06/1.22  (-. (c4_2 (a729) (a714)))
% 1.06/1.22  ((a744) != (a730))
% 1.06/1.22  (zenon_X10 != zenon_X53)
% 1.06/1.22  (-. (c3_2 zenon_X21 (a664)))
% 1.06/1.22  (c10_2 (a701) (a702))
% 1.06/1.22  (c8_2 (a618) (a664))
% 1.06/1.22  (-. (c3_2 (a622) (a629)))
% 1.06/1.22  ((a737) != (a669))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X52))
% 1.06/1.22  ((a657) != (a732))
% 1.06/1.22  (-. (c4_2 (a622) zenon_X62))
% 1.06/1.22  ((a702) != zenon_X38)
% 1.06/1.22  ((a658) != (a701))
% 1.06/1.22  (c10_2 zenon_X9 (a629))
% 1.06/1.22  (zenon_X27 != zenon_X44)
% 1.06/1.22  (-. (c1_2 (a622) (a626)))
% 1.06/1.22  (-. (c4_2 (a618) zenon_X8))
% 1.06/1.22  ((a702) != zenon_X56)
% 1.06/1.22  ((a629) != zenon_X52)
% 1.06/1.22  (-. (c1_2 zenon_X28 (a657)))
% 1.06/1.22  ((a732) != zenon_X12)
% 1.06/1.22  (c10_2 zenon_X9 (a626))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X70))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X10))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X1))
% 1.06/1.22  (c4_2 (a669) (a629))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X66))
% 1.06/1.22  ((a626) != (a629))
% 1.06/1.22  (-. (c3_2 (a729) (a744)))
% 1.06/1.22  ((a702) != zenon_X48)
% 1.06/1.22  ((a677) != zenon_X53)
% 1.06/1.22  ((a669) != (a729))
% 1.06/1.22  (c4_2 (a669) zenon_X42)
% 1.06/1.22  ((a732) != (a662))
% 1.06/1.22  (-. (c4_2 (a622) (a629)))
% 1.06/1.22  (-. (c3_2 (a753) (a629)))
% 1.06/1.22  ((a623) != zenon_X56)
% 1.06/1.22  (c1_1 (a625))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a677)))
% 1.06/1.22  ((a732) != zenon_X55)
% 1.06/1.22  (-. (c4_2 zenon_X25 zenon_X82))
% 1.06/1.22  ((a623) != zenon_X16)
% 1.06/1.22  (zenon_X54 != zenon_X8)
% 1.06/1.22  ((a731) != zenon_X12)
% 1.06/1.22  (zenon_X56 != zenon_X46)
% 1.06/1.22  (c6_2 (a701) (a702))
% 1.06/1.22  (c7_2 (a708) (a714))
% 1.06/1.22  (zenon_X10 != (a629))
% 1.06/1.22  (-. (c4_2 (a737) (a754)))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X1))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X39))
% 1.06/1.22  ((a626) != (a691))
% 1.06/1.22  (zenon_X82 != zenon_X46)
% 1.06/1.22  (zenon_X41 != zenon_X57)
% 1.06/1.22  ((a623) != zenon_X0)
% 1.06/1.22  ((a618) != (a737))
% 1.06/1.22  (-. (c3_2 (a753) (a744)))
% 1.06/1.22  (c8_2 (a753) (a731))
% 1.06/1.22  ((a702) != zenon_X51)
% 1.06/1.22  ((a626) != zenon_X55)
% 1.06/1.22  (zenon_X19 != zenon_X53)
% 1.06/1.22  ((a664) != zenon_X27)
% 1.06/1.22  (c8_2 (a753) zenon_X58)
% 1.06/1.22  ((a744) != zenon_X79)
% 1.06/1.22  (-. (c4_2 (a729) (a702)))
% 1.06/1.22  ((a629) != zenon_X44)
% 1.06/1.22  (zenon_X10 != zenon_X41)
% 1.06/1.22  (zenon_X10 != zenon_X12)
% 1.06/1.22  ((a730) != (a662))
% 1.06/1.22  ((a622) != zenon_X28)
% 1.06/1.22  ((a754) != zenon_X8)
% 1.06/1.22  ((a670) != (a701))
% 1.06/1.22  (zenon_X21 != (a639))
% 1.06/1.22  (zenon_X25 != zenon_X23)
% 1.06/1.22  (zenon_X56 != zenon_X53)
% 1.06/1.22  ((a629) != zenon_X57)
% 1.06/1.22  (c4_2 (a690) (a623))
% 1.06/1.22  (zenon_X53 != zenon_X8)
% 1.06/1.22  (-. (c4_2 zenon_X25 (a664)))
% 1.06/1.22  ((a657) != zenon_X19)
% 1.06/1.22  ((a626) != zenon_X72)
% 1.06/1.22  (-. (c3_2 (a737) (a664)))
% 1.06/1.22  ((a662) != zenon_X64)
% 1.06/1.22  (c8_2 (a618) (a662))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X72))
% 1.06/1.22  ((a738) != zenon_X29)
% 1.06/1.22  ((a658) != (a628))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a731)))
% 1.06/1.22  (-. (c3_2 (a729) (a738)))
% 1.06/1.22  (-. (c3_2 (a729) (a657)))
% 1.06/1.22  (-. (c1_2 (a622) zenon_X43))
% 1.06/1.22  ((a657) != zenon_X52)
% 1.06/1.22  ((a738) != zenon_X8)
% 1.06/1.22  (ndr1_0)
% 1.06/1.22  (zenon_X15 != (a738))
% 1.06/1.22  ((a626) != zenon_X50)
% 1.06/1.22  ((a677) != zenon_X57)
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X48))
% 1.06/1.22  ((a625) != (a639))
% 1.06/1.22  ((a656) != (a622))
% 1.06/1.22  ((a623) != (a677))
% 1.06/1.22  ((a662) != zenon_X27)
% 1.06/1.22  (c3_2 (a669) (a664))
% 1.06/1.22  ((a625) != (a701))
% 1.06/1.22  (zenon_X21 != zenon_X23)
% 1.06/1.22  (c4_2 (a618) (a744))
% 1.06/1.22  (-. (c1_2 (a622) zenon_X10))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X39))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X55))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X66))
% 1.06/1.22  (c2_1 (a656))
% 1.06/1.22  ((a664) != zenon_X1)
% 1.06/1.22  (-. (c3_2 (a656) (a662)))
% 1.06/1.22  (-. (c3_2 (a669) zenon_X53))
% 1.06/1.22  (zenon_X29 != (a731))
% 1.06/1.22  (c7_1 (a658))
% 1.06/1.22  ((a629) != zenon_X82)
% 1.06/1.22  ((a618) != (a690))
% 1.06/1.22  (-. (c6_1 (a755)))
% 1.06/1.22  (zenon_X7 != zenon_X4)
% 1.06/1.22  (c1_2 (a669) (a744))
% 1.06/1.22  (-. (c3_2 (a737) zenon_X66))
% 1.06/1.22  ((a744) != (a754))
% 1.06/1.22  (-. (c3_2 (a622) (a738)))
% 1.06/1.22  (-. (c8_1 (a701)))
% 1.06/1.22  (zenon_X12 != zenon_X56)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X58))
% 1.06/1.22  (c5_2 (a669) zenon_X53)
% 1.06/1.22  (zenon_X48 != zenon_X66)
% 1.06/1.22  ((a662) != zenon_X60)
% 1.06/1.22  (-. (c3_2 zenon_X7 (a662)))
% 1.06/1.22  (-. (c4_2 (a701) zenon_X64))
% 1.06/1.22  (-. (c3_2 (a729) (a714)))
% 1.06/1.22  ((a709) != (a753))
% 1.06/1.22  (-. (c3_2 (a639) (a738)))
% 1.06/1.22  ((a709) != (a701))
% 1.06/1.22  (-. (c6_2 (a690) zenon_X19))
% 1.06/1.22  ((a623) != zenon_X60)
% 1.06/1.22  (c4_2 (a669) zenon_X16)
% 1.06/1.22  ((a702) != zenon_X44)
% 1.06/1.22  (-. (c4_2 (a737) zenon_X58))
% 1.06/1.22  ((a738) != zenon_X57)
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X16))
% 1.06/1.22  ((a640) != zenon_X60)
% 1.06/1.22  (zenon_X29 != (a657))
% 1.06/1.22  (c5_2 (a669) (a677))
% 1.06/1.22  ((a664) != zenon_X8)
% 1.06/1.22  (zenon_X48 != zenon_X53)
% 1.06/1.22  (c4_2 (a690) (a702))
% 1.06/1.22  (-. (c1_2 (a737) zenon_X57))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X8))
% 1.06/1.22  (c10_2 zenon_X9 (a732))
% 1.06/1.22  (-. (c4_2 (a628) (a677)))
% 1.06/1.22  (-. (c3_2 zenon_X21 (a640)))
% 1.06/1.22  ((a702) != zenon_X60)
% 1.06/1.22  (c4_2 (a669) (a626))
% 1.06/1.22  ((a629) != zenon_X27)
% 1.06/1.22  (zenon_X12 != (a754))
% 1.06/1.22  ((a731) != (a677))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X42))
% 1.06/1.22  ((a732) != zenon_X38)
% 1.06/1.22  ((a702) != zenon_X40)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X56))
% 1.06/1.22  ((a744) != zenon_X53)
% 1.06/1.22  (-. (c5_2 (a708) zenon_X19))
% 1.06/1.22  (-. (c8_1 (a628)))
% 1.06/1.22  ((a744) != (a664))
% 1.06/1.22  (zenon_X41 != (a732))
% 1.06/1.22  (c3_2 (a669) (a657))
% 1.06/1.22  (c9_1 zenon_X21)
% 1.06/1.22  ((a629) != zenon_X46)
% 1.06/1.22  (c2_1 (a701))
% 1.06/1.22  (zenon_X25 != (a618))
% 1.06/1.22  (c1_2 (a669) (a677))
% 1.06/1.22  (c3_2 zenon_X25 (a731))
% 1.06/1.22  (c1_2 (a622) (a623))
% 1.06/1.22  (c3_2 (a670) (a714))
% 1.06/1.22  (c3_2 (a669) (a744))
% 1.06/1.22  (zenon_X43 != zenon_X44)
% 1.06/1.22  (-. (c4_2 (a729) (a754)))
% 1.06/1.22  (c6_2 (a669) (a657))
% 1.06/1.22  (-. (c6_2 (a701) zenon_X11))
% 1.06/1.22  (-. (c3_2 (a639) zenon_X72))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X54))
% 1.06/1.22  ((a731) != zenon_X51)
% 1.06/1.22  (c3_2 (a669) zenon_X40)
% 1.06/1.22  (zenon_X38 != zenon_X66)
% 1.06/1.22  ((a629) != zenon_X70)
% 1.06/1.22  (-. (c3_2 (a753) (a731)))
% 1.06/1.22  (-. (c8_1 zenon_X7))
% 1.06/1.22  (zenon_X43 != (a732))
% 1.06/1.22  ((a732) != zenon_X8)
% 1.06/1.22  (zenon_X10 != (a664))
% 1.06/1.22  ((a626) != zenon_X56)
% 1.06/1.22  ((a658) != (a709))
% 1.06/1.22  ((a625) != zenon_X23)
% 1.06/1.22  (zenon_X40 != zenon_X53)
% 1.06/1.22  (zenon_X12 != (a744))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X56))
% 1.06/1.22  (c10_2 (a669) (a623))
% 1.06/1.22  ((a755) != zenon_X7)
% 1.06/1.22  (c4_2 (a618) (a702))
% 1.06/1.22  (zenon_X42 != zenon_X79)
% 1.06/1.22  ((a710) != (a691))
% 1.06/1.22  ((a690) != (a628))
% 1.06/1.22  (-. (c5_2 (a670) (a714)))
% 1.06/1.22  (-. (c1_2 zenon_X28 (a623)))
% 1.06/1.22  ((a731) != zenon_X19)
% 1.06/1.22  (zenon_X10 != zenon_X54)
% 1.06/1.22  ((a625) != zenon_X7)
% 1.06/1.22  ((a702) != (a710))
% 1.06/1.22  (zenon_X10 != zenon_X58)
% 1.06/1.22  ((a656) != (a625))
% 1.06/1.22  (zenon_X1 != zenon_X66)
% 1.06/1.22  ((a714) != zenon_X0)
% 1.06/1.22  (c7_2 (a708) (a629))
% 1.06/1.22  ((a702) != zenon_X53)
% 1.06/1.22  (zenon_X58 != zenon_X79)
% 1.06/1.22  (-. (c8_1 zenon_X21))
% 1.06/1.22  ((a677) != zenon_X44)
% 1.06/1.22  (-. (c3_2 (a625) (a623)))
% 1.06/1.22  (-. (c4_2 (a729) (a623)))
% 1.06/1.22  (c3_1 zenon_X13)
% 1.06/1.22  (-. (c3_2 (a729) zenon_X66))
% 1.06/1.22  (zenon_X48 != zenon_X8)
% 1.06/1.22  (-. (c4_2 (a658) zenon_X24))
% 1.06/1.22  (ndr1_1 (a622))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a754)))
% 1.06/1.22  ((a714) != zenon_X53)
% 1.06/1.22  (-. (c3_2 (a729) zenon_X19))
% 1.06/1.22  (zenon_X40 != zenon_X79)
% 1.06/1.22  (c4_2 (a618) (a730))
% 1.06/1.22  (-. (c4_2 (a737) (a657)))
% 1.06/1.22  ((a732) != zenon_X48)
% 1.06/1.22  (-. (c3_2 (a622) zenon_X79))
% 1.06/1.22  (c7_2 (a690) (a731))
% 1.06/1.22  ((a629) != zenon_X12)
% 1.06/1.22  (-. (c3_2 (a701) (a657)))
% 1.06/1.22  ((a738) != (a710))
% 1.06/1.22  (-. (c4_2 (a737) (a629)))
% 1.06/1.22  (-. (c10_2 (a618) zenon_X44))
% 1.06/1.22  ((a732) != zenon_X19)
% 1.06/1.22  ((a702) != zenon_X1)
% 1.06/1.22  (ndr1_1 (a709))
% 1.06/1.22  ((a731) != zenon_X50)
% 1.06/1.22  (-. (c4_2 (a737) zenon_X12))
% 1.06/1.22  (zenon_X55 != (a664))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X16))
% 1.06/1.22  ((a623) != zenon_X64)
% 1.06/1.22  ((a640) != zenon_X79)
% 1.06/1.22  ((a657) != zenon_X72)
% 1.06/1.22  (-. (c3_2 zenon_X7 (a640)))
% 1.06/1.22  ((a744) != zenon_X65)
% 1.06/1.22  (-. (c3_2 (a628) (a738)))
% 1.06/1.22  ((a677) != zenon_X8)
% 1.06/1.22  (-. (c1_2 (a669) (a626)))
% 1.06/1.22  ((a629) != zenon_X8)
% 1.06/1.22  ((a744) != (a677))
% 1.06/1.22  ((a737) != (a628))
% 1.06/1.22  (-. (c1_2 zenon_X28 zenon_X57))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X53))
% 1.06/1.22  ((a702) != zenon_X58)
% 1.06/1.22  (c9_2 (a670) (a731))
% 1.06/1.22  ((a738) != zenon_X39)
% 1.06/1.22  (-. (c5_1 (a669)))
% 1.06/1.22  (-. (c4_2 (a656) (a744)))
% 1.06/1.22  (c1_1 (a628))
% 1.06/1.22  ((a709) != (a669))
% 1.06/1.22  ((a709) != zenon_X4)
% 1.06/1.22  (-. (c3_2 (a737) (a623)))
% 1.06/1.22  (c7_2 (a708) zenon_X48)
% 1.06/1.22  ((a629) != zenon_X24)
% 1.06/1.22  (-. (c4_2 (a658) zenon_X12))
% 1.06/1.22  (zenon_X58 != zenon_X60)
% 1.06/1.22  (c9_2 zenon_X20 (a731))
% 1.06/1.22  ((a626) != zenon_X60)
% 1.06/1.22  ((a702) != zenon_X55)
% 1.06/1.22  (-. (c3_2 (a622) (a626)))
% 1.06/1.22  ((a623) != (a731))
% 1.06/1.22  (zenon_X58 != (a677))
% 1.06/1.22  ((a690) != (a658))
% 1.06/1.22  ((a658) != zenon_X21)
% 1.06/1.22  (-. (c9_1 zenon_X4))
% 1.06/1.22  ((a744) != (a691))
% 1.06/1.22  (-. (c3_2 (a656) zenon_X79))
% 1.06/1.22  ((a744) != zenon_X16)
% 1.06/1.22  ((a657) != (a731))
% 1.06/1.22  (-. (c10_2 (a618) zenon_X27))
% 1.06/1.22  (zenon_X16 != (a677))
% 1.06/1.22  (c8_2 (a753) (a629))
% 1.06/1.22  (zenon_X19 != zenon_X46)
% 1.06/1.22  ((a708) != (a755))
% 1.06/1.22  (-. (c6_2 (a690) zenon_X42))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X57))
% 1.06/1.22  (c4_2 (a669) zenon_X58)
% 1.06/1.22  (zenon_X10 != zenon_X38)
% 1.06/1.22  (zenon_X19 != zenon_X48)
% 1.06/1.22  (c3_2 (a625) (a626))
% 1.06/1.22  (-. (c4_2 (a737) (a626)))
% 1.06/1.22  (-. (c4_2 (a658) (a732)))
% 1.06/1.22  (zenon_X10 != zenon_X49)
% 1.06/1.22  ((a732) != zenon_X65)
% 1.06/1.22  (-. (c3_2 (a622) zenon_X53))
% 1.06/1.22  (c4_2 (a690) zenon_X42)
% 1.06/1.22  (-. (c4_2 (a658) zenon_X8))
% 1.06/1.22  (zenon_X48 != zenon_X72)
% 1.06/1.22  ((a662) != zenon_X8)
% 1.06/1.22  (c8_2 (a753) (a626))
% 1.06/1.22  (zenon_X19 != zenon_X79)
% 1.06/1.22  (-. (c3_2 (a737) (a732)))
% 1.06/1.22  ((a730) != (a714))
% 1.06/1.22  ((a731) != zenon_X79)
% 1.06/1.22  (c9_2 zenon_X25 (a731))
% 1.06/1.22  ((a677) != (a691))
% 1.06/1.22  (zenon_X70 != zenon_X66)
% 1.06/1.22  (c4_2 (a690) (a629))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X48))
% 1.06/1.22  ((a664) != zenon_X52)
% 1.06/1.22  (zenon_X51 != zenon_X53)
% 1.06/1.22  ((a657) != (a691))
% 1.06/1.22  (c8_2 (a753) (a623))
% 1.06/1.22  (zenon_X16 != zenon_X51)
% 1.06/1.22  (-. (c3_2 (a622) zenon_X16))
% 1.06/1.22  ((a753) != (a656))
% 1.06/1.22  (zenon_X70 != zenon_X52)
% 1.06/1.22  ((a732) != zenon_X57)
% 1.06/1.22  (c1_2 (a669) zenon_X41)
% 1.06/1.22  ((a625) != (a729))
% 1.06/1.22  (zenon_X10 != (a626))
% 1.06/1.22  (-. (c6_1 (a709)))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X79))
% 1.06/1.22  (-. (c4_2 (a753) zenon_X74))
% 1.06/1.22  ((a753) != (a639))
% 1.06/1.22  (-. (c7_2 (a755) (a730)))
% 1.06/1.22  ((a737) != zenon_X21)
% 1.06/1.22  (-. (c1_2 (a639) (a640)))
% 1.06/1.22  (c9_2 (a709) (a710))
% 1.06/1.22  ((a622) != (a639))
% 1.06/1.22  (zenon_X10 != zenon_X66)
% 1.06/1.22  (c4_2 (a690) (a730))
% 1.06/1.22  ((a731) != zenon_X8)
% 1.06/1.22  (zenon_X12 != (a738))
% 1.06/1.22  (c3_2 (a669) (a640))
% 1.06/1.22  (-. (c1_2 zenon_X28 (a732)))
% 1.06/1.22  (zenon_X70 != zenon_X8)
% 1.06/1.22  (-. (c3_2 (a753) (a702)))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X70))
% 1.06/1.22  ((a730) != zenon_X53)
% 1.06/1.22  (-. (c1_2 (a737) (a732)))
% 1.06/1.22  (zenon_X20 != (a625))
% 1.06/1.22  (zenon_X25 != (a656))
% 1.06/1.22  (c3_2 (a669) (a714))
% 1.06/1.22  (zenon_X58 != zenon_X70)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X40))
% 1.06/1.22  (zenon_X58 != zenon_X56)
% 1.06/1.22  (zenon_X48 != zenon_X56)
% 1.06/1.22  (zenon_X54 != zenon_X66)
% 1.06/1.22  (-. (c4_2 (a628) zenon_X10))
% 1.06/1.22  (c3_2 (a669) (a662))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X49))
% 1.06/1.22  (zenon_X66 != zenon_X8)
% 1.06/1.22  (c6_2 zenon_X23 (a731))
% 1.06/1.22  (zenon_X49 != zenon_X8)
% 1.06/1.22  (-. (c3_2 zenon_X21 (a731)))
% 1.06/1.22  ((a629) != zenon_X55)
% 1.06/1.22  ((a623) != zenon_X66)
% 1.06/1.22  (-. (c8_1 (a729)))
% 1.06/1.22  (c1_2 (a669) zenon_X10)
% 1.06/1.22  ((a618) != (a658))
% 1.06/1.22  (c7_2 (a618) (a702))
% 1.06/1.22  ((a690) != zenon_X21)
% 1.06/1.22  (zenon_X15 != (a640))
% 1.06/1.22  (zenon_X10 != zenon_X19)
% 1.06/1.22  (c7_2 (a737) (a731))
% 1.06/1.22  (-. (c6_2 (a690) zenon_X12))
% 1.06/1.22  (c7_2 (a708) zenon_X72)
% 1.06/1.22  (c9_0)
% 1.06/1.22  ((a702) != zenon_X12)
% 1.06/1.22  ((a702) != (a691))
% 1.06/1.22  (-. (c3_2 (a622) zenon_X48))
% 1.06/1.22  ((a744) != (a731))
% 1.06/1.22  (c6_2 (a622) (a623))
% 1.06/1.22  ((a754) != zenon_X42)
% 1.06/1.22  ((a640) != zenon_X12)
% 1.06/1.22  (-. (c4_2 (a628) zenon_X55))
% 1.06/1.22  (-. (c8_2 (a618) zenon_X26))
% 1.06/1.22  ((a664) != zenon_X66)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X27))
% 1.06/1.22  (c8_2 (a753) (a662))
% 1.06/1.22  ((a657) != zenon_X40)
% 1.06/1.22  (-. (c4_2 (a658) (a662)))
% 1.06/1.22  (c7_2 (a628) (a629))
% 1.06/1.22  (c4_2 (a690) zenon_X56)
% 1.06/1.22  (c7_2 (a708) (a626))
% 1.06/1.22  (zenon_X15 != zenon_X11)
% 1.06/1.22  ((a754) != (a732))
% 1.06/1.22  ((a730) != zenon_X79)
% 1.06/1.22  (-. (c6_1 (a753)))
% 1.06/1.22  ((a753) != zenon_X23)
% 1.06/1.22  (zenon_X55 != zenon_X48)
% 1.06/1.22  (zenon_X16 != zenon_X38)
% 1.06/1.22  (zenon_X16 != zenon_X54)
% 1.06/1.22  (-. (c3_2 (a639) zenon_X58))
% 1.06/1.22  (-. (c3_2 zenon_X2 (a626)))
% 1.06/1.22  (-. (c4_2 (a618) zenon_X12))
% 1.06/1.22  ((a730) != zenon_X48)
% 1.06/1.22  ((a731) != zenon_X52)
% 1.06/1.22  (c4_2 (a690) (a657))
% 1.06/1.22  ((a730) != zenon_X12)
% 1.06/1.22  (-. (c4_2 (a625) (a662)))
% 1.06/1.22  (-. (c1_2 zenon_X28 (a629)))
% 1.06/1.22  ((a662) != zenon_X39)
% 1.06/1.22  (c6_2 (a669) zenon_X15)
% 1.06/1.22  ((a618) != zenon_X21)
% 1.06/1.22  (-. (c3_2 (a628) zenon_X53))
% 1.06/1.22  ((a658) != (a669))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X38))
% 1.06/1.22  (-. (c3_2 (a625) zenon_X53))
% 1.06/1.22  (c3_2 (a669) (a731))
% 1.06/1.22  (-. (c4_2 (a658) (a626)))
% 1.06/1.22  ((a669) != zenon_X23)
% 1.06/1.22  (c9_1 (a628))
% 1.06/1.22  (-. (c4_2 (a618) zenon_X53))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X70))
% 1.06/1.22  ((a732) != zenon_X51)
% 1.06/1.22  (-. (c3_2 (a656) (a677)))
% 1.06/1.22  (-. (c4_2 (a729) (a626)))
% 1.06/1.22  (-. (c4_2 (a701) (a744)))
% 1.06/1.22  ((a732) != zenon_X79)
% 1.06/1.22  ((a664) != zenon_X48)
% 1.06/1.22  ((a622) != zenon_X23)
% 1.06/1.22  ((a744) != (a738))
% 1.06/1.22  ((a730) != (a626))
% 1.06/1.22  (zenon_X46 != (a662))
% 1.06/1.22  (zenon_X25 != zenon_X21)
% 1.06/1.22  (c7_2 (a690) (a626))
% 1.06/1.22  (c7_2 (a690) (a744))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X46))
% 1.06/1.22  ((a744) != zenon_X42)
% 1.06/1.22  (-. (c3_2 (a628) zenon_X16))
% 1.06/1.22  (-. (c3_2 zenon_X4 (a677)))
% 1.06/1.22  ((a626) != (a732))
% 1.06/1.22  (-. (c8_1 (a625)))
% 1.06/1.22  (-. (c4_2 (a625) (a623)))
% 1.06/1.22  (-. (c3_2 (a737) zenon_X79))
% 1.06/1.22  ((a702) != zenon_X52)
% 1.06/1.22  (zenon_X51 != (a677))
% 1.06/1.22  ((a731) != zenon_X40)
% 1.06/1.22  (-. (c2_2 zenon_X18 (a662)))
% 1.06/1.22  (c6_2 (a669) (a626))
% 1.06/1.22  ((a662) != zenon_X61)
% 1.06/1.22  (zenon_X48 != (a640))
% 1.06/1.22  ((a754) != (a664))
% 1.06/1.22  (-. (c3_2 (a729) (a730)))
% 1.06/1.22  ((a629) != zenon_X49)
% 1.06/1.22  (zenon_X55 != zenon_X8)
% 1.06/1.22  (zenon_X7 != zenon_X23)
% 1.06/1.22  (-. (c3_2 (a737) zenon_X8))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X60))
% 1.06/1.22  ((a626) != zenon_X11)
% 1.06/1.22  ((a658) != zenon_X4)
% 1.06/1.22  (c4_2 (a669) zenon_X70)
% 1.06/1.22  (-. (c3_2 (a701) (a732)))
% 1.06/1.22  (c10_2 (a669) (a738))
% 1.06/1.22  ((a738) != zenon_X16)
% 1.06/1.22  (-. (c4_2 (a701) (a629)))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X10))
% 1.06/1.22  (c7_1 (a656))
% 1.06/1.22  (c3_2 (a669) zenon_X16)
% 1.06/1.22  (-. (c4_2 (a729) (a677)))
% 1.06/1.22  ((a702) != (a657))
% 1.06/1.22  ((a744) != zenon_X19)
% 1.06/1.22  (zenon_X56 != zenon_X66)
% 1.06/1.22  (-. (c3_2 (a690) (a626)))
% 1.06/1.22  (c10_2 zenon_X9 (a677))
% 1.06/1.22  (-. (c3_2 (a729) (a731)))
% 1.06/1.22  (-. (c4_2 zenon_X23 (a732)))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a738)))
% 1.06/1.22  ((a623) != zenon_X43)
% 1.06/1.22  (c6_2 (a669) zenon_X27)
% 1.06/1.22  (-. (c3_2 (a639) zenon_X16))
% 1.06/1.22  (zenon_X48 != (a677))
% 1.06/1.22  (zenon_X19 != (a677))
% 1.06/1.22  (-. (c3_2 (a639) (a731)))
% 1.06/1.22  (-. (c3_2 (a753) zenon_X53))
% 1.06/1.22  (-. (c4_2 (a658) (a664)))
% 1.06/1.22  (-. (c4_2 (a618) (a732)))
% 1.06/1.22  ((a623) != zenon_X54)
% 1.06/1.22  ((a656) != (a639))
% 1.06/1.22  (c8_2 zenon_X3 (a744))
% 1.06/1.22  ((a640) != zenon_X44)
% 1.06/1.22  (c7_2 (a708) (a640))
% 1.06/1.22  (-. (c4_2 (a628) zenon_X48))
% 1.06/1.22  (-. (c4_2 (a737) (a664)))
% 1.06/1.22  (c7_2 (a618) (a744))
% 1.06/1.22  (c2_1 (a618))
% 1.06/1.22  (c5_2 zenon_X17 (a664))
% 1.06/1.22  (zenon_X20 != (a639))
% 1.06/1.22  (zenon_X25 != (a753))
% 1.06/1.22  (-. (c3_2 (a701) (a626)))
% 1.06/1.22  (-. (c1_2 (a737) (a657)))
% 1.06/1.22  (c3_2 (a669) zenon_X70)
% 1.06/1.22  (-. (c4_2 (a625) (a744)))
% 1.06/1.22  (c3_2 (a669) zenon_X79)
% 1.06/1.22  (c4_2 (a669) (a664))
% 1.06/1.22  ((a656) != zenon_X2)
% 1.06/1.22  ((a623) != (a626))
% 1.06/1.22  (-. (c4_2 (a737) (a702)))
% 1.06/1.22  (zenon_X16 != (a731))
% 1.06/1.22  (-. (c9_2 (a618) (a629)))
% 1.06/1.22  ((a623) != zenon_X39)
% 1.06/1.22  ((a738) != zenon_X54)
% 1.06/1.22  (c7_2 zenon_X25 (a731))
% 1.06/1.22  ((a664) != zenon_X26)
% 1.06/1.22  (c4_2 (a625) (a732))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X24))
% 1.06/1.22  (-. (c4_2 zenon_X25 zenon_X12))
% 1.06/1.22  (ndr1_1 zenon_X25)
% 1.06/1.22  (-. (c3_2 (a729) zenon_X8))
% 1.06/1.22  (c1_2 (a737) (a738))
% 1.06/1.22  ((a744) != (a629))
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X79))
% 1.06/1.22  (c9_1 (a656))
% 1.06/1.22  ((a738) != zenon_X41)
% 1.06/1.22  (-. (c4_2 (a618) zenon_X46))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X60))
% 1.06/1.22  (-. (c4_2 (a658) (a702)))
% 1.06/1.22  ((a629) != zenon_X72)
% 1.06/1.22  ((a657) != zenon_X1)
% 1.06/1.22  (zenon_X70 != zenon_X53)
% 1.06/1.22  ((a662) != (a710))
% 1.06/1.22  (zenon_X49 != zenon_X53)
% 1.06/1.22  (-. (c3_2 (a729) (a623)))
% 1.06/1.22  ((a626) != zenon_X54)
% 1.06/1.22  (c10_2 (a669) (a754))
% 1.06/1.22  ((a737) != (a625))
% 1.06/1.22  (c4_2 (a618) (a738))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X16))
% 1.06/1.22  ((a738) != zenon_X43)
% 1.06/1.22  ((a628) != zenon_X7)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X39))
% 1.06/1.22  (-. (c4_2 (a618) (a731)))
% 1.06/1.22  ((a753) != (a669))
% 1.06/1.22  ((a754) != zenon_X48)
% 1.06/1.22  ((a690) != zenon_X4)
% 1.06/1.22  ((a702) != zenon_X26)
% 1.06/1.22  (-. (c9_2 zenon_X14 (a677)))
% 1.06/1.22  ((a731) != zenon_X68)
% 1.06/1.22  (zenon_X41 != (a657))
% 1.06/1.22  (c6_2 (a669) zenon_X57)
% 1.06/1.22  (c8_2 (a618) (a732))
% 1.06/1.22  ((a731) != zenon_X46)
% 1.06/1.22  (zenon_X11 != (a732))
% 1.06/1.22  (c3_2 (a737) (a731))
% 1.06/1.22  ((a629) != zenon_X53)
% 1.06/1.22  ((a669) != (a708))
% 1.06/1.22  ((a738) != zenon_X52)
% 1.06/1.22  (c7_2 (a690) (a730))
% 1.06/1.22  (-. (c3_2 (a639) (a664)))
% 1.06/1.22  (-. (c3_2 (a656) (a744)))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X72))
% 1.06/1.22  (c5_2 (a701) (a626))
% 1.06/1.22  ((a618) != (a753))
% 1.06/1.22  (-. (c1_2 zenon_X28 (a640)))
% 1.06/1.22  ((a755) != (a701))
% 1.06/1.22  (c9_1 zenon_X25)
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X58))
% 1.06/1.22  (-. (c1_2 (a622) (a738)))
% 1.06/1.22  ((a669) != zenon_X9)
% 1.06/1.22  (c10_2 zenon_X9 (a662))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X8))
% 1.06/1.22  ((a755) != (a639))
% 1.06/1.22  (-. (c4_2 zenon_X23 zenon_X19))
% 1.06/1.22  (-. (c3_2 (a669) (a677)))
% 1.06/1.22  (zenon_X10 != (a731))
% 1.06/1.22  (c3_2 (a669) zenon_X66)
% 1.06/1.22  ((a730) != (a710))
% 1.06/1.22  (zenon_X58 != zenon_X8)
% 1.06/1.22  ((a730) != zenon_X58)
% 1.06/1.22  (-. (c4_2 zenon_X23 (a744)))
% 1.06/1.22  (zenon_X70 != zenon_X40)
% 1.06/1.22  (-. (c3_2 (a737) zenon_X52))
% 1.06/1.22  (c7_2 (a708) (a732))
% 1.06/1.22  ((a744) != (a657))
% 1.06/1.22  ((a731) != (a640))
% 1.06/1.22  (-. (c3_2 (a737) (a657)))
% 1.06/1.22  (zenon_X16 != zenon_X52)
% 1.06/1.22  (-. (c3_2 (a701) zenon_X48))
% 1.06/1.22  ((a623) != zenon_X1)
% 1.06/1.22  ((a738) != zenon_X10)
% 1.06/1.22  (c2_2 (a690) zenon_X46)
% 1.06/1.22  (c4_2 (a690) (a732))
% 1.06/1.22  (-. (c3_2 (a753) zenon_X10))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X52))
% 1.06/1.22  (zenon_X66 != (a677))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X79))
% 1.06/1.22  ((a664) != zenon_X44)
% 1.06/1.22  (zenon_X10 != zenon_X57)
% 1.06/1.22  ((a754) != (a640))
% 1.06/1.22  (-. (c4_2 (a628) zenon_X58))
% 1.06/1.22  (ndr1_1 (a737))
% 1.06/1.22  ((a670) != (a669))
% 1.06/1.22  ((a662) != zenon_X43)
% 1.06/1.22  (zenon_X51 != zenon_X8)
% 1.06/1.22  ((a744) != zenon_X82)
% 1.06/1.22  (zenon_X58 != zenon_X38)
% 1.06/1.22  ((a732) != (a664))
% 1.06/1.22  ((a732) != (a677))
% 1.06/1.22  (c3_2 (a618) (a731))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X54))
% 1.06/1.22  (zenon_X15 != zenon_X44)
% 1.06/1.22  (c7_2 (a618) (a730))
% 1.06/1.22  (zenon_X58 != zenon_X52)
% 1.06/1.22  (zenon_X29 != (a640))
% 1.06/1.22  (-. (c3_2 (a639) zenon_X79))
% 1.06/1.22  (zenon_X58 != (a640))
% 1.06/1.22  (ndr1_1 (a639))
% 1.06/1.22  (zenon_X12 != (a662))
% 1.06/1.22  (-. (c4_2 zenon_X25 (a629)))
% 1.06/1.22  ((a657) != zenon_X38)
% 1.06/1.22  ((a618) != (a625))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X58))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X79))
% 1.06/1.22  ((a731) != zenon_X70)
% 1.06/1.22  (c4_2 (a618) (a662))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X56))
% 1.06/1.22  (zenon_X48 != zenon_X60)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X10))
% 1.06/1.22  (-. (c3_2 zenon_X23 zenon_X76))
% 1.06/1.22  (-. (c3_2 (a737) zenon_X53))
% 1.06/1.22  (-. (c3_2 (a656) zenon_X16))
% 1.06/1.22  (c4_2 (a690) (a640))
% 1.06/1.22  ((a738) != zenon_X51)
% 1.06/1.22  (-. (c8_2 (a709) (a710)))
% 1.06/1.22  ((a629) != zenon_X62)
% 1.06/1.22  (-. (c1_2 zenon_X28 zenon_X44))
% 1.06/1.22  (zenon_X39 != (a677))
% 1.06/1.22  ((a744) != zenon_X38)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X15))
% 1.06/1.22  (c5_2 (a701) (a657))
% 1.06/1.22  (-. (c3_2 (a753) (a662)))
% 1.06/1.22  ((a731) != zenon_X39)
% 1.06/1.22  (c10_2 (a669) zenon_X27)
% 1.06/1.22  ((a657) != (a664))
% 1.06/1.22  ((a623) != (a640))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X46))
% 1.06/1.22  (zenon_X55 != (a677))
% 1.06/1.22  ((a669) != zenon_X7)
% 1.06/1.22  ((a738) != zenon_X55)
% 1.06/1.22  ((a744) != zenon_X46)
% 1.06/1.22  (zenon_X48 != zenon_X40)
% 1.06/1.22  (-. (c3_2 (a639) (a702)))
% 1.06/1.22  (zenon_X70 != zenon_X60)
% 1.06/1.22  (zenon_X43 != (a626))
% 1.06/1.22  ((a753) != zenon_X2)
% 1.06/1.22  (zenon_X39 != zenon_X53)
% 1.06/1.22  (ndr1_1 zenon_X18)
% 1.06/1.22  ((a658) != zenon_X7)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X56))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X52))
% 1.06/1.22  (zenon_X43 != (a731))
% 1.06/1.22  (c8_2 (a639) (a640))
% 1.06/1.22  ((a626) != (a640))
% 1.06/1.22  (c9_1 zenon_X7)
% 1.06/1.22  ((a730) != zenon_X61)
% 1.06/1.22  ((a738) != zenon_X53)
% 1.06/1.22  (-. (c4_2 zenon_X23 (a629)))
% 1.06/1.22  (-. (c4_2 (a729) (a640)))
% 1.06/1.22  (c8_1 (a670))
% 1.06/1.22  ((a731) != zenon_X57)
% 1.06/1.22  ((a701) != zenon_X4)
% 1.06/1.22  (-. (c3_2 (a701) (a744)))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X10))
% 1.06/1.22  (zenon_X21 != zenon_X4)
% 1.06/1.22  ((a753) != zenon_X4)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X66))
% 1.06/1.22  (-. (c3_2 zenon_X21 (a702)))
% 1.06/1.22  ((a755) != (a628))
% 1.06/1.22  (c2_1 zenon_X7)
% 1.06/1.22  (-. (c3_2 zenon_X2 (a657)))
% 1.06/1.22  ((a670) != (a755))
% 1.06/1.22  (-. (c1_2 (a622) (a657)))
% 1.06/1.22  (-. (c3_2 zenon_X21 (a730)))
% 1.06/1.22  (-. (c3_2 (a628) (a626)))
% 1.06/1.22  ((a701) != (a729))
% 1.06/1.22  (zenon_X41 != (a664))
% 1.06/1.22  ((a664) != zenon_X40)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X66))
% 1.06/1.22  ((a737) != (a639))
% 1.06/1.22  (-. (c5_0))
% 1.06/1.22  (c7_2 (a622) (a732))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X42))
% 1.06/1.22  (c8_2 (a753) zenon_X72)
% 1.06/1.22  (c8_2 (a753) (a714))
% 1.06/1.22  (-. (c3_2 zenon_X2 (a629)))
% 1.06/1.22  (-. (c3_2 (a701) zenon_X16))
% 1.06/1.22  (zenon_X52 != (a677))
% 1.06/1.22  (c4_2 (a628) (a732))
% 1.06/1.22  ((a730) != zenon_X66)
% 1.06/1.22  (-. (c4_2 zenon_X21 zenon_X80))
% 1.06/1.22  (zenon_X58 != zenon_X54)
% 1.06/1.22  (-. (c9_2 (a618) (a626)))
% 1.06/1.22  ((a730) != (a732))
% 1.06/1.22  ((a662) != (a754))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X8))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X16))
% 1.06/1.22  (c5_2 (a701) (a731))
% 1.06/1.22  ((a731) != zenon_X72)
% 1.06/1.22  (-. (c4_2 (a618) zenon_X16))
% 1.06/1.22  (c1_2 (a669) (a702))
% 1.06/1.22  (c7_2 (a690) zenon_X24)
% 1.06/1.22  (zenon_X16 != zenon_X49)
% 1.06/1.22  ((a738) != zenon_X42)
% 1.06/1.22  (-. (c3_2 (a656) (a731)))
% 1.06/1.22  ((a656) != zenon_X21)
% 1.06/1.22  (zenon_X11 != (a664))
% 1.06/1.22  (-. (c1_2 (a737) zenon_X41))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X48))
% 1.06/1.22  (zenon_X24 != (a664))
% 1.06/1.22  (-. (c3_2 (a701) (a664)))
% 1.06/1.22  ((a730) != zenon_X26)
% 1.06/1.22  ((a657) != zenon_X79)
% 1.06/1.22  ((a738) != (a754))
% 1.06/1.22  (c5_2 zenon_X14 (a677))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X70))
% 1.06/1.22  ((a737) != (a755))
% 1.06/1.22  (-. (c9_2 (a690) (a691)))
% 1.06/1.22  (c3_2 zenon_X23 (a731))
% 1.06/1.22  (-. (c1_2 (a737) zenon_X15))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X51))
% 1.06/1.22  (ndr1_1 zenon_X14)
% 1.06/1.22  (-. (c5_2 zenon_X20 (a714)))
% 1.06/1.22  ((a731) != zenon_X48)
% 1.06/1.22  (-. (c1_2 (a622) (a662)))
% 1.06/1.22  (-. (c3_2 (a625) zenon_X79))
% 1.06/1.22  (zenon_X25 != zenon_X2)
% 1.06/1.22  (-. (c3_2 zenon_X4 (a731)))
% 1.06/1.22  ((a640) != (a691))
% 1.06/1.22  (zenon_X21 != (a729))
% 1.06/1.22  ((a618) != zenon_X7)
% 1.06/1.22  (c4_2 (a656) (a732))
% 1.06/1.22  ((a731) != zenon_X54)
% 1.06/1.22  ((a657) != zenon_X24)
% 1.06/1.22  ((a732) != zenon_X24)
% 1.06/1.22  ((a690) != (a622))
% 1.06/1.22  ((a690) != zenon_X23)
% 1.06/1.22  ((a640) != zenon_X53)
% 1.06/1.22  (-. (c1_2 zenon_X28 (a664)))
% 1.06/1.22  (ndr1_1 (a658))
% 1.06/1.22  (-. (c6_2 (a701) zenon_X44))
% 1.06/1.22  (-. (c3_2 (a622) (a677)))
% 1.06/1.22  ((a640) != (a677))
% 1.06/1.22  (zenon_X82 != (a664))
% 1.06/1.22  (zenon_X52 != zenon_X53)
% 1.06/1.22  (-. (c3_2 (a729) zenon_X40))
% 1.06/1.22  (c4_2 (a669) (a730))
% 1.06/1.22  ((a662) != zenon_X66)
% 1.06/1.22  ((a622) != zenon_X2)
% 1.06/1.22  (-. (c9_2 (a618) (a677)))
% 1.06/1.22  (zenon_X20 != (a618))
% 1.06/1.22  ((a754) != (a626))
% 1.06/1.22  (ndr1_1 (a618))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X19))
% 1.06/1.22  (c7_2 (a729) (a730))
% 1.06/1.22  (-. (c3_2 (a729) (a702)))
% 1.06/1.22  (-. (c4_2 (a628) (a662)))
% 1.06/1.22  ((a702) != (a629))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X16))
% 1.06/1.22  ((a628) != zenon_X2)
% 1.06/1.22  ((a730) != (a664))
% 1.06/1.22  ((a732) != zenon_X15)
% 1.06/1.22  ((a623) != (a710))
% 1.06/1.22  ((a754) != zenon_X44)
% 1.06/1.22  (-. (c3_2 (a625) zenon_X58))
% 1.06/1.22  (-. (c4_2 zenon_X23 (a662)))
% 1.06/1.22  (c7_2 (a708) (a657))
% 1.06/1.22  (c2_1 (a658))
% 1.06/1.22  (c7_2 (a690) (a738))
% 1.06/1.22  (-. (c3_2 (a656) zenon_X53))
% 1.06/1.22  (c3_2 zenon_X20 (a731))
% 1.06/1.22  (zenon_X23 != (a639))
% 1.06/1.22  (zenon_X56 != zenon_X79)
% 1.06/1.22  (zenon_X38 != zenon_X53)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X52))
% 1.06/1.22  (zenon_X16 != zenon_X53)
% 1.06/1.22  ((a623) != zenon_X52)
% 1.06/1.22  ((a670) != (a639))
% 1.06/1.22  (zenon_X10 != zenon_X11)
% 1.06/1.22  ((a702) != zenon_X27)
% 1.06/1.22  (zenon_X16 != zenon_X19)
% 1.06/1.22  (-. (c1_2 (a622) zenon_X44))
% 1.06/1.22  (-. (c4_2 (a658) (a677)))
% 1.06/1.22  (c7_2 (a618) (a664))
% 1.06/1.22  ((a731) != zenon_X24)
% 1.06/1.22  (-. (c9_1 (a753)))
% 1.06/1.22  (zenon_X20 != (a690))
% 1.06/1.22  ((a670) != (a737))
% 1.06/1.22  (c8_1 (a709))
% 1.06/1.22  (c3_2 (a669) zenon_X58)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X54))
% 1.06/1.22  (c5_2 (a701) (a744))
% 1.06/1.22  ((a629) != zenon_X51)
% 1.06/1.22  (-. (c4_2 zenon_X25 (a738)))
% 1.06/1.22  (zenon_X16 != (a714))
% 1.06/1.22  (c4_2 (a669) zenon_X48)
% 1.06/1.22  ((a640) != zenon_X42)
% 1.06/1.22  (-. (c4_2 (a622) (a623)))
% 1.06/1.22  (-. (c6_2 (a701) zenon_X15))
% 1.06/1.22  ((a657) != zenon_X56)
% 1.06/1.22  (ndr1_1 (a656))
% 1.06/1.22  ((a690) != zenon_X25)
% 1.06/1.22  (c3_2 (a669) zenon_X39)
% 1.06/1.22  (c2_1 (a625))
% 1.06/1.22  (c2_1 zenon_X25)
% 1.06/1.22  ((a744) != zenon_X58)
% 1.06/1.22  (zenon_X10 != (a732))
% 1.06/1.22  ((a664) != (a626))
% 1.06/1.22  (zenon_X1 != zenon_X48)
% 1.06/1.22  ((a731) != zenon_X69)
% 1.06/1.22  (c5_2 (a701) (a623))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X56))
% 1.06/1.22  (c8_0)
% 1.06/1.22  (-. (c1_2 (a737) (a629)))
% 1.06/1.22  (zenon_X24 != (a662))
% 1.06/1.22  ((a744) != (a714))
% 1.06/1.22  ((a623) != (a657))
% 1.06/1.22  ((a625) != (a670))
% 1.06/1.22  (-. (c1_2 (a737) (a626)))
% 1.06/1.22  ((a618) != (a669))
% 1.06/1.22  (-. (c2_1 zenon_X2))
% 1.06/1.22  (c2_1 zenon_X20)
% 1.06/1.22  (zenon_X21 != zenon_X2)
% 1.06/1.22  ((a629) != zenon_X42)
% 1.06/1.22  (c10_2 (a669) (a744))
% 1.06/1.22  (c5_2 (a701) (a629))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X58))
% 1.06/1.22  (-. (c3_2 zenon_X4 (a657)))
% 1.06/1.22  ((a626) != zenon_X8)
% 1.06/1.22  ((a753) != zenon_X21)
% 1.06/1.22  ((a731) != zenon_X66)
% 1.06/1.22  ((a738) != zenon_X49)
% 1.06/1.22  (zenon_X20 != (a729))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X40))
% 1.06/1.22  (zenon_X15 != zenon_X29)
% 1.06/1.22  (c6_2 (a669) (a738))
% 1.06/1.22  ((a662) != zenon_X38)
% 1.06/1.22  ((a709) != zenon_X21)
% 1.06/1.22  ((a732) != zenon_X54)
% 1.06/1.22  (ndr1_1 zenon_X3)
% 1.06/1.22  (zenon_X49 != (a677))
% 1.06/1.22  ((a626) != zenon_X79)
% 1.06/1.22  (-. (c4_2 (a656) zenon_X63))
% 1.06/1.22  (-. (c3_2 (a737) (a629)))
% 1.06/1.22  ((a657) != (a738))
% 1.06/1.22  ((a656) != (a628))
% 1.06/1.22  (zenon_X54 != zenon_X53)
% 1.06/1.22  ((a753) != (a729))
% 1.06/1.22  (zenon_X24 != zenon_X55)
% 1.06/1.22  (c6_2 (a669) zenon_X11)
% 1.06/1.22  (zenon_X72 != zenon_X40)
% 1.06/1.22  ((a640) != (a629))
% 1.06/1.22  ((a664) != (a629))
% 1.06/1.22  ((a754) != (a657))
% 1.06/1.22  (c6_2 (a669) (a732))
% 1.06/1.22  (zenon_X12 != zenon_X24)
% 1.06/1.22  (zenon_X58 != zenon_X40)
% 1.06/1.22  ((a629) != zenon_X65)
% 1.06/1.22  (-. (c4_2 zenon_X25 zenon_X56))
% 1.06/1.22  ((a640) != zenon_X26)
% 1.06/1.22  ((a732) != zenon_X39)
% 1.06/1.22  (c3_2 (a669) zenon_X10)
% 1.06/1.22  (c6_2 (a669) zenon_X41)
% 1.06/1.22  (zenon_X25 != (a669))
% 1.06/1.22  ((a629) != zenon_X1)
% 1.06/1.22  (c7_2 (a690) (a732))
% 1.06/1.22  ((a731) != zenon_X42)
% 1.06/1.22  (-. (c3_2 (a625) (a731)))
% 1.06/1.22  (c8_2 (a618) (a702))
% 1.06/1.22  (zenon_X10 != zenon_X55)
% 1.06/1.22  (-. (c8_1 (a690)))
% 1.06/1.22  (-. (c3_2 (a658) zenon_X69))
% 1.06/1.22  ((a658) != (a639))
% 1.06/1.22  ((a709) != (a729))
% 1.06/1.22  (-. (c4_2 (a709) zenon_X73))
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X38))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a702)))
% 1.06/1.22  ((a657) != zenon_X8)
% 1.06/1.22  ((a754) != zenon_X46)
% 1.06/1.22  ((a690) != (a753))
% 1.06/1.22  ((a754) != zenon_X16)
% 1.06/1.22  ((a754) != zenon_X53)
% 1.06/1.22  (ndr1_1 zenon_X20)
% 1.06/1.22  ((a744) != zenon_X8)
% 1.06/1.22  (c3_2 (a669) zenon_X49)
% 1.06/1.22  ((a626) != zenon_X51)
% 1.06/1.22  (-. (c4_2 (a729) (a744)))
% 1.06/1.22  (zenon_X16 != zenon_X1)
% 1.06/1.22  (-. (c4_1 (a670)))
% 1.06/1.22  (-. (c3_2 (a729) (a640)))
% 1.06/1.22  ((a732) != zenon_X66)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X49))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X48))
% 1.06/1.22  ((a690) != (a701))
% 1.06/1.22  (c8_2 (a753) (a657))
% 1.06/1.22  (zenon_X10 != zenon_X39)
% 1.06/1.22  ((a664) != zenon_X49)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X38))
% 1.06/1.22  ((a629) != (a731))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X79))
% 1.06/1.22  (zenon_X82 != (a738))
% 1.06/1.22  (c4_2 (a690) (a731))
% 1.06/1.22  (c4_2 (a618) (a664))
% 1.06/1.22  (c3_2 (a669) zenon_X48)
% 1.06/1.22  (-. (c9_1 (a669)))
% 1.06/1.22  ((a738) != zenon_X63)
% 1.06/1.22  (c4_2 (a669) zenon_X66)
% 1.06/1.22  (c4_2 (a669) zenon_X38)
% 1.06/1.22  (zenon_X42 != zenon_X8)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X38))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X46))
% 1.06/1.22  (-. (c3_2 (a753) (a714)))
% 1.06/1.22  (c6_2 (a669) (a744))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X8))
% 1.06/1.22  (zenon_X40 != zenon_X66)
% 1.06/1.22  (ndr1_1 zenon_X21)
% 1.06/1.22  (c4_2 (a669) zenon_X56)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X39))
% 1.06/1.22  (-. (c3_2 (a737) zenon_X58))
% 1.06/1.22  (zenon_X19 != zenon_X8)
% 1.06/1.22  (-. (c10_1 zenon_X5))
% 1.06/1.22  ((a658) != (a753))
% 1.06/1.22  ((a732) != zenon_X63)
% 1.06/1.22  (-. (c4_2 (a729) zenon_X19))
% 1.06/1.22  ((a754) != zenon_X60)
% 1.06/1.22  ((a738) != zenon_X79)
% 1.06/1.22  ((a731) != zenon_X67)
% 1.06/1.22  (zenon_X29 != (a664))
% 1.06/1.22  (-. (c3_2 (a625) (a738)))
% 1.06/1.22  (zenon_X41 != zenon_X44)
% 1.06/1.22  (zenon_X10 != zenon_X1)
% 1.06/1.22  ((a731) != zenon_X76)
% 1.06/1.22  (-. (c3_2 (a701) zenon_X10))
% 1.06/1.22  ((a626) != zenon_X66)
% 1.06/1.22  ((a657) != zenon_X42)
% 1.06/1.22  (zenon_X52 != zenon_X79)
% 1.06/1.22  ((a732) != zenon_X82)
% 1.06/1.22  ((a623) != (a662))
% 1.06/1.22  (zenon_X48 != zenon_X52)
% 1.06/1.22  ((a626) != zenon_X1)
% 1.06/1.22  ((a738) != zenon_X11)
% 1.06/1.22  (-. (c3_2 (a639) (a677)))
% 1.06/1.22  (zenon_X16 != zenon_X58)
% 1.06/1.22  (zenon_X11 != zenon_X57)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X51))
% 1.06/1.22  (-. (c3_2 (a656) (a664)))
% 1.06/1.22  (-. (c4_2 zenon_X23 zenon_X46))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X10))
% 1.06/1.22  (zenon_X54 != zenon_X79)
% 1.06/1.22  ((a677) != (a714))
% 1.06/1.22  (-. (c1_2 (a737) (a623)))
% 1.06/1.22  ((a744) != zenon_X15)
% 1.06/1.22  (zenon_X20 != (a701))
% 1.06/1.22  (c1_2 (a669) (a738))
% 1.06/1.22  ((a744) != (a662))
% 1.06/1.22  (c7_2 (a690) (a623))
% 1.06/1.22  (c4_2 (a669) (a714))
% 1.06/1.22  ((a744) != zenon_X44)
% 1.06/1.22  (-. (c4_2 (a618) (a677)))
% 1.06/1.22  ((a629) != zenon_X58)
% 1.06/1.22  (c3_2 (a669) zenon_X55)
% 1.06/1.22  (-. (c3_2 (a622) (a732)))
% 1.06/1.22  (-. (c1_2 (a622) (a731)))
% 1.06/1.22  ((a662) != zenon_X44)
% 1.06/1.22  (-. (c4_2 (a737) (a738)))
% 1.06/1.22  ((a669) != (a639))
% 1.06/1.22  ((a658) != (a755))
% 1.06/1.22  (-. (c3_2 (a753) (a623)))
% 1.06/1.22  ((a626) != zenon_X70)
% 1.06/1.22  ((a690) != (a656))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X40))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X58))
% 1.06/1.22  ((a628) != (a701))
% 1.06/1.22  (-. (c4_2 zenon_X7 zenon_X71))
% 1.06/1.22  (c7_2 (a708) (a702))
% 1.06/1.22  (-. (c9_2 (a618) (a732)))
% 1.06/1.22  ((a640) != zenon_X27)
% 1.06/1.22  ((a702) != zenon_X54)
% 1.06/1.22  ((a731) != zenon_X15)
% 1.06/1.22  (zenon_X38 != zenon_X79)
% 1.06/1.22  (c6_2 (a669) (a640))
% 1.06/1.22  ((a702) != zenon_X16)
% 1.06/1.22  ((a628) != (a729))
% 1.06/1.22  (zenon_X10 != (a657))
% 1.06/1.22  ((a626) != zenon_X57)
% 1.06/1.22  ((a744) != zenon_X48)
% 1.06/1.22  (c9_1 (a690))
% 1.06/1.22  ((a623) != zenon_X26)
% 1.06/1.22  (c6_2 (a669) (a662))
% 1.06/1.22  (-. (c4_2 (a618) (a626)))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X48))
% 1.06/1.22  (zenon_X38 != zenon_X8)
% 1.06/1.22  (c4_2 (a690) zenon_X55)
% 1.06/1.22  ((a714) != zenon_X8)
% 1.06/1.22  (-. (c4_2 (a753) (a754)))
% 1.06/1.22  (-. (c1_2 zenon_X28 zenon_X41))
% 1.06/1.22  ((a737) != (a709))
% 1.06/1.22  (zenon_X12 != zenon_X55)
% 1.06/1.22  (-. (c3_2 (a628) (a677)))
% 1.06/1.22  ((a657) != zenon_X57)
% 1.06/1.22  (-. (c3_2 (a729) (a662)))
% 1.06/1.22  (c8_2 (a753) (a744))
% 1.06/1.22  (zenon_X43 != (a629))
% 1.06/1.22  ((a744) != zenon_X63)
% 1.06/1.22  ((a731) != zenon_X44)
% 1.06/1.22  (zenon_X13 != (a670))
% 1.06/1.22  (zenon_X20 != zenon_X7)
% 1.06/1.22  (c10_2 zenon_X9 (a731))
% 1.06/1.22  ((a690) != (a639))
% 1.06/1.22  (zenon_X29 != zenon_X44)
% 1.06/1.22  (zenon_X48 != zenon_X38)
% 1.06/1.22  ((a658) != (a622))
% 1.06/1.22  (c4_2 (a628) (a629))
% 1.06/1.22  (-. (c1_2 (a753) (a754)))
% 1.06/1.22  (zenon_X56 != (a662))
% 1.06/1.22  (zenon_X10 != zenon_X43)
% 1.06/1.22  (zenon_X51 != zenon_X66)
% 1.06/1.22  (-. (c4_2 (a701) (a662)))
% 1.06/1.22  (c1_2 (a669) zenon_X29)
% 1.06/1.22  (-. (c3_2 zenon_X21 (a732)))
% 1.06/1.22  ((a744) != zenon_X54)
% 1.06/1.22  (-. (c3_2 (a701) (a623)))
% 1.06/1.22  (-. (c4_2 (a628) zenon_X16))
% 1.06/1.22  ((a623) != zenon_X57)
% 1.06/1.22  (c3_2 (a669) zenon_X38)
% 1.06/1.22  (ndr1_1 (a628))
% 1.06/1.22  (-. (c3_2 zenon_X21 (a744)))
% 1.06/1.22  (-. (c3_2 (a729) (a754)))
% 1.06/1.22  ((a738) != zenon_X60)
% 1.06/1.22  ((a744) != zenon_X57)
% 1.06/1.22  (zenon_X58 != zenon_X55)
% 1.06/1.22  (zenon_X72 != zenon_X8)
% 1.06/1.22  (zenon_X10 != zenon_X8)
% 1.06/1.22  (-. (c7_2 (a755) zenon_X61))
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X16))
% 1.06/1.22  (c8_1 zenon_X20)
% 1.06/1.22  (-. (c3_2 (a737) (a626)))
% 1.06/1.22  (c6_2 (a669) (a731))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X38))
% 1.06/1.22  (zenon_X72 != (a677))
% 1.06/1.22  (-. (c3_2 (a656) (a702)))
% 1.06/1.22  ((a690) != zenon_X18)
% 1.06/1.22  ((a618) != (a701))
% 1.06/1.22  (zenon_X29 != zenon_X41)
% 1.06/1.22  (c7_2 (a618) (a754))
% 1.06/1.22  ((a754) != zenon_X57)
% 1.06/1.22  (c8_1 (a755))
% 1.06/1.22  (zenon_X15 != (a662))
% 1.06/1.22  ((a664) != zenon_X39)
% 1.06/1.22  (c7_2 (a618) (a623))
% 1.06/1.22  ((a670) != zenon_X2)
% 1.06/1.22  (-. (c3_2 (a639) (a732)))
% 1.06/1.22  (c10_2 zenon_X9 (a738))
% 1.06/1.22  (zenon_X10 != zenon_X42)
% 1.06/1.22  ((a662) != zenon_X57)
% 1.06/1.22  ((a623) != zenon_X55)
% 1.06/1.22  (-. (c6_2 (a701) zenon_X57))
% 1.06/1.22  ((a677) != (a629))
% 1.06/1.22  (zenon_X15 != zenon_X57)
% 1.06/1.22  (zenon_X55 != zenon_X53)
% 1.06/1.22  ((a662) != (a691))
% 1.06/1.22  ((a738) != zenon_X46)
% 1.06/1.22  ((a738) != zenon_X65)
% 1.06/1.22  (c2_1 (a628))
% 1.06/1.22  (-. (c3_2 (a729) (a664)))
% 1.06/1.22  ((a658) != (a656))
% 1.06/1.22  (c9_2 zenon_X3 (a744))
% 1.06/1.22  (zenon_X7 != zenon_X2)
% 1.06/1.22  ((a626) != zenon_X44)
% 1.06/1.22  (-. (c7_2 (a753) zenon_X60))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X51))
% 1.06/1.22  (zenon_X39 != zenon_X79)
% 1.06/1.22  (ndr1_1 (a690))
% 1.06/1.22  (c9_1 (a622))
% 1.06/1.22  (c8_2 (a753) (a730))
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X8))
% 1.06/1.22  ((a656) != (a701))
% 1.06/1.22  ((a702) != zenon_X39)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X49))
% 1.06/1.22  ((a662) != zenon_X11)
% 1.06/1.22  (c6_2 (a669) (a623))
% 1.06/1.22  (c4_2 (a669) zenon_X39)
% 1.06/1.22  (-. (c4_2 (a701) (a623)))
% 1.06/1.22  (-. (c8_1 zenon_X23))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X60))
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X60))
% 1.06/1.22  (zenon_X24 != zenon_X19)
% 1.06/1.22  (-. (c1_2 (a669) (a657)))
% 1.06/1.22  ((a662) != zenon_X79)
% 1.06/1.22  (zenon_X16 != zenon_X66)
% 1.06/1.22  (-. (c3_2 (a625) (a664)))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X44))
% 1.06/1.22  ((a738) != (a677))
% 1.06/1.22  ((a662) != zenon_X53)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X55))
% 1.06/1.22  ((a628) != (a622))
% 1.06/1.22  (zenon_X12 != zenon_X82)
% 1.06/1.22  ((a732) != zenon_X1)
% 1.06/1.22  ((a629) != zenon_X26)
% 1.06/1.22  (c4_2 (a690) zenon_X12)
% 1.06/1.22  ((a657) != zenon_X11)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X66))
% 1.06/1.22  ((a628) != (a669))
% 1.06/1.22  (-. (c3_2 (a737) zenon_X10))
% 1.06/1.22  (-. (c1_2 (a669) (a629)))
% 1.06/1.22  (-. (c4_2 (a618) zenon_X66))
% 1.06/1.22  ((a731) != zenon_X58)
% 1.06/1.22  ((a738) != (a714))
% 1.06/1.22  (zenon_X55 != zenon_X46)
% 1.06/1.22  ((a664) != zenon_X53)
% 1.06/1.22  (c8_1 (a753))
% 1.06/1.22  (zenon_X54 != (a677))
% 1.06/1.22  (-. (c4_2 zenon_X25 (a732)))
% 1.06/1.22  ((a658) != (a625))
% 1.06/1.22  ((a755) != zenon_X23)
% 1.06/1.22  (-. (c1_2 zenon_X28 (a731)))
% 1.06/1.22  (c4_2 (a690) (a738))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X70))
% 1.06/1.22  (c10_2 (a669) (a677))
% 1.06/1.22  (-. (c3_2 (a729) (a626)))
% 1.06/1.22  ((a623) != (a691))
% 1.06/1.22  (-. (c1_2 (a622) zenon_X57))
% 1.06/1.22  (-. (c4_2 (a628) (a623)))
% 1.06/1.22  ((a657) != zenon_X44)
% 1.06/1.22  (c4_2 zenon_X25 (a731))
% 1.06/1.22  ((a622) != (a729))
% 1.06/1.22  (-. (c8_1 zenon_X4))
% 1.06/1.22  (zenon_X43 != zenon_X57)
% 1.06/1.22  (-. (c3_2 (a753) (a738)))
% 1.06/1.22  ((a623) != zenon_X49)
% 1.06/1.22  ((a626) != zenon_X40)
% 1.06/1.22  (c8_2 (a753) zenon_X70)
% 1.06/1.22  (c7_2 (a708) (a677))
% 1.06/1.22  (c8_2 (a729) (a730))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a744)))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X72))
% 1.06/1.22  ((a657) != zenon_X66)
% 1.06/1.22  (zenon_X15 != zenon_X41)
% 1.06/1.22  (c8_2 (a753) (a640))
% 1.06/1.22  (zenon_X58 != zenon_X19)
% 1.06/1.22  (zenon_X49 != zenon_X79)
% 1.06/1.22  (c5_2 (a701) (a732))
% 1.06/1.22  (zenon_X79 != zenon_X8)
% 1.06/1.22  ((a709) != zenon_X23)
% 1.06/1.22  (c3_2 (a670) (a731))
% 1.06/1.22  (zenon_X16 != (a657))
% 1.06/1.22  (-. (c4_2 (a690) (a662)))
% 1.06/1.22  ((a622) != (a737))
% 1.06/1.22  (c8_2 (a753) zenon_X48)
% 1.06/1.22  (-. (c3_2 (a625) zenon_X10))
% 1.06/1.22  ((a737) != zenon_X2)
% 1.06/1.22  (c3_2 (a669) (a623))
% 1.06/1.22  (c3_1 (a618))
% 1.06/1.22  ((a690) != (a709))
% 1.06/1.22  (-. (c3_2 zenon_X2 (a731)))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X72))
% 1.06/1.22  (-. (c3_2 zenon_X7 (a623)))
% 1.06/1.22  (-. (c3_2 (a628) (a662)))
% 1.06/1.22  (c6_2 (a656) (a657))
% 1.06/1.22  ((a738) != (a629))
% 1.06/1.22  (c6_2 (a669) zenon_X29)
% 1.06/1.22  (c6_2 (a669) (a702))
% 1.06/1.22  (c5_2 (a701) (a738))
% 1.06/1.22  ((a732) != zenon_X53)
% 1.06/1.22  (zenon_X51 != zenon_X79)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X41))
% 1.06/1.22  ((a738) != zenon_X38)
% 1.06/1.22  ((a732) != (a691))
% 1.06/1.22  (zenon_X1 != zenon_X53)
% 1.06/1.22  (-. (c2_0))
% 1.06/1.22  ((a657) != zenon_X70)
% 1.06/1.22  (-. (c5_2 (a708) zenon_X55))
% 1.06/1.22  (-. (c5_2 (a709) (a714)))
% 1.06/1.22  ((a730) != zenon_X0)
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X55))
% 1.06/1.22  (-. (c3_2 (a701) (a677)))
% 1.06/1.22  (zenon_X42 != (a677))
% 1.06/1.22  ((a714) != zenon_X66)
% 1.06/1.22  (c2_2 (a690) (a662))
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X40))
% 1.06/1.22  (-. (c1_2 (a669) zenon_X44))
% 1.06/1.22  (c6_2 (a618) (a731))
% 1.06/1.22  (-. (c3_2 (a639) (a629)))
% 1.06/1.22  ((a625) != zenon_X4)
% 1.06/1.22  (-. (c4_2 (a618) zenon_X58))
% 1.06/1.22  (-. (c3_2 zenon_X2 (a640)))
% 1.06/1.22  (c6_2 (a669) zenon_X43)
% 1.06/1.22  (c6_2 (a625) (a626))
% 1.06/1.22  (-. (c3_2 zenon_X4 zenon_X53))
% 1.06/1.22  (c3_2 (a669) zenon_X42)
% 1.06/1.22  ((a664) != zenon_X0)
% 1.06/1.22  (zenon_X25 != (a701))
% 1.06/1.22  (zenon_X25 != (a622))
% 1.06/1.22  (-. (c6_2 zenon_X18 (a662)))
% 1.06/1.22  ((a702) != (a731))
% 1.06/1.22  (-. (c1_2 zenon_X28 (a626)))
% 1.06/1.22  ((a730) != (a677))
% 1.06/1.22  ((a702) != zenon_X8)
% 1.06/1.22  (-. (c10_2 (a618) zenon_X57))
% 1.06/1.22  ((a662) != zenon_X58)
% 1.06/1.22  (c10_2 (a669) zenon_X15)
% 1.06/1.22  ((a670) != zenon_X23)
% 1.06/1.22  ((a657) != zenon_X54)
% 1.06/1.22  (-. (c4_2 (a729) (a731)))
% 1.06/1.22  (ndr1_1 (a753))
% 1.06/1.22  ((a669) != zenon_X4)
% 1.06/1.22  (c10_2 (a669) zenon_X43)
% 1.06/1.22  (-. (c4_2 zenon_X23 (a664)))
% 1.06/1.22  ((a657) != zenon_X60)
% 1.06/1.22  ((a738) != zenon_X40)
% 1.06/1.22  ((a662) != zenon_X54)
% 1.06/1.22  ((a662) != zenon_X16)
% 1.06/1.22  (-. (c3_2 zenon_X7 (a730)))
% 1.06/1.22  ((a664) != (a714))
% 1.06/1.22  (c2_1 zenon_X23)
% 1.06/1.22  (-. (c4_2 (a628) (a744)))
% 1.06/1.22  ((a618) != (a622))
% 1.06/1.22  (-. (c8_1 zenon_X2))
% 1.06/1.22  (ndr1_1 zenon_X7)
% 1.06/1.22  (zenon_X29 != (a626))
% 1.06/1.22  ((a744) != zenon_X49)
% 1.06/1.22  ((a669) != zenon_X2)
% 1.06/1.22  (-. (c3_2 (a622) zenon_X8))
% 1.06/1.22  (-. (c8_1 (a669)))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X49))
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X58))
% 1.06/1.22  (-. (c3_2 (a625) zenon_X48))
% 1.06/1.22  (c6_2 (a669) (a629))
% 1.06/1.22  ((a702) != (a626))
% 1.06/1.22  (zenon_X29 != (a732))
% 1.06/1.22  ((a690) != (a670))
% 1.06/1.22  (zenon_X20 != (a658))
% 1.06/1.22  (-. (c3_2 (a656) (a738)))
% 1.06/1.22  (-. (c3_2 (a622) zenon_X38))
% 1.06/1.22  (zenon_X11 != zenon_X44)
% 1.06/1.22  ((a702) != (a732))
% 1.06/1.22  (-. (c3_2 (a701) zenon_X79))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X79))
% 1.06/1.22  (c10_0)
% 1.06/1.22  ((a662) != zenon_X51)
% 1.06/1.22  (c4_2 zenon_X7 (a732))
% 1.06/1.22  ((a629) != zenon_X66)
% 1.06/1.22  (-. (c4_2 (a729) (a664)))
% 1.06/1.22  (zenon_X48 != zenon_X79)
% 1.06/1.22  (zenon_X48 != zenon_X70)
% 1.06/1.22  (c7_2 (a708) (a623))
% 1.06/1.22  ((a732) != zenon_X60)
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X53))
% 1.06/1.22  ((a744) != zenon_X24)
% 1.06/1.22  (zenon_X16 != (a626))
% 1.06/1.22  ((a623) != (a738))
% 1.06/1.22  (-. (c3_2 (a737) (a738)))
% 1.06/1.22  (-. (c7_1 (a628)))
% 1.06/1.22  (-. (c4_2 (a658) (a623)))
% 1.06/1.22  (-. (c3_2 (a622) (a731)))
% 1.06/1.22  (c10_1 (a670))
% 1.06/1.22  ((a657) != zenon_X12)
% 1.06/1.22  ((a657) != zenon_X27)
% 1.06/1.22  (-. (c3_2 zenon_X2 zenon_X72))
% 1.06/1.22  (c7_2 (a708) (a754))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X53))
% 1.06/1.22  (c7_2 (a708) (a662))
% 1.06/1.22  ((a662) != zenon_X65)
% 1.06/1.22  (c4_2 (a690) (a744))
% 1.06/1.22  (-. (c3_2 (a656) (a732)))
% 1.06/1.22  (zenon_X10 != zenon_X52)
% 1.06/1.22  ((a623) != zenon_X62)
% 1.06/1.22  (zenon_X25 != zenon_X4)
% 1.06/1.22  (-. (c2_2 (a701) (a702)))
% 1.06/1.22  (c10_2 (a669) zenon_X29)
% 1.06/1.22  ((a732) != zenon_X16)
% 1.06/1.22  ((a755) != (a729))
% 1.06/1.22  ((a626) != (a662))
% 1.06/1.22  (zenon_X20 != zenon_X4)
% 1.06/1.22  ((a626) != zenon_X26)
% 1.06/1.22  ((a677) != zenon_X27)
% 1.06/1.22  ((a754) != zenon_X56)
% 1.06/1.22  (c7_2 zenon_X17 (a664))
% 1.06/1.22  ((a623) != zenon_X51)
% 1.06/1.22  (-. (c8_2 (a628) (a629)))
% 1.06/1.22  (c9_2 (a690) (a731))
% 1.06/1.22  (-. (c4_2 (a628) zenon_X79))
% 1.06/1.22  ((a753) != (a625))
% 1.06/1.22  (c6_2 (a669) zenon_X10)
% 1.06/1.22  (-. (c3_2 (a625) zenon_X8))
% 1.06/1.22  ((a664) != zenon_X12)
% 1.06/1.22  (-. (c4_0))
% 1.06/1.22  (-. (c4_2 (a628) zenon_X24))
% 1.06/1.22  (-. (c4_2 (a737) zenon_X10))
% 1.06/1.22  (-. (c4_2 zenon_X4 zenon_X81))
% 1.06/1.22  (c3_2 (a656) (a657))
% 1.06/1.22  (-. (c3_2 zenon_X21 zenon_X16))
% 1.06/1.22  (c6_0)
% 1.06/1.22  (zenon_X66 != zenon_X53)
% 1.06/1.22  ((a626) != zenon_X48)
% 1.06/1.22  (-. (c3_2 (a737) (a702)))
% 1.06/1.22  ((a623) != zenon_X42)
% 1.06/1.22  (zenon_X10 != zenon_X79)
% 1.06/1.22  (zenon_X19 != (a664))
% 1.06/1.22  ((a625) != (a721))
% 1.06/1.22  (zenon_X42 != zenon_X53)
% 1.06/1.22  (-. (c3_2 (a625) (a677)))
% 1.06/1.22  (zenon_X15 != (a754))
% 1.06/1.22  (-. (c3_2 (a656) (a623)))
% 1.06/1.22  (zenon_X10 != zenon_X48)
% 1.06/1.22  ((a737) != (a753))
% 1.06/1.22  ((a629) != zenon_X38)
% 1.06/1.22  ((a730) != (a657))
% 1.06/1.22  (c10_2 (a669) zenon_X10)
% 1.06/1.22  ((a670) != zenon_X5)
% 1.06/1.22  (c5_2 (a701) (a662))
% 1.06/1.22  (-. (c3_2 (a625) zenon_X49))
% 1.06/1.22  (zenon_X56 != zenon_X8)
% 1.06/1.22  (-. (c3_2 (a625) (a629)))
% 1.06/1.22  ((a626) != zenon_X53)
% 1.06/1.22  (c4_2 (a669) zenon_X1)
% 1.06/1.22  (zenon_X11 != (a629))
% 1.06/1.22  (-. (c4_2 (a729) zenon_X52))
% 1.06/1.22  (c4_2 (a669) zenon_X49)
% 1.06/1.22  ((a626) != zenon_X27)
% 1.06/1.22  ((a623) != zenon_X10)
% 1.06/1.22  ((a623) != zenon_X65)
% 1.06/1.22  (-. (c3_2 zenon_X7 zenon_X53))
% 1.06/1.22  (zenon_X16 != zenon_X70)
% 1.06/1.22  ((a737) != zenon_X28)
% 1.06/1.22  (c8_2 (a753) zenon_X10)
% 1.06/1.22  (c4_2 (a690) (a626))
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X26))
% 1.06/1.22  ((a623) != zenon_X41)
% 1.06/1.22  (-. (c3_2 (a753) (a664)))
% 1.06/1.22  (-. (c8_1 zenon_X25))
% 1.06/1.22  ((a656) != (a755))
% 1.06/1.22  ((a626) != zenon_X39)
% 1.06/1.22  (-. (c3_2 zenon_X4 (a629)))
% 1.06/1.22  ((a628) != zenon_X21)
% 1.06/1.22  (-. (c4_2 zenon_X25 zenon_X24))
% 1.06/1.22  (-. (c3_2 zenon_X25 zenon_X67))
% 1.06/1.22  ((a670) != (a753))
% 1.06/1.22  (zenon_X70 != (a640))
% 1.06/1.22  (c7_2 (a690) (a657))
% 1.06/1.22  (c5_2 (a701) (a664))
% 1.06/1.22  (c7_2 zenon_X20 (a714))
% 1.06/1.22  ((a754) != (a629))
% 1.06/1.22  (c10_2 (a753) (a754))
% 1.06/1.22  (c3_2 (a669) (a730))
% 1.06/1.22  ((a664) != zenon_X15)
% 1.06/1.22  ((a623) != (a664))
% 1.06/1.22  (c4_2 (a690) (a754))
% 1.06/1.22  (-. (c3_2 zenon_X4 (a626)))
% 1.06/1.22  (-. (c4_2 (a737) (a744)))
% 1.06/1.22  (zenon_X10 != (a640))
% 1.06/1.22  (zenon_X79 != (a677))
% 1.06/1.22  (c3_2 (a669) (a702))
% 1.06/1.22  ((a657) != zenon_X58)
% 1.06/1.22  (c3_2 (a669) (a732))
% 1.06/1.22  (-. (c3_2 (a729) (a629)))
% 1.06/1.22  (zenon_X16 != zenon_X55)
% 1.06/1.22  (zenon_X39 != zenon_X66)
% 1.06/1.22  (-. (c3_2 (a701) zenon_X39))
% 1.06/1.22  (-. (c3_2 zenon_X21 (a714)))
% 1.06/1.22  ((a730) != zenon_X16)
% 1.06/1.22  (zenon_X48 != zenon_X49)
% 1.06/1.22  (zenon_X10 != zenon_X46)
% 1.06/1.22  (-. (c3_2 (a701) (a731)))
% 1.06/1.22  (zenon_X10 != zenon_X16)
% 1.06/1.22  (-. (c3_2 (a701) zenon_X58))
% 1.06/1.22  (-. (c9_1 (a709)))
% 1.06/1.22  (-. (c3_2 (a729) zenon_X52))
% 1.06/1.22  ((a737) != zenon_X7)
% 1.06/1.22  ((a640) != (a710))
% 1.06/1.22  ((a738) != zenon_X26)
% 1.06/1.22  (zenon_X58 != zenon_X48)
% 1.06/1.22  (-. (c4_2 zenon_X23 zenon_X55))
% 1.06/1.22  (-. (c1_2 (a737) (a664)))
% 1.06/1.22  ((a662) != zenon_X62)
% 1.06/1.22  ((a732) != (a738))
% 1.06/1.22  ((a732) != zenon_X27)
% 1.06/1.22  (-. (c3_2 (a656) zenon_X51))
% 1.06/1.22  (ndr1_1 zenon_X23)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X39))
% 1.06/1.22  (-. (c4_2 (a658) zenon_X10))
% 1.06/1.22  ((a732) != zenon_X71)
% 1.06/1.22  (zenon_X16 != zenon_X42)
% 1.06/1.22  (-. (c5_2 (a708) zenon_X54))
% 1.06/1.22  ((a732) != zenon_X56)
% 1.06/1.22  (-. (c3_2 (a639) zenon_X48))
% 1.06/1.22  (zenon_X23 != (a729))
% 1.06/1.22  ((a629) != zenon_X64)
% 1.06/1.22  ((a664) != (a662))
% 1.06/1.22  ((a658) != zenon_X2)
% 1.06/1.22  (zenon_X41 != (a731))
% 1.06/1.22  (-. (c1_1 (a721)))
% 1.06/1.22  ((a657) != zenon_X15)
% 1.06/1.22  (zenon_X12 != zenon_X42)
% 1.06/1.22  (-. (c4_2 (a618) (a657)))
% 1.06/1.22  ((a730) != zenon_X8)
% 1.06/1.22  ((a729) != (a670))
% 1.06/1.22  (c3_2 (a669) zenon_X56)
% 1.06/1.22  (c4_2 (a618) zenon_X10)
% 1.06/1.22  (-. (c3_2 (a628) zenon_X79))
% 1.06/1.22  ((a640) != zenon_X57)
% 1.06/1.22  ((a623) != zenon_X8)
% 1.06/1.22  (c1_2 (a669) zenon_X27)
% 1.06/1.22  (zenon_X10 != (a662))
% 1.06/1.22  (-. (c3_2 (a737) (a662)))
% 1.06/1.22  ((a657) != (a640))
% 1.06/1.22  (zenon_X10 != zenon_X27)
% 1.06/1.22  (zenon_X41 != (a629))
% 1.06/1.22  ((a721) != (a737))
% 1.06/1.22  (c8_2 (a618) (a677))
% 1.06/1.22  (-. (c2_1 (a669)))
% 1.06/1.22  (zenon_X20 != (a656))
% 1.06/1.22  (-. (c3_2 (a690) zenon_X50))
% 1.06/1.22  ((a738) != zenon_X19)
% 1.06/1.22  (-. (c4_2 (a622) (a744)))
% 1.06/1.22  (-. (c1_2 (a737) zenon_X44))
% 1.06/1.22  (-. (c5_2 (a708) zenon_X8))
% 1.06/1.22  ((a656) != zenon_X4)
% 1.06/1.22  (c4_2 (a669) zenon_X51)
% 1.06/1.22  ((a626) != (a738))
% 1.06/1.22  ((a623) != zenon_X61)
% 1.06/1.22  (-. (c1_2 zenon_X9 zenon_X55))
% 1.06/1.22  ((a629) != zenon_X79)
% 1.06/1.22  (-. (c3_2 (a729) zenon_X16))
% 1.06/1.22  ((a623) != (a702))
% 1.06/1.22  ((a664) != (a731))
% 1.06/1.22  (zenon_X10 != zenon_X51)
% 1.06/1.22  (c3_1 (a625))
% 1.06/1.22  (c4_2 (a669) zenon_X54)
% 1.06/1.22  (-. (c4_2 (a737) (a732)))
% 1.06/1.22  (c7_2 (a708) (a664))
% 1.06/1.22  (c6_2 (a658) (a731))
% 1.06/1.22  (-. (c6_2 (a690) zenon_X56))
% 1.06/1.22  (zenon_X52 != zenon_X66)
% 1.06/1.22  ((a623) != zenon_X38)
% 1.06/1.22  ((a662) != (a629))
% 1.06/1.22  ((a753) != (a628))
% 1.06/1.22  (-. (c3_2 (a628) (a664)))
% 1.06/1.22  ((a709) != (a622))
% 1.06/1.22  (-. (c1_2 (a737) zenon_X10))
% 1.06/1.22  ((a702) != zenon_X49)
% 1.06/1.22  ((a738) != zenon_X27)
% 1.06/1.22  ((a721) != (a670))
% 1.06/1.22  (-. (c3_2 (a628) zenon_X54))
% 1.06/1.22  ((a657) != zenon_X48)
% 1.06/1.22  (zenon_X20 != zenon_X25)
% 1.06/1.22  (c3_1 (a729))
% 1.06/1.22  ((a738) != zenon_X44)
% 1.06/1.22  (zenon_X20 != (a670))
% 1.06/1.22  ((a657) != (a714))
% 1.06/1.22  (zenon_X25 != (a625))
% 1.06/1.22  (c7_2 (a708) zenon_X10)
% 1.06/1.22  (c7_2 (a625) (a732))
% 1.06/1.22  (zenon_X19 != (a662))
% 1.06/1.22  (zenon_X25 != (a729))
% 1.06/1.22  (-. (c2_1 (a639)))
% 1.06/1.22  ((a657) != zenon_X55)
% 1.06/1.22  (zenon_X48 != zenon_X51)
% 1.06/1.22  (-. (c4_2 (a729) (a732)))
% 1.06/1.22  (c8_2 (a618) (a623))
% 1.06/1.22  (c7_2 (a618) (a738))
% 1.06/1.22  (-. (c9_2 (a618) (a657)))
% 1.06/1.22  *)
% 1.06/1.22  (* NO-PROOF *)
% 1.06/1.22  % SZS status GaveUp
% 1.06/1.22  Number of rewrites on terms: 0
% 1.06/1.22  Number of rewrites on props: 0
% 1.06/1.22  nodes searched: 36475
% 1.06/1.22  max branch formulas: 3480
% 1.06/1.22  proof nodes created: 466
% 1.06/1.22  formulas created: 36728
% 1.06/1.22  
%------------------------------------------------------------------------------