↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : NLP163-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n010.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:29 EDT 2024

% Result   : Unknown 1.01s 1.24s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12  % Problem  : NLP163-1 : TPTP v8.2.0. Released v2.4.0.
% 0.12/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.33  % Computer : n010.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 : Sat Jun 22 23:42:39 EDT 2024
% 0.12/0.33  % CPUTime  : 
% 1.01/1.23  Zenon error: exhausted search space without finding a proof
% 1.01/1.23  (* Current branch:
% 1.01/1.23  ((skf11 (skc63) (skc20)) != (skf11 zenon_X24 zenon_X25))
% 1.01/1.23  (member zenon_X866 (skf11 zenon_X866 zenon_X659) zenon_X659)
% 1.01/1.23  (zenon_X844 != (skc19))
% 1.01/1.23  ((skf23 (skc63) zenon_X0) != zenon_X152)
% 1.01/1.23  ((skf21 zenon_X153 (skc63) zenon_X798) != zenon_X152)
% 1.01/1.23  (member (skc19) (skf21 zenon_X0 (skc19) zenon_X812) zenon_X0)
% 1.01/1.23  ((skc64) != zenon_X155)
% 1.01/1.23  ((skc23) != zenon_X541)
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X694))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X108) != zenon_X152)
% 1.01/1.23  (zenon_X791 != (skc19))
% 1.01/1.23  ((skf11 (skc19) zenon_X16) != zenon_X154)
% 1.01/1.23  (member zenon_X790 (skf16 zenon_X8 zenon_X790 zenon_X108) zenon_X108)
% 1.01/1.23  (zenon_X769 != (skc63))
% 1.01/1.23  (hollywood_placename (skc19) (skc25))
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X153) zenon_X153)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X9) != zenon_X158)
% 1.01/1.23  ((skc70) != zenon_X503)
% 1.01/1.23  ((skf23 (skc63) zenon_X153) != zenon_X160)
% 1.01/1.23  (zenon_X171 != (skc19))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X9) zenon_X9)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X11) != zenon_X152)
% 1.01/1.23  ((skc69) != zenon_X723)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X537) != zenon_X152)
% 1.01/1.23  ((skf11 (skc19) zenon_X11) != zenon_X158)
% 1.01/1.23  (zenon_X659 != zenon_X537)
% 1.01/1.23  ((skf23 (skc63) zenon_X659) != zenon_X160)
% 1.01/1.23  ((skc19) != zenon_X24)
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X9) zenon_X9)
% 1.01/1.23  (-. (member (skc19) zenon_X5 (skc20)))
% 1.01/1.23  (young (skc63) (skf21 zenon_X97 (skc63) zenon_X936))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X155))
% 1.01/1.23  (zenon_X159 != zenon_X155)
% 1.01/1.23  (young (skc19) (skf21 zenon_X108 (skc19) zenon_X817))
% 1.01/1.23  (zenon_X179 != (skc63))
% 1.01/1.23  (-. (group (skc63) zenon_X616))
% 1.01/1.23  (zenon_X155 != zenon_X161)
% 1.01/1.23  (zenon_X813 != (skc19))
% 1.01/1.23  (member zenon_X882 (skf21 zenon_X16 zenon_X882 zenon_X883) zenon_X16)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X153))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X706))
% 1.01/1.23  (-. (city (skc63) zenon_X738))
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X155))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X161))
% 1.01/1.23  ((skf23 (skc63) zenon_X153) != zenon_X152)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X161) zenon_X161)
% 1.01/1.23  (zenon_X888 != (skc63))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X0) zenon_X0)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X537) != zenon_X154)
% 1.01/1.23  ((skf11 (skc19) (skc64)) != zenon_X154)
% 1.01/1.23  (member (skc63) (skf21 zenon_X659 (skc63) zenon_X949) zenon_X659)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X161) zenon_X161)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X153) zenon_X153)
% 1.01/1.23  ((skf21 zenon_X659 (skc19) zenon_X898) != zenon_X154)
% 1.01/1.23  (zenon_X9 != zenon_X161)
% 1.01/1.23  (zenon_X781 != (skc19))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X153))
% 1.01/1.23  (zenon_X9 != zenon_X155)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X159) != zenon_X158)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X659))
% 1.01/1.23  (-. (ssSkP0 zenon_X23 zenon_X21))
% 1.01/1.23  (young (skc19) (skf21 (skc64) (skc19) zenon_X201))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X0 (skc19) zenon_X812))
% 1.01/1.23  ((skf11 (skc19) zenon_X0) != zenon_X154)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X7)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X9) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X108))
% 1.01/1.23  ((skf11 (skc63) zenon_X161) != zenon_X152)
% 1.01/1.23  (zenon_X16 != zenon_X155)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X155) != zenon_X152)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X97) != zenon_X152)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X161) != zenon_X160)
% 1.01/1.23  ((skc69) != zenon_X737)
% 1.01/1.23  (barrel (skc63) (skc66))
% 1.01/1.23  (zenon_X659 != zenon_X153)
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X155) zenon_X155)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.01/1.23  ((skf11 (skc19) (skc20)) != zenon_X154)
% 1.01/1.23  (member zenon_X765 (skf19 zenon_X15 zenon_X765 zenon_X155) zenon_X155)
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X161) zenon_X161)
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X159))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X155) != zenon_X158)
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X9))
% 1.01/1.23  (zenon_X882 != (skc63))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 (skc64)) (skc64))
% 1.01/1.23  ((skf23 (skc63) zenon_X108) != zenon_X160)
% 1.01/1.23  (member zenon_X852 (skf16 zenon_X8 zenon_X852 zenon_X161) zenon_X161)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X97) != zenon_X160)
% 1.01/1.23  ((skf23 (skc19) zenon_X659) != zenon_X154)
% 1.01/1.23  (of (skc19) (skc25) (skc26))
% 1.01/1.23  ((skf11 (skc63) (skc64)) != zenon_X2)
% 1.01/1.23  (ssSkP0 (skc22) (skc19))
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X11))
% 1.01/1.23  (member (skc19) (skf21 zenon_X16 (skc19) zenon_X885) zenon_X16)
% 1.01/1.23  ((skc63) != zenon_X21)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X154)
% 1.01/1.23  ((skf11 (skc19) zenon_X9) != zenon_X154)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X155) != zenon_X152)
% 1.01/1.23  (zenon_X97 != zenon_X108)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X537 (skc63) zenon_X920))
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) (skc20)))
% 1.01/1.23  (zenon_X769 != (skc19))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X724))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X537))
% 1.01/1.23  (group (skc63) (skc65))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) (skc20)))
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X659))
% 1.01/1.23  (member (skc19) (skf21 zenon_X161 (skc19) zenon_X845) zenon_X161)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X659) != zenon_X154)
% 1.01/1.23  ((skf23 (skc19) (skc20)) != zenon_X158)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X97) zenon_X97)
% 1.01/1.23  ((skf21 zenon_X11 (skc19) zenon_X838) != zenon_X154)
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X537))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X11))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X16))
% 1.01/1.23  ((skf11 (skc63) (skc64)) != zenon_X152)
% 1.01/1.23  ((skf11 (skc63) zenon_X161) != zenon_X160)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X161) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X7)
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X153) zenon_X153)
% 1.01/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.01/1.23  ((skc65) != zenon_X685)
% 1.01/1.23  ((skf23 (skc19) zenon_X159) != zenon_X158)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X9) != zenon_X158)
% 1.01/1.23  (-. (group (skc63) zenon_X583))
% 1.01/1.23  ((skf11 (skc63) zenon_X16) != zenon_X152)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X155))
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X159))
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X537) zenon_X537)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc20)) != zenon_X160)
% 1.01/1.23  (-. (city (skc63) zenon_X746))
% 1.01/1.23  ((skc21) != zenon_X611)
% 1.01/1.23  ((skf11 (skc19) zenon_X97) != zenon_X154)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X659))
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) (skc64)))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X97))
% 1.01/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X153) zenon_X153)
% 1.01/1.23  ((skf11 (skc19) zenon_X16) != zenon_X158)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X9))
% 1.01/1.23  ((skc68) != zenon_X704)
% 1.01/1.23  ((skf23 (skc63) zenon_X537) != zenon_X152)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X153))
% 1.01/1.23  ((skf21 zenon_X0 (skc63) zenon_X811) != zenon_X160)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X159) != zenon_X160)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X108))
% 1.01/1.23  ((skf23 (skc63) zenon_X659) != zenon_X152)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X659) != zenon_X160)
% 1.01/1.23  (white (skc63) (skc70))
% 1.01/1.23  ((skc24) != zenon_X548)
% 1.01/1.23  (fellow (skc19) (skf21 (skc20) (skc19) zenon_X235))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X159))
% 1.01/1.23  (zenon_X108 != (skc64))
% 1.01/1.23  ((skf11 (skc19) zenon_X161) != zenon_X154)
% 1.01/1.23  ((skc64) != zenon_X161)
% 1.01/1.23  ((skc22) != zenon_X594)
% 1.01/1.23  ((skf11 (skc63) (skc64)) != zenon_X3)
% 1.01/1.23  (zenon_X537 != zenon_X161)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X11))
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X108 (skc63) zenon_X818))
% 1.01/1.23  (zenon_X9 != zenon_X11)
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X161))
% 1.01/1.23  ((skc19) != zenon_X486)
% 1.01/1.23  (member zenon_X781 (skf21 zenon_X155 zenon_X781 zenon_X782) zenon_X155)
% 1.01/1.23  ((skf21 zenon_X97 (skc19) zenon_X937) != zenon_X158)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X153))
% 1.01/1.23  (member zenon_X785 (skf19 zenon_X15 zenon_X785 zenon_X108) zenon_X108)
% 1.01/1.23  ((skf23 (skc19) zenon_X16) != zenon_X154)
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X700))
% 1.01/1.23  (down (skc63) (skc66) (skc67))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X710))
% 1.01/1.23  (zenon_X0 != zenon_X108)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X9) zenon_X9)
% 1.01/1.23  (member zenon_X166 (skf21 (skc20) zenon_X166 zenon_X167) (skc20))
% 1.01/1.23  ((skc69) != zenon_X736)
% 1.01/1.23  (member (skc63) (skf21 zenon_X97 (skc63) zenon_X936) zenon_X97)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X155) zenon_X155)
% 1.01/1.23  (zenon_X97 != zenon_X9)
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X0) zenon_X0)
% 1.01/1.23  (zenon_X802 != (skc63))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc20)) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X161) != zenon_X152)
% 1.01/1.23  (member zenon_X793 (skf19 zenon_X15 zenon_X793 zenon_X537) zenon_X537)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) (skc64)) (skc64))
% 1.01/1.23  ((skf21 zenon_X155 (skc63) zenon_X913) != zenon_X160)
% 1.01/1.23  (member (skc19) (skf21 zenon_X153 (skc19) zenon_X853) zenon_X153)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X161) != zenon_X158)
% 1.01/1.23  (-. (city (skc63) zenon_X739))
% 1.01/1.23  (down (skc19) (skc23) (skc24))
% 1.01/1.23  (zenon_X159 != zenon_X161)
% 1.01/1.23  (young (skc19) (skf21 zenon_X11 (skc19) zenon_X838))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X16))
% 1.01/1.23  ((skf21 zenon_X9 (skc19) zenon_X891) != zenon_X154)
% 1.01/1.23  (zenon_X868 != (skc19))
% 1.01/1.23  (present (skc19) (skc23))
% 1.01/1.23  (zenon_X852 != (skc19))
% 1.01/1.23  ((skf23 (skc63) zenon_X537) != zenon_X160)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X108) != zenon_X154)
% 1.01/1.23  ((skc68) != zenon_X718)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X108) zenon_X108)
% 1.01/1.23  (-. (member (skc19) zenon_X7 (skc20)))
% 1.01/1.23  (zenon_X0 != zenon_X153)
% 1.01/1.23  (-. (member (skc19) zenon_X154 (skc64)))
% 1.01/1.23  (coat (skc63) (skf23 (skc63) (skc64)))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X729))
% 1.01/1.23  (-. (barrel (skc63) zenon_X576))
% 1.01/1.23  (member zenon_X10 (skf16 zenon_X8 zenon_X10 zenon_X9) zenon_X9)
% 1.01/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.01/1.23  (member (skc63) (skf21 zenon_X108 (skc63) zenon_X818) zenon_X108)
% 1.01/1.23  (-. (member (skc19) zenon_X6 (skc20)))
% 1.01/1.23  (ssSkP0 (skc71) (skc63))
% 1.01/1.23  (-. (member (skc19) zenon_X154 (skc20)))
% 1.01/1.23  (zenon_X827 != (skc19))
% 1.01/1.23  ((skf21 zenon_X659 (skc63) zenon_X949) != zenon_X160)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X155 (skc63) zenon_X913))
% 1.01/1.23  (young (skc63) (skf23 (skc63) (skc20)))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X160)
% 1.01/1.23  (event (skc63) (skc66))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X161) != zenon_X154)
% 1.01/1.23  ((skc64) != zenon_X688)
% 1.01/1.23  (zenon_X781 != (skc63))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X0) != zenon_X158)
% 1.01/1.23  ((skf23 (skc19) zenon_X11) != zenon_X154)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X97))
% 1.01/1.23  (-. (city (skc63) zenon_X737))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X11) != zenon_X154)
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X0))
% 1.01/1.23  ((skc65) != zenon_X616)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X153))
% 1.01/1.23  (member zenon_X784 (skf19 zenon_X15 zenon_X784 zenon_X153) zenon_X153)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X0) zenon_X0)
% 1.01/1.23  (zenon_X941 != (skc19))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X704))
% 1.01/1.23  (member zenon_X867 (skf19 zenon_X15 zenon_X867 zenon_X0) zenon_X0)
% 1.01/1.23  ((skc64) != zenon_X159)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X11))
% 1.01/1.23  (member (skc19) (skf23 (skc19) (skc64)) (skc64))
% 1.01/1.23  (cheap (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X537))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X97))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X0) zenon_X0)
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X0))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X155))
% 1.01/1.23  (zenon_X784 != (skc63))
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X108))
% 1.01/1.23  (zenon_X0 != (skc20))
% 1.01/1.23  (zenon_X97 != (skc20))
% 1.01/1.23  (zenon_X16 != zenon_X161)
% 1.01/1.23  (zenon_X659 != zenon_X108)
% 1.01/1.23  ((skc67) != zenon_X588)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X161) zenon_X161)
% 1.01/1.23  (zenon_X868 != (skc63))
% 1.01/1.23  (zenon_X108 != (skc20))
% 1.01/1.23  (member (skc63) (skf21 (skc20) (skc63) zenon_X237) (skc20))
% 1.01/1.23  ((skc68) != zenon_X724)
% 1.01/1.23  (black (skc63) (skf23 (skc63) (skc64)))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X659) != zenon_X152)
% 1.01/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X6)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) (skc64)))
% 1.01/1.23  ((skc63) != zenon_X486)
% 1.01/1.23  ((skc68) != zenon_X714)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X153) != zenon_X158)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X161))
% 1.01/1.23  ((skc71) != zenon_X111)
% 1.01/1.23  (member zenon_X819 (skf11 zenon_X819 zenon_X16) zenon_X16)
% 1.01/1.23  (street (skc63) (skc67))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X161))
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X16) zenon_X16)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X11))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X97))
% 1.01/1.23  (young (skc19) (skf11 (skc19) (skc64)))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.01/1.23  ((skf23 (skc19) (skc64)) != zenon_X154)
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X9))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc64)) != zenon_X154)
% 1.01/1.23  (zenon_X659 != zenon_X11)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X16) zenon_X16)
% 1.01/1.23  (zenon_X16 != zenon_X537)
% 1.01/1.23  (member zenon_X918 (skf21 zenon_X537 zenon_X918 zenon_X919) zenon_X537)
% 1.01/1.23  ((skf23 (skc19) zenon_X9) != zenon_X158)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X153) != zenon_X154)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X9) != zenon_X160)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X9))
% 1.01/1.23  ((skc71) != zenon_X679)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X659))
% 1.01/1.23  ((skf23 (skc19) zenon_X97) != zenon_X154)
% 1.01/1.23  (fellow (skc19) (skf21 (skc64) (skc19) zenon_X201))
% 1.01/1.23  ((skc69) != zenon_X720)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X9))
% 1.01/1.23  ((skc69) != zenon_X735)
% 1.01/1.23  (zenon_X934 != (skc63))
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X11))
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X659 (skc63) zenon_X949))
% 1.01/1.23  ((skf21 zenon_X11 (skc63) zenon_X764) != zenon_X152)
% 1.01/1.23  (member (skc63) (skf21 zenon_X153 (skc63) zenon_X798) zenon_X153)
% 1.01/1.23  (-. (member (skc63) zenon_X2 (skc64)))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X155))
% 1.01/1.23  (member zenon_X886 (skf19 zenon_X15 zenon_X886 zenon_X161) zenon_X161)
% 1.01/1.23  (zenon_X777 != (skc19))
% 1.01/1.23  ((skf11 (skc63) zenon_X108) != zenon_X160)
% 1.01/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X108) zenon_X108)
% 1.01/1.23  (zenon_X0 != zenon_X537)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X9))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X155) != zenon_X154)
% 1.01/1.23  (-. (old (skc63) zenon_X503))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X159) != zenon_X160)
% 1.01/1.23  (member zenon_X839 (skf16 zenon_X8 zenon_X839 zenon_X659) zenon_X659)
% 1.01/1.23  ((skf21 zenon_X0 (skc19) zenon_X812) != zenon_X158)
% 1.01/1.23  ((skf21 (skc20) (skc63) zenon_X237) != zenon_X160)
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X712))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X159))
% 1.01/1.23  ((skf23 (skc63) (skc64)) != zenon_X2)
% 1.01/1.23  ((skf23 (skc63) zenon_X155) != zenon_X160)
% 1.01/1.23  ((skc71) != zenon_X685)
% 1.01/1.23  ((skf23 (skc19) zenon_X155) != zenon_X154)
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X155))
% 1.01/1.23  ((skf11 (skc63) zenon_X11) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X659))
% 1.01/1.23  (zenon_X659 != (skc20))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X537))
% 1.01/1.23  ((skc70) != zenon_X495)
% 1.01/1.23  ((skc64) != zenon_X652)
% 1.01/1.23  ((skc69) != zenon_X740)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X108))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X161))
% 1.01/1.23  (member zenon_X171 (skf19 zenon_X15 zenon_X171 (skc20)) (skc20))
% 1.01/1.23  (-. (group (skc63) zenon_X688))
% 1.01/1.23  (coat (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.01/1.23  (nonreflexive zenon_X49 (skf17 zenon_X49 zenon_X55 zenon_X53))
% 1.01/1.23  (member zenon_X777 (skf11 zenon_X777 zenon_X153) zenon_X153)
% 1.01/1.23  ((skf21 zenon_X97 (skc19) zenon_X937) != zenon_X154)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X153))
% 1.01/1.23  (coat (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.01/1.23  (member (skc19) (skf21 zenon_X11 (skc19) zenon_X838) zenon_X11)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X159) != zenon_X154)
% 1.01/1.23  ((skf11 (skc19) (skc20)) != zenon_X5)
% 1.01/1.23  (zenon_X11 != zenon_X161)
% 1.01/1.23  ((skc69) != zenon_X742)
% 1.01/1.23  (zenon_X0 != (skc64))
% 1.01/1.23  (member zenon_X101 (skf10 zenon_X101 zenon_X108) zenon_X108)
% 1.01/1.23  ((skc64) != zenon_X583)
% 1.01/1.23  (zenon_X171 != (skc63))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X5)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X108) zenon_X108)
% 1.01/1.23  ((skc66) != zenon_X563)
% 1.01/1.23  ((skf21 zenon_X108 (skc63) zenon_X818) != zenon_X160)
% 1.01/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X153))
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X159) zenon_X159)
% 1.01/1.23  (zenon_X910 != (skc63))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X155) != zenon_X160)
% 1.01/1.23  ((skf11 (skc19) zenon_X159) != zenon_X158)
% 1.01/1.23  (-. (city (skc63) zenon_X734))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X16) != zenon_X154)
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X0) zenon_X0)
% 1.01/1.23  (zenon_X97 != (skc64))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X97))
% 1.01/1.23  ((skf11 (skc19) zenon_X97) != zenon_X158)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X4)
% 1.01/1.23  (-. (street (skc19) zenon_X548))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X9))
% 1.01/1.23  ((skf21 zenon_X11 (skc63) zenon_X764) != zenon_X160)
% 1.01/1.23  (zenon_X815 != (skc63))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X159))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X153) != zenon_X152)
% 1.01/1.23  (group (skc63) (skc71))
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) (skc20)))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X11) zenon_X11)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X0))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X159))
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X11 (skc63) zenon_X764))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X97) zenon_X97)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X155))
% 1.01/1.23  (-. (old (skc19) zenon_X511))
% 1.01/1.23  (cheap (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.01/1.23  (young (skc19) (skf21 zenon_X16 (skc19) zenon_X885))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X108) != zenon_X158)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X153) zenon_X153)
% 1.01/1.23  ((skf21 zenon_X537 (skc19) zenon_X921) != zenon_X154)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X161))
% 1.01/1.23  (zenon_X9 != zenon_X153)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) (skc20)) (skc20))
% 1.01/1.23  (zenon_X9 != zenon_X0)
% 1.01/1.23  (zenon_X791 != (skc63))
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X97 (skc63) zenon_X936))
% 1.01/1.23  ((skf21 zenon_X161 (skc63) zenon_X837) != zenon_X152)
% 1.01/1.23  ((skf21 zenon_X659 (skc19) zenon_X898) != zenon_X158)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X16))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X161) != zenon_X160)
% 1.01/1.23  (zenon_X659 != zenon_X9)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X160)
% 1.01/1.23  (two (skc19) (skc22))
% 1.01/1.23  (in (skc19) (skc23) (skc26))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X161) zenon_X161)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X0))
% 1.01/1.23  ((skf11 (skc63) zenon_X97) != zenon_X160)
% 1.01/1.23  (member zenon_X198 (skf11 zenon_X198 (skc64)) (skc64))
% 1.01/1.23  (zenon_X16 != zenon_X11)
% 1.01/1.23  (zenon_X97 != zenon_X537)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X97) zenon_X97)
% 1.01/1.23  (member zenon_X948 (skf11 zenon_X948 zenon_X97) zenon_X97)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X9))
% 1.01/1.23  (-. (old (skc19) zenon_X519))
% 1.01/1.23  ((skf23 (skc19) zenon_X153) != zenon_X158)
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X9))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X153) != zenon_X154)
% 1.01/1.23  ((skf21 zenon_X108 (skc19) zenon_X817) != zenon_X154)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X155))
% 1.01/1.23  ((skf21 zenon_X9 (skc63) zenon_X890) != zenon_X152)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X153) zenon_X153)
% 1.01/1.23  ((skf23 (skc63) zenon_X155) != zenon_X152)
% 1.01/1.23  (young (skc63) (skf11 (skc63) (skc20)))
% 1.01/1.23  (city (skc63) (skc69))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X714))
% 1.01/1.23  (young (skc63) (skf21 zenon_X108 (skc63) zenon_X818))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X108) zenon_X108)
% 1.01/1.23  (member zenon_X896 (skf21 zenon_X659 zenon_X896 zenon_X897) zenon_X659)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X659))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X11) != zenon_X158)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X97))
% 1.01/1.23  ((skc68) != zenon_X710)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X0))
% 1.01/1.23  (zenon_X97 != zenon_X153)
% 1.01/1.23  ((skf11 (skc19) (skc20)) != (skf11 zenon_X24 zenon_X25))
% 1.01/1.23  (zenon_X950 != (skc63))
% 1.01/1.23  (coat (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.01/1.23  (zenon_X108 != zenon_X153)
% 1.01/1.23  (group (skc63) (skc64))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X698))
% 1.01/1.23  (member zenon_X827 (skf19 zenon_X15 zenon_X827 zenon_X11) zenon_X11)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X155))
% 1.01/1.23  (member zenon_X802 (skf11 zenon_X802 zenon_X11) zenon_X11)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X159) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X2)
% 1.01/1.23  ((skf23 (skc19) zenon_X537) != zenon_X154)
% 1.01/1.23  (barrel (skc19) (skc23))
% 1.01/1.23  (member zenon_X922 (skf16 zenon_X8 zenon_X922 zenon_X537) zenon_X537)
% 1.01/1.23  (member (skc63) (skf23 (skc63) (skc64)) (skc64))
% 1.01/1.23  (black (skc63) (skf11 (skc63) (skc64)))
% 1.01/1.23  ((skf23 (skc19) zenon_X0) != zenon_X158)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X153 (skc63) zenon_X798))
% 1.01/1.23  (zenon_X888 != (skc19))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X721))
% 1.01/1.23  (black (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.01/1.23  ((skf23 (skc19) zenon_X108) != zenon_X154)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X537))
% 1.01/1.23  ((skc27) != zenon_X511)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X159))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X97))
% 1.01/1.23  (cheap (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.01/1.23  ((skf23 (skc63) (skc20)) != zenon_X160)
% 1.01/1.23  ((skc69) != zenon_X743)
% 1.01/1.23  ((skf23 (skc63) (skc64)) != zenon_X160)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X659))
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) (skc20)) (skc20))
% 1.01/1.23  (zenon_X213 != (skc19))
% 1.01/1.23  (zenon_X922 != (skc63))
% 1.01/1.23  (young (skc63) (skf21 zenon_X659 (skc63) zenon_X949))
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X11) zenon_X11)
% 1.01/1.23  (zenon_X0 != zenon_X155)
% 1.01/1.23  ((skf23 (skc63) zenon_X9) != zenon_X160)
% 1.01/1.23  (zenon_X896 != (skc63))
% 1.01/1.23  (zenon_X659 != zenon_X161)
% 1.01/1.23  (zenon_X166 != (skc63))
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X11))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X159) zenon_X159)
% 1.01/1.23  (zenon_X790 != (skc63))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X0))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X16 (skc19) zenon_X885))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X0) != zenon_X160)
% 1.01/1.23  ((skc20) != zenon_X25)
% 1.01/1.23  (ssSkP1 zenon_X78 zenon_X81 zenon_X76)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X155))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X159) zenon_X159)
% 1.01/1.23  ((skc69) != zenon_X746)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc20)) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X11))
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X659))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X161) zenon_X161)
% 1.01/1.23  (agent (skc19) (skc23) (skc27))
% 1.01/1.23  (zenon_X882 != (skc19))
% 1.01/1.23  (member zenon_X960 (skf16 zenon_X8 zenon_X960 zenon_X0) zenon_X0)
% 1.01/1.23  (-. (city (skc63) zenon_X735))
% 1.01/1.23  ((skc64) != zenon_X636)
% 1.01/1.23  (coat (skc63) (skf11 (skc63) (skc64)))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X537))
% 1.01/1.23  (-. (city (skc63) zenon_X745))
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X159) zenon_X159)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X108))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X16) != zenon_X160)
% 1.01/1.23  (zenon_X819 != (skc63))
% 1.01/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X5)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X9) zenon_X9)
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X537))
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X161))
% 1.01/1.23  ((skf11 (skc63) zenon_X159) != zenon_X160)
% 1.01/1.23  (zenon_X13 != (skc19))
% 1.01/1.23  ((skf11 (skc63) zenon_X0) != zenon_X160)
% 1.01/1.23  (dirty (skc63) (skc70))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X9) != zenon_X154)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X11) != zenon_X160)
% 1.01/1.23  (old (skc63) (skc70))
% 1.01/1.23  (zenon_X777 != (skc63))
% 1.01/1.23  ((skf23 (skc63) zenon_X161) != zenon_X152)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X108))
% 1.01/1.23  (member zenon_X835 (skf21 zenon_X161 zenon_X835 zenon_X836) zenon_X161)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X155) zenon_X155)
% 1.01/1.23  ((skf23 (skc19) (skc20)) != zenon_X6)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X9))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X97) != zenon_X154)
% 1.01/1.23  ((skf11 (skc63) (skc20)) != zenon_X152)
% 1.01/1.23  ((skf11 (skc63) zenon_X11) != zenon_X152)
% 1.01/1.23  ((skc69) != zenon_X744)
% 1.01/1.23  (black (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.01/1.23  (zenon_X918 != (skc19))
% 1.01/1.23  (lonely (skc19) (skc24))
% 1.01/1.23  ((skc71) != zenon_X688)
% 1.01/1.23  (zenon_X198 != (skc63))
% 1.01/1.23  ((skf23 (skc19) zenon_X159) != zenon_X154)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X97) zenon_X97)
% 1.01/1.23  ((skf11 (skc63) zenon_X659) != zenon_X152)
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X159))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) (skc64)))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X732))
% 1.01/1.23  ((skc69) != zenon_X741)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X108) != zenon_X154)
% 1.01/1.23  (young (skc19) (skf21 zenon_X9 (skc19) zenon_X891))
% 1.01/1.23  (zenon_X932 != (skc63))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X108))
% 1.01/1.23  ((skc20) != zenon_X153)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X153) != zenon_X160)
% 1.01/1.23  ((skf11 (skc63) zenon_X155) != zenon_X152)
% 1.01/1.23  (fellow (skc63) (skf21 (skc20) (skc63) zenon_X237))
% 1.01/1.23  (event zenon_X63 (skf17 zenon_X63 zenon_X69 zenon_X67))
% 1.01/1.23  (-. (member (skc63) zenon_X160 (skc20)))
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X108) zenon_X108)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X0) != zenon_X154)
% 1.01/1.23  ((skf21 zenon_X537 (skc19) zenon_X921) != zenon_X158)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X4)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) (skc64)))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X16) zenon_X16)
% 1.01/1.23  (zenon_X960 != (skc63))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X9 (skc19) zenon_X891))
% 1.01/1.23  ((skf21 zenon_X159 (skc63) zenon_X797) != zenon_X160)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X155))
% 1.01/1.23  (member (skc19) (skf21 zenon_X659 (skc19) zenon_X898) zenon_X659)
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X153) zenon_X153)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X159))
% 1.01/1.23  ((skf21 zenon_X16 (skc63) zenon_X884) != zenon_X152)
% 1.01/1.23  (-. (city (skc63) zenon_X731))
% 1.01/1.23  (-. (ssSkC0))
% 1.01/1.23  (zenon_X790 != (skc19))
% 1.01/1.23  (member zenon_X813 (skf16 zenon_X8 zenon_X813 zenon_X159) zenon_X159)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X97) != zenon_X158)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X108))
% 1.01/1.23  (dirty (skc19) (skc27))
% 1.01/1.23  ((skf11 (skc19) (skc20)) != zenon_X7)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X537) zenon_X537)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X97) != zenon_X158)
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X161) zenon_X161)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X155) != zenon_X158)
% 1.01/1.23  ((skc68) != zenon_X698)
% 1.01/1.23  (young (skc19) (skf21 (skc20) (skc19) zenon_X235))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X9))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X11) zenon_X11)
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X155 (skc19) zenon_X783))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X97) != zenon_X152)
% 1.01/1.23  (zenon_X11 != zenon_X153)
% 1.01/1.23  (-. (group (skc63) zenon_X691))
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X159))
% 1.01/1.23  ((skf21 (skc64) (skc19) zenon_X201) != zenon_X158)
% 1.01/1.23  (member zenon_X795 (skf21 zenon_X153 zenon_X795 zenon_X796) zenon_X153)
% 1.01/1.23  ((skf23 (skc19) zenon_X153) != zenon_X154)
% 1.01/1.23  ((skc69) != zenon_X747)
% 1.01/1.23  ((skf21 zenon_X0 (skc19) zenon_X812) != zenon_X154)
% 1.01/1.23  ((skc64) != zenon_X599)
% 1.01/1.23  ((skc65) != zenon_X691)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X603))
% 1.01/1.23  ((skc19) != zenon_X18)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X652))
% 1.01/1.23  ((skf11 (skc63) zenon_X9) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X659))
% 1.01/1.23  ((skf23 (skc63) zenon_X108) != zenon_X152)
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X161))
% 1.01/1.23  (agent (skc63) (skc66) (skc70))
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X3)
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X9) zenon_X9)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X108))
% 1.01/1.23  ((skc65) != zenon_X682)
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X537) zenon_X537)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X537))
% 1.01/1.23  ((skf11 (skc63) (skc20)) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf11 (skc63) (skc64)))
% 1.01/1.23  (zenon_X159 != zenon_X537)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X537) zenon_X537)
% 1.01/1.23  (zenon_X16 != (skc20))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X153))
% 1.01/1.23  ((skf21 zenon_X537 (skc63) zenon_X920) != zenon_X152)
% 1.01/1.23  ((skc64) != zenon_X153)
% 1.01/1.23  (zenon_X97 != zenon_X155)
% 1.01/1.23  (-. (group (skc63) zenon_X679))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X153) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X108) != zenon_X158)
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X97))
% 1.01/1.23  (of (skc63) (skc68) (skc69))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X159) != zenon_X152)
% 1.01/1.23  (zenon_X844 != (skc63))
% 1.01/1.23  ((skf23 (skc19) (skc20)) != zenon_X154)
% 1.01/1.23  (-. (city (skc63) zenon_X720))
% 1.01/1.23  (member (skc19) (skf21 zenon_X537 (skc19) zenon_X921) zenon_X537)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X9 (skc63) zenon_X890))
% 1.01/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X648)))
% 1.01/1.23  (zenon_X827 != (skc63))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X537))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X0) != zenon_X154)
% 1.01/1.23  (zenon_X772 != (skc19))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X659) != zenon_X158)
% 1.01/1.23  ((skc63) != zenon_X18)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X161))
% 1.01/1.23  (-. (old (skc63) zenon_X495))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X16))
% 1.01/1.23  (zenon_X169 != (skc63))
% 1.01/1.23  (zenon_X1 != (skc63))
% 1.01/1.23  ((skc71) != zenon_X583)
% 1.01/1.23  (zenon_X835 != (skc63))
% 1.01/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.01/1.23  (zenon_X793 != (skc19))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc20)) != zenon_X152)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X161 (skc63) zenon_X837))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X537) != zenon_X158)
% 1.01/1.23  ((skc68) != zenon_X708)
% 1.01/1.23  ((skc68) != zenon_X712)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X155))
% 1.01/1.23  (zenon_X10 != (skc19))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) (skc64)) (skc64))
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X16) zenon_X16)
% 1.01/1.23  ((skf11 (skc19) zenon_X153) != zenon_X154)
% 1.01/1.23  ((skf23 (skc19) zenon_X161) != zenon_X154)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X16))
% 1.01/1.23  (zenon_X9 != zenon_X108)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X159))
% 1.01/1.23  (zenon_X852 != (skc63))
% 1.01/1.23  (group (skc19) (skc21))
% 1.01/1.23  (-. (frontseat (skc63) (skc69)))
% 1.01/1.23  (zenon_X866 != (skc19))
% 1.01/1.23  (state zenon_X27 (skf13 zenon_X27 zenon_X31 zenon_X32))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X161 (skc19) zenon_X845))
% 1.01/1.23  ((skf21 zenon_X108 (skc19) zenon_X817) != zenon_X158)
% 1.01/1.23  ((skc66) != zenon_X576)
% 1.01/1.23  (frontseat (skc63) (skc72))
% 1.01/1.23  (zenon_X97 != zenon_X11)
% 1.01/1.23  (member zenon_X844 (skf19 zenon_X15 zenon_X844 zenon_X659) zenon_X659)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc64)) != zenon_X154)
% 1.01/1.23  (young (skc63) (skf21 zenon_X0 (skc63) zenon_X811))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X11))
% 1.01/1.23  (zenon_X172 != (skc63))
% 1.01/1.23  (-. (member (skc19) zenon_X158 (skc20)))
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X97) zenon_X97)
% 1.01/1.23  (member (skc19) (skf21 zenon_X159 (skc19) zenon_X774) zenon_X159)
% 1.01/1.23  ((skc64) != zenon_X676)
% 1.01/1.23  (ssSkP0 zenon_X363 (skc19))
% 1.01/1.23  (wear zenon_X42 (skf17 zenon_X42 zenon_X48 zenon_X46))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X155))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X159))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X16))
% 1.01/1.23  (zenon_X164 != (skc63))
% 1.01/1.23  (young (skc19) (skf21 zenon_X537 (skc19) zenon_X921))
% 1.01/1.23  (member zenon_X941 (skf19 zenon_X15 zenon_X941 zenon_X97) zenon_X97)
% 1.01/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.01/1.23  (city (skc19) (skc26))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X161))
% 1.01/1.23  (young (skc19) (skf11 (skc19) (skc20)))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.01/1.23  (zenon_X795 != (skc19))
% 1.01/1.23  (-. (two zenon_X112 zenon_X111))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X726))
% 1.01/1.23  ((skc20) != zenon_X594)
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X159) zenon_X159)
% 1.01/1.23  (in (skc63) (skc66) (skc69))
% 1.01/1.23  (-. (city (skc63) zenon_X736))
% 1.01/1.23  (zenon_X10 != (skc63))
% 1.01/1.23  ((skf11 (skc63) zenon_X537) != zenon_X152)
% 1.01/1.23  (zenon_X9 != zenon_X16)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) (skc64)) (skc64))
% 1.01/1.23  ((skf11 (skc19) (skc20)) != (skf11 zenon_X24 (skc20)))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 (skc20)) (skc20))
% 1.01/1.23  (zenon_X11 != (skc64))
% 1.01/1.23  (actual_world (skc63))
% 1.01/1.23  ((skf23 (skc19) zenon_X108) != zenon_X158)
% 1.01/1.23  (young (skc19) (skf21 zenon_X153 (skc19) zenon_X853))
% 1.01/1.23  (zenon_X960 != (skc19))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X0))
% 1.01/1.23  (member (skc63) (skf21 zenon_X9 (skc63) zenon_X890) zenon_X9)
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X659))
% 1.01/1.23  (zenon_X93 != (skc63))
% 1.01/1.23  (member (skc63) (skf11 (skc63) (skc64)) (skc64))
% 1.01/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X621)))
% 1.01/1.23  (member zenon_X792 (skf11 zenon_X792 zenon_X161) zenon_X161)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X161))
% 1.01/1.23  (zenon_X159 != zenon_X153)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X537) != zenon_X160)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X159))
% 1.01/1.23  (zenon_X0 != zenon_X161)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) (skc64)))
% 1.01/1.23  (young (skc63) (skf21 zenon_X9 (skc63) zenon_X890))
% 1.01/1.23  (zenon_X819 != (skc19))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X0))
% 1.01/1.23  ((skf23 (skc63) zenon_X159) != zenon_X152)
% 1.01/1.23  (-. (ssSkP0 zenon_X20 zenon_X18))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc64)) != zenon_X158)
% 1.01/1.23  ((skf11 (skc19) zenon_X153) != zenon_X158)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X97) != zenon_X160)
% 1.01/1.23  (member (skc19) (skf11 (skc19) (skc64)) (skc64))
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X659))
% 1.01/1.23  ((skf23 (skc19) zenon_X9) != zenon_X154)
% 1.01/1.23  ((skf23 (skc63) zenon_X16) != zenon_X160)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X0 (skc63) zenon_X811))
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X153))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X153))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X108))
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X537))
% 1.01/1.23  ((skf21 zenon_X159 (skc19) zenon_X774) != zenon_X154)
% 1.01/1.23  (-. (city (skc63) zenon_X743))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X16) != zenon_X158)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X11))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X11) != zenon_X160)
% 1.01/1.23  ((skf11 (skc19) zenon_X11) != zenon_X154)
% 1.01/1.23  ((skc69) != zenon_X738)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X97))
% 1.01/1.23  (hollywood_placename (skc63) (skc68))
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X153))
% 1.01/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X636)))
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X16))
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X599))
% 1.01/1.23  (-. (barrel (skc19) zenon_X527))
% 1.01/1.23  (agent zenon_X70 (skf17 zenon_X70 zenon_X71 zenon_X75) zenon_X71)
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X0))
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X155) zenon_X155)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X153))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X659))
% 1.01/1.23  ((skf11 (skc63) (skc20)) != (skf11 zenon_X24 (skc20)))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) (skc64)))
% 1.01/1.23  (group (skc19) (skc20))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X97) zenon_X97)
% 1.01/1.23  (member zenon_X17 (skf19 zenon_X15 zenon_X17 zenon_X16) zenon_X16)
% 1.01/1.23  (zenon_X770 != (skc19))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X16) != zenon_X158)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X159) zenon_X159)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X537))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X108))
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X97) zenon_X97)
% 1.01/1.23  (zenon_X97 != zenon_X161)
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X0))
% 1.01/1.23  (chevy (skc63) (skc70))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X159) zenon_X159)
% 1.01/1.23  (member zenon_X769 (skf16 zenon_X8 zenon_X769 zenon_X155) zenon_X155)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X153) != zenon_X158)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X155))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X155))
% 1.01/1.23  (member (skc63) (skf21 zenon_X155 (skc63) zenon_X913) zenon_X155)
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X159 (skc63) zenon_X797))
% 1.01/1.23  (zenon_X659 != (skc64))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X9) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X11) != zenon_X154)
% 1.01/1.23  ((skf21 zenon_X97 (skc63) zenon_X936) != zenon_X152)
% 1.01/1.23  (in zenon_X33 (skf12 zenon_X34 zenon_X33 zenon_X36) zenon_X36)
% 1.01/1.23  ((skf11 (skc19) zenon_X159) != zenon_X154)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X11))
% 1.01/1.23  (zenon_X789 != (skc63))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X0) != zenon_X152)
% 1.01/1.23  ((skc68) != zenon_X732)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X154)
% 1.01/1.23  ((skf23 (skc19) zenon_X16) != zenon_X158)
% 1.01/1.23  (member zenon_X772 (skf21 zenon_X159 zenon_X772 zenon_X773) zenon_X159)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) (skc20)))
% 1.01/1.23  (member (skc19) (skf21 (skc64) (skc19) zenon_X201) (skc64))
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X108))
% 1.01/1.23  (ssSkP0 zenon_X753 (skc63))
% 1.01/1.23  (zenon_X155 != zenon_X153)
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X155) zenon_X155)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X159))
% 1.01/1.23  (ssSkP2 (skc65) (skc64) (skc63))
% 1.01/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.01/1.23  ((skc68) != zenon_X700)
% 1.01/1.23  ((skf21 zenon_X659 (skc63) zenon_X949) != zenon_X152)
% 1.01/1.23  (fellow (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.01/1.23  (zenon_X784 != (skc19))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X0) != zenon_X158)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.01/1.23  ((skf11 (skc63) zenon_X537) != zenon_X160)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X155))
% 1.01/1.23  ((skf21 zenon_X16 (skc19) zenon_X885) != zenon_X154)
% 1.01/1.23  (member zenon_X179 (skf16 zenon_X8 zenon_X179 (skc20)) (skc20))
% 1.01/1.23  (ssSkP1 (skc72) (skc71) (skc63))
% 1.01/1.23  (zenon_X785 != (skc63))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X16))
% 1.01/1.23  (zenon_X789 != (skc19))
% 1.01/1.23  (zenon_X886 != (skc63))
% 1.01/1.23  (-. (street (skc19) zenon_X557))
% 1.01/1.23  ((skf11 (skc63) zenon_X159) != zenon_X152)
% 1.01/1.23  (zenon_X198 != (skc19))
% 1.01/1.23  ((skf11 (skc63) zenon_X155) != zenon_X160)
% 1.01/1.23  (zenon_X896 != (skc19))
% 1.01/1.23  (zenon_X11 != zenon_X155)
% 1.01/1.23  (zenon_X948 != (skc63))
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X161))
% 1.01/1.23  (member (skc19) (skf21 zenon_X9 (skc19) zenon_X891) zenon_X9)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X632))
% 1.01/1.23  ((skf11 (skc63) zenon_X153) != zenon_X160)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X659) zenon_X659)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X659) != zenon_X152)
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X153 (skc19) zenon_X853))
% 1.01/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X108) != zenon_X152)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X97) != zenon_X154)
% 1.01/1.23  (zenon_X659 != zenon_X159)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X0))
% 1.01/1.23  ((skf11 (skc19) (skc20)) != zenon_X158)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X16))
% 1.01/1.23  (member zenon_X762 (skf11 zenon_X762 zenon_X155) zenon_X155)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X16))
% 1.01/1.23  (zenon_X108 != zenon_X161)
% 1.01/1.23  (zenon_X172 != (skc19))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X9) zenon_X9)
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X16))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) (skc20)) (skc20))
% 1.01/1.23  (zenon_X839 != (skc19))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X9))
% 1.01/1.23  ((skc64) != zenon_X679)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X159) zenon_X159)
% 1.01/1.23  (-. (fellow zenon_X24 (skf11 zenon_X24 (skc20))))
% 1.01/1.23  ((skc69) != zenon_X734)
% 1.01/1.23  ((skf21 zenon_X161 (skc19) zenon_X845) != zenon_X154)
% 1.01/1.23  ((skc64) != zenon_X691)
% 1.01/1.23  (member zenon_X789 (skf16 zenon_X8 zenon_X789 zenon_X153) zenon_X153)
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X2)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X9))
% 1.01/1.23  (zenon_X169 != (skc19))
% 1.01/1.23  (young (skc19) (skf23 (skc19) (skc20)))
% 1.01/1.23  (zenon_X537 != (skc64))
% 1.01/1.23  ((skc63) != zenon_X477)
% 1.01/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X663)))
% 1.01/1.23  ((skf21 zenon_X9 (skc19) zenon_X891) != zenon_X158)
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X11))
% 1.01/1.23  ((skf11 (skc19) zenon_X155) != zenon_X154)
% 1.01/1.23  ((skf23 (skc19) zenon_X97) != zenon_X158)
% 1.01/1.23  (member zenon_X213 (skf11 zenon_X213 (skc20)) (skc20))
% 1.01/1.23  (member zenon_X13 (skf21 zenon_X11 zenon_X13 zenon_X14) zenon_X11)
% 1.01/1.23  ((skf23 (skc19) (skc20)) != zenon_X7)
% 1.01/1.23  ((skc68) != zenon_X702)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X16))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X159) zenon_X159)
% 1.01/1.23  (zenon_X918 != (skc63))
% 1.01/1.23  (zenon_X9 != zenon_X159)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X659) zenon_X659)
% 1.01/1.23  (-. (barrel (skc19) zenon_X541))
% 1.01/1.23  ((skc67) != zenon_X570)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X159))
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X11) zenon_X11)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X11))
% 1.01/1.23  (street (skc19) (skc24))
% 1.01/1.23  ((skf23 (skc19) (skc20)) != zenon_X5)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X11))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X9))
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X16))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X716))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X153) zenon_X153)
% 1.01/1.23  ((skc64) != zenon_X632)
% 1.01/1.23  ((skc64) != zenon_X685)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) (skc20)))
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X153))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X108))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X159) != zenon_X154)
% 1.01/1.23  (-. (member (skc63) zenon_X4 (skc64)))
% 1.01/1.23  (zenon_X108 != zenon_X159)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X108) zenon_X108)
% 1.01/1.23  (cheap (skc63) (skf11 (skc63) (skc64)))
% 1.01/1.23  (-. (group (skc63) zenon_X676))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X108) zenon_X108)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X11) zenon_X11)
% 1.01/1.23  (member (skc63) (skf21 zenon_X537 (skc63) zenon_X920) zenon_X537)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X108))
% 1.01/1.23  (member zenon_X868 (skf11 zenon_X868 zenon_X9) zenon_X9)
% 1.01/1.23  (zenon_X108 != zenon_X155)
% 1.01/1.23  ((skf21 zenon_X16 (skc19) zenon_X885) != zenon_X158)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X537))
% 1.01/1.23  (zenon_X537 != zenon_X153)
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X97 (skc19) zenon_X937))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X702))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X537 (skc19) zenon_X921))
% 1.01/1.23  ((skf23 (skc19) zenon_X11) != zenon_X158)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X161))
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X659))
% 1.01/1.23  ((skf23 (skc63) zenon_X161) != zenon_X160)
% 1.01/1.23  (member (skc63) (skf21 zenon_X161 (skc63) zenon_X837) zenon_X161)
% 1.01/1.23  (zenon_X16 != (skc64))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X9))
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X153))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) (skc20)))
% 1.01/1.23  (zenon_X772 != (skc63))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X155) != zenon_X160)
% 1.01/1.23  (zenon_X867 != (skc63))
% 1.01/1.23  (zenon_X922 != (skc19))
% 1.01/1.23  ((skf11 (skc63) zenon_X9) != zenon_X152)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X659) != zenon_X158)
% 1.01/1.23  (placename (skc19) (skc25))
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) (skc20)))
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X0) zenon_X0)
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X659))
% 1.01/1.23  (fellow (skc63) (skf21 zenon_X16 (skc63) zenon_X884))
% 1.01/1.23  (two (skc63) (skc71))
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X161))
% 1.01/1.23  (-. (city (skc63) zenon_X728))
% 1.01/1.23  (young (skc63) (skf21 zenon_X159 (skc63) zenon_X797))
% 1.01/1.23  (zenon_X97 != zenon_X159)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X153))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X537))
% 1.01/1.23  (member zenon_X164 (skf16 zenon_X8 zenon_X164 (skc64)) (skc64))
% 1.01/1.23  (-. (actual_world zenon_X477))
% 1.01/1.23  (zenon_X809 != (skc19))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X659) zenon_X659)
% 1.01/1.23  (young (skc19) (skf21 zenon_X659 (skc19) zenon_X898))
% 1.01/1.23  (-. (city (skc63) zenon_X723))
% 1.01/1.23  (member zenon_X770 (skf19 zenon_X15 zenon_X770 zenon_X159) zenon_X159)
% 1.01/1.23  (member (skc63) (skf21 zenon_X159 (skc63) zenon_X797) zenon_X159)
% 1.01/1.23  (zenon_X765 != (skc63))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X11) != zenon_X158)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X9))
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X161))
% 1.01/1.23  (zenon_X9 != (skc20))
% 1.01/1.23  ((skf21 zenon_X97 (skc63) zenon_X936) != zenon_X160)
% 1.01/1.23  ((skc64) != zenon_X682)
% 1.01/1.23  (zenon_X839 != (skc63))
% 1.01/1.23  (-. (street (skc63) zenon_X570))
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X11) zenon_X11)
% 1.01/1.23  (young (skc19) (skf21 zenon_X97 (skc19) zenon_X937))
% 1.01/1.23  (zenon_X941 != (skc63))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X3)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X158)
% 1.01/1.23  ((skc22) != zenon_X611)
% 1.01/1.23  ((skf11 (skc19) zenon_X659) != zenon_X154)
% 1.01/1.23  ((skf21 (skc20) (skc63) zenon_X237) != zenon_X152)
% 1.01/1.23  ((skc71) != zenon_X616)
% 1.01/1.23  (zenon_X11 != zenon_X0)
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X159))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X0))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X9))
% 1.01/1.23  ((skf11 (skc19) zenon_X659) != zenon_X158)
% 1.01/1.23  (placename (skc63) (skc68))
% 1.01/1.23  ((skc68) != zenon_X721)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X16) != zenon_X152)
% 1.01/1.23  (member zenon_X169 (skf21 (skc64) zenon_X169 zenon_X170) (skc64))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X11))
% 1.01/1.23  (zenon_X659 != zenon_X16)
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X97))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X159))
% 1.01/1.23  (young (skc63) (skf21 zenon_X11 (skc63) zenon_X764))
% 1.01/1.23  ((skc69) != zenon_X739)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X537))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X108) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf21 zenon_X155 (skc63) zenon_X913))
% 1.01/1.23  (zenon_X16 != zenon_X159)
% 1.01/1.23  ((skc68) != zenon_X726)
% 1.01/1.23  (zenon_X770 != (skc63))
% 1.01/1.23  (zenon_X659 != zenon_X155)
% 1.01/1.23  ((skf21 zenon_X155 (skc63) zenon_X913) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X11) != zenon_X152)
% 1.01/1.23  (present zenon_X56 (skf17 zenon_X56 zenon_X62 zenon_X60))
% 1.01/1.23  ((skc69) != zenon_X728)
% 1.01/1.23  (zenon_X16 != zenon_X108)
% 1.01/1.23  (-. (member (skc63) zenon_X152 (skc20)))
% 1.01/1.23  ((skc27) != zenon_X519)
% 1.01/1.23  (-. (member (skc63) zenon_X160 (skc64)))
% 1.01/1.23  ((skf11 (skc63) zenon_X108) != zenon_X152)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X537) != zenon_X154)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X9) != zenon_X154)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X0))
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X0))
% 1.01/1.23  (member (skc19) (skf21 zenon_X97 (skc19) zenon_X937) zenon_X97)
% 1.01/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X603)))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X152)
% 1.01/1.23  (member (skc19) (skf21 (skc20) (skc19) zenon_X235) (skc20))
% 1.01/1.23  (zenon_X93 != (skc19))
% 1.01/1.23  ((skc23) != zenon_X527)
% 1.01/1.23  (zenon_X11 != zenon_X159)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X11) zenon_X11)
% 1.01/1.23  (young (skc19) (skf21 zenon_X159 (skc19) zenon_X774))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X0))
% 1.01/1.23  (zenon_X765 != (skc19))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X659) != zenon_X154)
% 1.01/1.23  (member zenon_X815 (skf21 zenon_X108 zenon_X815 zenon_X816) zenon_X108)
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X97))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X11))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.01/1.23  (member zenon_X809 (skf21 zenon_X0 zenon_X809 zenon_X810) zenon_X0)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X16))
% 1.01/1.23  ((skf23 (skc63) (skc64)) != zenon_X3)
% 1.01/1.23  (zenon_X166 != (skc19))
% 1.01/1.23  ((skf11 (skc63) zenon_X0) != zenon_X152)
% 1.01/1.23  (young (skc19) (skf23 (skc19) (skc64)))
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X636))
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) (skc64)))
% 1.01/1.23  (young (skc63) (skf21 zenon_X161 (skc63) zenon_X837))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X158)
% 1.01/1.23  (-. (city (skc63) zenon_X747))
% 1.01/1.23  (member zenon_X791 (skf11 zenon_X791 zenon_X108) zenon_X108)
% 1.01/1.23  (be zenon_X37 (skf13 zenon_X37 zenon_X41 zenon_X38) zenon_X38 (skf12 zenon_X38 zenon_X37 zenon_X41))
% 1.01/1.23  ((skc68) != zenon_X706)
% 1.01/1.23  (zenon_X97 != zenon_X0)
% 1.01/1.23  (old (skc19) (skc27))
% 1.01/1.23  (young (skc19) (skf21 zenon_X155 (skc19) zenon_X783))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X696))
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X659))
% 1.01/1.23  (zenon_X11 != (skc20))
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X161) zenon_X161)
% 1.01/1.23  (member zenon_X763 (skf11 zenon_X763 zenon_X159) zenon_X159)
% 1.01/1.23  ((skf23 (skc63) (skc64)) != zenon_X152)
% 1.01/1.23  (zenon_X164 != (skc19))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X16))
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X97))
% 1.01/1.23  (zenon_X840 != (skc19))
% 1.01/1.23  ((skf23 (skc63) zenon_X159) != zenon_X160)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X9) zenon_X9)
% 1.01/1.23  (member (skc63) (skf21 zenon_X16 (skc63) zenon_X884) zenon_X16)
% 1.01/1.23  ((skf23 (skc19) zenon_X659) != zenon_X158)
% 1.01/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X607)))
% 1.01/1.23  (zenon_X934 != (skc19))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X16) != zenon_X154)
% 1.01/1.23  ((skf23 (skc19) zenon_X537) != zenon_X158)
% 1.01/1.23  (-. (fellow zenon_X24 (skf11 zenon_X24 zenon_X25)))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.01/1.23  (member (skc19) (skf23 (skc19) (skc20)) (skc20))
% 1.01/1.23  (member zenon_X923 (skf19 zenon_X15 zenon_X923 zenon_X9) zenon_X9)
% 1.01/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X7)
% 1.01/1.23  ((skc63) != (skc19))
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X659) zenon_X659)
% 1.01/1.23  (zenon_X923 != (skc19))
% 1.01/1.23  ((skc19) != zenon_X21)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X4)
% 1.01/1.23  ((skc64) != (skc20))
% 1.01/1.23  (member (skc63) (skf11 (skc63) (skc20)) (skc20))
% 1.01/1.23  (young (skc63) (skf23 (skc63) zenon_X0))
% 1.01/1.23  ((skf23 (skc19) zenon_X161) != zenon_X158)
% 1.01/1.23  (zenon_X948 != (skc19))
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X537))
% 1.01/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X154)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X659))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X97))
% 1.01/1.23  ((skf21 zenon_X153 (skc19) zenon_X853) != zenon_X158)
% 1.01/1.23  (black (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.01/1.23  ((skf11 (skc63) zenon_X97) != zenon_X152)
% 1.01/1.23  ((skc64) != zenon_X616)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X152)
% 1.01/1.23  ((skf23 (skc19) (skc64)) != zenon_X158)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X159))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X11))
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X9) zenon_X9)
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X108))
% 1.01/1.23  (-. (group (skc63) zenon_X685))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X11))
% 1.01/1.23  ((skc68) != zenon_X716)
% 1.01/1.23  ((skc68) != zenon_X696)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X9) != zenon_X152)
% 1.01/1.23  ((skc69) != zenon_X731)
% 1.01/1.23  (member (skc19) (skf21 zenon_X155 (skc19) zenon_X783) zenon_X155)
% 1.01/1.23  ((skc65) != zenon_X583)
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X153) zenon_X153)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X537) zenon_X537)
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X659))
% 1.01/1.23  (-. (street (skc63) zenon_X588))
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X16))
% 1.01/1.23  ((skf21 zenon_X537 (skc63) zenon_X920) != zenon_X160)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X0) zenon_X0)
% 1.01/1.23  (-. (actual_world zenon_X486))
% 1.01/1.23  ((skc65) != zenon_X679)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X537) zenon_X537)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X161))
% 1.01/1.23  ((skf11 (skc63) zenon_X16) != zenon_X160)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X161))
% 1.01/1.23  ((skf23 (skc63) zenon_X0) != zenon_X160)
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X537))
% 1.01/1.23  (young (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.01/1.23  (present (skc63) (skc66))
% 1.01/1.23  (ssSkP2 (skc21) (skc20) (skc19))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X108))
% 1.01/1.23  (young (skc63) (skf21 zenon_X537 (skc63) zenon_X920))
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X97))
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X2)
% 1.01/1.23  (zenon_X795 != (skc63))
% 1.01/1.23  ((skf11 (skc19) zenon_X108) != zenon_X154)
% 1.01/1.23  ((skf21 zenon_X159 (skc63) zenon_X797) != zenon_X152)
% 1.01/1.23  ((skf23 (skc63) zenon_X11) != zenon_X152)
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X159 (skc19) zenon_X774))
% 1.01/1.23  (zenon_X213 != (skc63))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X155))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X155) zenon_X155)
% 1.01/1.23  (zenon_X0 != zenon_X159)
% 1.01/1.23  ((skf11 (skc63) (skc64)) != zenon_X160)
% 1.01/1.23  (zenon_X16 != zenon_X0)
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X159))
% 1.01/1.23  (zenon_X179 != (skc19))
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X9) zenon_X9)
% 1.01/1.23  ((skf23 (skc63) zenon_X97) != zenon_X160)
% 1.01/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X640)))
% 1.01/1.23  (-. (member (skc63) zenon_X152 (skc64)))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X537))
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X659) zenon_X659)
% 1.01/1.23  ((skc19) != zenon_X477)
% 1.01/1.23  ((skf11 (skc63) (skc64)) != zenon_X4)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X155))
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X97))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X97))
% 1.01/1.23  ((skc72) != (skc69))
% 1.01/1.23  ((skf23 (skc63) (skc20)) != zenon_X152)
% 1.01/1.23  ((skc65) != zenon_X676)
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X155) zenon_X155)
% 1.01/1.23  (zenon_X793 != (skc63))
% 1.01/1.23  ((skf23 (skc63) zenon_X97) != zenon_X152)
% 1.01/1.23  (young (skc63) (skf21 zenon_X153 (skc63) zenon_X798))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X153))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X161))
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X16))
% 1.01/1.23  (frontseat (skc19) (skc26))
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) (skc64)))
% 1.01/1.23  (-. (city (skc63) zenon_X744))
% 1.01/1.23  (zenon_X1 != (skc19))
% 1.01/1.23  (-. (group (skc19) zenon_X611))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X161) != zenon_X154)
% 1.01/1.23  (young (skc19) (skf21 zenon_X161 (skc19) zenon_X845))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X16))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X153))
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X537) zenon_X537)
% 1.01/1.23  (young (skc63) (skf23 (skc63) (skc64)))
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X11) zenon_X11)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X161) zenon_X161)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X160)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X659))
% 1.01/1.23  ((skf11 (skc19) (skc20)) != zenon_X6)
% 1.01/1.23  ((skf11 (skc19) zenon_X537) != zenon_X154)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X155) != zenon_X154)
% 1.01/1.23  ((skf21 zenon_X153 (skc63) zenon_X798) != zenon_X160)
% 1.01/1.23  (member zenon_X888 (skf21 zenon_X9 zenon_X888 zenon_X889) zenon_X9)
% 1.01/1.23  (actual_world (skc19))
% 1.01/1.23  ((skc20) != zenon_X159)
% 1.01/1.23  ((skc68) != zenon_X729)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X108) zenon_X108)
% 1.01/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.01/1.23  ((skf21 zenon_X161 (skc19) zenon_X845) != zenon_X158)
% 1.01/1.23  ((skf21 zenon_X0 (skc63) zenon_X811) != zenon_X152)
% 1.01/1.23  (zenon_X950 != (skc19))
% 1.01/1.23  (young (skc63) (skf11 (skc63) zenon_X0))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X153))
% 1.01/1.23  (zenon_X802 != (skc19))
% 1.01/1.23  (zenon_X659 != zenon_X97)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X537) != zenon_X160)
% 1.01/1.23  (zenon_X867 != (skc19))
% 1.01/1.23  (-. (member (skc63) zenon_X160 zenon_X659))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X718))
% 1.01/1.23  (zenon_X13 != (skc63))
% 1.01/1.23  ((skf11 (skc19) zenon_X0) != zenon_X158)
% 1.01/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X632)))
% 1.01/1.23  (zenon_X108 != zenon_X537)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X16))
% 1.01/1.23  ((skf23 (skc63) zenon_X9) != zenon_X152)
% 1.01/1.23  ((skf23 (skc63) zenon_X16) != zenon_X152)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X537) != zenon_X152)
% 1.01/1.23  ((skf23 (skc63) zenon_X11) != zenon_X160)
% 1.01/1.23  ((skc71) != zenon_X682)
% 1.01/1.23  ((skf21 zenon_X16 (skc63) zenon_X884) != zenon_X160)
% 1.01/1.23  (zenon_X785 != (skc19))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X0))
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X97) zenon_X97)
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X11))
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X16) zenon_X16)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X97))
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X155))
% 1.01/1.23  (member zenon_X840 (skf16 zenon_X8 zenon_X840 zenon_X11) zenon_X11)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X159))
% 1.01/1.23  (member zenon_X934 (skf21 zenon_X97 zenon_X934 zenon_X935) zenon_X97)
% 1.01/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.01/1.23  (young (skc63) (skf21 (skc20) (skc63) zenon_X237))
% 1.01/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X158)
% 1.01/1.23  (member zenon_X910 (skf11 zenon_X910 zenon_X537) zenon_X537)
% 1.01/1.23  (-. (city (skc63) zenon_X741))
% 1.01/1.23  (young (skc19) (skf11 (skc19) zenon_X16))
% 1.01/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X537))
% 1.01/1.23  (zenon_X9 != zenon_X537)
% 1.01/1.23  (member zenon_X172 (skf19 zenon_X15 zenon_X172 (skc64)) (skc64))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X537) zenon_X537)
% 1.01/1.23  (young (skc19) (skf23 (skc19) zenon_X108))
% 1.01/1.23  (cheap (skc63) (skf23 (skc63) (skc64)))
% 1.01/1.23  (lonely (skc63) (skc67))
% 1.01/1.23  ((skf21 zenon_X9 (skc63) zenon_X890) != zenon_X160)
% 1.01/1.23  (zenon_X815 != (skc19))
% 1.01/1.23  (zenon_X762 != (skc63))
% 1.01/1.23  ((skf11 (skc63) zenon_X153) != zenon_X152)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X155) zenon_X155)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) zenon_X537) != zenon_X158)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X155))
% 1.01/1.23  (zenon_X155 != zenon_X537)
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) (skc20)))
% 1.01/1.23  (zenon_X11 != zenon_X537)
% 1.01/1.23  (member (skc19) (skf11 (skc19) (skc20)) (skc20))
% 1.01/1.23  (zenon_X101 != (skc19))
% 1.01/1.23  ((skf23 (skc63) (skc64)) != zenon_X4)
% 1.01/1.23  ((skc68) != zenon_X694)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X97))
% 1.01/1.23  (member (skc63) (skf21 (skc64) (skc63) zenon_X236) (skc64))
% 1.01/1.23  (zenon_X840 != (skc63))
% 1.01/1.23  (young (skc63) (skf21 zenon_X16 (skc63) zenon_X884))
% 1.01/1.23  (zenon_X537 != (skc20))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X11 (skc19) zenon_X838))
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X97))
% 1.01/1.23  (young (skc63) (skf16 zenon_X8 (skc63) (skc20)))
% 1.01/1.23  (zenon_X763 != (skc63))
% 1.01/1.23  (group (skc19) (skc22))
% 1.01/1.23  (member (skc63) (skf11 (skc63) zenon_X11) zenon_X11)
% 1.01/1.23  (zenon_X11 != zenon_X108)
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X108))
% 1.01/1.23  ((skc71) != zenon_X676)
% 1.01/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X640))
% 1.01/1.23  ((skc22) != zenon_X111)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X659) zenon_X659)
% 1.01/1.23  (-. (group (skc63) zenon_X682))
% 1.01/1.23  (-. (member (skc19) zenon_X154 zenon_X11))
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X16) zenon_X16)
% 1.01/1.23  ((skf11 (skc19) zenon_X537) != zenon_X158)
% 1.01/1.23  (zenon_X923 != (skc63))
% 1.01/1.23  (ssSkP2 zenon_X89 zenon_X91 zenon_X87)
% 1.01/1.23  ((skc65) != zenon_X688)
% 1.01/1.23  (-. (member (skc19) zenon_X158 zenon_X0))
% 1.01/1.23  (zenon_X97 != zenon_X16)
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X659) zenon_X659)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X5)
% 1.01/1.23  (member (skc63) (skf23 (skc63) zenon_X659) zenon_X659)
% 1.01/1.23  ((skf21 zenon_X155 (skc19) zenon_X783) != zenon_X154)
% 1.01/1.23  ((skc20) != zenon_X161)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X161))
% 1.01/1.23  (-. (member (skc63) zenon_X3 (skc64)))
% 1.01/1.23  (patient zenon_X82 (skf17 zenon_X82 zenon_X83 zenon_X85) zenon_X85)
% 1.01/1.23  (-. (member (skc19) zenon_X158 (skc64)))
% 1.01/1.23  ((skc24) != zenon_X557)
% 1.01/1.23  ((skf11 (skc19) (skc64)) != zenon_X158)
% 1.01/1.23  (zenon_X153 != zenon_X161)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X108) != zenon_X160)
% 1.01/1.23  (zenon_X17 != (skc63))
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X108))
% 1.01/1.23  (young (skc19) (skf21 zenon_X0 (skc19) zenon_X812))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.01/1.23  (fellow (skc19) (skf11 (skc19) zenon_X0))
% 1.01/1.23  (ssSkP1 (skc26) (skc22) (skc19))
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X159) != zenon_X158)
% 1.01/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X644)))
% 1.01/1.23  (-. (group (skc19) zenon_X594))
% 1.01/1.23  (young (skc63) (skf19 zenon_X15 (skc63) (skc20)))
% 1.01/1.23  (member zenon_X932 (skf16 zenon_X8 zenon_X932 zenon_X16) zenon_X16)
% 1.01/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) (skc20)))
% 1.01/1.23  (zenon_X659 != zenon_X0)
% 1.01/1.23  (zenon_X16 != zenon_X153)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X0) != zenon_X160)
% 1.01/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X153))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X16) != zenon_X160)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X153))
% 1.01/1.23  ((skc64) != zenon_X640)
% 1.01/1.23  (zenon_X763 != (skc19))
% 1.01/1.23  (zenon_X9 != (skc64))
% 1.01/1.23  ((skc64) != zenon_X603)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X0) != zenon_X152)
% 1.01/1.23  (member (skc63) (skf23 (skc63) (skc20)) (skc20))
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) (skc20)))
% 1.01/1.23  (zenon_X835 != (skc19))
% 1.01/1.23  ((skf23 (skc19) zenon_X0) != zenon_X154)
% 1.01/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X599)))
% 1.01/1.23  (zenon_X792 != (skc63))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X108 (skc19) zenon_X817))
% 1.01/1.23  ((skc21) != zenon_X594)
% 1.01/1.23  (-. (city (skc63) zenon_X742))
% 1.01/1.23  (-. (hollywood_placename (skc63) zenon_X708))
% 1.01/1.23  ((skf21 zenon_X159 (skc19) zenon_X774) != zenon_X158)
% 1.01/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X9))
% 1.01/1.23  (-. (barrel (skc63) zenon_X563))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X153) != zenon_X160)
% 1.01/1.23  (zenon_X792 != (skc19))
% 1.01/1.23  (zenon_X762 != (skc19))
% 1.01/1.23  (member (skc19) (skf21 zenon_X108 (skc19) zenon_X817) zenon_X108)
% 1.01/1.23  (white (skc19) (skc27))
% 1.01/1.23  ((skf11 (skc19) zenon_X108) != zenon_X158)
% 1.01/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X16) zenon_X16)
% 1.01/1.23  (fellow (skc19) (skf23 (skc19) zenon_X97))
% 1.01/1.23  ((skc63) != zenon_X24)
% 1.01/1.23  (fellow (skc63) (skf11 (skc63) zenon_X537))
% 1.01/1.23  (fellow (skc19) (skf21 zenon_X659 (skc19) zenon_X898))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X152)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X155) zenon_X155)
% 1.01/1.23  ((skf21 zenon_X11 (skc19) zenon_X838) != zenon_X158)
% 1.01/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X16) zenon_X16)
% 1.01/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X3)
% 1.01/1.23  ((skc71) != zenon_X691)
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X659) zenon_X659)
% 1.01/1.23  (-. (city (skc63) zenon_X740))
% 1.01/1.23  (zenon_X813 != (skc63))
% 1.01/1.23  ((skc20) != zenon_X611)
% 1.01/1.23  ((skf21 zenon_X161 (skc63) zenon_X837) != zenon_X160)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X161))
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X6)
% 1.01/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X652)))
% 1.01/1.23  ((skf21 zenon_X108 (skc63) zenon_X818) != zenon_X152)
% 1.01/1.23  (member (skc19) (skf23 (skc19) zenon_X0) zenon_X0)
% 1.01/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X537))
% 1.01/1.23  (zenon_X101 != (skc63))
% 1.01/1.23  ((skf23 (skc19) zenon_X155) != zenon_X158)
% 1.01/1.23  (zenon_X886 != (skc19))
% 1.01/1.23  ((skf19 zenon_X15 (skc63) zenon_X16) != zenon_X152)
% 1.01/1.23  ((skf21 (skc64) (skc19) zenon_X201) != zenon_X154)
% 1.01/1.23  (member (skc19) (skf16 zenon_X8 (skc19) (skc20)) (skc20))
% 1.01/1.23  (zenon_X17 != (skc19))
% 1.01/1.23  ((skc69) != zenon_X745)
% 1.01/1.23  (member (skc63) (skf21 zenon_X0 (skc63) zenon_X811) zenon_X0)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X108) zenon_X108)
% 1.01/1.23  ((skf11 (skc19) zenon_X155) != zenon_X158)
% 1.01/1.23  ((skf16 zenon_X8 (skc63) zenon_X659) != zenon_X160)
% 1.01/1.23  ((skf19 zenon_X15 (skc19) (skc64)) != zenon_X158)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X6)
% 1.01/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X537) zenon_X537)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X16) zenon_X16)
% 1.01/1.23  (fellow (skc63) (skf23 (skc63) zenon_X108))
% 1.01/1.23  ((skf21 zenon_X153 (skc19) zenon_X853) != zenon_X154)
% 1.01/1.23  ((skf11 (skc19) zenon_X161) != zenon_X158)
% 1.01/1.23  ((skc20) != zenon_X155)
% 1.01/1.23  (member zenon_X1 (skf11 zenon_X1 zenon_X0) zenon_X0)
% 1.01/1.23  (member (skc63) (skf21 zenon_X11 (skc63) zenon_X764) zenon_X11)
% 1.01/1.23  (chevy (skc19) (skc27))
% 1.01/1.23  (zenon_X866 != (skc63))
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X0) zenon_X0)
% 1.01/1.23  (member (skc63) (skf19 zenon_X15 (skc63) (skc64)) (skc64))
% 1.01/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.01/1.23  (member (skc19) (skf11 (skc19) zenon_X97) zenon_X97)
% 1.01/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X9))
% 1.01/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.01/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X625)))
% 1.01/1.23  ((skf11 (skc63) zenon_X659) != zenon_X160)
% 1.01/1.23  ((skf21 zenon_X155 (skc19) zenon_X783) != zenon_X158)
% 1.01/1.23  ((skf16 zenon_X8 (skc19) zenon_X161) != zenon_X158)
% 1.01/1.23  ((skf11 (skc19) zenon_X9) != zenon_X158)
% 1.01/1.23  (zenon_X910 != (skc19))
% 1.01/1.23  (zenon_X932 != (skc19))
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X659))
% 1.01/1.23  (-. (member (skc63) zenon_X152 zenon_X9))
% 1.01/1.23  (member zenon_X950 (skf16 zenon_X8 zenon_X950 zenon_X97) zenon_X97)
% 1.01/1.23  (zenon_X809 != (skc63))
% 1.01/1.23  (event (skc19) (skc23))
% 1.01/1.23  *)
% 1.01/1.23  (* NO-PROOF *)
% 1.01/1.23  % SZS status GaveUp
% 1.01/1.23  Number of rewrites on terms: 0
% 1.01/1.23  Number of rewrites on props: 0
% 1.01/1.23  nodes searched: 19468
% 1.01/1.23  max branch formulas: 3063
% 1.01/1.23  proof nodes created: 1314
% 1.01/1.23  formulas created: 67726
% 1.01/1.23  
%------------------------------------------------------------------------------