ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n016.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:03:37 EDT 2024

% Result   : Unknown 18.37s 18.55s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NLP222-1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.33  % Computer : n016.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 00:33:09 EDT 2024
% 0.12/0.33  % CPUTime  : 
% 18.37/18.54  Zenon error: exhausted search space without finding a proof
% 18.37/18.54  (* Current branch:
% 18.37/18.54  ((skc19) != zenon_X12024)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10628)
% 18.37/18.54  (-. (forename (skc17) zenon_X10375))
% 18.37/18.54  ((skc18) != zenon_X12027)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10396)
% 18.37/18.54  ((skc35) != zenon_X10373)
% 18.37/18.54  ((skc19) != zenon_X11612)
% 18.37/18.54  ((skc24) != zenon_X12255)
% 18.37/18.54  ((skc25) != (skf11 zenon_X23))
% 18.37/18.54  ((skc21) != zenon_X10838)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11691)
% 18.37/18.54  ((skc21) != zenon_X10517)
% 18.37/18.54  (-. (man (skc17) zenon_X11691))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10601)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10879)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X12628)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11612)
% 18.37/18.54  ((skc25) != zenon_X11607)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X12629))
% 18.37/18.54  ((skc19) != zenon_X11598)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10537))
% 18.37/18.54  ((skc19) != zenon_X10652)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12088))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11733)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12470))
% 18.37/18.54  ((skc36) != zenon_X13244)
% 18.37/18.54  ((skc20) != zenon_X10853)
% 18.37/18.54  ((skc19) != zenon_X10651)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10393)
% 18.37/18.54  ((skc24) != zenon_X10855)
% 18.37/18.54  ((skc36) != zenon_X11011)
% 18.37/18.54  ((skc25) != zenon_X10348)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X12542)
% 18.37/18.54  ((skf5 zenon_X9) != (skc23))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13526)
% 18.37/18.54  (-. (man (skc22) (skc36)))
% 18.37/18.54  (-. (event (skc33) (skf5 zenon_X11053)))
% 18.37/18.54  (-. (man (skc17) zenon_X10860))
% 18.37/18.54  (-. (forename (skc17) zenon_X10857))
% 18.37/18.54  ((skc32) != zenon_X12607)
% 18.37/18.54  ((skc25) != zenon_X10549)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10644)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X12573)
% 18.37/18.54  (-. (smoke (skc22) (skf5 zenon_X12930)))
% 18.37/18.54  ((skc20) != zenon_X10359)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13041)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13222))
% 18.37/18.54  ((skc20) != zenon_X10368)
% 18.37/18.54  ((skc31) != zenon_X13043)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10558)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11011)
% 18.37/18.54  (-. (event (skc29) zenon_X10953))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11200)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12573)
% 18.37/18.54  ((skc32) != zenon_X10643)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10950)
% 18.37/18.54  ((skc36) != zenon_X10355)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X11404))
% 18.37/18.54  ((skc32) != zenon_X10880)
% 18.37/18.54  ((skc20) != zenon_X10511)
% 18.37/18.54  (-. (man (skc17) zenon_X11202))
% 18.37/18.54  ((skc31) != zenon_X12518)
% 18.37/18.54  ((skc21) != zenon_X12453)
% 18.37/18.54  ((skc20) != zenon_X11729)
% 18.37/18.54  ((skc35) != zenon_X10681)
% 18.37/18.54  ((skc36) != zenon_X10646)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11249)
% 18.37/18.54  ((skf5 zenon_X11) != (skf5 zenon_X11131))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X12026)
% 18.37/18.54  ((skc30) != zenon_X10661)
% 18.37/18.54  ((skc32) != zenon_X10511)
% 18.37/18.54  ((skc31) != zenon_X13577)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10599)
% 18.37/18.54  ((skc20) != zenon_X10375)
% 18.37/18.54  ((skc35) != zenon_X10391)
% 18.37/18.54  ((skc21) != zenon_X10551)
% 18.37/18.54  (-. (man (skc17) zenon_X10401))
% 18.37/18.54  ((skc19) != zenon_X11759)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13245)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10483)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11588))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10551)
% 18.37/18.54  ((skc20) != zenon_X11652)
% 18.37/18.54  ((skc20) != zenon_X10850)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13420)
% 18.37/18.54  ((skc20) != zenon_X11806)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X12542)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10517)
% 18.37/18.54  ((skc35) != (skc20))
% 18.37/18.54  (-. (forename (skc29) zenon_X13040))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10515)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11176))
% 18.37/18.54  (-. (man (skc29) zenon_X13400))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11412)
% 18.37/18.54  ((skc31) != zenon_X13229)
% 18.37/18.54  ((skc31) != zenon_X10648)
% 18.37/18.54  ((skf5 zenon_X11053) != zenon_X10877)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10774)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13385)
% 18.37/18.54  (-. (event (skc33) (skf5 zenon_X9)))
% 18.37/18.54  ((skc20) != zenon_X10492)
% 18.37/18.54  (-. (accessible_world (skc29) (skc29)))
% 18.37/18.54  (-. (state (skc17) zenon_X12027))
% 18.37/18.54  ((skc21) != zenon_X11612)
% 18.37/18.54  ((skc20) != zenon_X10676)
% 18.37/18.54  ((skc36) != zenon_X10551)
% 18.37/18.54  (forename (skc17) (skc20))
% 18.37/18.54  ((skc21) != zenon_X8)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11657)
% 18.37/18.54  ((skf9 zenon_X1) != (skc23))
% 18.37/18.54  ((skc21) != zenon_X10729)
% 18.37/18.54  ((skc36) != zenon_X10648)
% 18.37/18.54  ((skc32) != zenon_X10377)
% 18.37/18.54  ((skc36) != zenon_X11412)
% 18.37/18.54  ((skc32) != zenon_X13386)
% 18.37/18.54  ((skc32) != zenon_X11391)
% 18.37/18.54  ((skc18) != zenon_X10728)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10856)
% 18.37/18.54  ((skc21) != zenon_X11199)
% 18.37/18.54  (-. (state (skc29) zenon_X13009))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10995)
% 18.37/18.54  ((skc19) != zenon_X10404)
% 18.37/18.54  ((skc20) != zenon_X11567)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11655)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13245)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10648)
% 18.37/18.54  ((skc21) != zenon_X10856)
% 18.37/18.54  ((skc32) != zenon_X10925)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10597)
% 18.37/18.54  ((skc36) != zenon_X10628)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10951)
% 18.37/18.54  (-. (forename (skc29) zenon_X13540))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11412)
% 18.37/18.54  ((skc19) != zenon_X10499)
% 18.37/18.54  ((skc24) != zenon_X10389)
% 18.37/18.54  ((skc20) != zenon_X10730)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10608))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13545)
% 18.37/18.54  ((skc20) != zenon_X11930)
% 18.37/18.54  (-. (event (skc33) zenon_X10450))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10551)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10514)
% 18.37/18.54  (event (skc22) (skf5 zenon_X11053))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10950)
% 18.37/18.54  ((skc19) != zenon_X10602)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10542))
% 18.37/18.54  ((skc32) != zenon_X13426)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13229)
% 18.37/18.54  (-. (man (skc29) zenon_X10912))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X12606)
% 18.37/18.54  (-. (man (skc17) zenon_X11633))
% 18.37/18.54  ((skc36) != zenon_X13400)
% 18.37/18.54  (-. (man (skc29) zenon_X10552))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11606)
% 18.37/18.54  ((skc31) != zenon_X10602)
% 18.37/18.54  ((skc31) != zenon_X13435)
% 18.37/18.54  ((skc20) != zenon_X11874)
% 18.37/18.54  ((skc20) != zenon_X12121)
% 18.37/18.54  (zenon_X11073 != (skc17))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12596)
% 18.37/18.54  ((skf5 zenon_X9) != zenon_X10292)
% 18.37/18.54  ((skc36) != zenon_X10683)
% 18.37/18.54  (-. (forename (skc17) zenon_X10598))
% 18.37/18.54  (-. (state (skc17) zenon_X10327))
% 18.37/18.54  (-. (man (skc29) zenon_X10910))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10579)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10895)
% 18.37/18.54  ((skc36) != zenon_X13213)
% 18.37/18.54  (-. (man (skc29) zenon_X13435))
% 18.37/18.54  (-. (man (skc17) zenon_X12050))
% 18.37/18.54  ((skc20) != zenon_X10839)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13400)
% 18.37/18.54  ((skc20) != zenon_X11181)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11237))
% 18.37/18.54  ((skc18) != zenon_X12465)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13400)
% 18.37/18.54  ((skc17) != zenon_X10233)
% 18.37/18.54  ((skf5 zenon_X12930) != (skf5 zenon_X7))
% 18.37/18.54  ((skc31) != zenon_X12596)
% 18.37/18.54  ((skc30) != zenon_X10606)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11733)
% 18.37/18.54  ((skc20) != zenon_X10608)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10951)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10854)
% 18.37/18.54  ((skc24) != zenon_X11597)
% 18.37/18.54  (-. (man (skc29) zenon_X12606))
% 18.37/18.54  ((skc32) != zenon_X10673)
% 18.37/18.54  ((skc32) != zenon_X13575)
% 18.37/18.54  ((skc25) != zenon_X10750)
% 18.37/18.54  ((skc25) != zenon_X11251)
% 18.37/18.54  ((skc19) != zenon_X11691)
% 18.37/18.54  ((skc20) != zenon_X10619)
% 18.37/18.54  (-. (man (skc17) zenon_X10628))
% 18.37/18.54  ((skf5 zenon_X11799) != zenon_X10234)
% 18.37/18.54  ((skc25) != zenon_X12453)
% 18.37/18.54  ((skc24) != zenon_X11198)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10995)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X12597)
% 18.37/18.54  (-. (man (skc29) zenon_X10420))
% 18.37/18.54  ((skc25) != zenon_X12413)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11581))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13542)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13400)
% 18.37/18.54  ((skc32) != zenon_X10381)
% 18.37/18.54  ((skc29) != zenon_X10225)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13402)
% 18.37/18.54  ((skc20) != zenon_X10505)
% 18.37/18.54  (-. (man (skc17) zenon_X10776))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13404)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10652)
% 18.37/18.54  ((skc20) != zenon_X11160)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12161))
% 18.37/18.54  (-. (man (skc29) zenon_X10950))
% 18.37/18.54  ((skc32) != zenon_X13567)
% 18.37/18.54  ((skc32) != zenon_X10684)
% 18.37/18.54  (-. (of (skc29) (skc35) (skc31)))
% 18.37/18.54  (-. (man (skc17) zenon_X11194))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11759)
% 18.37/18.54  ((skc31) != zenon_X13244)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13429))
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10362))
% 18.37/18.54  (-. (forename (skc29) zenon_X10511))
% 18.37/18.54  ((skc36) != zenon_X12596)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10492))
% 18.37/18.54  ((skc34) != zenon_X12540)
% 18.37/18.54  ((skc34) != zenon_X10655)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10991)
% 18.37/18.54  (zenon_X11 != zenon_X11131)
% 18.37/18.54  ((skc36) != zenon_X10579)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10629))
% 18.37/18.54  (-. (event (skc17) zenon_X10727))
% 18.37/18.54  ((skc30) != zenon_X12605)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10936))
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12029))
% 18.37/18.54  ((skc21) != zenon_X11602)
% 18.37/18.54  ((skc18) != zenon_X10778)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10776)
% 18.37/18.54  (agent (skc29) (skc34) (skc36))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11600)
% 18.37/18.54  ((skc36) != zenon_X13576)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10558)
% 18.37/18.54  ((skc30) != zenon_X13403)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12441))
% 18.37/18.54  ((skc30) != zenon_X12513)
% 18.37/18.54  ((skc32) != zenon_X10972)
% 18.37/18.54  ((skc20) != zenon_X11594)
% 18.37/18.54  ((skc36) != zenon_X12573)
% 18.37/18.54  ((skc20) != zenon_X11176)
% 18.37/18.54  ((skc35) != zenon_X10645)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11598)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11598)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11154)
% 18.37/18.54  ((skc24) != zenon_X11652)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10420)
% 18.37/18.54  ((skc36) != zenon_X13545)
% 18.37/18.54  ((skc20) != zenon_X12493)
% 18.37/18.54  ((skc20) != zenon_X10570)
% 18.37/18.54  ((skc36) != zenon_X10995)
% 18.37/18.54  (theme (skc29) (skc34) (skc33))
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11567))
% 18.37/18.54  ((skc35) != (skc32))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13541)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10895)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13229)
% 18.37/18.54  ((skf9 zenon_X1) != zenon_X12387)
% 18.37/18.54  ((skc31) != zenon_X10517)
% 18.37/18.54  ((skc25) != zenon_X10772)
% 18.37/18.54  (-. (man (skc29) zenon_X13213))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11600)
% 18.37/18.54  ((skc21) != zenon_X10344)
% 18.37/18.54  ((skc21) != zenon_X10860)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10858)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X12518)
% 18.37/18.54  ((skc30) != zenon_X10336)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13230))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10666)
% 18.37/18.54  ((skf5 zenon_X9) != zenon_X10279)
% 18.37/18.54  ((skc25) != zenon_X10856)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11768))
% 18.37/18.54  (-. (man (skc17) zenon_X10791))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X12083)
% 18.37/18.54  (zenon_X11066 != (skc22))
% 18.37/18.54  ((skc20) != zenon_X12423)
% 18.37/18.54  ((skc25) != zenon_X10597)
% 18.37/18.54  ((skc21) != zenon_X10603)
% 18.37/18.54  ((skc20) != zenon_X10806)
% 18.37/18.54  ((skc21) != zenon_X10854)
% 18.37/18.54  ((skc21) != zenon_X10648)
% 18.37/18.54  ((skc36) != zenon_X13541)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10489))
% 18.37/18.54  (-. (event (skc33) zenon_X12387))
% 18.37/18.54  ((skc20) != zenon_X10735)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10628)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X12596)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13519))
% 18.37/18.54  ((skf5 zenon_X9) != zenon_X10234)
% 18.37/18.54  (-. (man (skc17) zenon_X10729))
% 18.37/18.54  ((skf5 zenon_X11053) != zenon_X10316)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13435)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11219))
% 18.37/18.54  (-. (forename (skc17) zenon_X10647))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X12991)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13249))
% 18.37/18.54  ((skc18) != zenon_X11690)
% 18.37/18.54  (-. (event (skc29) zenon_X10292))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13561)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11730)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11249)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10603)
% 18.37/18.54  (-. (forename (skc17) zenon_X10389))
% 18.37/18.54  ((skc24) != zenon_X10391)
% 18.37/18.54  ((skc32) != zenon_X12548)
% 18.37/18.54  (-. (man (skc17) zenon_X10838))
% 18.37/18.54  (-. (forename (skc17) zenon_X10402))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10421)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13526)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13420)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10483)
% 18.37/18.54  (event (skc22) (skf5 zenon_X12945))
% 18.37/18.54  (-. (accessible_world (skc29) (skc17)))
% 18.37/18.54  ((skc18) != zenon_X10336)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10854)
% 18.37/18.54  ((skc31) != zenon_X10394)
% 18.37/18.54  ((skc31) != zenon_X10355)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11251)
% 18.37/18.54  (-. (man (skc29) zenon_X12645))
% 18.37/18.54  ((skf9 zenon_X1) != zenon_X10265)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10595)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13043)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11659)
% 18.37/18.54  ((skc24) != (skc32))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10514)
% 18.37/18.54  (-. (state (skc29) zenon_X10994))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11202)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10628)
% 18.37/18.54  (-. (smoke (skc22) (skf5 zenon_X12945)))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13279)
% 18.37/18.54  ((skc31) != zenon_X13561)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13257))
% 18.37/18.54  ((skc32) != zenon_X13249)
% 18.37/18.54  (-. (smoke (skc17) (skc23)))
% 18.37/18.54  ((skc21) != zenon_X11659)
% 18.37/18.54  ((skc19) != zenon_X10421)
% 18.37/18.54  ((skc32) != zenon_X13235)
% 18.37/18.54  ((skc31) != (skf7 zenon_X15))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10774)
% 18.37/18.54  ((skc25) != zenon_X11559)
% 18.37/18.54  (-. (man (skc17) zenon_X11653))
% 18.37/18.54  ((skc23) != zenon_X12457)
% 18.37/18.54  (-. (event zenon_X10225 zenon_X10226))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10380)
% 18.37/18.54  (-. (man (skc29) zenon_X13010))
% 18.37/18.54  ((skc32) != zenon_X10548)
% 18.37/18.54  ((skc21) != zenon_X10597)
% 18.37/18.54  ((skf9 zenon_X1) != (skf5 zenon_X7))
% 18.37/18.54  ((skc36) != zenon_X10879)
% 18.37/18.54  ((skf9 zenon_X1) != zenon_X10279)
% 18.37/18.54  ((skc31) != zenon_X10935)
% 18.37/18.54  (-. (man (skc17) zenon_X10393))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10404)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12160)
% 18.37/18.54  ((skc34) != zenon_X10265)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11600)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13527))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10420)
% 18.37/18.54  ((skc25) != zenon_X10394)
% 18.37/18.54  (of (skc17) (skc20) (skc21))
% 18.37/18.54  ((skc35) != zenon_X10594)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10401)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10421)
% 18.37/18.54  ((skc20) != zenon_X11163)
% 18.37/18.54  ((skc20) != zenon_X11871)
% 18.37/18.54  ((skc20) != zenon_X12166)
% 18.37/18.54  ((skc36) != zenon_X13248)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13420)
% 18.37/18.54  ((skc19) != zenon_X10579)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13264)
% 18.37/18.54  ((skc19) != zenon_X11247)
% 18.37/18.54  (-. (event zenon_X10225 (skc34)))
% 18.37/18.54  (-. (man (skc17) zenon_X11730))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10536)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13026)
% 18.37/18.54  ((skc20) != zenon_X11243)
% 18.37/18.54  ((skc25) != zenon_X11175)
% 18.37/18.54  (-. (forename (skc17) zenon_X10771))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11777)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13008)
% 18.37/18.54  ((skc30) != zenon_X13212)
% 18.37/18.54  (-. (state (skc29) zenon_X12541))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11598)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13542)
% 18.37/18.54  ((skc20) != zenon_X12097)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11957))
% 18.37/18.54  ((skc20) != zenon_X10386)
% 18.37/18.54  ((skc20) != zenon_X10756)
% 18.37/18.54  ((skc20) != zenon_X11768)
% 18.37/18.54  ((skc25) != zenon_X11865)
% 18.37/18.54  (-. (man (skc29) zenon_X13436))
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10972))
% 18.37/18.54  ((skf9 zenon_X3) != (skf5 zenon_X7))
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10508))
% 18.37/18.54  (-. (event (skc29) zenon_X10316))
% 18.37/18.54  ((skf5 zenon_X11053) != (skf5 zenon_X7))
% 18.37/18.54  ((skc21) != zenon_X10808)
% 18.37/18.54  ((skc32) != zenon_X13035)
% 18.37/18.54  ((skc23) != (skc34))
% 18.37/18.54  ((skc24) != zenon_X10681)
% 18.37/18.54  (-. (man (skc29) zenon_X10332))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10992)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13213)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13369)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10332)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11251)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10607)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13577)
% 18.37/18.54  ((skc21) != zenon_X10397)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10646)
% 18.37/18.54  ((skc20) != zenon_X12145)
% 18.37/18.54  (zenon_X11073 != zenon_X15)
% 18.37/18.54  ((skc20) != zenon_X11822)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12139)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11925))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11945)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11240))
% 18.37/18.54  (-. (event (skc29) zenon_X10299))
% 18.37/18.54  (-. (man (skc29) zenon_X13542))
% 18.37/18.54  (-. (man (skc17) zenon_X11655))
% 18.37/18.54  (-. (man (skc29) zenon_X10951))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X12628)
% 18.37/18.54  (state (skc29) (skc30))
% 18.37/18.54  ((skc21) != zenon_X10776)
% 18.37/18.54  (-. (man (skc17) zenon_X11661))
% 18.37/18.54  (-. (man (skc17) zenon_X10750))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10652)
% 18.37/18.54  ((skc21) != zenon_X11598)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13369)
% 18.37/18.54  ((skf9 zenon_X1) != zenon_X10450)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13567))
% 18.37/18.54  (-. (man (skc29) zenon_X13244))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X12604)
% 18.37/18.54  ((skc36) != zenon_X10652)
% 18.37/18.54  ((skf5 zenon_X12944) != zenon_X10422)
% 18.37/18.54  ((skc23) != zenon_X10422)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11886)
% 18.37/18.54  ((skc20) != zenon_X12140)
% 18.37/18.54  ((skc32) != zenon_X13265)
% 18.37/18.54  ((skc19) != zenon_X11251)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11559)
% 18.37/18.54  ((skf5 zenon_X7) != zenon_X10234)
% 18.37/18.54  ((skc25) != zenon_X10783)
% 18.37/18.54  ((skc36) != zenon_X10520)
% 18.37/18.54  ((skc21) != zenon_X11175)
% 18.37/18.54  ((skc32) != zenon_X10619)
% 18.37/18.54  ((skc32) != zenon_X10391)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11653)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12991)
% 18.37/18.54  ((skc36) != zenon_X12606)
% 18.37/18.54  ((skc20) != zenon_X10640)
% 18.37/18.54  ((skf9 zenon_X3) != (skf9 zenon_X1))
% 18.37/18.54  ((skc20) != zenon_X12441)
% 18.37/18.54  ((skc36) != zenon_X10394)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10759))
% 18.37/18.54  ((skc30) != zenon_X10482)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13577)
% 18.37/18.54  ((skc19) != zenon_X10595)
% 18.37/18.54  ((skc36) != zenon_X13245)
% 18.37/18.54  ((skc36) != zenon_X13561)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11200)
% 18.37/18.54  ((skc32) != zenon_X10521)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11247)
% 18.37/18.54  ((skc24) != zenon_X11601)
% 18.37/18.54  ((skc20) != zenon_X10564)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13402)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12051))
% 18.37/18.54  ((skc18) != zenon_X11558)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10599)
% 18.37/18.54  ((skc25) != zenon_X12087)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10520)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10735))
% 18.37/18.54  ((skc21) != zenon_X12083)
% 18.37/18.54  (-. (event (skc17) zenon_X11800))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10729)
% 18.37/18.54  ((skc20) != zenon_X10670)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10860)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11659)
% 18.37/18.54  ((skc32) != zenon_X12976)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10799))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13435)
% 18.37/18.54  ((skc36) != zenon_X12645)
% 18.37/18.54  (-. (event (skc29) (skc23)))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13510)
% 18.37/18.54  ((skc18) != zenon_X12431)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13265))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13248)
% 18.37/18.54  ((skc25) != zenon_X10401)
% 18.37/18.54  ((skc25) != zenon_X10420)
% 18.37/18.54  ((skf5 zenon_X12923) != zenon_X10422)
% 18.37/18.54  ((skc20) != zenon_X10559)
% 18.37/18.54  ((skc32) != zenon_X13375)
% 18.37/18.54  ((skc36) != zenon_X8)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12087)
% 18.37/18.54  ((skc20) != zenon_X10513)
% 18.37/18.54  ((skc18) != zenon_X11834)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11759)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10551)
% 18.37/18.54  ((skc32) != zenon_X11004)
% 18.37/18.54  ((skc24) != zenon_X10853)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10348)
% 18.37/18.54  ((skc25) != zenon_X11659)
% 18.37/18.54  (-. (man (skc17) zenon_X10607))
% 18.37/18.54  ((skc19) != zenon_X11210)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X13016))
% 18.37/18.54  ((skc25) != zenon_X11832)
% 18.37/18.54  ((skc23) != zenon_X10765)
% 18.37/18.54  (-. (state (skc29) zenon_X10954))
% 18.37/18.54  ((skc19) != (skf7 zenon_X11073))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11030)
% 18.37/18.54  ((skc20) != zenon_X12255)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13229)
% 18.37/18.54  ((skc31) != zenon_X12532)
% 18.37/18.54  ((skc36) != zenon_X13010)
% 18.37/18.54  ((skc32) != zenon_X12582)
% 18.37/18.54  (proposition (skc17) (skc22))
% 18.37/18.54  ((skc19) != zenon_X10512)
% 18.37/18.54  ((skf9 zenon_X1) != zenon_X10316)
% 18.37/18.54  ((skc35) != zenon_X10550)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12172))
% 18.37/18.54  ((skc18) != zenon_X11209)
% 18.37/18.54  ((skc31) != (skc36))
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12100))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13404)
% 18.37/18.54  ((skc20) != zenon_X12110)
% 18.37/18.54  ((skc18) != zenon_X10482)
% 18.37/18.54  ((skc32) != zenon_X10564)
% 18.37/18.54  ((skc20) != zenon_X11936)
% 18.37/18.54  (-. (state (skc29) zenon_X12513))
% 18.37/18.54  ((skc32) != zenon_X10920)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10977))
% 18.37/18.54  ((skc30) != zenon_X13247)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10788))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13281)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10919)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X12548))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13576)
% 18.37/18.54  ((skc20) != zenon_X11887)
% 18.37/18.54  (-. (man (skc29) zenon_X13006))
% 18.37/18.54  ((skc36) != zenon_X10514)
% 18.37/18.54  (man (skc17) (skc19))
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10683)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10644)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10552)
% 18.37/18.54  ((skc19) != (skf7 zenon_X15))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11030)
% 18.37/18.54  ((skc19) != zenon_X10549)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10858)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10554)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11936))
% 18.37/18.54  ((skc31) != zenon_X13402)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10729)
% 18.37/18.54  ((skc25) != zenon_X10603)
% 18.37/18.54  ((skc20) != zenon_X11819)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10729)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11253)
% 18.37/18.54  ((skc20) != zenon_X12062)
% 18.37/18.54  ((skc21) != zenon_X10421)
% 18.37/18.54  ((skf5 zenon_X11053) != zenon_X10299)
% 18.37/18.54  ((skc20) != zenon_X10594)
% 18.37/18.54  ((skc31) != zenon_X10971)
% 18.37/18.54  ((skc20) != zenon_X10585)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10808)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10521))
% 18.37/18.54  (-. (man (skc29) zenon_X10879))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X11202)
% 18.37/18.54  (-. (event (skc17) zenon_X10655))
% 18.37/18.54  ((skc25) != zenon_X10558)
% 18.37/18.54  (event (skc22) (skf5 zenon_X11378))
% 18.37/18.54  ((skc35) != zenon_X13005)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10552)
% 18.37/18.54  ((skc32) != zenon_X12629)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10995)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X13010)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X12975)
% 18.37/18.54  (-. (event (skc29) zenon_X12554))
% 18.37/18.54  ((skf5 zenon_X11053) != zenon_X10292)
% 18.37/18.54  (ssSkC0)
% 18.37/18.54  ((skc25) != zenon_X10776)
% 18.37/18.54  ((skc36) != zenon_X10910)
% 18.37/18.54  (-. (man (skc17) zenon_X12139))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X8)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10396)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X12083)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11777)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X13541)
% 18.37/18.54  (-. (man (skc29) zenon_X13041))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10483)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10579)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10955)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X12597)
% 18.37/18.54  ((skc31) != zenon_X12573)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10559))
% 18.37/18.54  ((skc24) != zenon_X10548)
% 18.37/18.54  ((skc20) != zenon_X10548)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11253)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10579)
% 18.37/18.54  ((skc34) != zenon_X10450)
% 18.37/18.54  ((skc21) != zenon_X10644)
% 18.37/18.54  (present (skc22) (skf5 zenon_X12945))
% 18.37/18.54  (-. (event (skc33) (skc34)))
% 18.37/18.54  ((skc31) != zenon_X10404)
% 18.37/18.54  ((skc30) != zenon_X10918)
% 18.37/18.54  ((skc32) != zenon_X12522)
% 18.37/18.54  ((skc35) != zenon_X10381)
% 18.37/18.54  ((skc23) != zenon_X10655)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10536)
% 18.37/18.54  (event (skc22) (skf5 zenon_X11131))
% 18.37/18.54  (-. (state (skc17) zenon_X12086))
% 18.37/18.54  ((skc36) != zenon_X10396)
% 18.37/18.54  ((skc32) != zenon_X13413)
% 18.37/18.54  ((skc19) != zenon_X10552)
% 18.37/18.54  ((skc36) != zenon_X13436)
% 18.37/18.54  (-. (man (skc17) zenon_X11251))
% 18.37/18.54  (accessible_world (skc17) (skc22))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13026)
% 18.37/18.54  ((skc21) != zenon_X11210)
% 18.37/18.54  (zenon_X11066 != zenon_X15)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13041)
% 18.37/18.54  ((skc18) != zenon_X10786)
% 18.37/18.54  (-. (man (skc29) zenon_X12569))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11811)
% 18.37/18.54  ((skc23) != zenon_X10234)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10951)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10348)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10505))
% 18.37/18.54  ((skc24) != zenon_X10373)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11780)
% 18.37/18.54  ((skc32) != zenon_X10542)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12115))
% 18.37/18.54  ((skc21) != zenon_X10601)
% 18.37/18.54  ((skc30) != zenon_X10311)
% 18.37/18.54  ((skc19) != zenon_X11249)
% 18.37/18.54  (-. (man (skc17) zenon_X10601))
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10515)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11580)
% 18.37/18.54  ((skc31) != zenon_X10395)
% 18.37/18.54  (-. (forename (skc17) zenon_X10645))
% 18.37/18.54  ((skc24) != zenon_X11806)
% 18.37/18.54  ((skc32) != zenon_X10681)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11646))
% 18.37/18.54  ((skc25) != zenon_X11606)
% 18.37/18.54  (-. (state (skc29) zenon_X10336))
% 18.37/18.54  ((skc21) != zenon_X10774)
% 18.37/18.54  ((skc32) != zenon_X13570)
% 18.37/18.54  ((skc30) != zenon_X10327)
% 18.37/18.54  ((skc25) != zenon_X10601)
% 18.37/18.54  ((skc25) != zenon_X11580)
% 18.37/18.54  ((skc32) != zenon_X12525)
% 18.37/18.54  ((skc31) != zenon_X13213)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10558)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10396)
% 18.37/18.54  ((skc21) != zenon_X12087)
% 18.37/18.54  ((skf5 zenon_X11053) != zenon_X10450)
% 18.37/18.54  (-. (forename (skc17) zenon_X10681))
% 18.37/18.54  ((skc19) != zenon_X10607)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11951))
% 18.37/18.54  ((skc19) != zenon_X10860)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X12035))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10910)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X12518)
% 18.37/18.54  ((skc19) != zenon_X11653)
% 18.37/18.54  ((skc31) != zenon_X10552)
% 18.37/18.54  (-. (man (skc29) zenon_X10536))
% 18.37/18.54  (-. (forename (skc29) zenon_X13243))
% 18.37/18.54  (zenon_X11066 != (skc17))
% 18.37/18.54  ((skc20) != zenon_X12056)
% 18.37/18.54  (-. (man (skc17) zenon_X10579))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10648)
% 18.37/18.54  ((skc25) != zenon_X10859)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10791)
% 18.37/18.54  ((skc25) != zenon_X11202)
% 18.37/18.54  ((skc21) != zenon_X11655)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13435)
% 18.37/18.54  ((skc20) != zenon_X11248)
% 18.37/18.54  ((skc25) != zenon_X10344)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X12634))
% 18.37/18.54  (-. (man (skc17) zenon_X11886))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10854)
% 18.37/18.54  ((skf9 zenon_X1) != zenon_X10765)
% 18.37/18.54  ((skc21) != zenon_X11733)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X11229)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10383))
% 18.37/18.54  ((skf5 zenon_X9) != zenon_X10450)
% 18.37/18.54  ((skf11 zenon_X23) != zenon_X10395)
% 18.37/18.54  ((skc20) != zenon_X11750)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X12579))
% 18.37/18.54  ((skc32) != zenon_X13532)
% 18.37/18.54  ((skc32) != zenon_X10616)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10545))
% 18.37/18.54  ((skc31) != zenon_X12991)
% 18.37/18.54  ((skc20) != zenon_X10673)
% 18.37/18.54  ((skc25) != zenon_X11653)
% 18.37/18.54  ((skc21) != zenon_X11154)
% 18.37/18.54  (-. (man (skc22) zenon_X8))
% 18.37/18.54  ((skc24) != (skc20))
% 18.37/18.54  (-. (man (skc17) zenon_X11712))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X13008)
% 18.37/18.54  ((skc20) != zenon_X12029)
% 18.37/18.54  ((skc23) != zenon_X10316)
% 18.37/18.54  ((skc19) != zenon_X10394)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10607)
% 18.37/18.54  ((skc32) != zenon_X13421)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11594))
% 18.37/18.54  ((skc32) != zenon_X10588)
% 18.37/18.54  ((skc32) != zenon_X10492)
% 18.37/18.54  ((skc32) != zenon_X13019)
% 18.37/18.54  ((skf5 zenon_X11131) != zenon_X10316)
% 18.37/18.54  ((skc35) != zenon_X12595)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X11713))
% 18.37/18.54  ((skc36) != zenon_X10395)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11633)
% 18.37/18.54  ((skc30) != zenon_X12541)
% 18.37/18.54  (-. (jules_forename (skc17) zenon_X10588))
% 18.37/18.54  ((skc31) != zenon_X13436)
% 18.37/18.54  ((skc23) != zenon_X10226)
% 18.37/18.54  ((skf9 zenon_X5) != (skc23))
% 18.37/18.54  ((skc21) != zenon_X12024)
% 18.37/18.54  ((skc18) != zenon_X12408)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10783)
% 18.37/18.54  ((skc19) != zenon_X10517)
% 18.37/18.54  ((skf7 zenon_X11066) != (skf7 zenon_X15))
% 18.37/18.54  ((skc20) != zenon_X11184)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X10991)
% 18.37/18.54  (-. (event zenon_X10233 (skc34)))
% 18.37/18.54  (-. (man (skc17) zenon_X10558))
% 18.37/18.54  (event (skc22) (skf5 zenon_X12931))
% 18.37/18.54  ((skc25) != zenon_X10628)
% 18.37/18.54  (-. (man (skc17) zenon_X11738))
% 18.37/18.54  (-. (smoke (skc22) (skf5 zenon_X12923)))
% 18.37/18.54  ((skc19) != zenon_X11600)
% 18.37/18.54  ((skc25) != zenon_X11662)
% 18.37/18.54  (-. (man (skc17) zenon_X11229))
% 18.37/18.54  ((skc32) != zenon_X13011)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X11412)
% 18.37/18.54  ((skc21) != zenon_X10683)
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13545)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X11865)
% 18.37/18.54  ((skc20) != zenon_X10542)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X10964))
% 18.37/18.54  ((skc31) != zenon_X10393)
% 18.37/18.54  (agent (skc17) (skc23) (skc25))
% 18.37/18.54  ((skc21) != zenon_X11600)
% 18.37/18.54  ((skc21) != zenon_X11661)
% 18.37/18.54  ((skc17) != zenon_X14)
% 18.37/18.54  ((skc34) != zenon_X10305)
% 18.37/18.54  ((skc33) != (skc17))
% 18.37/18.54  ((skc20) != zenon_X10391)
% 18.37/18.54  (-. (man (skc29) zenon_X13043))
% 18.37/18.54  (zenon_X11 != zenon_X12923)
% 18.37/18.54  (-. (jules_forename (skc29) zenon_X11407))
% 18.37/18.54  ((skf7 zenon_X11066) != zenon_X13561)
% 18.37/18.54  ((skc31) != zenon_X10646)
% 18.37/18.54  ((skc36) != zenon_X12628)
% 18.37/18.54  ((skc33) != zenon_X10225)
% 18.37/18.54  ((skc25) != zenon_X11945)
% 18.37/18.54  (-. (man (skc17) zenon_X10602))
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10955)
% 18.37/18.54  ((skc20) != zenon_X12216)
% 18.37/18.54  ((skf7 zenon_X11073) != zenon_X10858)
% 18.37/18.54  ((skc20) != zenon_X10389)
% 18.37/18.54  ((skc20) != zenon_X11570)
% 18.37/18.54  (zenon_X12931 != zenon_X7)
% 18.37/18.54  ((skf7 zenon_X15) != zenon_X10380)
% 18.37/18.55  ((skf5 zenon_X7) != (skc23))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10421)
% 18.37/18.55  ((skc19) != zenon_X10683)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10808)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12518)
% 18.37/18.55  ((skc32) != zenon_X11024)
% 18.37/18.55  ((skc32) != zenon_X10896)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11832)
% 18.37/18.55  ((skc21) != zenon_X12413)
% 18.37/18.55  (-. (forename (skc17) zenon_X11248))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12454))
% 18.37/18.55  ((skc20) != zenon_X10489)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12140))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12139)
% 18.37/18.55  ((skc35) != zenon_X13040)
% 18.37/18.55  ((skc19) != zenon_X11865)
% 18.37/18.55  ((skc20) != zenon_X10810)
% 18.37/18.55  ((skc32) != zenon_X10365)
% 18.37/18.55  ((skc20) != zenon_X10637)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11634))
% 18.37/18.55  ((skc31) != zenon_X11412)
% 18.37/18.55  ((skc24) != zenon_X10647)
% 18.37/18.55  (-. (smoke (skc22) (skf5 zenon_X12944)))
% 18.37/18.55  ((skc36) != zenon_X10895)
% 18.37/18.55  (-. (state (skc29) zenon_X13212))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13561)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10750)
% 18.37/18.55  ((skc25) != zenon_X11738)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10854)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12551))
% 18.37/18.55  ((skc32) != zenon_X10418)
% 18.37/18.55  ((skc35) != zenon_X10513)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X11021))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11253)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13577)
% 18.37/18.55  ((skc20) != zenon_X12161)
% 18.37/18.55  ((skc32) != zenon_X10901)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11247)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13526)
% 18.37/18.55  (-. (forename (skc29) zenon_X10368))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13279)
% 18.37/18.55  ((skc19) != zenon_X10348)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10597)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13270))
% 18.37/18.55  ((skc35) != zenon_X10511)
% 18.37/18.55  ((skc19) != zenon_X12219)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13577)
% 18.37/18.55  ((skc25) != zenon_X11759)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11253)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10944))
% 18.37/18.55  ((skc32) != zenon_X13230)
% 18.37/18.55  ((skc32) != zenon_X10961)
% 18.37/18.55  ((skc19) != zenon_X10514)
% 18.37/18.55  (-. (man (skc17) zenon_X11780))
% 18.37/18.55  (-. (event zenon_X10225 (skc23)))
% 18.37/18.55  ((skc25) != zenon_X10808)
% 18.37/18.55  ((skf5 zenon_X11) != (skf5 zenon_X12945))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10599)
% 18.37/18.55  (zenon_X11073 != (skc22))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10332)
% 18.37/18.55  (-. (man (skc17) zenon_X12026))
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10299)
% 18.37/18.55  (-. (man (skc29) zenon_X12643))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10512)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13410))
% 18.37/18.55  (-. (man (skc22) (skc21)))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11163))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10554)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11662)
% 18.37/18.55  (-. (man (skc17) zenon_X12024))
% 18.37/18.55  ((skc31) != zenon_X11396)
% 18.37/18.55  ((skc25) != (skf7 zenon_X11073))
% 18.37/18.55  ((skc32) != zenon_X13394)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10956))
% 18.37/18.55  ((skc32) != zenon_X10613)
% 18.37/18.55  ((skc32) != zenon_X10362)
% 18.37/18.55  ((skc25) != zenon_X11780)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10750)
% 18.37/18.55  (event (skc22) (skf5 zenon_X12923))
% 18.37/18.55  ((skc21) != zenon_X10595)
% 18.37/18.55  (theme (skc17) (skc23) (skc22))
% 18.37/18.55  ((skc23) != zenon_X10272)
% 18.37/18.55  (-. (event (skc17) zenon_X11152))
% 18.37/18.55  ((skc21) != zenon_X10750)
% 18.37/18.55  ((skc19) != zenon_X11200)
% 18.37/18.55  (-. (man (skc17) zenon_X11608))
% 18.37/18.55  (-. (forename (skc17) zenon_X11250))
% 18.37/18.55  (-. (forename (skc17) zenon_X10775))
% 18.37/18.55  ((skc19) != zenon_X10838)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10776)
% 18.37/18.55  (event (skc22) (skf5 zenon_X9))
% 18.37/18.55  ((skc25) != zenon_X10652)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13436)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10595)
% 18.37/18.55  ((skc19) != zenon_X10344)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X8)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12444))
% 18.37/18.55  (-. (event (skc17) (skc34)))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10628)
% 18.37/18.55  ((skc35) != zenon_X13434)
% 18.37/18.55  ((skc20) != zenon_X11626)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12041))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11612)
% 18.37/18.55  ((skc21) != zenon_X10380)
% 18.37/18.55  (-. (state (skc17) zenon_X10322))
% 18.37/18.55  (present (skc22) (skf5 zenon_X11131))
% 18.37/18.55  ((skc20) != zenon_X12252)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11181))
% 18.37/18.55  (-. (forename (skc17) zenon_X12216))
% 18.37/18.55  ((skc32) != zenon_X13257)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12596)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10888))
% 18.37/18.55  ((skc19) != zenon_X10859)
% 18.37/18.55  (-. (man (skc29) zenon_X13008))
% 18.37/18.55  ((skc25) != zenon_X11777)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10595)
% 18.37/18.55  ((skc36) != zenon_X12604)
% 18.37/18.55  ((skc36) != zenon_X10517)
% 18.37/18.55  (present (skc22) (skf5 zenon_X12930))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13219))
% 18.37/18.55  ((skc20) != zenon_X11573)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11396)
% 18.37/18.55  ((skc30) != zenon_X10994)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11657)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13273))
% 18.37/18.55  ((skc20) != zenon_X11643)
% 18.37/18.55  ((skc31) != zenon_X10652)
% 18.37/18.55  ((skc31) != zenon_X10512)
% 18.37/18.55  ((skc22) != (skc29))
% 18.37/18.55  ((skc35) != zenon_X10684)
% 18.37/18.55  ((skc25) != zenon_X10650)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13281)
% 18.37/18.55  ((skc19) != zenon_X10355)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12219)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10791)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11730)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10880))
% 18.37/18.55  ((skc36) != zenon_X10536)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10515)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11166))
% 18.37/18.55  (-. (of (skc17) (skc24) (skc19)))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10599)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10895)
% 18.37/18.55  (-. (man (skc29) zenon_X10995))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11655)
% 18.37/18.55  (-. (event zenon_X10233 (skc23)))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10847))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12087)
% 18.37/18.55  ((skc31) != zenon_X10397)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11898))
% 18.37/18.55  ((skc25) != zenon_X10396)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10644)
% 18.37/18.55  ((skc36) != zenon_X12569)
% 18.37/18.55  ((skc36) != zenon_X12643)
% 18.37/18.55  ((skc21) != (skf7 zenon_X11073))
% 18.37/18.55  (-. (man (skc17) zenon_X10648))
% 18.37/18.55  ((skc25) != zenon_X11886)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12643)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11653)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11412)
% 18.37/18.55  (-. (man (skc17) zenon_X11865))
% 18.37/18.55  (-. (man (skc29) zenon_X10971))
% 18.37/18.55  (agent (skc22) (skf5 zenon_X13) zenon_X13)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13405))
% 18.37/18.55  ((skc32) != zenon_X12570)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10359))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12542)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11945)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11600)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12433))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10860)
% 18.37/18.55  ((skc25) != zenon_X12217)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11886)
% 18.37/18.55  ((skf5 zenon_X11) != (skf5 zenon_X12923))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12038))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13244)
% 18.37/18.55  ((skc20) != zenon_X11765)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11655)
% 18.37/18.55  ((skc20) != zenon_X10684)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13213)
% 18.37/18.55  ((skc32) != zenon_X13238)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10941))
% 18.37/18.55  ((skc20) != zenon_X11747)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10640))
% 18.37/18.55  ((skc32) != zenon_X10977)
% 18.37/18.55  ((skc19) != zenon_X11229)
% 18.37/18.55  ((skc24) != zenon_X10803)
% 18.37/18.55  (-. (forename (skc29) zenon_X10381))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10996))
% 18.37/18.55  (-. (man (skc29) zenon_X10499))
% 18.37/18.55  ((skc31) != zenon_X13264)
% 18.37/18.55  ((skc25) != zenon_X10421)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10597)
% 18.37/18.55  (-. (man (skc17) zenon_X11580))
% 18.37/18.55  ((skc25) != zenon_X10380)
% 18.37/18.55  ((skc21) != zenon_X10396)
% 18.37/18.55  ((skc23) != zenon_X12402)
% 18.37/18.55  (-. (man (skc22) (skc19)))
% 18.37/18.55  (-. (man (skc29) zenon_X10554))
% 18.37/18.55  ((skc23) != zenon_X10279)
% 18.37/18.55  ((skc25) != zenon_X11608)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11930))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13394))
% 18.37/18.55  ((skc21) != zenon_X10552)
% 18.37/18.55  ((skc35) != zenon_X10990)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12569)
% 18.37/18.55  (man (skc17) (skc21))
% 18.37/18.55  ((skf5 zenon_X12945) != (skf5 zenon_X7))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13213)
% 18.37/18.55  (zenon_X15 != (skc22))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12518)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13238))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10499)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13244)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10499)
% 18.37/18.55  ((skc19) != zenon_X10603)
% 18.37/18.55  ((skc25) != zenon_X11249)
% 18.37/18.55  (-. (smoke (skc22) (skf5 zenon_X12931)))
% 18.37/18.55  ((skf9 zenon_X5) != (skc34))
% 18.37/18.55  (think_believe_consider (skc29) (skc34))
% 18.37/18.55  ((skc20) != zenon_X10762)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10910)
% 18.37/18.55  (zenon_X3 != zenon_X1)
% 18.37/18.55  ((skc21) != zenon_X12219)
% 18.37/18.55  (-. (man (skc17) zenon_X12217))
% 18.37/18.55  ((skc32) != zenon_X10637)
% 18.37/18.55  (-. (accessible_world (skc17) (skc17)))
% 18.37/18.55  ((skc36) != zenon_X10515)
% 18.37/18.55  ((skc36) != zenon_X10950)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13404)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10607)
% 18.37/18.55  (present (skc22) (skf5 zenon_X12923))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13510)
% 18.37/18.55  ((skc21) != zenon_X11657)
% 18.37/18.55  ((skc32) != zenon_X10909)
% 18.37/18.55  ((skc31) != zenon_X10536)
% 18.37/18.55  ((skc32) != zenon_X10370)
% 18.37/18.55  ((skc25) != zenon_X12109)
% 18.37/18.55  (-. (man (skc29) zenon_X13577))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10750)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10810))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X11004))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11216))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13041)
% 18.37/18.55  ((skc24) != zenon_X10596)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10859)
% 18.37/18.55  (zenon_X15 != (skc17))
% 18.37/18.55  ((skc36) != zenon_X13577)
% 18.37/18.55  ((skc25) != zenon_X12024)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10950)
% 18.37/18.55  ((skc36) != zenon_X12532)
% 18.37/18.55  (-. (vincent_forename (skc29) (skc32)))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11011)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11032)
% 18.37/18.55  (-. (state (skc17) zenon_X11209))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11874))
% 18.37/18.55  ((skc21) != zenon_X10395)
% 18.37/18.55  ((skc25) != zenon_X10520)
% 18.37/18.55  ((skc32) != zenon_X13405)
% 18.37/18.55  (-. (man (skc17) zenon_X10858))
% 18.37/18.55  ((skc32) != zenon_X10375)
% 18.37/18.55  ((skc20) != zenon_X10738)
% 18.37/18.55  ((skc19) != zenon_X12256)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12487))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11924)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10644)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13400)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10776)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11602)
% 18.37/18.55  ((skf5 zenon_X7) != (skc34))
% 18.37/18.55  ((skc17) != zenon_X31)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10650)
% 18.37/18.55  ((skc21) != zenon_X11606)
% 18.37/18.55  (-. (man (skc17) zenon_X10599))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10859)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11886)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10991)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11924)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12604)
% 18.37/18.55  ((skc21) != zenon_X11194)
% 18.37/18.55  (-. (man (skc29) zenon_X12975))
% 18.37/18.55  ((skc19) != zenon_X10856)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10738))
% 18.37/18.55  ((skc36) != zenon_X11396)
% 18.37/18.55  ((skc32) != zenon_X10580)
% 18.37/18.55  ((skc19) != zenon_X10380)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10393)
% 18.37/18.55  (-. (state (skc29) zenon_X13509))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12062))
% 18.37/18.55  ((skc32) != zenon_X13222)
% 18.37/18.55  (-. (state (skc17) zenon_X10606))
% 18.37/18.55  ((skc32) != zenon_X10585)
% 18.37/18.55  (-. (state (skc17) zenon_X11153))
% 18.37/18.55  ((skc35) != zenon_X11029)
% 18.37/18.55  ((skc35) != zenon_X10402)
% 18.37/18.55  ((skc21) != zenon_X10599)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13008)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10955)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12525))
% 18.37/18.55  ((skc35) != zenon_X10596)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10520)
% 18.37/18.55  ((skc32) != zenon_X10629)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10401)
% 18.37/18.55  ((skc20) != zenon_X12148)
% 18.37/18.55  ((skc20) != zenon_X11246)
% 18.37/18.55  (-. (forename (skc29) zenon_X12530))
% 18.37/18.55  ((skc20) != zenon_X11951)
% 18.37/18.55  (-. (forename (skc29) zenon_X12593))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11608)
% 18.37/18.55  (-. (of (skc17) (skc24) (skc21)))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11877))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10597)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10783)
% 18.37/18.55  ((skc36) != zenon_X13006)
% 18.37/18.55  ((skc31) != zenon_X10607)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10520)
% 18.37/18.55  (of (skc29) (skc32) (skc31))
% 18.37/18.55  ((skc32) != zenon_X10591)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11251)
% 18.37/18.55  ((skc36) != zenon_X12518)
% 18.37/18.55  ((skc25) != zenon_X10683)
% 18.37/18.55  ((skc20) != zenon_X10508)
% 18.37/18.55  ((skc31) != zenon_X12975)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11886)
% 18.37/18.55  (-. (man (skc17) zenon_X11811))
% 18.37/18.55  ((skc34) != zenon_X10422)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13551))
% 18.37/18.55  ((skc25) != zenon_X12256)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10727)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12628)
% 18.37/18.55  ((skc31) != zenon_X13526)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13245)
% 18.37/18.55  ((skc35) != zenon_X13540)
% 18.37/18.55  (-. (man (skc29) zenon_X13420))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10344)
% 18.37/18.55  ((skc19) != zenon_X10666)
% 18.37/18.55  ((skf5 zenon_X11131) != (skf5 zenon_X7))
% 18.37/18.55  ((skc25) != zenon_X11598)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11819))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12585))
% 18.37/18.55  ((skc20) != zenon_X10484)
% 18.37/18.55  ((skc36) != zenon_X10919)
% 18.37/18.55  ((skc20) != zenon_X11588)
% 18.37/18.55  ((skc20) != zenon_X10545)
% 18.37/18.55  ((skc25) != (skc19))
% 18.37/18.55  ((skc34) != zenon_X12554)
% 18.37/18.55  (-. (man (skc29) zenon_X13369))
% 18.37/18.55  ((skc25) != zenon_X12028)
% 18.37/18.55  (zenon_X12944 != zenon_X7)
% 18.37/18.55  ((skc31) != zenon_X13541)
% 18.37/18.55  ((skc21) != zenon_X11759)
% 18.37/18.55  ((skc21) != zenon_X11691)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12991)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11865)
% 18.37/18.55  ((skc30) != zenon_X10878)
% 18.37/18.55  ((skc25) != zenon_X11730)
% 18.37/18.55  ((skc21) != zenon_X11865)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10856)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10)
% 18.37/18.55  ((skc31) != zenon_X10554)
% 18.37/18.55  ((skc24) != zenon_X11250)
% 18.37/18.55  ((skc34) != zenon_X10299)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13436)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13561)
% 18.37/18.55  (present (skc17) (skc23))
% 18.37/18.55  (-. (man (skc29) zenon_X12573))
% 18.37/18.55  ((skc19) != zenon_X11253)
% 18.37/18.55  ((skc21) != zenon_X11229)
% 18.37/18.55  (-. (state (skc29) zenon_X11414))
% 18.37/18.55  ((skc20) != zenon_X10365)
% 18.37/18.55  ((skc24) != zenon_X10773)
% 18.37/18.55  ((skc35) != zenon_X10909)
% 18.37/18.55  ((skc32) != zenon_X13527)
% 18.37/18.55  ((skc31) != zenon_X13420)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10860)
% 18.37/18.55  ((skc31) != zenon_X12597)
% 18.37/18.55  (-. (man (skc22) zenon_X10))
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10953)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11892))
% 18.37/18.55  ((skc20) != zenon_X11211)
% 18.37/18.55  ((skc32) != zenon_X13027)
% 18.37/18.55  ((skc19) != zenon_X10401)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10676))
% 18.37/18.55  ((skc20) != zenon_X11649)
% 18.37/18.55  ((skc18) != zenon_X12194)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10787)
% 18.37/18.55  ((skc25) != zenon_X10599)
% 18.37/18.55  ((skc25) != (skf7 zenon_X15))
% 18.37/18.55  (-. (forename (skc17) zenon_X11656))
% 18.37/18.55  (-. (man (skc17) zenon_X11606))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11697))
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10877)
% 18.37/18.55  ((skc20) != zenon_X12038)
% 18.37/18.55  ((skc32) != zenon_X10594)
% 18.37/18.55  (-. (event (skc17) zenon_X10765))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11620))
% 18.37/18.55  ((skc20) != zenon_X10418)
% 18.37/18.55  ((skc20) != zenon_X11760)
% 18.37/18.55  (-. (forename (skc17) zenon_X10855))
% 18.37/18.55  ((skc32) != zenon_X10996)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10858)
% 18.37/18.55  ((skc20) != zenon_X10613)
% 18.37/18.55  (-. (event (skc33) (skf5 zenon_X11378)))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13248)
% 18.37/18.55  ((skc19) != zenon_X11832)
% 18.37/18.55  ((skc31) != zenon_X10651)
% 18.37/18.55  (-. (man (skc17) zenon_X11602))
% 18.37/18.55  ((skc19) != zenon_X10646)
% 18.37/18.55  ((skc31) != zenon_X10895)
% 18.37/18.55  ((skc20) != zenon_X11771)
% 18.37/18.55  ((skc20) != zenon_X11613)
% 18.37/18.55  ((skc25) != zenon_X11247)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11243))
% 18.37/18.55  ((skc31) != zenon_X10551)
% 18.37/18.55  (-. (man (skc17) zenon_X12432))
% 18.37/18.55  ((skc36) != zenon_X13420)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10646)
% 18.37/18.55  ((skc32) != zenon_X10545)
% 18.37/18.55  (-. (man (skc29) zenon_X10955))
% 18.37/18.55  ((skc31) != zenon_X13369)
% 18.37/18.55  ((skc32) != zenon_X12992)
% 18.37/18.55  ((skc17) != zenon_X10225)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10286)
% 18.37/18.55  ((skc19) != (skf11 zenon_X23))
% 18.37/18.55  ((skc25) != zenon_X11194)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10517)
% 18.37/18.55  ((skc20) != zenon_X12115)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12645)
% 18.37/18.55  ((skc32) != zenon_X10608)
% 18.37/18.55  ((skc21) != zenon_X10791)
% 18.37/18.55  (-. (smoke (skc22) (skf5 zenon_X11053)))
% 18.37/18.55  (-. (accessible_world (skc29) zenon_X10233))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11229)
% 18.37/18.55  (-. (forename (skc17) zenon_X12082))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10591))
% 18.37/18.55  ((skc21) != zenon_X11253)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12219)
% 18.37/18.55  (-. (man (skc22) (skf7 zenon_X11066)))
% 18.37/18.55  ((skc35) != zenon_X10368)
% 18.37/18.55  (-. (man (skc17) zenon_X10652))
% 18.37/18.55  ((skc25) != zenon_X10499)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10912)
% 18.37/18.55  (-. (man (skc29) zenon_X12542))
% 18.37/18.55  (-. (event (skc29) zenon_X12507))
% 18.37/18.55  ((skc32) != zenon_X13562)
% 18.37/18.55  (-. (man (skc29) zenon_X13510))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11780)
% 18.37/18.55  ((skc32) != zenon_X13243)
% 18.37/18.55  ((skc23) != zenon_X10299)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12493))
% 18.37/18.55  (-. (state (skc29) zenon_X11415))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13041)
% 18.37/18.55  ((skc19) != zenon_X10520)
% 18.37/18.55  (-. (state (skc17) zenon_X10728))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11608)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10355)
% 18.37/18.55  ((skc34) != zenon_X10556)
% 18.37/18.55  ((skc20) != zenon_X12082)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10838)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12532)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10762))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13526)
% 18.37/18.55  (-. (accessible_world (skc29) (skc22)))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13006)
% 18.37/18.55  (-. (state (skc17) zenon_X10778))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13542)
% 18.37/18.55  (-. (man (skc17) zenon_X11832))
% 18.37/18.55  (-. (event (skc17) zenon_X11922))
% 18.37/18.55  ((skc19) != zenon_X10554)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11661)
% 18.37/18.55  ((skc36) != zenon_X10558)
% 18.37/18.55  (zenon_X12945 != zenon_X7)
% 18.37/18.55  ((skf5 zenon_X11378) != zenon_X10450)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10838)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10651)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10772)
% 18.37/18.55  ((skc32) != zenon_X10928)
% 18.37/18.55  (-. (forename (skc17) zenon_X10806))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11633)
% 18.37/18.55  (-. (man (skc17) zenon_X12087))
% 18.37/18.55  ((skc20) != zenon_X11219)
% 18.37/18.55  (-. (man (skc17) zenon_X12109))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13404)
% 18.37/18.55  (-. (man (skc29) zenon_X10380))
% 18.37/18.55  (-. (event (skc29) zenon_X10877))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10355)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12607))
% 18.37/18.55  ((skc32) != zenon_X11404)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13420)
% 18.37/18.55  ((skc36) != zenon_X11030)
% 18.37/18.55  ((skc20) != zenon_X11739)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11811)
% 18.37/18.55  ((skc18) != zenon_X11611)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11580)
% 18.37/18.55  (-. (be (skc17) (skc18) (skc21) (skc21)))
% 18.37/18.55  ((skc19) != zenon_X10551)
% 18.37/18.55  ((skc31) != zenon_X10595)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10355)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11777)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10305)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10404)
% 18.37/18.55  (-. (man (skc17) (skf7 zenon_X15)))
% 18.37/18.55  ((skc24) != zenon_X10771)
% 18.37/18.55  ((skc25) != zenon_X10515)
% 18.37/18.55  ((skc21) != zenon_X11886)
% 18.37/18.55  ((skc31) != zenon_X10955)
% 18.37/18.55  ((skc19) != zenon_X11154)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11194)
% 18.37/18.55  ((skc32) != zenon_X12615)
% 18.37/18.55  ((skc25) != zenon_X10791)
% 18.37/18.55  ((skc20) != zenon_X11591)
% 18.37/18.55  ((skc25) != zenon_X11210)
% 18.37/18.55  ((skc24) != zenon_X10645)
% 18.37/18.55  ((skc20) != zenon_X12051)
% 18.37/18.55  ((skc19) != zenon_X10791)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10401)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13554))
% 18.37/18.55  ((skc21) != zenon_X12139)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11030)
% 18.37/18.55  ((skc36) != zenon_X10992)
% 18.37/18.55  ((skc32) != zenon_X12981)
% 18.37/18.55  ((skc21) != zenon_X11200)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11811)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10404)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11657)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11712)
% 18.37/18.55  (zenon_X23 != (skc22))
% 18.37/18.55  ((skc20) != zenon_X11646)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11738)
% 18.37/18.55  ((skc25) != zenon_X12257)
% 18.37/18.55  ((skc18) != zenon_X10557)
% 18.37/18.55  ((skc21) != zenon_X11202)
% 18.37/18.55  (-. (man (skc29) zenon_X10992))
% 18.37/18.55  ((skc19) != zenon_X11712)
% 18.37/18.55  ((skc25) != zenon_X10729)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11210)
% 18.37/18.55  ((skc20) != zenon_X10634)
% 18.37/18.55  ((skc32) != zenon_X10941)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10393)
% 18.37/18.55  ((skc32) != zenon_X10505)
% 18.37/18.55  (-. (man (skc29) zenon_X13541))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10529))
% 18.37/18.55  (-. (man (skc29) zenon_X11030))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13214))
% 18.37/18.55  (-. (man (skc17) zenon_X10646))
% 18.37/18.55  ((skc20) != zenon_X12035)
% 18.37/18.55  (-. (forename (skc29) zenon_X13434))
% 18.37/18.55  (-. (man (skc29) zenon_X10355))
% 18.37/18.55  ((skc32) != zenon_X10634)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11229)
% 18.37/18.55  ((skc20) != zenon_X12433)
% 18.37/18.55  ((skc32) != zenon_X10964)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11607)
% 18.37/18.55  (-. (man (skc17) zenon_X10348))
% 18.37/18.55  ((skc20) != zenon_X11898)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12606)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11718))
% 18.37/18.55  (-. (of (skc17) (skc20) (skc19)))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11662)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10397)
% 18.37/18.55  (-. (man (skc17) zenon_X11199))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11612)
% 18.37/18.55  ((skc25) != zenon_X11600)
% 18.37/18.55  ((skc20) != zenon_X11187)
% 18.37/18.55  ((skc20) != zenon_X10857)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12569)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10398))
% 18.37/18.55  ((skc21) != zenon_X10858)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11712)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11871))
% 18.37/18.55  ((skc19) != zenon_X10808)
% 18.37/18.55  ((skc20) != zenon_X10596)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10420)
% 18.37/18.55  ((skc32) != zenon_X12579)
% 18.37/18.55  ((skc35) != zenon_X10647)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10377))
% 18.37/18.55  ((skc19) != zenon_X11607)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12569)
% 18.37/18.55  ((skf5 zenon_X9) != (skf9 zenon_X1))
% 18.37/18.55  ((skc18) != zenon_X10606)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12213))
% 18.37/18.55  ((skc31) != zenon_X10401)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10316)
% 18.37/18.55  ((skc20) != zenon_X10629)
% 18.37/18.55  (-. (man (skc17) zenon_X11657))
% 18.37/18.55  ((skc31) != zenon_X11030)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12256)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10286)
% 18.37/18.55  ((skc24) != zenon_X11599)
% 18.37/18.55  (zenon_X12923 != zenon_X7)
% 18.37/18.55  ((skc36) != zenon_X13369)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10919)
% 18.37/18.55  ((skc34) != zenon_X10226)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11607)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10393)
% 18.37/18.55  ((skc31) != zenon_X10601)
% 18.37/18.55  ((skc21) != zenon_X10607)
% 18.37/18.55  (-. (event (skc29) zenon_X11385))
% 18.37/18.55  (-. (man (skc17) zenon_X12083))
% 18.37/18.55  ((skf5 zenon_X11799) != zenon_X10422)
% 18.37/18.55  ((skc19) != zenon_X10783)
% 18.37/18.55  (-. (state (skc17) zenon_X11834))
% 18.37/18.55  (-. (forename (skc29) zenon_X10550))
% 18.37/18.55  ((skc36) != zenon_X10380)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11777)
% 18.37/18.55  ((skc25) != zenon_X10595)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10601)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11780)
% 18.37/18.55  (-. (forename (skc17) zenon_X11597))
% 18.37/18.55  (-. (man (skc17) zenon_X12479))
% 18.37/18.55  ((skc36) != zenon_X13385)
% 18.37/18.55  ((skc20) != zenon_X11724)
% 18.37/18.55  ((skc32) != zenon_X12530)
% 18.37/18.55  ((skc32) != zenon_X11029)
% 18.37/18.55  (-. (man (skc29) zenon_X13229))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12151))
% 18.37/18.55  ((skc32) != zenon_X13399)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11580)
% 18.37/18.55  ((skc25) != zenon_X10483)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12252))
% 18.37/18.55  (-. (state (skc17) zenon_X12194))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10651)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11691)
% 18.37/18.55  (-. (man (skc17) zenon_X10603))
% 18.37/18.55  ((skc32) != zenon_X12642)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10765)
% 18.37/18.55  (-. (forename (skc29) zenon_X12595))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10950)
% 18.37/18.55  ((skc32) != zenon_X10489)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10856)
% 18.37/18.55  ((skc25) != zenon_X10332)
% 18.37/18.55  ((skc25) != zenon_X10536)
% 18.37/18.55  ((skc25) != zenon_X11712)
% 18.37/18.55  ((skc20) != zenon_X11697)
% 18.37/18.55  ((skc20) != zenon_X12417)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11760))
% 18.37/18.55  ((skc25) != zenon_X10854)
% 18.37/18.55  (event (skc22) (skf5 zenon_X12944))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12615))
% 18.37/18.55  ((skc19) != zenon_X10787)
% 18.37/18.55  ((skc19) != zenon_X10420)
% 18.37/18.55  (-. (man (skc17) zenon_X10404))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10912)
% 18.37/18.55  ((skc20) != zenon_X10377)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10935)
% 18.37/18.55  ((skc18) != zenon_X11737)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11211))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10348)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10650)
% 18.37/18.55  ((skc21) != zenon_X11777)
% 18.37/18.55  ((skc32) != zenon_X13000)
% 18.37/18.55  (-. (man (skc17) zenon_X10774))
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10655)
% 18.37/18.55  ((skc21) != zenon_X11580)
% 18.37/18.55  ((skf9 zenon_X1) != (skc34))
% 18.37/18.55  ((skc31) != zenon_X10950)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11602)
% 18.37/18.55  ((skc20) != zenon_X10759)
% 18.37/18.55  (-. (event (skc17) zenon_X10556))
% 18.37/18.55  ((skc20) != zenon_X11721)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12024)
% 18.37/18.55  ((skc25) != zenon_X10554)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10652)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10272)
% 18.37/18.55  (state (skc17) (skc18))
% 18.37/18.55  ((skc21) != zenon_X10859)
% 18.37/18.55  ((skc21) != zenon_X11662)
% 18.37/18.55  ((skc36) != zenon_X13026)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10481)
% 18.37/18.55  ((skf5 zenon_X11378) != zenon_X10422)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13421))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13006)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10226)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11832)
% 18.37/18.55  ((skc30) != zenon_X13368)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10971)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10549)
% 18.37/18.55  (-. (man (skc29) zenon_X12597))
% 18.37/18.55  ((skc18) != zenon_X10311)
% 18.37/18.55  (-. (man (skc17) zenon_X10683))
% 18.37/18.55  ((skc20) != zenon_X11713)
% 18.37/18.55  (-. (of (skc29) (skc32) (skc36)))
% 18.37/18.55  ((skc36) != zenon_X10332)
% 18.37/18.55  ((skc19) != zenon_X11199)
% 18.37/18.55  ((skc32) != zenon_X10904)
% 18.37/18.55  (-. (forename (skc29) zenon_X12642))
% 18.37/18.55  ((skc19) != zenon_X10729)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10602)
% 18.37/18.55  (man zenon_X23 (skf11 zenon_X23))
% 18.37/18.55  ((skc25) != zenon_X11199)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13026)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11396)
% 18.37/18.55  ((skc32) != zenon_X13378)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13385)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13043)
% 18.37/18.55  ((skc36) != zenon_X12597)
% 18.37/18.55  ((skc24) != zenon_X10598)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X8)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10395)
% 18.37/18.55  ((skc24) != zenon_X10550)
% 18.37/18.55  ((skc21) != (skf7 zenon_X15))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10791)
% 18.37/18.55  ((skc25) != zenon_X12050)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13369)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12597)
% 18.37/18.55  ((skc31) != zenon_X13006)
% 18.37/18.55  (be (skc17) (skc18) (skc21) (skc19))
% 18.37/18.55  (-. (man (skc17) zenon_X12453))
% 18.37/18.55  ((skc31) != zenon_X12606)
% 18.37/18.55  ((skc31) != zenon_X10421)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12643)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12110))
% 18.37/18.55  ((skc21) != zenon_X12479)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10536)
% 18.37/18.55  ((skc22) != zenon_X10225)
% 18.37/18.55  ((skc20) != zenon_X10647)
% 18.37/18.55  ((skc31) != zenon_X10515)
% 18.37/18.55  ((skf5 zenon_X11053) != zenon_X10953)
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10234)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10935)
% 18.37/18.55  (-. (man (skc17) zenon_X10595))
% 18.37/18.55  ((skc32) != zenon_X10389)
% 18.37/18.55  ((skc19) != zenon_X11945)
% 18.37/18.55  ((skc24) != zenon_X10513)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13532))
% 18.37/18.55  ((skc31) != zenon_X12569)
% 18.37/18.55  ((skc34) != zenon_X11385)
% 18.37/18.55  (-. (man (skc29) zenon_X10991))
% 18.37/18.55  ((skc19) != zenon_X11662)
% 18.37/18.55  (actual_world (skc29))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10651)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12522))
% 18.37/18.55  (-. (event (skc33) (skc23)))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10352))
% 18.37/18.55  (present (skc22) (skf5 zenon_X12931))
% 18.37/18.55  ((skc24) != zenon_X10643)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11655)
% 18.37/18.55  (-. (forename (skc17) zenon_X10596))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10787)
% 18.37/18.55  ((skf5 zenon_X12931) != zenon_X10422)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11194)
% 18.37/18.55  (agent (skc33) (skf9 zenon_X12) zenon_X12)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X8)
% 18.37/18.55  (-. (forename (skc29) zenon_X10909))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10603)
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10450)
% 18.37/18.55  ((skc20) != zenon_X10828)
% 18.37/18.55  ((skc32) != zenon_X10570)
% 18.37/18.55  ((skc19) != zenon_X11659)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11865)
% 18.37/18.55  (-. (man (skc17) zenon_X10859))
% 18.37/18.55  (-. (of (skc17) (skc20) (skc25)))
% 18.37/18.55  ((skc20) != zenon_X11744)
% 18.37/18.55  ((skc32) != zenon_X13219)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13279)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10951)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11602)
% 18.37/18.55  ((skc24) != zenon_X10418)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12145))
% 18.37/18.55  ((skc32) != zenon_X10936)
% 18.37/18.55  ((skc20) != zenon_X10383)
% 18.37/18.55  ((skc31) != zenon_X13026)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10877)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11199)
% 18.37/18.55  ((skc36) != zenon_X10404)
% 18.37/18.55  ((skc32) != zenon_X10944)
% 18.37/18.55  ((skc24) != zenon_X11193)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10397)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12975)
% 18.37/18.55  (-. (man (skc17) zenon_X10856))
% 18.37/18.55  (-. (man (skc17) zenon_X11598))
% 18.37/18.55  (-. (state (skc29) zenon_X13403))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13026)
% 18.37/18.55  (-. (forename (skc17) zenon_X10773))
% 18.37/18.55  ((skc31) != zenon_X12645)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11733)
% 18.37/18.55  ((skc20) != zenon_X11933)
% 18.37/18.55  (-. (state (skc29) zenon_X10311))
% 18.37/18.55  ((skc25) != zenon_X10607)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12024)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10305)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13244)
% 18.37/18.55  ((skc34) != zenon_X10234)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13426))
% 18.37/18.55  ((skc35) != zenon_X10389)
% 18.37/18.55  ((skc20) != zenon_X10679)
% 18.37/18.55  ((skc20) != zenon_X10341)
% 18.37/18.55  ((skc33) != (skc29))
% 18.37/18.55  (-. (forename (skc17) zenon_X10679))
% 18.37/18.55  ((skc19) != zenon_X11580)
% 18.37/18.55  ((skc21) != zenon_X11780)
% 18.37/18.55  ((skc32) != zenon_X12543)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10776)
% 18.37/18.55  ((skc34) != zenon_X10272)
% 18.37/18.55  ((skc20) != zenon_X10567)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13035))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11626))
% 18.37/18.55  ((skc30) != zenon_X12974)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10838)
% 18.37/18.55  ((skc19) != zenon_X12139)
% 18.37/18.55  (-. (man (skc17) zenon_X11210))
% 18.37/18.55  ((skc24) != zenon_X10679)
% 18.37/18.55  ((skf5 zenon_X11131) != (skf9 zenon_X1))
% 18.37/18.55  (-. (present (skc33) (skf9 zenon_X1)))
% 18.37/18.55  ((skc20) != zenon_X12438)
% 18.37/18.55  ((skc36) != (skf7 zenon_X15))
% 18.37/18.55  ((skc20) != zenon_X10537)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10370))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12612))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11570))
% 18.37/18.55  ((skc35) != zenon_X10949)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11643))
% 18.37/18.55  ((skc21) != zenon_X11608)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10885))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11560))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12604)
% 18.37/18.55  ((skc25) != zenon_X10774)
% 18.37/18.55  ((skf5 zenon_X11) != (skc34))
% 18.37/18.55  ((skc20) != zenon_X12470)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13043)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12604)
% 18.37/18.55  ((skc32) != zenon_X12612)
% 18.37/18.55  ((skf5 zenon_X11053) != zenon_X10422)
% 18.37/18.55  ((skf5 zenon_X11) != (skc23))
% 18.37/18.55  (-. (man (skc22) (skc25)))
% 18.37/18.55  (-. (forename (skc29) zenon_X13005))
% 18.37/18.55  (-. (forename (skc17) zenon_X11246))
% 18.37/18.55  ((skc32) != zenon_X10529)
% 18.37/18.55  (-. (event (skc33) (skf5 zenon_X11131)))
% 18.37/18.55  ((skc34) != zenon_X12973)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10421)
% 18.37/18.55  ((skc19) != zenon_X10332)
% 18.37/18.55  (-. (man (skc17) zenon_X11253))
% 18.37/18.55  ((skc36) != zenon_X13526)
% 18.37/18.55  ((skc35) != zenon_X10548)
% 18.37/18.55  ((skc21) != zenon_X10483)
% 18.37/18.55  ((skc25) != zenon_X10355)
% 18.37/18.55  (-. (forename (skc17) zenon_X11652))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12573)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11653)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10928))
% 18.37/18.55  ((skc32) != zenon_X10402)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10808)
% 18.37/18.55  ((skc32) != zenon_X10359)
% 18.37/18.55  ((skc31) != zenon_X13545)
% 18.37/18.55  ((skc19) != zenon_X10601)
% 18.37/18.55  ((skc25) != zenon_X12139)
% 18.37/18.55  (-. (man (skc17) zenon_X11600))
% 18.37/18.55  (-. (man (skc17) zenon_X10666))
% 18.37/18.55  (-. (forename (skc29) zenon_X10949))
% 18.37/18.55  ((skc32) != zenon_X13370)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10646)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11580)
% 18.37/18.55  ((skc19) != zenon_X12085)
% 18.37/18.55  ((skc21) != zenon_X10650)
% 18.37/18.55  ((skc32) != zenon_X13273)
% 18.37/18.55  (-. (man (skc17) (skf7 zenon_X11066)))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11559)
% 18.37/18.55  ((skc24) != zenon_X10684)
% 18.37/18.55  ((skc18) != zenon_X12086)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10355)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13541)
% 18.37/18.55  ((skc31) != zenon_X10995)
% 18.37/18.55  ((skc20) != zenon_X10521)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11249)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11591))
% 18.37/18.55  ((skc19) != zenon_X10397)
% 18.37/18.55  ((skc20) != zenon_X10352)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10634))
% 18.37/18.55  ((skc32) != zenon_X12997)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13570))
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10299)
% 18.37/18.55  (-. (man (skc17) zenon_X12256))
% 18.37/18.55  (-. (smoke (skc29) (skc34)))
% 18.37/18.55  ((skc20) != zenon_X10822)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11730)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11247)
% 18.37/18.55  (-. (man (skc17) zenon_X12219))
% 18.37/18.55  ((skc21) != zenon_X10558)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10514)
% 18.37/18.55  (-. (man (skc17) zenon_X11662))
% 18.37/18.55  (-. (man (skc29) zenon_X12532))
% 18.37/18.55  (-. (man (skc17) zenon_X10787))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11606)
% 18.37/18.55  (-. (man (skc29) zenon_X10396))
% 18.37/18.55  ((skc20) != zenon_X12473)
% 18.37/18.55  (-. (state (skc29) zenon_X10878))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11691)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10844))
% 18.37/18.55  (-. (event (skc29) zenon_X12973))
% 18.37/18.55  ((skc21) != (skf11 zenon_X23))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13281)
% 18.37/18.55  (present (skc22) (skf5 zenon_X11053))
% 18.37/18.55  ((skc36) != zenon_X13542)
% 18.37/18.55  (-. (forename (skc29) zenon_X10990))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10787)
% 18.37/18.55  ((skc31) != zenon_X10597)
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10481)
% 18.37/18.55  (present (skc22) (skf5 zenon_X11799))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13378))
% 18.37/18.55  (-. (forename (skc17) zenon_X11193))
% 18.37/18.55  ((skc36) != zenon_X10607)
% 18.37/18.55  ((skc23) != zenon_X10305)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11032)
% 18.37/18.55  ((skc32) != zenon_X10990)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11633)
% 18.37/18.55  ((skc36) != zenon_X13281)
% 18.37/18.55  ((skc19) != zenon_X12109)
% 18.37/18.55  ((skc36) != zenon_X10666)
% 18.37/18.55  ((skc35) != zenon_X10643)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11945)
% 18.37/18.55  ((skc19) != zenon_X10393)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11832)
% 18.37/18.55  (-. (event (skc29) zenon_X13508))
% 18.37/18.55  (actual_world (skc17))
% 18.37/18.55  ((skc19) != zenon_X10536)
% 18.37/18.55  ((skc25) != zenon_X11733)
% 18.37/18.55  ((skc32) != zenon_X12595)
% 18.37/18.55  ((skc31) != zenon_X13245)
% 18.37/18.55  ((skc31) != zenon_X13400)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13235))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10774)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11194)
% 18.37/18.55  (-. (event (skc33) (skf5 zenon_X7)))
% 18.37/18.55  ((skc20) != zenon_X12172)
% 18.37/18.55  (-. (vincent_forename (skc17) (skc20)))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10499)
% 18.37/18.55  ((skc31) != zenon_X10558)
% 18.37/18.55  ((skc34) != zenon_X10481)
% 18.37/18.55  ((skc35) != zenon_X12593)
% 18.37/18.55  ((skc33) != (skc22))
% 18.37/18.55  (-. (state (skc17) zenon_X12408))
% 18.37/18.55  (zenon_X11 != zenon_X12931)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12028)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10344)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12532)
% 18.37/18.55  (-. (event (skc22) zenon_X10422))
% 18.37/18.55  ((skc32) != zenon_X12637)
% 18.37/18.55  (proposition (skc29) (skc33))
% 18.37/18.55  ((skc23) != zenon_X10556)
% 18.37/18.55  ((skc23) != zenon_X11557)
% 18.37/18.55  ((skc20) != zenon_X12444)
% 18.37/18.55  ((skc19) != zenon_X11661)
% 18.37/18.55  ((skc25) != zenon_X12219)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11175)
% 18.37/18.55  ((skc20) != zenon_X11623)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10265)
% 18.37/18.55  ((skc20) != zenon_X10788)
% 18.37/18.55  (-. (man (skc17) zenon_X11559))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10365))
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10727)
% 18.37/18.55  ((skc25) != zenon_X12432)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13510)
% 18.37/18.55  ((skc31) != zenon_X10483)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12532)
% 18.37/18.55  ((skc32) != zenon_X10679)
% 18.37/18.55  (-. (man (skc17) zenon_X11945))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10992)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10901))
% 18.37/18.55  (man zenon_X15 (skf7 zenon_X15))
% 18.37/18.55  ((skc32) != zenon_X13551)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13562))
% 18.37/18.55  (-. (state (skc17) zenon_X11690))
% 18.37/18.55  ((skc20) != zenon_X12020)
% 18.37/18.55  ((skc32) != zenon_X10484)
% 18.37/18.55  ((skc20) != zenon_X11216)
% 18.37/18.55  (-. (man (skc17) zenon_X12160))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10601)
% 18.37/18.55  ((skc19) != zenon_X10558)
% 18.37/18.55  ((skc36) != zenon_X11032)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10422)
% 18.37/18.55  ((skc21) != zenon_X10394)
% 18.37/18.55  ((skc31) != zenon_X10599)
% 18.37/18.55  (-. (forename (skc29) zenon_X13278))
% 18.37/18.55  (zenon_X11066 != zenon_X11073)
% 18.37/18.55  (event (skc29) (skc34))
% 18.37/18.55  ((skc32) != zenon_X10956)
% 18.37/18.55  (man zenon_X11073 (skf7 zenon_X11073))
% 18.37/18.55  ((skc32) != zenon_X12593)
% 18.37/18.55  ((skc20) != zenon_X10751)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12975)
% 18.37/18.55  (-. (man (skc29) zenon_X13248))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11780)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10896))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11187))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10648)
% 18.37/18.55  ((skc21) != zenon_X10404)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10772)
% 18.37/18.55  ((skc31) != zenon_X10520)
% 18.37/18.55  (-. (forename (skc29) zenon_X11391))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12596)
% 18.37/18.55  (forename (skc29) (skc32))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10912)
% 18.37/18.55  ((skc32) != zenon_X10352)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10558)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10655)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11691)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11633)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11607)
% 18.37/18.55  ((skc19) != zenon_X11886)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10991)
% 18.37/18.55  ((skc20) != zenon_X12151)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11229)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11661)
% 18.37/18.55  ((skc31) != zenon_X11011)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10601)
% 18.37/18.55  ((skf5 zenon_X12923) != (skf5 zenon_X7))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10613))
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10450)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10859)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10616))
% 18.37/18.55  ((skc36) != zenon_X13402)
% 18.37/18.55  ((skc23) != zenon_X11863)
% 18.37/18.55  ((skc23) != zenon_X10265)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10567))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11738)
% 18.37/18.55  (-. (event (skc29) zenon_X12540))
% 18.37/18.55  ((skc21) != zenon_X11633)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10919)
% 18.37/18.55  ((skc19) != zenon_X11606)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10877)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12573)
% 18.37/18.55  ((skc20) != zenon_X10643)
% 18.37/18.55  (present (skc22) (skf5 zenon_X9))
% 18.37/18.55  ((skc24) != zenon_X11776)
% 18.37/18.55  ((skc24) != zenon_X12023)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10517)
% 18.37/18.55  ((skc32) != zenon_X10386)
% 18.37/18.55  ((skc20) != zenon_X10526)
% 18.37/18.55  ((skc20) != zenon_X11877)
% 18.37/18.55  (-. (man (skc29) zenon_X12628))
% 18.37/18.55  (of (skc29) (skc35) (skc36))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10910)
% 18.37/18.55  ((skf5 zenon_X11799) != (skf5 zenon_X7))
% 18.37/18.55  ((skc36) != zenon_X10549)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10483)
% 18.37/18.55  ((skc21) != zenon_X10772)
% 18.37/18.55  ((skf5 zenon_X12930) != zenon_X10422)
% 18.37/18.55  (-. (state (skc29) zenon_X13544))
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10727)
% 18.37/18.55  (zenon_X11 != zenon_X11053)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13369)
% 18.37/18.55  ((skc32) != zenon_X10980)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12166))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12570))
% 18.37/18.55  ((skc19) != zenon_X11602)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10683)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12109)
% 18.37/18.55  ((skc20) != zenon_X10616)
% 18.37/18.55  (-. (man (skc17) zenon_X11924))
% 18.37/18.55  ((skc25) != zenon_X10860)
% 18.37/18.55  ((skc21) != zenon_X11924)
% 18.37/18.55  (-. (forename (skc17) zenon_X10594))
% 18.37/18.55  ((skc19) != zenon_X10597)
% 18.37/18.55  ((skc36) != zenon_X10650)
% 18.37/18.55  ((skc36) != zenon_X13404)
% 18.37/18.55  ((skc20) != zenon_X11692)
% 18.37/18.55  ((skc20) != zenon_X12041)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12097))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12606)
% 18.37/18.55  ((skc35) != zenon_X13278)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10683)
% 18.37/18.55  ((skc36) != zenon_X10912)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10517)
% 18.37/18.55  (present (skc22) (skf5 zenon_X11378))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10344)
% 18.37/18.55  ((skc20) != zenon_X11166)
% 18.37/18.55  ((skc32) != zenon_X12588)
% 18.37/18.55  (think_believe_consider (skc17) (skc23))
% 18.37/18.55  ((skc20) != zenon_X11776)
% 18.37/18.55  ((skc31) != zenon_X13576)
% 18.37/18.55  ((skc30) != zenon_X13509)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11154)
% 18.37/18.55  (present (skc22) (skf5 zenon_X12944))
% 18.37/18.55  ((skc21) != (skc36))
% 18.37/18.55  ((skc19) != zenon_X12413)
% 18.37/18.55  ((skc20) != zenon_X11700)
% 18.37/18.55  ((skc32) != zenon_X13410)
% 18.37/18.55  ((skc25) != zenon_X10404)
% 18.37/18.55  ((skc21) != zenon_X10549)
% 18.37/18.55  ((skc23) != zenon_X10727)
% 18.37/18.55  ((skc21) != zenon_X10393)
% 18.37/18.55  (-. (state (skc17) zenon_X11558))
% 18.37/18.55  ((skc32) != zenon_X13032)
% 18.37/18.55  ((skc35) != zenon_X10679)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13248)
% 18.37/18.55  ((skc19) != zenon_X11733)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10551)
% 18.37/18.55  ((skc30) != zenon_X12564)
% 18.37/18.55  ((skc35) != zenon_X11391)
% 18.37/18.55  ((skc32) != zenon_X10645)
% 18.37/18.55  ((skc25) != zenon_X11253)
% 18.37/18.55  ((skc25) != zenon_X11661)
% 18.37/18.55  (-. (man (skc17) zenon_X10772))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12532)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10953)
% 18.37/18.55  ((skc32) != zenon_X10341)
% 18.37/18.55  ((skc32) != zenon_X10559)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10953)
% 18.37/18.55  ((skc20) != zenon_X10402)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10380)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12473))
% 18.37/18.55  ((skc36) != zenon_X10348)
% 18.37/18.55  (-. (man (skc17) (skf11 zenon_X23)))
% 18.37/18.55  ((skc34) != zenon_X10292)
% 18.37/18.55  (-. (man (skc29) zenon_X10514))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12984))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11825))
% 18.37/18.55  ((skc36) != zenon_X10599)
% 18.37/18.55  (-. (forename (skc17) zenon_X10643))
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10234)
% 18.37/18.55  ((skc20) != zenon_X10799)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10646)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11811)
% 18.37/18.55  ((skc19) != zenon_X11194)
% 18.37/18.55  ((skc32) != zenon_X13270)
% 18.37/18.55  ((skc31) != zenon_X12643)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10666)
% 18.37/18.55  ((skc19) != zenon_X10628)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10500))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10512)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12026)
% 18.37/18.55  ((skc36) != zenon_X10601)
% 18.37/18.55  ((skc25) != zenon_X12085)
% 18.37/18.55  ((skc21) != zenon_X12160)
% 18.37/18.55  (-. (man (skc17) zenon_X12085))
% 18.37/18.55  ((skc36) != zenon_X10935)
% 18.37/18.55  ((skc31) != zenon_X10514)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12981))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12085)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12643)
% 18.37/18.55  (-. (state (skc29) zenon_X12605))
% 18.37/18.55  ((skc19) != zenon_X11738)
% 18.37/18.55  ((skc29) != zenon_X10233)
% 18.37/18.55  (event (skc22) (skf5 zenon_X11799))
% 18.37/18.55  ((skc23) != zenon_X10286)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10552)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10992)
% 18.37/18.55  ((skc32) != zenon_X10383)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10971)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11733)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10401)
% 18.37/18.55  ((skc25) != zenon_X10551)
% 18.37/18.55  (-. (man (skc17) zenon_X10394))
% 18.37/18.55  (-. (man (skc17) zenon_X12257))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11661)
% 18.37/18.55  (smoke (skc22) (skf5 zenon_X11))
% 18.37/18.55  ((skc36) != zenon_X13041)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11598)
% 18.37/18.55  ((skc31) != zenon_X10344)
% 18.37/18.55  ((skc24) != zenon_X10511)
% 18.37/18.55  (-. (man (skc29) zenon_X13402))
% 18.37/18.55  (-. (actual_world zenon_X31))
% 18.37/18.55  ((skc32) != zenon_X10500)
% 18.37/18.55  (-. (man (skc17) zenon_X11175))
% 18.37/18.55  ((skc21) != zenon_X10646)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10420)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11154)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11738)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11199)
% 18.37/18.55  ((skc24) != zenon_X12082)
% 18.37/18.55  ((skc20) != zenon_X10370)
% 18.37/18.55  ((skc20) != zenon_X11581)
% 18.37/18.55  (zenon_X23 != (skc17))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12597)
% 18.37/18.55  ((skc21) != zenon_X10520)
% 18.37/18.55  ((skc25) != zenon_X10787)
% 18.37/18.55  ((skc21) != zenon_X10499)
% 18.37/18.55  ((skc31) != zenon_X10650)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10850))
% 18.37/18.55  ((skc34) != zenon_X10877)
% 18.37/18.55  (event (skc33) (skf9 zenon_X1))
% 18.37/18.55  ((skc18) != zenon_X10322)
% 18.37/18.55  ((skc32) != zenon_X13554)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10925))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12582))
% 18.37/18.55  ((skf5 zenon_X12931) != (skf5 zenon_X7))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13576)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11700))
% 18.37/18.55  (-. (man (skc29) zenon_X10919))
% 18.37/18.55  ((skc20) != zenon_X11892)
% 18.37/18.55  (-. (state (skc17) zenon_X10786))
% 18.37/18.55  ((skc24) != zenon_X11246)
% 18.37/18.55  ((skc32) != zenon_X11001)
% 18.37/18.55  ((skc36) != zenon_X10401)
% 18.37/18.55  ((skc31) != zenon_X10603)
% 18.37/18.55  ((skc20) != zenon_X10847)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10484))
% 18.37/18.55  ((skc36) != zenon_X10344)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11184))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10514)
% 18.37/18.55  ((skc21) != zenon_X10652)
% 18.37/18.55  ((skf7 zenon_X11066) != (skf7 zenon_X11073))
% 18.37/18.55  ((skc25) != zenon_X10579)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10564))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10595)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11661)
% 18.37/18.55  ((skc36) != zenon_X12975)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12079))
% 18.37/18.55  ((skc23) != zenon_X11800)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13264)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10879)
% 18.37/18.55  ((skc31) != zenon_X13010)
% 18.37/18.55  ((skc25) != zenon_X11154)
% 18.37/18.55  ((skc34) != zenon_X13508)
% 18.37/18.55  ((skc31) != zenon_X11032)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10341))
% 18.37/18.55  ((skc19) != zenon_X10854)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10396)
% 18.37/18.55  (-. (man (skc22) (skf11 zenon_X23)))
% 18.37/18.55  (-. (man (skc29) zenon_X10549))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10912)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10666)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11230))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13436)
% 18.37/18.55  (-. (state (skc29) zenon_X13368))
% 18.37/18.55  ((skc25) != zenon_X10838)
% 18.37/18.55  ((skc21) != zenon_X11247)
% 18.37/18.55  ((skc20) != zenon_X11656)
% 18.37/18.55  ((skc35) != zenon_X13575)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11608)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10549)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11759)
% 18.37/18.55  ((skc21) != (skc19))
% 18.37/18.55  ((skc32) != zenon_X13429)
% 18.37/18.55  ((skc19) != zenon_X12432)
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10422)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10751))
% 18.37/18.55  ((skc21) != zenon_X10332)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11623))
% 18.37/18.55  ((skc20) != zenon_X10795)
% 18.37/18.55  ((skc31) != zenon_X13510)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11200)
% 18.37/18.55  ((skc18) != zenon_X10519)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10556)
% 18.37/18.55  ((skc34) != zenon_X13211)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13281)
% 18.37/18.55  ((skc25) != zenon_X10666)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13542)
% 18.37/18.55  ((skc32) != zenon_X13535)
% 18.37/18.55  ((skc24) != zenon_X10594)
% 18.37/18.55  (-. (man (skc29) zenon_X10895))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10750)
% 18.37/18.55  ((skc20) != zenon_X10741)
% 18.37/18.55  (-. (forename (skc29) zenon_X11029))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10650)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11199)
% 18.37/18.55  ((skf5 zenon_X11) != (skf5 zenon_X11053))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11653)
% 18.37/18.55  ((skc32) != zenon_X13546)
% 18.37/18.55  (-. (man (skc22) (skf7 zenon_X11073)))
% 18.37/18.55  ((skc19) != zenon_X12087)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10920))
% 18.37/18.55  ((skc29) != zenon_X14)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10332)
% 18.37/18.55  (accessible_world (skc29) (skc33))
% 18.37/18.55  ((skf5 zenon_X11378) != (skf5 zenon_X7))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11765))
% 18.37/18.55  ((skc19) != zenon_X11811)
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10292)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10570))
% 18.37/18.55  ((skf5 zenon_X11) != (skf5 zenon_X12944))
% 18.37/18.55  ((skc32) != zenon_X10598)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10512)
% 18.37/18.55  ((skc21) != zenon_X12256)
% 18.37/18.55  ((skc31) != zenon_X13385)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13413))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11747))
% 18.37/18.55  (-. (accessible_world (skc17) (skc29)))
% 18.37/18.55  ((skf5 zenon_X9) != (skc34))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12606)
% 18.37/18.55  (-. (forename (skc17) zenon_X10803))
% 18.37/18.55  ((skc20) != zenon_X11240)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10955)
% 18.37/18.55  (-. (man (skc29) zenon_X13576))
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10556)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10655)
% 18.37/18.55  ((skc21) != zenon_X12217)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10226)
% 18.37/18.55  ((skc24) != zenon_X10806)
% 18.37/18.55  (-. (event (skc17) zenon_X11689))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11608)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13006)
% 18.37/18.55  ((skc32) != zenon_X12634)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10935)
% 18.37/18.55  ((skc19) != zenon_X10395)
% 18.37/18.55  (-. (forename (skc17) zenon_X11806))
% 18.37/18.55  (zenon_X11378 != zenon_X7)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10783)
% 18.37/18.55  (-. (man (skc17) (skf7 zenon_X11073)))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13545)
% 18.37/18.55  ((skc19) != zenon_X10650)
% 18.37/18.55  ((skc20) != zenon_X12213)
% 18.37/18.55  ((skc23) != zenon_X10450)
% 18.37/18.55  (jules_forename (skc17) (skc20))
% 18.37/18.55  (-. (man (skc29) zenon_X10515))
% 18.37/18.55  (-. (man (skc17) zenon_X10650))
% 18.37/18.55  ((skf5 zenon_X11378) != (skf9 zenon_X1))
% 18.37/18.55  ((skc31) != zenon_X10910)
% 18.37/18.55  ((skc21) != zenon_X11730)
% 18.37/18.55  ((skc36) != zenon_X10955)
% 18.37/18.55  ((skc32) != zenon_X10373)
% 18.37/18.55  ((skc31) != zenon_X10644)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10935)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13006)
% 18.37/18.55  (-. (state (skc29) zenon_X10918))
% 18.37/18.55  ((skc20) != zenon_X10681)
% 18.37/18.55  ((skc32) != zenon_X10398)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11657)
% 18.37/18.55  ((skc32) != zenon_X11012)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10299)
% 18.37/18.55  ((skc21) != zenon_X12050)
% 18.37/18.55  ((skc20) != zenon_X11601)
% 18.37/18.55  (-. (state (skc17) zenon_X10557))
% 18.37/18.55  ((skc21) != zenon_X10579)
% 18.37/18.55  ((skc36) != zenon_X10554)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13010)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11612)
% 18.37/18.55  ((skc20) != zenon_X12088)
% 18.37/18.55  ((skc32) != zenon_X10508)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10895)
% 18.37/18.55  ((skc19) != zenon_X11175)
% 18.37/18.55  (-. (state (skc17) zenon_X10661))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11606)
% 18.37/18.55  ((skc20) != zenon_X11866)
% 18.37/18.55  (-. (event (skc17) zenon_X11863))
% 18.37/18.55  ((skc31) != zenon_X10992)
% 18.37/18.55  ((skc36) != zenon_X10421)
% 18.37/18.55  (-. (man (skc17) zenon_X10651))
% 18.37/18.55  (event (skc22) (skf5 zenon_X7))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11924)
% 18.37/18.55  (zenon_X11 != zenon_X12930)
% 18.37/18.55  ((skc21) != zenon_X10401)
% 18.37/18.55  ((skc19) != zenon_X10599)
% 18.37/18.55  ((skc19) != zenon_X10858)
% 18.37/18.55  (-. (man (skc17) zenon_X11247))
% 18.37/18.55  (-. (state (skc17) zenon_X11737))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10756))
% 18.37/18.55  (-. (man (skc29) zenon_X13281))
% 18.37/18.55  ((skc32) != zenon_X10550)
% 18.37/18.55  ((skc20) != zenon_X11620)
% 18.37/18.55  ((skc32) != zenon_X10676)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10286)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10386))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10520)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X12645)
% 18.37/18.55  ((skc32) != zenon_X10513)
% 18.37/18.55  (-. (event (skc17) zenon_X12457))
% 18.37/18.55  ((skc36) != zenon_X10552)
% 18.37/18.55  ((skc35) != zenon_X10375)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10585))
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10316)
% 18.37/18.55  ((skc23) != zenon_X10481)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10670))
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10292)
% 18.37/18.55  (-. (state (skc29) zenon_X13247))
% 18.37/18.55  ((skc21) != zenon_X11559)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11703))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11933))
% 18.37/18.55  ((skc30) != zenon_X10519)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11866))
% 18.37/18.55  ((skc20) != zenon_X11193)
% 18.37/18.55  ((skc20) != zenon_X11925)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11724))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11249)
% 18.37/18.55  ((skc24) != zenon_X11729)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X11001))
% 18.37/18.55  ((skc30) != zenon_X10557)
% 18.37/18.55  ((skc25) != zenon_X10517)
% 18.37/18.55  ((skc24) != zenon_X11654)
% 18.37/18.55  ((skc19) != zenon_X12217)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13213)
% 18.37/18.55  ((skc25) != zenon_X10646)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11210)
% 18.37/18.55  ((skc20) != zenon_X11703)
% 18.37/18.55  ((skc19) != zenon_X10772)
% 18.37/18.55  ((skc20) != zenon_X11946)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13391))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11750))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10619))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11175)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11659)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11559)
% 18.37/18.55  ((skc25) != zenon_X10512)
% 18.37/18.55  ((skc20) != zenon_X11222)
% 18.37/18.55  ((skc21) != zenon_X10554)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10397)
% 18.37/18.55  ((skc20) != zenon_X10825)
% 18.37/18.55  ((skc21) != zenon_X12432)
% 18.37/18.55  ((skc32) != zenon_X13519)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13402)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10549)
% 18.37/18.55  ((skc19) != zenon_X8)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12637))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12217)
% 18.37/18.55  (-. (forename (skc17) zenon_X11654))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10795))
% 18.37/18.55  ((skc21) != zenon_X12109)
% 18.37/18.55  ((skc21) != zenon_X10628)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10879)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10971)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13010)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X11024))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13229)
% 18.37/18.55  ((skc19) != zenon_X10776)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13032))
% 18.37/18.55  ((skf5 zenon_X12945) != zenon_X10422)
% 18.37/18.55  ((skc36) != zenon_X13510)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13576)
% 18.37/18.55  (-. (man (skc29) zenon_X10483))
% 18.37/18.55  (-. (man (skc17) zenon_X11777))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11011)
% 18.37/18.55  (-. (event (skc17) zenon_X10286))
% 18.37/18.55  (-. (forename (skc17) zenon_X11776))
% 18.37/18.55  ((skc20) != zenon_X12023)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10556)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13535))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10992)
% 18.37/18.55  (-. (man (skc29) zenon_X10512))
% 18.37/18.55  (man (skc29) (skc36))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13370))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11011)
% 18.37/18.55  (-. (man (skc29) zenon_X13526))
% 18.37/18.55  ((skc21) != zenon_X11251)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10265)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12423))
% 18.37/18.55  ((skc19) != zenon_X11608)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11573))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11662)
% 18.37/18.55  (jules_forename (skc29) (skc32))
% 18.37/18.55  (-. (man (skc17) zenon_X11659))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11730)
% 18.37/18.55  (-. (state (skc17) zenon_X12431))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12217)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12109)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11202)
% 18.37/18.55  (-. (event (skc29) zenon_X13211))
% 18.37/18.55  ((skc32) != zenon_X13540)
% 18.37/18.55  ((skc19) != zenon_X12479)
% 18.37/18.55  ((skc32) != zenon_X10537)
% 18.37/18.55  ((skc19) != zenon_X10750)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11155))
% 18.37/18.55  (-. (event (skc17) zenon_X12402))
% 18.37/18.55  (-. (man (skc29) zenon_X13385))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10825))
% 18.37/18.55  (-. (man (skc29) zenon_X12991))
% 18.37/18.55  ((skc25) != zenon_X10393)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11194)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10730))
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10877)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X11012))
% 18.37/18.55  ((skc34) != zenon_X10286)
% 18.37/18.55  (-. (man (skc29) zenon_X11412))
% 18.37/18.55  (-. (man (skc29) zenon_X13026))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13019))
% 18.37/18.55  (-. (man (skc17) zenon_X11249))
% 18.37/18.55  ((skc20) != zenon_X12094)
% 18.37/18.55  (be (skc29) (skc30) (skc31) (skc31))
% 18.37/18.55  ((skc32) != zenon_X10888)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10552)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10860)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11887))
% 18.37/18.55  ((skc23) != zenon_X11689)
% 18.37/18.55  ((skc21) != zenon_X10420)
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10305)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11032)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10348)
% 18.37/18.55  ((skc34) != zenon_X13367)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10607)
% 18.37/18.55  ((skc32) != zenon_X13434)
% 18.37/18.55  (-. (forename (skc17) zenon_X12255))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13402)
% 18.37/18.55  ((skc21) != zenon_X10787)
% 18.37/18.55  ((skc20) != zenon_X11599)
% 18.37/18.55  ((skc25) != zenon_X11655)
% 18.37/18.55  (vincent_forename (skc29) (skc35))
% 18.37/18.55  ((skc25) != zenon_X11612)
% 18.37/18.55  ((skc21) != zenon_X11653)
% 18.37/18.55  ((skc31) != zenon_X13542)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13510)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10859)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11606)
% 18.37/18.55  ((skc31) != zenon_X10332)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13435)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10673))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10395)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12085)
% 18.37/18.55  ((skc32) != zenon_X13254)
% 18.37/18.55  ((skc30) != zenon_X10322)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13576)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12569)
% 18.37/18.55  (zenon_X11 != zenon_X12945)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10515)
% 18.37/18.55  ((skc21) != zenon_X12257)
% 18.37/18.55  (-. (state (skc29) zenon_X10482))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13385)
% 18.37/18.55  (-. (man (skc29) zenon_X11396))
% 18.37/18.55  (-. (man (skc17) zenon_X11759))
% 18.37/18.55  (-. (man (skc17) zenon_X10421))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11251)
% 18.37/18.55  ((skc31) != zenon_X10579)
% 18.37/18.55  (-. (man (skc17) zenon_X10783))
% 18.37/18.55  ((skc31) != zenon_X13248)
% 18.37/18.55  ((skc20) != zenon_X11250)
% 18.37/18.55  ((skc20) != zenon_X10373)
% 18.37/18.55  (-. (forename (skc17) zenon_X10684))
% 18.37/18.55  ((skc20) != zenon_X12100)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12020))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12542)
% 18.37/18.55  (-. (man (skc17) zenon_X11607))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13000))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10791)
% 18.37/18.55  ((skc25) != zenon_X10514)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10272)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10650)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13043)
% 18.37/18.55  ((skc29) != zenon_X31)
% 18.37/18.55  ((skc18) != zenon_X10661)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11692))
% 18.37/18.55  ((skc25) != zenon_X10602)
% 18.37/18.55  ((skc21) != zenon_X10536)
% 18.37/18.55  ((skc18) != zenon_X11864)
% 18.37/18.55  ((skc31) != zenon_X12604)
% 18.37/18.55  ((skc21) != zenon_X11249)
% 18.37/18.55  ((skc20) != zenon_X11560)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12992))
% 18.37/18.55  ((skc20) != zenon_X10580)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11822))
% 18.37/18.55  (forename (skc29) (skc35))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11175)
% 18.37/18.55  ((skc25) != zenon_X11602)
% 18.37/18.55  ((skc20) != zenon_X10381)
% 18.37/18.55  ((skc20) != zenon_X10771)
% 18.37/18.55  ((skc31) != zenon_X10666)
% 18.37/18.55  (-. (man (skc17) zenon_X11200))
% 18.37/18.55  ((skc19) != zenon_X12026)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10554)
% 18.37/18.55  (man (skc29) (skc31))
% 18.37/18.55  ((skc18) != zenon_X11153)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10828))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12056))
% 18.37/18.55  ((skc19) != zenon_X10396)
% 18.37/18.55  ((skc32) != zenon_X13391)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11738)
% 18.37/18.55  ((skc36) != zenon_X10595)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10772)
% 18.37/18.55  ((skc20) != zenon_X11155)
% 18.37/18.55  ((skc36) != (skf11 zenon_X23))
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10953)
% 18.37/18.55  ((skc25) != (skf7 zenon_X11066))
% 18.37/18.55  (-. (man (skc17) zenon_X10808))
% 18.37/18.55  ((skc32) != zenon_X13214)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10839))
% 18.37/18.55  (-. (state (skc29) zenon_X12564))
% 18.37/18.55  ((skc32) != zenon_X13516)
% 18.37/18.55  (present (skc33) (skf9 zenon_X3))
% 18.37/18.55  ((skc36) != zenon_X10420)
% 18.37/18.55  ((skf5 zenon_X11) != (skf5 zenon_X12930))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12050)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10879)
% 18.37/18.55  ((skc20) != zenon_X10775)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10787)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10602)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10904))
% 18.37/18.55  (-. (state (skc17) zenon_X12465))
% 18.37/18.55  ((skc31) != zenon_X13281)
% 18.37/18.55  ((skc33) != zenon_X10233)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10549)
% 18.37/18.55  ((skc36) != zenon_X13008)
% 18.37/18.55  ((skc24) != zenon_X10381)
% 18.37/18.55  ((skc32) != zenon_X10670)
% 18.37/18.55  ((skc36) != zenon_X10644)
% 18.37/18.55  (-. (man (skc17) zenon_X11733))
% 18.37/18.55  ((skc20) != zenon_X10844)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13254))
% 18.37/18.55  (-. (man (skc17) zenon_X10344))
% 18.37/18.55  ((skc20) != zenon_X12487)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11832)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12121))
% 18.37/18.55  (-. (man (skc29) zenon_X11032))
% 18.37/18.55  ((skc31) != zenon_X10912)
% 18.37/18.55  ((skc36) != zenon_X10512)
% 18.37/18.55  ((skc25) != zenon_X10648)
% 18.37/18.55  ((skc21) != zenon_X10602)
% 18.37/18.55  ((skc32) != zenon_X10368)
% 18.37/18.55  (-. (man (skc29) zenon_X13245))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10332)
% 18.37/18.55  ((skc21) != zenon_X11832)
% 18.37/18.55  (-. (event (skc17) zenon_X11557))
% 18.37/18.55  ((skc36) != zenon_X10951)
% 18.37/18.55  (-. (man (skc29) zenon_X13561))
% 18.37/18.55  ((skc23) != zenon_X10292)
% 18.37/18.55  ((skc36) != zenon_X10603)
% 18.37/18.55  ((skc20) != zenon_X10645)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10499)
% 18.37/18.55  ((skc21) != (skc25))
% 18.37/18.55  ((skc25) != zenon_X10552)
% 18.37/18.55  ((skc19) != zenon_X12160)
% 18.37/18.55  ((skc32) != zenon_X12551)
% 18.37/18.55  ((skc31) != zenon_X10879)
% 18.37/18.55  ((skc25) != zenon_X11811)
% 18.37/18.55  (-. (man (skc29) zenon_X12604))
% 18.37/18.55  (-. (forename (skc29) zenon_X13399))
% 18.37/18.55  ((skc32) != zenon_X13005)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11154)
% 18.37/18.55  ((skc19) != zenon_X11924)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13386))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13245)
% 18.37/18.55  (man (skc17) (skc25))
% 18.37/18.55  ((skc31) != zenon_X10683)
% 18.37/18.55  (zenon_X9 != zenon_X7)
% 18.37/18.55  ((skc36) != zenon_X10971)
% 18.37/18.55  ((skc24) != zenon_X10368)
% 18.37/18.55  ((skc21) != zenon_X10666)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11202)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10512)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12094))
% 18.37/18.55  (-. (accessible_world (skc17) zenon_X10225))
% 18.37/18.55  ((skc20) != zenon_X10773)
% 18.37/18.55  ((skc25) != zenon_X11229)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11200)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11759)
% 18.37/18.55  ((skf5 zenon_X11053) != zenon_X10279)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10395)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12028)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10651)
% 18.37/18.55  ((skc31) != zenon_X13404)
% 18.37/18.55  ((skc20) != zenon_X11718)
% 18.37/18.55  (-. (event (skc29) zenon_X10279))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12628)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10765)
% 18.37/18.55  ((skc25) != zenon_X12083)
% 18.37/18.55  (-. (man (skc22) (skf7 zenon_X15)))
% 18.37/18.55  ((skc20) != zenon_X10398)
% 18.37/18.55  ((skc25) != zenon_X11657)
% 18.37/18.55  ((skc36) != zenon_X12991)
% 18.37/18.55  ((skc19) != zenon_X11780)
% 18.37/18.55  ((skc21) != zenon_X10512)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10603)
% 18.37/18.55  ((skc21) != zenon_X11607)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10394)
% 18.37/18.55  ((skf5 zenon_X12944) != (skf5 zenon_X7))
% 18.37/18.55  ((skc31) != zenon_X13279)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10394)
% 18.37/18.55  (zenon_X12930 != zenon_X7)
% 18.37/18.55  ((skf5 zenon_X11053) != zenon_X10481)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12438))
% 18.37/18.55  (-. (event (skc17) zenon_X10272))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12148))
% 18.37/18.55  ((skc32) != zenon_X10567)
% 18.37/18.55  (-. (forename (skc29) zenon_X10548))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11199)
% 18.37/18.55  ((skc21) != zenon_X12085)
% 18.37/18.55  ((skc31) != zenon_X10396)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10808)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10394)
% 18.37/18.55  ((skc35) != zenon_X13399)
% 18.37/18.55  ((skc20) != zenon_X10591)
% 18.37/18.55  (-. (man (skc17) zenon_X11154))
% 18.37/18.55  (-. (actual_world zenon_X14))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11662)
% 18.37/18.55  ((skc36) != zenon_X10651)
% 18.37/18.55  (-. (state (skc17) zenon_X11864))
% 18.37/18.55  ((skc36) != zenon_X12542)
% 18.37/18.55  ((skc32) != zenon_X10885)
% 18.37/18.55  (-. (state (skc17) zenon_X12138))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11712)
% 18.37/18.55  ((skf5 zenon_X9) != (skf5 zenon_X7))
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10279)
% 18.37/18.55  ((skc25) != zenon_X10395)
% 18.37/18.55  (event (skc22) (skf5 zenon_X12930))
% 18.37/18.55  ((skf5 zenon_X11131) != zenon_X10279)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10971)
% 18.37/18.55  (-. (forename (skc17) zenon_X11729))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11721))
% 18.37/18.55  (-. (forename (skc17) zenon_X11599))
% 18.37/18.55  ((skc25) != zenon_X11633)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11160))
% 18.37/18.55  ((skc19) != zenon_X12453)
% 18.37/18.55  (-. (present (skc22) (skf5 zenon_X7)))
% 18.37/18.55  ((skc20) != zenon_X10550)
% 18.37/18.55  ((skc25) != zenon_X11200)
% 18.37/18.55  ((skc31) != zenon_X10991)
% 18.37/18.55  ((skc31) != zenon_X13008)
% 18.37/18.55  ((skc21) != zenon_X10355)
% 18.37/18.55  ((skc25) != zenon_X8)
% 18.37/18.55  (-. (state (skc17) zenon_X11923))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12643)
% 18.37/18.55  (-. (man (skc17) zenon_X10597))
% 18.37/18.55  (-. (event (skc17) zenon_X10265))
% 18.37/18.55  ((skc19) != zenon_X12257)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13546))
% 18.37/18.55  ((skc36) != zenon_X10597)
% 18.37/18.55  ((skf5 zenon_X11053) != (skc23))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X13264)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12160)
% 18.37/18.55  ((skc20) != zenon_X10529)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11032)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10602)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13027))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11222))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13008)
% 18.37/18.55  ((skc18) != zenon_X11923)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11396)
% 18.37/18.55  ((skc32) != zenon_X12585)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10603)
% 18.37/18.55  ((skc32) != zenon_X10647)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10637))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13011))
% 18.37/18.55  ((skc21) != zenon_X11712)
% 18.37/18.55  ((skc25) != zenon_X10397)
% 18.37/18.55  (-. (man (skc29) zenon_X13264))
% 18.37/18.55  (-. (man (skc17) zenon_X10395))
% 18.37/18.55  ((skc24) != zenon_X10857)
% 18.37/18.55  ((skf5 zenon_X11378) != zenon_X10234)
% 18.37/18.55  ((skc36) != zenon_X13264)
% 18.37/18.55  ((skc19) != zenon_X11730)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X12645)
% 18.37/18.55  ((skc20) != zenon_X10500)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11030)
% 18.37/18.55  (-. (man (skc17) zenon_X12028))
% 18.37/18.55  ((skc35) != zenon_X13243)
% 18.37/18.55  ((skc20) != zenon_X12079)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13248)
% 18.37/18.55  ((skc24) != zenon_X11248)
% 18.37/18.55  ((skc19) != zenon_X10648)
% 18.37/18.55  ((skc32) != zenon_X11407)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12645)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10397)
% 18.37/18.55  ((skc21) != zenon_X10515)
% 18.37/18.55  ((skc32) != zenon_X13511)
% 18.37/18.55  ((skc20) != zenon_X10588)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11771))
% 18.37/18.55  (of (skc17) (skc24) (skc25))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11559)
% 18.37/18.55  ((skc32) != zenon_X11021)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11744))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10838)
% 18.37/18.55  ((skc20) != zenon_X10855)
% 18.37/18.55  ((skc21) != zenon_X10514)
% 18.37/18.55  (-. (man (skc29) zenon_X10397))
% 18.37/18.55  ((skc24) != zenon_X10375)
% 18.37/18.55  (-. (man (skc29) zenon_X12596))
% 18.37/18.55  ((skc19) != zenon_X11202)
% 18.37/18.55  ((skc30) != zenon_X13009)
% 18.37/18.55  ((skc19) != (skf7 zenon_X11066))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10683)
% 18.37/18.55  ((skc22) != zenon_X10233)
% 18.37/18.55  ((skc19) != zenon_X12050)
% 18.37/18.55  ((skc20) != zenon_X10803)
% 18.37/18.55  ((skc18) != zenon_X10327)
% 18.37/18.55  ((skc24) != zenon_X12216)
% 18.37/18.55  ((skc20) != zenon_X11230)
% 18.37/18.55  (-. (event (skc29) zenon_X10481))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11247)
% 18.37/18.55  ((skc34) != zenon_X12507)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10856)
% 18.37/18.55  ((skc36) != zenon_X10483)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12991)
% 18.37/18.55  (-. (forename (skc17) zenon_X10853))
% 18.37/18.55  ((skc34) != zenon_X10279)
% 18.37/18.55  ((skc18) != zenon_X12138)
% 18.37/18.55  ((skc19) != zenon_X10644)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12257)
% 18.37/18.55  ((skc25) != zenon_X10644)
% 18.37/18.55  ((skc19) != zenon_X12083)
% 18.37/18.55  (-. (forename (skc17) zenon_X11198))
% 18.37/18.55  ((skc36) != zenon_X10602)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11210)
% 18.37/18.55  ((skc36) != zenon_X13279)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X11712)
% 18.37/18.55  (-. (man (skc29) zenon_X13545))
% 18.37/18.55  ((skc20) != zenon_X11825)
% 18.37/18.55  ((skc30) != zenon_X13544)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12543))
% 18.37/18.55  ((skc19) != zenon_X10774)
% 18.37/18.55  ((skc20) != zenon_X10598)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X12050)
% 18.37/18.55  ((skc19) != zenon_X12028)
% 18.37/18.55  (-. (man (skc29) zenon_X12518))
% 18.37/18.55  (-. (man (skc29) zenon_X13404))
% 18.37/18.55  ((skc24) != zenon_X10775)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10579)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10536)
% 18.37/18.55  ((skc34) != zenon_X10316)
% 18.37/18.55  ((skc19) != zenon_X10483)
% 18.37/18.55  ((skc21) != zenon_X12026)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13264)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10580))
% 18.37/18.55  ((skc21) != zenon_X12028)
% 18.37/18.55  (smoke (skc33) (skf9 zenon_X5))
% 18.37/18.55  (-. (forename (skc29) zenon_X10418))
% 18.37/18.55  ((skf5 zenon_X9) != zenon_X10299)
% 18.37/18.55  (-. (man (skc17) zenon_X11612))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11613))
% 18.37/18.55  (-. (forename (skc17) zenon_X10373))
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10741))
% 18.37/18.55  (-. (forename (skc29) zenon_X13575))
% 18.37/18.55  ((skc31) != (skf11 zenon_X23))
% 18.37/18.55  ((skc32) != zenon_X10949)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13545)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13516))
% 18.37/18.55  (-. (forename (skc17) zenon_X12023))
% 18.37/18.55  (zenon_X11 != zenon_X12944)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10729)
% 18.37/18.55  ((skc21) != zenon_X10348)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10481)
% 18.37/18.55  ((skc31) != zenon_X10348)
% 18.37/18.55  ((skc20) != zenon_X11198)
% 18.37/18.55  ((skc32) != zenon_X10596)
% 18.37/18.55  ((skc19) != zenon_X11633)
% 18.37/18.55  (present (skc29) (skc34))
% 18.37/18.55  ((skc25) != zenon_X10651)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X13010)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X12417))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10648)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13385)
% 18.37/18.55  ((skc21) != zenon_X11738)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10910)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11607)
% 18.37/18.55  ((skc21) != zenon_X10651)
% 18.37/18.55  (-. (event (skc17) zenon_X10305))
% 18.37/18.55  ((skc35) != zenon_X10598)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10380)
% 18.37/18.55  (-. (man (skc29) zenon_X11011))
% 18.37/18.55  ((skc32) != zenon_X13016)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13511))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12588))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11865)
% 18.37/18.55  ((skc31) != zenon_X10420)
% 18.37/18.55  ((skf7 zenon_X11073) != (skf7 zenon_X15))
% 18.37/18.55  ((skc35) != zenon_X12642)
% 18.37/18.55  ((skc25) != zenon_X12479)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11602)
% 18.37/18.55  (-. (man (skc29) zenon_X10551))
% 18.37/18.55  ((skc31) != zenon_X10549)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10292)
% 18.37/18.55  ((skc23) != zenon_X11922)
% 18.37/18.55  ((skc36) != zenon_X10397)
% 18.37/18.55  ((skc19) != zenon_X11777)
% 18.37/18.55  (zenon_X11131 != zenon_X7)
% 18.37/18.55  ((skf5 zenon_X11053) != zenon_X10234)
% 18.37/18.55  (forename (skc17) (skc24))
% 18.37/18.55  ((skc32) != zenon_X12984)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13541)
% 18.37/18.55  ((skc36) != zenon_X13229)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X13375))
% 18.37/18.55  ((skc32) != zenon_X10640)
% 18.37/18.55  ((skc21) != zenon_X10783)
% 18.37/18.55  (-. (state (skc29) zenon_X10519))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X11396)
% 18.37/18.55  ((skc32) != zenon_X10526)
% 18.37/18.55  ((skc25) != zenon_X10858)
% 18.37/18.55  ((skf5 zenon_X11131) != (skc23))
% 18.37/18.55  ((skc30) != zenon_X11414)
% 18.37/18.55  (-. (man (skc29) zenon_X10520))
% 18.37/18.55  ((skc21) != zenon_X11811)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10772)
% 18.37/18.55  ((skf5 zenon_X11053) != (skf9 zenon_X1))
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10422)
% 18.37/18.55  ((skc20) != zenon_X11957)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11210)
% 18.37/18.55  ((skc20) != zenon_X11597)
% 18.37/18.55  (-. (man (skc29) zenon_X10517))
% 18.37/18.55  ((skc19) != zenon_X11657)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10774)
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10422)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10404)
% 18.37/18.55  (event (skc17) (skc23))
% 18.37/18.55  ((skc20) != zenon_X11237)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10554)
% 18.37/18.55  (-. (forename (skc17) zenon_X10391))
% 18.37/18.55  ((skf5 zenon_X7) != zenon_X10272)
% 18.37/18.55  (man zenon_X11066 (skf7 zenon_X11066))
% 18.37/18.55  ((skc25) != zenon_X12026)
% 18.37/18.55  ((skc31) != zenon_X13041)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10980))
% 18.37/18.55  (-. (man (skc17) zenon_X10854))
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12997))
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X13244)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10526))
% 18.37/18.55  (-. (man (skc22) (skc31)))
% 18.37/18.55  ((skc19) != zenon_X10515)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X10394)
% 18.37/18.55  (vincent_forename (skc17) (skc24))
% 18.37/18.55  (-. (man (skc17) zenon_X10644))
% 18.37/18.55  ((skc25) != zenon_X11691)
% 18.37/18.55  ((skf9 zenon_X1) != zenon_X10481)
% 18.37/18.55  ((skc31) != zenon_X12542)
% 18.37/18.55  ((skc36) != zenon_X10499)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X10961))
% 18.37/18.55  (-. (forename (skc17) zenon_X11601))
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13436)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10652)
% 18.37/18.55  ((skc35) != zenon_X12530)
% 18.37/18.55  ((skc25) != zenon_X12160)
% 18.37/18.55  (zenon_X11799 != zenon_X7)
% 18.37/18.55  (-. (event (skc29) zenon_X13367))
% 18.37/18.55  (-. (state (skc29) zenon_X12974))
% 18.37/18.55  ((skc21) != (skf7 zenon_X11066))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10344)
% 18.37/18.55  (-. (man (skc17) zenon_X12413))
% 18.37/18.55  ((skc24) != zenon_X11656)
% 18.37/18.55  ((skf7 zenon_X11073) != zenon_X13279)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X12975)
% 18.37/18.55  (-. (jules_forename (skc29) zenon_X12976))
% 18.37/18.55  ((skc30) != zenon_X10954)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X11659)
% 18.37/18.55  ((skc36) != zenon_X13435)
% 18.37/18.55  ((skc30) != zenon_X11415)
% 18.37/18.55  ((skc24) != zenon_X10402)
% 18.37/18.55  ((skc34) != zenon_X10953)
% 18.37/18.55  ((skc36) != zenon_X10393)
% 18.37/18.55  (-. (man (skc29) zenon_X10935))
% 18.37/18.55  ((skc32) != zenon_X13278)
% 18.37/18.55  (-. (state (skc17) zenon_X11611))
% 18.37/18.55  ((skc19) != zenon_X11655)
% 18.37/18.55  ((skc20) != zenon_X12454)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10783)
% 18.37/18.55  ((skc32) != zenon_X13040)
% 18.37/18.55  (-. (smoke (skc22) (skf5 zenon_X11131)))
% 18.37/18.55  ((skc23) != zenon_X11152)
% 18.37/18.55  ((skc20) != zenon_X11634)
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X11175)
% 18.37/18.55  (zenon_X11053 != zenon_X7)
% 18.37/18.55  ((skc20) != zenon_X10362)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11739))
% 18.37/18.55  (-. (event zenon_X10233 zenon_X10234))
% 18.37/18.55  ((skc36) != zenon_X13043)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X10822))
% 18.37/18.55  ((skc31) != zenon_X10380)
% 18.37/18.55  (-. (man (skc29) zenon_X13279))
% 18.37/18.55  ((skc36) != zenon_X10991)
% 18.37/18.55  ((skc31) != zenon_X10919)
% 18.37/18.55  ((skf7 zenon_X15) != zenon_X10602)
% 18.37/18.55  ((skc20) != zenon_X11654)
% 18.37/18.55  ((skc22) != (skc17))
% 18.37/18.55  ((skc31) != zenon_X10951)
% 18.37/18.55  ((skc19) != zenon_X11559)
% 18.37/18.55  ((skc21) != zenon_X11945)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11649))
% 18.37/18.55  ((skc31) != zenon_X10628)
% 18.37/18.55  ((skc29) != (skc17))
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10995)
% 18.37/18.55  ((skc31) != zenon_X12628)
% 18.37/18.55  ((skf7 zenon_X11066) != zenon_X10666)
% 18.37/18.55  (-. (jules_forename (skc17) zenon_X11946))
% 18.37/18.55  ((skc25) != zenon_X11924)
% 18.37/18.55  ((skc35) != zenon_X10418)
% 18.37/18.55  ((skc31) != zenon_X8)
% 18.37/18.55  ((skf5 zenon_X11) != (skf5 zenon_X12931))
% 18.37/18.55  ((skf11 zenon_X23) != zenon_X10919)
% 18.37/18.55  (-. (forename (skc29) zenon_X10513))
% 18.37/18.55  ((skc31) != zenon_X10499)
% 18.37/18.55  *)
% 18.37/18.55  (* NO-PROOF *)
% 18.37/18.55  % SZS status GaveUp
% 18.37/18.55  Number of rewrites on terms: 0
% 18.37/18.55  Number of rewrites on props: 0
% 18.37/18.55  nodes searched: 110007
% 18.37/18.55  max branch formulas: 18165
% 18.37/18.55  proof nodes created: 14489
% 18.37/18.55  formulas created: 687399
% 18.37/18.55  
%------------------------------------------------------------------------------