↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

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

% Result   : Unknown 1.02s 1.23s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14  % Problem  : NLP164-1 : TPTP v8.2.0. Released v2.4.0.
% 0.04/0.14  % Command  : run_zenon_modulo %d %s
% 0.13/0.35  % Computer : n011.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 300
% 0.13/0.35  % DateTime : Sat Jun 22 23:59:54 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 1.02/1.23  Zenon error: exhausted search space without finding a proof
% 1.02/1.23  (* Current branch:
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X159) zenon_X159)
% 1.02/1.23  ((skf11 (skc63) (skc20)) != (skf11 zenon_X24 zenon_X25))
% 1.02/1.23  ((skf23 (skc63) zenon_X0) != zenon_X152)
% 1.02/1.23  ((skf21 zenon_X153 (skc63) zenon_X800) != zenon_X152)
% 1.02/1.23  (zenon_X97 != zenon_X0)
% 1.02/1.23  (member (skc19) (skf21 zenon_X0 (skc19) zenon_X869) zenon_X0)
% 1.02/1.23  ((skc64) != zenon_X155)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X108) != zenon_X152)
% 1.02/1.23  (zenon_X825 != (skc19))
% 1.02/1.23  (-. (barrel (skc63) zenon_X563))
% 1.02/1.23  (zenon_X659 != zenon_X108)
% 1.02/1.23  ((skf11 (skc19) zenon_X16) != zenon_X154)
% 1.02/1.23  (member zenon_X794 (skf16 zenon_X8 zenon_X794 zenon_X108) zenon_X108)
% 1.02/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X599)))
% 1.02/1.23  (zenon_X108 != zenon_X537)
% 1.02/1.23  (zenon_X773 != (skc63))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X537) zenon_X537)
% 1.02/1.23  ((skc68) != zenon_X702)
% 1.02/1.23  (hollywood_placename (skc19) (skc25))
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X153) zenon_X153)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X9) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X97) != zenon_X152)
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X97))
% 1.02/1.23  ((skf23 (skc63) zenon_X153) != zenon_X160)
% 1.02/1.23  (zenon_X171 != (skc19))
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X9) zenon_X9)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X11) != zenon_X152)
% 1.02/1.23  ((skf11 (skc19) zenon_X11) != zenon_X158)
% 1.02/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X640)))
% 1.02/1.23  ((skc19) != zenon_X24)
% 1.02/1.23  (-. (member (skc19) zenon_X5 (skc20)))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X155))
% 1.02/1.23  (zenon_X159 != zenon_X155)
% 1.02/1.23  (young (skc19) (skf21 zenon_X108 (skc19) zenon_X789))
% 1.02/1.23  (zenon_X179 != (skc63))
% 1.02/1.23  (zenon_X756 != (skc19))
% 1.02/1.23  (member zenon_X875 (skf21 zenon_X16 zenon_X875 zenon_X876) zenon_X16)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X153))
% 1.02/1.23  (zenon_X937 != (skc63))
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X155))
% 1.02/1.23  (member zenon_X886 (skf11 zenon_X886 zenon_X97) zenon_X97)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X161))
% 1.02/1.23  (zenon_X97 != (skc64))
% 1.02/1.23  ((skf23 (skc63) zenon_X153) != zenon_X152)
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X161) zenon_X161)
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X537))
% 1.02/1.23  (zenon_X804 != (skc63))
% 1.02/1.23  ((skf11 (skc19) (skc64)) != zenon_X154)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X161) zenon_X161)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X153) zenon_X153)
% 1.02/1.23  (member zenon_X937 (skf21 zenon_X659 zenon_X937 zenon_X938) zenon_X659)
% 1.02/1.23  (zenon_X9 != zenon_X161)
% 1.02/1.23  (zenon_X659 != (skc64))
% 1.02/1.23  ((skc68) != zenon_X710)
% 1.02/1.23  (zenon_X891 != (skc19))
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X153))
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X659) zenon_X659)
% 1.02/1.23  (zenon_X9 != zenon_X155)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X537) zenon_X537)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X159) != zenon_X158)
% 1.02/1.23  (-. (ssSkP0 zenon_X23 zenon_X21))
% 1.02/1.23  (young (skc19) (skf21 (skc64) (skc19) zenon_X201))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X0 (skc19) zenon_X869))
% 1.02/1.23  ((skf11 (skc19) zenon_X0) != zenon_X154)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X7)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X9) != zenon_X160)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X97) != zenon_X158)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X108))
% 1.02/1.23  ((skc69) != zenon_X720)
% 1.02/1.23  ((skf11 (skc63) zenon_X161) != zenon_X152)
% 1.02/1.23  (zenon_X16 != zenon_X155)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X155) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X161) != zenon_X160)
% 1.02/1.23  (barrel (skc63) (skc66))
% 1.02/1.23  ((skf11 (skc19) (skc20)) != zenon_X154)
% 1.02/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.02/1.23  (member zenon_X896 (skf19 zenon_X15 zenon_X896 zenon_X155) zenon_X155)
% 1.02/1.23  (zenon_X930 != (skc19))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X161) zenon_X161)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X159))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X155) != zenon_X158)
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X9))
% 1.02/1.23  (zenon_X875 != (skc63))
% 1.02/1.23  ((skc65) != zenon_X583)
% 1.02/1.23  ((skc64) != zenon_X636)
% 1.02/1.23  ((skf23 (skc63) zenon_X108) != zenon_X160)
% 1.02/1.23  (member zenon_X767 (skf16 zenon_X8 zenon_X767 zenon_X161) zenon_X161)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X537))
% 1.02/1.23  ((skf21 zenon_X659 (skc63) zenon_X939) != zenon_X152)
% 1.02/1.23  (zenon_X537 != zenon_X159)
% 1.02/1.23  (of (skc19) (skc25) (skc26))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != zenon_X2)
% 1.02/1.23  (ssSkP0 (skc22) (skc19))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X11))
% 1.02/1.23  (member (skc19) (skf21 zenon_X16 (skc19) zenon_X895) zenon_X16)
% 1.02/1.23  ((skc63) != zenon_X21)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X154)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X537))
% 1.02/1.23  ((skf11 (skc19) zenon_X9) != zenon_X154)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X155) != zenon_X152)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) (skc20)))
% 1.02/1.23  (zenon_X773 != (skc19))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X537) zenon_X537)
% 1.02/1.23  ((skf23 (skc63) zenon_X659) != zenon_X152)
% 1.02/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X632)))
% 1.02/1.23  (group (skc63) (skc65))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) (skc20)))
% 1.02/1.23  (member (skc19) (skf21 zenon_X161 (skc19) zenon_X793) zenon_X161)
% 1.02/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X648)))
% 1.02/1.23  ((skf23 (skc19) (skc20)) != zenon_X158)
% 1.02/1.23  ((skf21 zenon_X11 (skc19) zenon_X855) != zenon_X154)
% 1.02/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X621)))
% 1.02/1.23  ((skc65) != zenon_X676)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X11))
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X16))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X161) != zenon_X152)
% 1.02/1.23  ((skf11 (skc63) zenon_X161) != zenon_X160)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X7)
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X153) zenon_X153)
% 1.02/1.23  ((skf23 (skc19) zenon_X159) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X9) != zenon_X158)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X652))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X97) zenon_X97)
% 1.02/1.23  ((skf11 (skc63) zenon_X16) != zenon_X152)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X155))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X159))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X659) zenon_X659)
% 1.02/1.23  (zenon_X155 != zenon_X537)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc20)) != zenon_X160)
% 1.02/1.23  ((skc64) != zenon_X652)
% 1.02/1.23  (member (skc63) (skf21 zenon_X659 (skc63) zenon_X939) zenon_X659)
% 1.02/1.23  (-. (barrel (skc19) zenon_X541))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X537 (skc19) zenon_X882))
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) (skc64)))
% 1.02/1.23  ((skc23) != zenon_X541)
% 1.02/1.23  (-. (group (skc63) zenon_X616))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X153) zenon_X153)
% 1.02/1.23  ((skf11 (skc19) zenon_X16) != zenon_X158)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X9))
% 1.02/1.23  (zenon_X16 != zenon_X97)
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X153))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X159) != zenon_X160)
% 1.02/1.23  ((skf21 zenon_X0 (skc63) zenon_X870) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X108))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X714))
% 1.02/1.23  (white (skc63) (skc70))
% 1.02/1.23  (-. (actual_world zenon_X477))
% 1.02/1.23  ((skf11 (skc63) zenon_X537) != zenon_X152)
% 1.02/1.23  (fellow (skc19) (skf21 (skc20) (skc19) zenon_X235))
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X159))
% 1.02/1.23  (zenon_X108 != (skc64))
% 1.02/1.23  ((skf21 zenon_X659 (skc19) zenon_X940) != zenon_X154)
% 1.02/1.23  (zenon_X161 != zenon_X155)
% 1.02/1.23  ((skf11 (skc19) zenon_X161) != zenon_X154)
% 1.02/1.23  ((skc64) != zenon_X161)
% 1.02/1.23  ((skf11 (skc63) (skc64)) != zenon_X3)
% 1.02/1.23  ((skc71) != zenon_X616)
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X11))
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X108 (skc63) zenon_X809))
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X161))
% 1.02/1.23  (member zenon_X891 (skf21 zenon_X155 zenon_X891 zenon_X892) zenon_X155)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X153))
% 1.02/1.23  (member zenon_X898 (skf19 zenon_X15 zenon_X898 zenon_X108) zenon_X108)
% 1.02/1.23  ((skf23 (skc19) zenon_X16) != zenon_X154)
% 1.02/1.23  (down (skc63) (skc66) (skc67))
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X9) zenon_X9)
% 1.02/1.23  (member zenon_X166 (skf21 (skc20) zenon_X166 zenon_X167) (skc20))
% 1.02/1.23  (zenon_X836 != (skc63))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X155) zenon_X155)
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X721))
% 1.02/1.23  ((skf21 zenon_X97 (skc19) zenon_X951) != zenon_X154)
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X0) zenon_X0)
% 1.02/1.23  (zenon_X897 != (skc63))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc20)) != zenon_X152)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X161) != zenon_X152)
% 1.02/1.23  (young (skc19) (skf21 zenon_X97 (skc19) zenon_X951))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) (skc64)) (skc64))
% 1.02/1.23  ((skc68) != zenon_X708)
% 1.02/1.23  ((skf21 zenon_X155 (skc63) zenon_X894) != zenon_X160)
% 1.02/1.23  ((skc63) != zenon_X477)
% 1.02/1.23  (-. (group (skc63) zenon_X583))
% 1.02/1.23  (member (skc19) (skf21 zenon_X153 (skc19) zenon_X842) zenon_X153)
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X97) zenon_X97)
% 1.02/1.23  ((skc72) != (skc70))
% 1.02/1.23  ((skc64) != zenon_X640)
% 1.02/1.23  ((skf21 zenon_X659 (skc19) zenon_X940) != zenon_X158)
% 1.02/1.23  ((skc22) != zenon_X111)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X161) != zenon_X158)
% 1.02/1.23  (down (skc19) (skc23) (skc24))
% 1.02/1.23  (zenon_X159 != zenon_X161)
% 1.02/1.23  (zenon_X11 != zenon_X9)
% 1.02/1.23  (young (skc19) (skf21 zenon_X11 (skc19) zenon_X855))
% 1.02/1.23  (zenon_X97 != (skc20))
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X16))
% 1.02/1.23  ((skf21 zenon_X9 (skc19) zenon_X807) != zenon_X154)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X97))
% 1.02/1.23  (zenon_X808 != (skc19))
% 1.02/1.23  (present (skc19) (skc23))
% 1.02/1.23  (zenon_X767 != (skc19))
% 1.02/1.23  (frontseat (skc19) (skc27))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X108) != zenon_X154)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X108) zenon_X108)
% 1.02/1.23  (-. (member (skc19) zenon_X7 (skc20)))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X155) zenon_X155)
% 1.02/1.23  (zenon_X0 != zenon_X153)
% 1.02/1.23  (-. (member (skc19) zenon_X154 (skc64)))
% 1.02/1.23  ((skf23 (skc63) zenon_X659) != zenon_X160)
% 1.02/1.23  (coat (skc63) (skf23 (skc63) (skc64)))
% 1.02/1.23  (member zenon_X10 (skf16 zenon_X8 zenon_X10 zenon_X9) zenon_X9)
% 1.02/1.23  ((skc68) != zenon_X714)
% 1.02/1.23  (member (skc63) (skf21 zenon_X108 (skc63) zenon_X809) zenon_X108)
% 1.02/1.23  (-. (member (skc19) zenon_X6 (skc20)))
% 1.02/1.23  (ssSkP0 (skc71) (skc63))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.02/1.23  (-. (member (skc19) zenon_X154 (skc20)))
% 1.02/1.23  (zenon_X917 != (skc19))
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X155 (skc63) zenon_X894))
% 1.02/1.23  (young (skc63) (skf23 (skc63) (skc20)))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X160)
% 1.02/1.23  (event (skc63) (skc66))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X161) != zenon_X154)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.02/1.23  (-. (city (skc63) zenon_X720))
% 1.02/1.23  (zenon_X891 != (skc63))
% 1.02/1.23  ((skf23 (skc19) zenon_X11) != zenon_X154)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X0) != zenon_X158)
% 1.02/1.23  (zenon_X790 != (skc19))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X11) != zenon_X154)
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X0))
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X153))
% 1.02/1.23  (zenon_X9 != zenon_X97)
% 1.02/1.23  (member zenon_X772 (skf19 zenon_X15 zenon_X772 zenon_X153) zenon_X153)
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X0) zenon_X0)
% 1.02/1.23  (member zenon_X918 (skf19 zenon_X15 zenon_X918 zenon_X0) zenon_X0)
% 1.02/1.23  ((skc64) != zenon_X159)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X11))
% 1.02/1.23  (zenon_X878 != (skc19))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X97) zenon_X97)
% 1.02/1.23  (member (skc19) (skf23 (skc19) (skc64)) (skc64))
% 1.02/1.23  (cheap (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.02/1.23  (zenon_X97 != zenon_X159)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X0) zenon_X0)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X0))
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X155))
% 1.02/1.23  (zenon_X772 != (skc63))
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X108))
% 1.02/1.23  (zenon_X0 != (skc20))
% 1.02/1.23  (zenon_X16 != zenon_X161)
% 1.02/1.23  (zenon_X808 != (skc63))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X161) zenon_X161)
% 1.02/1.23  (zenon_X108 != (skc20))
% 1.02/1.23  (member (skc63) (skf21 (skc20) (skc63) zenon_X237) (skc20))
% 1.02/1.23  (black (skc63) (skf23 (skc63) (skc64)))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X97))
% 1.02/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X6)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) (skc64)))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X706))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X153) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X659) != zenon_X152)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X161))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.02/1.23  (member zenon_X919 (skf11 zenon_X919 zenon_X16) zenon_X16)
% 1.02/1.23  (street (skc63) (skc67))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X161))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X537))
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X659))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X16) zenon_X16)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X11))
% 1.02/1.23  (young (skc19) (skf11 (skc19) (skc64)))
% 1.02/1.23  ((skf23 (skc19) (skc64)) != zenon_X154)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X9))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc64)) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X16) zenon_X16)
% 1.02/1.23  (zenon_X659 != zenon_X155)
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X161) zenon_X161)
% 1.02/1.23  ((skf23 (skc19) zenon_X9) != zenon_X158)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X153) != zenon_X154)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X9) != zenon_X160)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X9))
% 1.02/1.23  ((skc19) != zenon_X486)
% 1.02/1.23  ((skf21 zenon_X537 (skc19) zenon_X882) != zenon_X154)
% 1.02/1.23  (fellow (skc19) (skf21 (skc64) (skc19) zenon_X201))
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X659))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.02/1.23  (zenon_X935 != (skc63))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X9))
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X11))
% 1.02/1.23  ((skf21 zenon_X11 (skc63) zenon_X764) != zenon_X152)
% 1.02/1.23  (member (skc63) (skf21 zenon_X153 (skc63) zenon_X800) zenon_X153)
% 1.02/1.23  (-. (member (skc63) zenon_X2 (skc64)))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X155))
% 1.02/1.23  (member zenon_X859 (skf19 zenon_X15 zenon_X859 zenon_X161) zenon_X161)
% 1.02/1.23  (zenon_X760 != (skc19))
% 1.02/1.23  ((skf11 (skc63) zenon_X108) != zenon_X160)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X108) zenon_X108)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X9))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X155) != zenon_X154)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X159) != zenon_X160)
% 1.02/1.23  ((skf21 zenon_X0 (skc19) zenon_X869) != zenon_X158)
% 1.02/1.23  ((skf21 (skc20) (skc63) zenon_X237) != zenon_X160)
% 1.02/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X159))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != zenon_X2)
% 1.02/1.23  ((skf23 (skc63) zenon_X155) != zenon_X160)
% 1.02/1.23  ((skf23 (skc19) zenon_X155) != zenon_X154)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X155))
% 1.02/1.23  ((skf11 (skc63) zenon_X11) != zenon_X160)
% 1.02/1.23  (-. (old (skc63) zenon_X503))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X724))
% 1.02/1.23  (zenon_X659 != (skc20))
% 1.02/1.23  ((skc64) != zenon_X603)
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X108))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X161))
% 1.02/1.23  (member zenon_X171 (skf19 zenon_X15 zenon_X171 (skc20)) (skc20))
% 1.02/1.23  (coat (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.02/1.23  (nonreflexive zenon_X49 (skf17 zenon_X49 zenon_X55 zenon_X53))
% 1.02/1.23  (member zenon_X760 (skf11 zenon_X760 zenon_X153) zenon_X153)
% 1.02/1.23  ((skc65) != zenon_X685)
% 1.02/1.23  ((skf11 (skc19) zenon_X97) != zenon_X158)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X153))
% 1.02/1.23  (coat (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X159) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf21 zenon_X11 (skc19) zenon_X855) zenon_X11)
% 1.02/1.23  ((skf11 (skc19) (skc20)) != zenon_X5)
% 1.02/1.23  (zenon_X11 != zenon_X161)
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X708))
% 1.02/1.23  (zenon_X0 != (skc64))
% 1.02/1.23  (member zenon_X101 (skf10 zenon_X101 zenon_X108) zenon_X108)
% 1.02/1.23  ((skc65) != zenon_X616)
% 1.02/1.23  (zenon_X171 != (skc63))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X97))
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X97))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X5)
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X702))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X108) zenon_X108)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X97) != zenon_X154)
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X537))
% 1.02/1.23  ((skf21 zenon_X108 (skc63) zenon_X809) != zenon_X160)
% 1.02/1.23  ((skf11 (skc63) zenon_X97) != zenon_X160)
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X153))
% 1.02/1.23  ((skf23 (skc19) zenon_X97) != zenon_X154)
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X659))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X159) zenon_X159)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X155) != zenon_X160)
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X537) zenon_X537)
% 1.02/1.23  ((skf11 (skc19) zenon_X159) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X16) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X0) zenon_X0)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X4)
% 1.02/1.23  (zenon_X878 != (skc63))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X11) zenon_X11)
% 1.02/1.23  ((skc23) != zenon_X527)
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X9))
% 1.02/1.23  (zenon_X787 != (skc63))
% 1.02/1.23  ((skf21 zenon_X11 (skc63) zenon_X764) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X159))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X153) != zenon_X152)
% 1.02/1.23  (group (skc63) (skc71))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) (skc20)))
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X11) zenon_X11)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X0))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X159))
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X11 (skc63) zenon_X764))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X155))
% 1.02/1.23  ((skf21 zenon_X537 (skc63) zenon_X838) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X537))
% 1.02/1.23  (cheap (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.02/1.23  (young (skc19) (skf21 zenon_X16 (skc19) zenon_X895))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X153) zenon_X153)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X108) != zenon_X158)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X161))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X97))
% 1.02/1.23  (zenon_X9 != zenon_X153)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) (skc20)) (skc20))
% 1.02/1.23  (zenon_X825 != (skc63))
% 1.02/1.23  (-. (barrel (skc63) zenon_X576))
% 1.02/1.23  ((skf21 zenon_X161 (skc63) zenon_X771) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X537) != zenon_X160)
% 1.02/1.23  ((skc68) != zenon_X698)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X16))
% 1.02/1.23  ((skf23 (skc63) zenon_X537) != zenon_X152)
% 1.02/1.23  ((skf23 (skc19) zenon_X537) != zenon_X154)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X161) != zenon_X160)
% 1.02/1.23  ((skf21 zenon_X659 (skc63) zenon_X939) != zenon_X160)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X160)
% 1.02/1.23  (-. (group (skc19) zenon_X611))
% 1.02/1.23  (two (skc19) (skc22))
% 1.02/1.23  (in (skc19) (skc23) (skc26))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X161) zenon_X161)
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X0))
% 1.02/1.23  (member zenon_X198 (skf11 zenon_X198 (skc64)) (skc64))
% 1.02/1.23  (zenon_X16 != zenon_X11)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X659))
% 1.02/1.23  (zenon_X11 != zenon_X97)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X9))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X716))
% 1.02/1.23  ((skc67) != zenon_X570)
% 1.02/1.23  ((skc22) != zenon_X594)
% 1.02/1.23  ((skf23 (skc19) zenon_X153) != zenon_X158)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X9))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X153) != zenon_X154)
% 1.02/1.23  ((skf21 zenon_X108 (skc19) zenon_X789) != zenon_X154)
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X155))
% 1.02/1.23  ((skf21 zenon_X9 (skc63) zenon_X806) != zenon_X152)
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X153) zenon_X153)
% 1.02/1.23  ((skf23 (skc63) zenon_X155) != zenon_X152)
% 1.02/1.23  (zenon_X948 != (skc19))
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X97))
% 1.02/1.23  (young (skc63) (skf11 (skc63) (skc20)))
% 1.02/1.23  (zenon_X537 != (skc20))
% 1.02/1.23  (city (skc63) (skc69))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X9) zenon_X9)
% 1.02/1.23  (young (skc63) (skf21 zenon_X108 (skc63) zenon_X809))
% 1.02/1.23  ((skc71) != zenon_X679)
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X704))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X11) != zenon_X158)
% 1.02/1.23  ((skf11 (skc19) zenon_X97) != zenon_X154)
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X0))
% 1.02/1.23  ((skf11 (skc19) (skc20)) != (skf11 zenon_X24 zenon_X25))
% 1.02/1.23  ((skc27) != zenon_X511)
% 1.02/1.23  (-. (group (skc19) zenon_X594))
% 1.02/1.23  (coat (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.02/1.23  (zenon_X108 != zenon_X153)
% 1.02/1.23  (group (skc63) (skc64))
% 1.02/1.23  (zenon_X659 != zenon_X0)
% 1.02/1.23  (member zenon_X917 (skf19 zenon_X15 zenon_X917 zenon_X11) zenon_X11)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X155))
% 1.02/1.23  (member zenon_X897 (skf11 zenon_X897 zenon_X11) zenon_X11)
% 1.02/1.23  ((skf23 (skc19) zenon_X537) != zenon_X158)
% 1.02/1.23  (-. (street (skc63) zenon_X588))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X159) != zenon_X152)
% 1.02/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X663)))
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X537) zenon_X537)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X2)
% 1.02/1.23  ((skc20) != zenon_X594)
% 1.02/1.23  (barrel (skc19) (skc23))
% 1.02/1.23  (member (skc63) (skf23 (skc63) (skc64)) (skc64))
% 1.02/1.23  (black (skc63) (skf11 (skc63) (skc64)))
% 1.02/1.23  ((skf23 (skc19) zenon_X0) != zenon_X158)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X153 (skc63) zenon_X800))
% 1.02/1.23  (zenon_X804 != (skc19))
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X640))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.02/1.23  (black (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.02/1.23  ((skf23 (skc19) zenon_X108) != zenon_X154)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X159))
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X97))
% 1.02/1.23  ((skc69) != zenon_X723)
% 1.02/1.23  (cheap (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.02/1.23  ((skf23 (skc63) (skc20)) != zenon_X160)
% 1.02/1.23  ((skf23 (skc63) (skc64)) != zenon_X160)
% 1.02/1.23  (young (skc19) (skf21 zenon_X659 (skc19) zenon_X940))
% 1.02/1.23  (zenon_X537 != zenon_X153)
% 1.02/1.23  ((skf23 (skc19) zenon_X659) != zenon_X154)
% 1.02/1.23  ((skc64) != zenon_X583)
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) (skc20)) (skc20))
% 1.02/1.23  (zenon_X213 != (skc19))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X97) != zenon_X152)
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X11) zenon_X11)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X537))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X659))
% 1.02/1.23  (zenon_X0 != zenon_X155)
% 1.02/1.23  ((skf23 (skc63) zenon_X9) != zenon_X160)
% 1.02/1.23  (young (skc19) (skf21 zenon_X537 (skc19) zenon_X882))
% 1.02/1.23  (zenon_X166 != (skc63))
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X11))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X159) zenon_X159)
% 1.02/1.23  (zenon_X794 != (skc63))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X0))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X16 (skc19) zenon_X895))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X0) != zenon_X160)
% 1.02/1.23  ((skc20) != zenon_X25)
% 1.02/1.23  (ssSkP1 zenon_X78 zenon_X81 zenon_X76)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X155))
% 1.02/1.23  ((skf11 (skc63) zenon_X659) != zenon_X152)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X159) zenon_X159)
% 1.02/1.23  (member (skc63) (skf21 zenon_X537 (skc63) zenon_X838) zenon_X537)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc20)) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X97))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X537))
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X11))
% 1.02/1.23  ((skc68) != zenon_X694)
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X161) zenon_X161)
% 1.02/1.23  (agent (skc19) (skc23) (skc27))
% 1.02/1.23  ((skc68) != zenon_X696)
% 1.02/1.23  (zenon_X875 != (skc19))
% 1.02/1.23  (member zenon_X926 (skf16 zenon_X8 zenon_X926 zenon_X0) zenon_X0)
% 1.02/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X659))
% 1.02/1.23  (coat (skc63) (skf11 (skc63) (skc64)))
% 1.02/1.23  (zenon_X935 != (skc19))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X159) zenon_X159)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X108))
% 1.02/1.23  (zenon_X0 != zenon_X9)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X16) != zenon_X160)
% 1.02/1.23  (-. (actual_world zenon_X486))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.02/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X607)))
% 1.02/1.23  (zenon_X919 != (skc63))
% 1.02/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X5)
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X9) zenon_X9)
% 1.02/1.23  (member zenon_X863 (skf16 zenon_X8 zenon_X863 zenon_X97) zenon_X97)
% 1.02/1.23  (zenon_X930 != (skc63))
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X161))
% 1.02/1.23  ((skf11 (skc63) zenon_X159) != zenon_X160)
% 1.02/1.23  (zenon_X13 != (skc19))
% 1.02/1.23  ((skf11 (skc63) zenon_X0) != zenon_X160)
% 1.02/1.23  ((skc66) != zenon_X576)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X659))
% 1.02/1.23  (-. (barrel (skc19) zenon_X527))
% 1.02/1.23  (dirty (skc63) (skc70))
% 1.02/1.23  ((skc68) != zenon_X712)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X9) != zenon_X154)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X11) != zenon_X160)
% 1.02/1.23  (old (skc63) (skc70))
% 1.02/1.23  (zenon_X760 != (skc63))
% 1.02/1.23  ((skf23 (skc63) zenon_X161) != zenon_X152)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X108))
% 1.02/1.23  (member zenon_X769 (skf21 zenon_X161 zenon_X769 zenon_X770) zenon_X161)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X155) zenon_X155)
% 1.02/1.23  ((skf23 (skc19) (skc20)) != zenon_X6)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X9))
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X537))
% 1.02/1.23  ((skf11 (skc63) (skc20)) != zenon_X152)
% 1.02/1.23  ((skf11 (skc63) zenon_X11) != zenon_X152)
% 1.02/1.23  (black (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.02/1.23  (lonely (skc19) (skc24))
% 1.02/1.23  (zenon_X198 != (skc63))
% 1.02/1.23  ((skf23 (skc19) zenon_X159) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf21 zenon_X537 (skc19) zenon_X882) zenon_X537)
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X159))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) (skc64)))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X108) != zenon_X154)
% 1.02/1.23  (young (skc19) (skf21 zenon_X9 (skc19) zenon_X807))
% 1.02/1.23  ((skf23 (skc63) zenon_X97) != zenon_X160)
% 1.02/1.23  (zenon_X815 != (skc63))
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X632))
% 1.02/1.23  ((skc70) != zenon_X495)
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X659))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X108))
% 1.02/1.23  ((skc20) != zenon_X153)
% 1.02/1.23  ((skf11 (skc63) zenon_X155) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X153) != zenon_X160)
% 1.02/1.23  (fellow (skc63) (skf21 (skc20) (skc63) zenon_X237))
% 1.02/1.23  (event zenon_X63 (skf17 zenon_X63 zenon_X69 zenon_X67))
% 1.02/1.23  (zenon_X537 != zenon_X97)
% 1.02/1.23  (-. (member (skc63) zenon_X160 (skc20)))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X108) zenon_X108)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X0) != zenon_X154)
% 1.02/1.23  ((skc27) != zenon_X519)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X4)
% 1.02/1.23  (member zenon_X960 (skf11 zenon_X960 zenon_X537) zenon_X537)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) (skc64)))
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X16) zenon_X16)
% 1.02/1.23  (zenon_X926 != (skc63))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X9 (skc19) zenon_X807))
% 1.02/1.23  ((skf21 zenon_X159 (skc63) zenon_X780) != zenon_X160)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X155))
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X153) zenon_X153)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X159))
% 1.02/1.23  ((skf21 zenon_X16 (skc63) zenon_X877) != zenon_X152)
% 1.02/1.23  (-. (ssSkC0))
% 1.02/1.23  (member zenon_X756 (skf16 zenon_X8 zenon_X756 zenon_X159) zenon_X159)
% 1.02/1.23  (zenon_X794 != (skc19))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X108))
% 1.02/1.23  (dirty (skc19) (skc27))
% 1.02/1.23  (-. (street (skc19) zenon_X557))
% 1.02/1.23  ((skf11 (skc19) (skc20)) != zenon_X7)
% 1.02/1.23  (zenon_X913 != (skc63))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X155) != zenon_X158)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X97) != zenon_X160)
% 1.02/1.23  (young (skc19) (skf21 (skc20) (skc19) zenon_X235))
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X9))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X155 (skc19) zenon_X893))
% 1.02/1.23  (zenon_X11 != zenon_X153)
% 1.02/1.23  ((skf21 zenon_X97 (skc63) zenon_X950) != zenon_X152)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X159))
% 1.02/1.23  ((skc71) != zenon_X691)
% 1.02/1.23  ((skf21 (skc64) (skc19) zenon_X201) != zenon_X158)
% 1.02/1.23  (member zenon_X798 (skf21 zenon_X153 zenon_X798 zenon_X799) zenon_X153)
% 1.02/1.23  ((skf23 (skc19) zenon_X153) != zenon_X154)
% 1.02/1.23  ((skf21 zenon_X0 (skc19) zenon_X869) != zenon_X154)
% 1.02/1.23  ((skf23 (skc63) zenon_X537) != zenon_X160)
% 1.02/1.23  ((skc65) != zenon_X682)
% 1.02/1.23  ((skc19) != zenon_X18)
% 1.02/1.23  ((skc19) != zenon_X477)
% 1.02/1.23  ((skf11 (skc63) zenon_X9) != zenon_X160)
% 1.02/1.23  ((skf23 (skc63) zenon_X108) != zenon_X152)
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X161))
% 1.02/1.23  (agent (skc63) (skc66) (skc70))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X659) != zenon_X152)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X3)
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X9) zenon_X9)
% 1.02/1.23  ((skc68) != zenon_X700)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X108))
% 1.02/1.23  ((skf11 (skc63) (skc20)) != zenon_X160)
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X710))
% 1.02/1.23  (zenon_X659 != zenon_X11)
% 1.02/1.23  (young (skc63) (skf11 (skc63) (skc64)))
% 1.02/1.23  ((skc71) != zenon_X685)
% 1.02/1.23  (zenon_X16 != (skc20))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X153))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X659))
% 1.02/1.23  ((skc64) != zenon_X153)
% 1.02/1.23  (zenon_X153 != zenon_X155)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X108) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X153) != zenon_X152)
% 1.02/1.23  (of (skc63) (skc68) (skc69))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X159) != zenon_X152)
% 1.02/1.23  ((skc70) != zenon_X503)
% 1.02/1.23  ((skf23 (skc19) (skc20)) != zenon_X154)
% 1.02/1.23  ((skc71) != zenon_X111)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X9 (skc63) zenon_X806))
% 1.02/1.23  (zenon_X537 != zenon_X161)
% 1.02/1.23  (zenon_X917 != (skc63))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X0) != zenon_X154)
% 1.02/1.23  (zenon_X775 != (skc19))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X537))
% 1.02/1.23  ((skc63) != zenon_X18)
% 1.02/1.23  ((skc66) != zenon_X563)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X161))
% 1.02/1.23  (member zenon_X935 (skf16 zenon_X8 zenon_X935 zenon_X537) zenon_X537)
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X696))
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X16))
% 1.02/1.23  (zenon_X169 != (skc63))
% 1.02/1.23  (zenon_X1 != (skc63))
% 1.02/1.23  (zenon_X769 != (skc63))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc20)) != zenon_X152)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X161 (skc63) zenon_X771))
% 1.02/1.23  (zenon_X97 != zenon_X161)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X155))
% 1.02/1.23  (zenon_X10 != (skc19))
% 1.02/1.23  ((skc64) != zenon_X682)
% 1.02/1.23  ((skf11 (skc19) zenon_X659) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) (skc64)) (skc64))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X97 (skc19) zenon_X951))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X659) != zenon_X158)
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X16) zenon_X16)
% 1.02/1.23  ((skf11 (skc19) zenon_X153) != zenon_X154)
% 1.02/1.23  ((skf23 (skc19) zenon_X161) != zenon_X154)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X537))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X0) zenon_X0)
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X16))
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X159))
% 1.02/1.23  (zenon_X767 != (skc63))
% 1.02/1.23  ((skf21 zenon_X97 (skc63) zenon_X950) != zenon_X160)
% 1.02/1.23  (group (skc19) (skc21))
% 1.02/1.23  ((skc21) != zenon_X611)
% 1.02/1.23  (state zenon_X27 (skf13 zenon_X27 zenon_X31 zenon_X32))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X161 (skc19) zenon_X793))
% 1.02/1.23  ((skf21 zenon_X108 (skc19) zenon_X789) != zenon_X158)
% 1.02/1.23  (-. (group (skc63) zenon_X676))
% 1.02/1.23  (frontseat (skc63) (skc72))
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X97))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc64)) != zenon_X154)
% 1.02/1.23  (young (skc63) (skf21 zenon_X0 (skc63) zenon_X870))
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X11))
% 1.02/1.23  (zenon_X172 != (skc63))
% 1.02/1.23  (-. (member (skc19) zenon_X158 (skc20)))
% 1.02/1.23  (member (skc19) (skf21 zenon_X159 (skc19) zenon_X777) zenon_X159)
% 1.02/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.02/1.23  (ssSkP0 zenon_X363 (skc19))
% 1.02/1.23  (wear zenon_X42 (skf17 zenon_X42 zenon_X48 zenon_X46))
% 1.02/1.23  ((skc24) != zenon_X548)
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X155))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X159))
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X16))
% 1.02/1.23  (zenon_X164 != (skc63))
% 1.02/1.23  (city (skc19) (skc26))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X161))
% 1.02/1.23  (young (skc19) (skf11 (skc19) (skc20)))
% 1.02/1.23  (zenon_X798 != (skc19))
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X97))
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X159) zenon_X159)
% 1.02/1.23  (in (skc63) (skc66) (skc69))
% 1.02/1.23  (zenon_X10 != (skc63))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) (skc64)) (skc64))
% 1.02/1.23  ((skf11 (skc19) (skc20)) != (skf11 zenon_X24 (skc20)))
% 1.02/1.23  (zenon_X960 != (skc63))
% 1.02/1.23  (zenon_X11 != (skc64))
% 1.02/1.23  (actual_world (skc63))
% 1.02/1.23  ((skf23 (skc19) zenon_X108) != zenon_X158)
% 1.02/1.23  ((skf23 (skc19) zenon_X659) != zenon_X158)
% 1.02/1.23  (young (skc19) (skf21 zenon_X153 (skc19) zenon_X842))
% 1.02/1.23  (zenon_X926 != (skc19))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X0))
% 1.02/1.23  (member (skc63) (skf21 zenon_X9 (skc63) zenon_X806) zenon_X9)
% 1.02/1.23  (zenon_X108 != zenon_X9)
% 1.02/1.23  (zenon_X659 != zenon_X9)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X537))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.02/1.23  (zenon_X913 != (skc19))
% 1.02/1.23  (member (skc63) (skf11 (skc63) (skc64)) (skc64))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X700))
% 1.02/1.23  (member zenon_X931 (skf11 zenon_X931 zenon_X161) zenon_X161)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X659 (skc63) zenon_X939))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X161))
% 1.02/1.23  (zenon_X159 != zenon_X153)
% 1.02/1.23  ((skf23 (skc63) zenon_X97) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X659) != zenon_X158)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X159))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 (skc20)) (skc20))
% 1.02/1.23  (zenon_X0 != zenon_X161)
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) (skc64)))
% 1.02/1.23  (young (skc63) (skf21 zenon_X9 (skc63) zenon_X806))
% 1.02/1.23  (zenon_X919 != (skc19))
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X0))
% 1.02/1.23  ((skf23 (skc63) zenon_X159) != zenon_X152)
% 1.02/1.23  (-. (ssSkP0 zenon_X20 zenon_X18))
% 1.02/1.23  (zenon_X659 != zenon_X159)
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X659) zenon_X659)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc64)) != zenon_X158)
% 1.02/1.23  ((skf11 (skc19) zenon_X153) != zenon_X158)
% 1.02/1.23  (member (skc19) (skf11 (skc19) (skc64)) (skc64))
% 1.02/1.23  ((skf23 (skc63) zenon_X16) != zenon_X160)
% 1.02/1.23  ((skf23 (skc19) zenon_X9) != zenon_X154)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X659))
% 1.02/1.23  ((skc64) != zenon_X685)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X0 (skc63) zenon_X870))
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X153))
% 1.02/1.23  ((skc64) != zenon_X688)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X153))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X108))
% 1.02/1.23  ((skf21 zenon_X159 (skc19) zenon_X777) != zenon_X154)
% 1.02/1.23  ((skc64) != zenon_X679)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X16) != zenon_X158)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X11))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X11) != zenon_X160)
% 1.02/1.23  ((skf11 (skc19) zenon_X11) != zenon_X154)
% 1.02/1.23  (hollywood_placename (skc63) (skc68))
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X153))
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X16))
% 1.02/1.23  (agent zenon_X70 (skf17 zenon_X70 zenon_X71 zenon_X75) zenon_X71)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X0))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X155) zenon_X155)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X537))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X153))
% 1.02/1.23  ((skf11 (skc63) (skc20)) != (skf11 zenon_X24 (skc20)))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) (skc64)))
% 1.02/1.23  (group (skc19) (skc20))
% 1.02/1.23  (member zenon_X899 (skf19 zenon_X15 zenon_X899 zenon_X537) zenon_X537)
% 1.02/1.23  (member (skc19) (skf21 zenon_X659 (skc19) zenon_X940) zenon_X659)
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X97))
% 1.02/1.23  (member zenon_X17 (skf19 zenon_X15 zenon_X17 zenon_X16) zenon_X16)
% 1.02/1.23  (zenon_X785 != (skc19))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X16) != zenon_X158)
% 1.02/1.23  (member (skc63) (skf21 zenon_X97 (skc63) zenon_X950) zenon_X97)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X159) zenon_X159)
% 1.02/1.23  (zenon_X537 != zenon_X11)
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X108))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X0))
% 1.02/1.23  (chevy (skc63) (skc70))
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) (skc64)))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X159) zenon_X159)
% 1.02/1.23  (member zenon_X773 (skf16 zenon_X8 zenon_X773 zenon_X155) zenon_X155)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X153) != zenon_X158)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X155))
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X155))
% 1.02/1.23  (member (skc63) (skf21 zenon_X155 (skc63) zenon_X894) zenon_X155)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X159 (skc63) zenon_X780))
% 1.02/1.23  ((skc65) != zenon_X679)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X9) != zenon_X152)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X11) != zenon_X154)
% 1.02/1.23  (in zenon_X33 (skf12 zenon_X34 zenon_X33 zenon_X36) zenon_X36)
% 1.02/1.23  ((skf11 (skc19) zenon_X159) != zenon_X154)
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X11))
% 1.02/1.23  (zenon_X801 != (skc63))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 (skc64)) (skc64))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X0) != zenon_X152)
% 1.02/1.23  ((skf11 (skc63) zenon_X659) != zenon_X160)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X537) != zenon_X154)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X154)
% 1.02/1.23  ((skf23 (skc19) zenon_X16) != zenon_X158)
% 1.02/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X644)))
% 1.02/1.23  (member zenon_X775 (skf21 zenon_X159 zenon_X775 zenon_X776) zenon_X159)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) (skc20)))
% 1.02/1.23  (member (skc19) (skf21 (skc64) (skc19) zenon_X201) (skc64))
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X108))
% 1.02/1.23  (ssSkP0 zenon_X751 (skc63))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X155) zenon_X155)
% 1.02/1.23  ((skf21 zenon_X97 (skc19) zenon_X951) != zenon_X158)
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X159))
% 1.02/1.23  (ssSkP2 (skc65) (skc64) (skc63))
% 1.02/1.23  (fellow (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.02/1.23  (zenon_X772 != (skc19))
% 1.02/1.23  (member zenon_X913 (skf19 zenon_X15 zenon_X913 zenon_X97) zenon_X97)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X0) != zenon_X158)
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X155))
% 1.02/1.23  ((skf21 zenon_X16 (skc19) zenon_X895) != zenon_X154)
% 1.02/1.23  (member zenon_X179 (skf16 zenon_X8 zenon_X179 (skc20)) (skc20))
% 1.02/1.23  (-. (old (skc63) zenon_X495))
% 1.02/1.23  (ssSkP1 (skc72) (skc71) (skc63))
% 1.02/1.23  (zenon_X898 != (skc63))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X16))
% 1.02/1.23  (zenon_X801 != (skc19))
% 1.02/1.23  (zenon_X859 != (skc63))
% 1.02/1.23  ((skc68) != zenon_X706)
% 1.02/1.23  ((skc20) != zenon_X611)
% 1.02/1.23  ((skf11 (skc63) zenon_X159) != zenon_X152)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X659))
% 1.02/1.23  (zenon_X198 != (skc19))
% 1.02/1.23  ((skf11 (skc63) zenon_X155) != zenon_X160)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X636))
% 1.02/1.23  (zenon_X11 != zenon_X155)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X161))
% 1.02/1.23  (member (skc19) (skf21 zenon_X9 (skc19) zenon_X807) zenon_X9)
% 1.02/1.23  (zenon_X16 != zenon_X9)
% 1.02/1.23  ((skf11 (skc63) zenon_X153) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X659))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X659 (skc19) zenon_X940))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X153 (skc19) zenon_X842))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X108) != zenon_X152)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X0))
% 1.02/1.23  ((skf11 (skc19) (skc20)) != zenon_X158)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X16))
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X537) zenon_X537)
% 1.02/1.23  (member zenon_X778 (skf11 zenon_X778 zenon_X155) zenon_X155)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X16))
% 1.02/1.23  (zenon_X108 != zenon_X161)
% 1.02/1.23  (-. (coat (skc19) (skf23 (skc19) zenon_X625)))
% 1.02/1.23  (zenon_X172 != (skc19))
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X9) zenon_X9)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X16))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) (skc20)) (skc20))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X659) zenon_X659)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X640))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X9))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X159) zenon_X159)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X659) zenon_X659)
% 1.02/1.23  (-. (fellow zenon_X24 (skf11 zenon_X24 (skc20))))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X97) zenon_X97)
% 1.02/1.23  ((skf21 zenon_X161 (skc19) zenon_X793) != zenon_X154)
% 1.02/1.23  (member zenon_X801 (skf16 zenon_X8 zenon_X801 zenon_X153) zenon_X153)
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) (skc64)))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X2)
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X9))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X659))
% 1.02/1.23  (zenon_X659 != zenon_X97)
% 1.02/1.23  (zenon_X169 != (skc19))
% 1.02/1.23  (young (skc19) (skf23 (skc19) (skc20)))
% 1.02/1.23  (zenon_X537 != (skc64))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X16) zenon_X16)
% 1.02/1.23  ((skf21 zenon_X9 (skc19) zenon_X807) != zenon_X158)
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X11))
% 1.02/1.23  ((skf11 (skc19) zenon_X155) != zenon_X154)
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X659))
% 1.02/1.23  (member zenon_X213 (skf11 zenon_X213 (skc20)) (skc20))
% 1.02/1.23  (member zenon_X13 (skf21 zenon_X11 zenon_X13 zenon_X14) zenon_X11)
% 1.02/1.23  ((skf23 (skc19) (skc20)) != zenon_X7)
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X97) zenon_X97)
% 1.02/1.23  (member zenon_X930 (skf16 zenon_X8 zenon_X930 zenon_X659) zenon_X659)
% 1.02/1.23  (young (skc63) (skf21 zenon_X537 (skc63) zenon_X838))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X16))
% 1.02/1.23  (young (skc63) (skf21 zenon_X97 (skc63) zenon_X950))
% 1.02/1.23  (zenon_X9 != zenon_X159)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X159))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X11) zenon_X11)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X11))
% 1.02/1.23  (street (skc19) (skc24))
% 1.02/1.23  ((skf23 (skc19) (skc20)) != zenon_X5)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X9))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X11))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X16))
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X153) zenon_X153)
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) (skc20)))
% 1.02/1.23  ((skc68) != zenon_X704)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X153))
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X108))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X159) != zenon_X154)
% 1.02/1.23  (-. (member (skc63) zenon_X4 (skc64)))
% 1.02/1.23  (zenon_X108 != zenon_X159)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X108) zenon_X108)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X97) != zenon_X158)
% 1.02/1.23  (cheap (skc63) (skf11 (skc63) (skc64)))
% 1.02/1.23  ((skc71) != zenon_X688)
% 1.02/1.23  ((skc22) != zenon_X611)
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X659) zenon_X659)
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X97) zenon_X97)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X537) != zenon_X158)
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X108) zenon_X108)
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X11) zenon_X11)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X108))
% 1.02/1.23  (member zenon_X808 (skf11 zenon_X808 zenon_X9) zenon_X9)
% 1.02/1.23  (zenon_X108 != zenon_X155)
% 1.02/1.23  ((skf21 zenon_X16 (skc19) zenon_X895) != zenon_X158)
% 1.02/1.23  ((skf23 (skc19) zenon_X11) != zenon_X158)
% 1.02/1.23  (zenon_X886 != (skc63))
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X161))
% 1.02/1.23  (-. (group (skc63) zenon_X685))
% 1.02/1.23  (member (skc63) (skf21 zenon_X161 (skc63) zenon_X771) zenon_X161)
% 1.02/1.23  ((skf23 (skc63) zenon_X161) != zenon_X160)
% 1.02/1.23  (zenon_X16 != (skc64))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X9))
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X153))
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) (skc20)))
% 1.02/1.23  (zenon_X775 != (skc63))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X155) != zenon_X160)
% 1.02/1.23  (zenon_X918 != (skc63))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X108) zenon_X108)
% 1.02/1.23  ((skf11 (skc63) zenon_X9) != zenon_X152)
% 1.02/1.23  (placename (skc19) (skc25))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) (skc20)))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X0) zenon_X0)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X16 (skc63) zenon_X877))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X599))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X537) != zenon_X154)
% 1.02/1.23  (two (skc63) (skc71))
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X161))
% 1.02/1.23  (young (skc63) (skf21 zenon_X159 (skc63) zenon_X780))
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X153))
% 1.02/1.23  (member zenon_X164 (skf16 zenon_X8 zenon_X164 (skc64)) (skc64))
% 1.02/1.23  (zenon_X867 != (skc19))
% 1.02/1.23  (member (skc63) (skf21 zenon_X159 (skc63) zenon_X780) zenon_X159)
% 1.02/1.23  (member zenon_X785 (skf19 zenon_X15 zenon_X785 zenon_X159) zenon_X159)
% 1.02/1.23  (zenon_X896 != (skc63))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X11) != zenon_X158)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X659) != zenon_X160)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X9))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X161))
% 1.02/1.23  (zenon_X9 != (skc20))
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X11) zenon_X11)
% 1.02/1.23  (-. (two zenon_X112 zenon_X111))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X3)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X158)
% 1.02/1.23  ((skf21 (skc20) (skc63) zenon_X237) != zenon_X152)
% 1.02/1.23  (zenon_X11 != zenon_X0)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X159))
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X0))
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X9))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X659) zenon_X659)
% 1.02/1.23  (placename (skc63) (skc68))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X16) != zenon_X152)
% 1.02/1.23  (member zenon_X169 (skf21 (skc64) zenon_X169 zenon_X170) (skc64))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X11))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X159))
% 1.02/1.23  ((skc64) != zenon_X691)
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X659))
% 1.02/1.23  (young (skc63) (skf21 zenon_X11 (skc63) zenon_X764))
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X659))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X108) != zenon_X160)
% 1.02/1.23  (young (skc63) (skf21 zenon_X155 (skc63) zenon_X894))
% 1.02/1.23  (zenon_X16 != zenon_X159)
% 1.02/1.23  (zenon_X785 != (skc63))
% 1.02/1.23  ((skf21 zenon_X155 (skc63) zenon_X894) != zenon_X152)
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X537))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X11) != zenon_X152)
% 1.02/1.23  (present zenon_X56 (skf17 zenon_X56 zenon_X62 zenon_X60))
% 1.02/1.23  (zenon_X16 != zenon_X108)
% 1.02/1.23  (-. (member (skc63) zenon_X152 (skc20)))
% 1.02/1.23  (-. (member (skc63) zenon_X160 (skc64)))
% 1.02/1.23  ((skf11 (skc63) zenon_X108) != zenon_X152)
% 1.02/1.23  (zenon_X108 != zenon_X0)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X9) != zenon_X154)
% 1.02/1.23  (zenon_X16 != zenon_X659)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X659) != zenon_X160)
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X0))
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X0))
% 1.02/1.23  ((skf11 (skc63) zenon_X97) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X152)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X97) != zenon_X154)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X97))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.02/1.23  (member (skc19) (skf21 (skc20) (skc19) zenon_X235) (skc20))
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X537))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X537) zenon_X537)
% 1.02/1.23  (zenon_X11 != zenon_X159)
% 1.02/1.23  (zenon_X659 != zenon_X153)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X11) zenon_X11)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X0))
% 1.02/1.23  (young (skc19) (skf21 zenon_X159 (skc19) zenon_X777))
% 1.02/1.23  (zenon_X836 != (skc19))
% 1.02/1.23  (zenon_X896 != (skc19))
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X97) zenon_X97)
% 1.02/1.23  (member zenon_X787 (skf21 zenon_X108 zenon_X787 zenon_X788) zenon_X108)
% 1.02/1.23  ((skc71) != zenon_X676)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X11))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.02/1.23  (member zenon_X867 (skf21 zenon_X0 zenon_X867 zenon_X868) zenon_X0)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X16))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != zenon_X3)
% 1.02/1.23  (zenon_X166 != (skc19))
% 1.02/1.23  ((skf11 (skc63) zenon_X0) != zenon_X152)
% 1.02/1.23  (young (skc19) (skf23 (skc19) (skc64)))
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) (skc64)))
% 1.02/1.23  (young (skc63) (skf21 zenon_X161 (skc63) zenon_X771))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X158)
% 1.02/1.23  (member zenon_X825 (skf11 zenon_X825 zenon_X108) zenon_X108)
% 1.02/1.23  (be zenon_X37 (skf13 zenon_X37 zenon_X41 zenon_X38) zenon_X38 (skf12 zenon_X38 zenon_X37 zenon_X41))
% 1.02/1.23  ((skc64) != zenon_X632)
% 1.02/1.23  (-. (old (skc19) zenon_X519))
% 1.02/1.23  (old (skc19) (skc27))
% 1.02/1.23  (zenon_X659 != zenon_X537)
% 1.02/1.23  (young (skc19) (skf21 zenon_X155 (skc19) zenon_X893))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X603))
% 1.02/1.23  (zenon_X11 != (skc20))
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X161) zenon_X161)
% 1.02/1.23  (member zenon_X779 (skf11 zenon_X779 zenon_X159) zenon_X159)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X659))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != zenon_X152)
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) zenon_X659))
% 1.02/1.23  (zenon_X164 != (skc19))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X16))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X97))
% 1.02/1.23  (zenon_X848 != (skc19))
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X9) zenon_X9)
% 1.02/1.23  ((skf23 (skc63) zenon_X159) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X537))
% 1.02/1.23  ((skc65) != zenon_X688)
% 1.02/1.23  (member (skc63) (skf21 zenon_X16 (skc63) zenon_X877) zenon_X16)
% 1.02/1.23  (zenon_X93 != (skc63))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X16) != zenon_X154)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X659))
% 1.02/1.23  (-. (fellow zenon_X24 (skf11 zenon_X24 zenon_X25)))
% 1.02/1.23  (member (skc19) (skf23 (skc19) (skc20)) (skc20))
% 1.02/1.23  (member zenon_X802 (skf19 zenon_X15 zenon_X802 zenon_X9) zenon_X9)
% 1.02/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X7)
% 1.02/1.23  (zenon_X899 != (skc63))
% 1.02/1.23  ((skc63) != (skc19))
% 1.02/1.23  (zenon_X802 != (skc19))
% 1.02/1.23  ((skc19) != zenon_X21)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X4)
% 1.02/1.23  ((skc64) != (skc20))
% 1.02/1.23  (member (skc63) (skf11 (skc63) (skc20)) (skc20))
% 1.02/1.23  (young (skc63) (skf23 (skc63) zenon_X0))
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != (skf23 (skc63) zenon_X603))
% 1.02/1.23  ((skf23 (skc19) zenon_X161) != zenon_X158)
% 1.02/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X154)
% 1.02/1.23  ((skf21 zenon_X153 (skc19) zenon_X842) != zenon_X158)
% 1.02/1.23  (black (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X537) != zenon_X160)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X152)
% 1.02/1.23  ((skf23 (skc19) (skc64)) != zenon_X158)
% 1.02/1.23  ((skc68) != zenon_X718)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X159))
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X11))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X9) zenon_X9)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X108))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X11))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X694))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X9) != zenon_X152)
% 1.02/1.23  (member (skc19) (skf21 zenon_X155 (skc19) zenon_X893) zenon_X155)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X97))
% 1.02/1.23  ((skf11 (skc19) zenon_X537) != zenon_X154)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X16))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X0) zenon_X0)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X161))
% 1.02/1.23  ((skf11 (skc63) zenon_X16) != zenon_X160)
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X161))
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X97) zenon_X97)
% 1.02/1.23  ((skc65) != zenon_X691)
% 1.02/1.23  ((skf23 (skc63) zenon_X0) != zenon_X160)
% 1.02/1.23  (young (skc63) (skf21 (skc64) (skc63) zenon_X236))
% 1.02/1.23  (present (skc63) (skc66))
% 1.02/1.23  (ssSkP2 (skc21) (skc20) (skc19))
% 1.02/1.23  (zenon_X537 != zenon_X9)
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X108))
% 1.02/1.23  ((skf11 (skc63) zenon_X537) != zenon_X160)
% 1.02/1.23  ((skf21 (skc64) (skc63) zenon_X236) != zenon_X2)
% 1.02/1.23  (zenon_X798 != (skc63))
% 1.02/1.23  ((skf21 zenon_X159 (skc63) zenon_X780) != zenon_X152)
% 1.02/1.23  ((skf11 (skc19) zenon_X108) != zenon_X154)
% 1.02/1.23  (-. (city (skc63) zenon_X723))
% 1.02/1.23  ((skf23 (skc63) zenon_X11) != zenon_X152)
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X159 (skc19) zenon_X777))
% 1.02/1.23  (zenon_X213 != (skc63))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X537) zenon_X537)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X155))
% 1.02/1.23  (zenon_X899 != (skc19))
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X155) zenon_X155)
% 1.02/1.23  (zenon_X0 != zenon_X159)
% 1.02/1.23  ((skf11 (skc63) (skc64)) != zenon_X160)
% 1.02/1.23  (zenon_X16 != zenon_X0)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X159))
% 1.02/1.23  (ssSkP1 (skc27) (skc22) (skc19))
% 1.02/1.23  (zenon_X179 != (skc19))
% 1.02/1.23  ((skc67) != zenon_X588)
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X9) zenon_X9)
% 1.02/1.23  (-. (member (skc63) zenon_X152 (skc64)))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != zenon_X4)
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X155))
% 1.02/1.23  ((skf23 (skc63) (skc20)) != zenon_X152)
% 1.02/1.23  (-. (group (skc63) zenon_X688))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X659) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf11 (skc19) zenon_X155) zenon_X155)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X97) != zenon_X160)
% 1.02/1.23  (young (skc63) (skf21 zenon_X153 (skc63) zenon_X800))
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X153))
% 1.02/1.23  (member (skc19) (skf21 zenon_X97 (skc19) zenon_X951) zenon_X97)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X161))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X698))
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X16))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X652))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) (skc64)))
% 1.02/1.23  (zenon_X1 != (skc19))
% 1.02/1.23  (young (skc63) (skf21 zenon_X659 (skc63) zenon_X939))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X161) != zenon_X154)
% 1.02/1.23  (young (skc19) (skf21 zenon_X161 (skc19) zenon_X793))
% 1.02/1.23  (-. (member (skc63) zenon_X160 zenon_X16))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X153))
% 1.02/1.23  ((skc68) != zenon_X721)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X97) zenon_X97)
% 1.02/1.23  (member zenon_X790 (skf11 zenon_X790 zenon_X659) zenon_X659)
% 1.02/1.23  ((skf21 zenon_X537 (skc19) zenon_X882) != zenon_X158)
% 1.02/1.23  (young (skc63) (skf23 (skc63) (skc64)))
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X161) zenon_X161)
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X11) zenon_X11)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X160)
% 1.02/1.23  ((skf11 (skc19) (skc20)) != zenon_X6)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X155) != zenon_X154)
% 1.02/1.23  (member zenon_X804 (skf21 zenon_X9 zenon_X804 zenon_X805) zenon_X9)
% 1.02/1.23  ((skf21 zenon_X153 (skc63) zenon_X800) != zenon_X160)
% 1.02/1.23  (actual_world (skc19))
% 1.02/1.23  ((skc20) != zenon_X159)
% 1.02/1.23  (member (skc63) (skf23 (skc63) zenon_X108) zenon_X108)
% 1.02/1.23  ((skf21 zenon_X161 (skc19) zenon_X793) != zenon_X158)
% 1.02/1.23  ((skf11 (skc19) zenon_X659) != zenon_X158)
% 1.02/1.23  ((skc64) != zenon_X599)
% 1.02/1.23  ((skf21 zenon_X0 (skc63) zenon_X870) != zenon_X152)
% 1.02/1.23  (young (skc63) (skf11 (skc63) zenon_X0))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X153))
% 1.02/1.23  (zenon_X897 != (skc19))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != (skf23 (skc63) zenon_X599))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X537) != zenon_X158)
% 1.02/1.23  (zenon_X918 != (skc19))
% 1.02/1.23  (zenon_X13 != (skc63))
% 1.02/1.23  ((skf11 (skc19) zenon_X0) != zenon_X158)
% 1.02/1.23  (-. (street (skc19) zenon_X548))
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X16))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X97))
% 1.02/1.23  ((skc64) != zenon_X676)
% 1.02/1.23  ((skf23 (skc63) zenon_X9) != zenon_X152)
% 1.02/1.23  ((skf23 (skc63) zenon_X16) != zenon_X152)
% 1.02/1.23  ((skf23 (skc63) zenon_X11) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X659))
% 1.02/1.23  ((skf21 zenon_X16 (skc63) zenon_X877) != zenon_X160)
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X0))
% 1.02/1.23  (zenon_X898 != (skc19))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X659) zenon_X659)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X11))
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X155))
% 1.02/1.23  (member zenon_X848 (skf16 zenon_X8 zenon_X848 zenon_X11) zenon_X11)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X97))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X537))
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X159))
% 1.02/1.23  (young (skc63) (skf21 (skc20) (skc63) zenon_X237))
% 1.02/1.23  ((skf21 (skc20) (skc19) zenon_X235) != zenon_X158)
% 1.02/1.23  (young (skc19) (skf11 (skc19) zenon_X16))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != (skf23 (skc63) zenon_X636))
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X537))
% 1.02/1.23  (member zenon_X172 (skf19 zenon_X15 zenon_X172 (skc64)) (skc64))
% 1.02/1.23  (young (skc19) (skf23 (skc19) zenon_X108))
% 1.02/1.23  (zenon_X886 != (skc19))
% 1.02/1.23  (-. (old (skc19) zenon_X511))
% 1.02/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X603)))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X659) zenon_X659)
% 1.02/1.23  (cheap (skc63) (skf23 (skc63) (skc64)))
% 1.02/1.23  (lonely (skc63) (skc67))
% 1.02/1.23  (young (skc19) (skf16 zenon_X8 (skc19) zenon_X97))
% 1.02/1.23  ((skf21 zenon_X9 (skc63) zenon_X806) != zenon_X160)
% 1.02/1.23  (zenon_X863 != (skc19))
% 1.02/1.23  (zenon_X787 != (skc19))
% 1.02/1.23  (zenon_X778 != (skc63))
% 1.02/1.23  (zenon_X960 != (skc19))
% 1.02/1.23  ((skf11 (skc63) zenon_X153) != zenon_X152)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X155) zenon_X155)
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X155))
% 1.02/1.23  (zenon_X659 != zenon_X161)
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) (skc20)))
% 1.02/1.23  (member (skc19) (skf11 (skc19) (skc20)) (skc20))
% 1.02/1.23  (-. (street (skc63) zenon_X570))
% 1.02/1.23  (zenon_X108 != zenon_X97)
% 1.02/1.23  (zenon_X101 != (skc19))
% 1.02/1.23  ((skf23 (skc63) (skc64)) != zenon_X4)
% 1.02/1.23  (member (skc63) (skf21 (skc64) (skc63) zenon_X236) (skc64))
% 1.02/1.23  ((skc63) != zenon_X486)
% 1.02/1.23  (zenon_X848 != (skc63))
% 1.02/1.23  (young (skc63) (skf21 zenon_X16 (skc63) zenon_X877))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X11 (skc19) zenon_X855))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) (skc20)))
% 1.02/1.23  (zenon_X97 != zenon_X155)
% 1.02/1.23  (zenon_X779 != (skc63))
% 1.02/1.23  (group (skc19) (skc22))
% 1.02/1.23  (member (skc63) (skf11 (skc63) zenon_X11) zenon_X11)
% 1.02/1.23  (zenon_X790 != (skc63))
% 1.02/1.23  (zenon_X11 != zenon_X108)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) zenon_X108))
% 1.02/1.23  (-. (group (skc63) zenon_X679))
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X11))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X153) zenon_X153)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X16) zenon_X16)
% 1.02/1.23  ((skc21) != zenon_X594)
% 1.02/1.23  ((skc71) != zenon_X682)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X537) != zenon_X152)
% 1.02/1.23  (zenon_X802 != (skc63))
% 1.02/1.23  (ssSkP2 zenon_X89 zenon_X91 zenon_X87)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X0))
% 1.02/1.23  (member zenon_X93 (skf23 zenon_X93 zenon_X537) zenon_X537)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X5)
% 1.02/1.23  (member zenon_X836 (skf21 zenon_X537 zenon_X836 zenon_X837) zenon_X537)
% 1.02/1.23  ((skf21 zenon_X155 (skc19) zenon_X893) != zenon_X154)
% 1.02/1.23  ((skc20) != zenon_X161)
% 1.02/1.23  (fellow (skc19) (skf23 (skc19) zenon_X161))
% 1.02/1.23  (-. (member (skc63) zenon_X3 (skc64)))
% 1.02/1.23  (patient zenon_X82 (skf17 zenon_X82 zenon_X83 zenon_X85) zenon_X85)
% 1.02/1.23  (-. (member (skc19) zenon_X158 (skc64)))
% 1.02/1.23  ((skf11 (skc63) (skc64)) != (skf23 (skc63) zenon_X632))
% 1.02/1.23  (zenon_X93 != (skc19))
% 1.02/1.23  ((skf11 (skc19) (skc64)) != zenon_X158)
% 1.02/1.23  (zenon_X153 != zenon_X161)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X108) != zenon_X160)
% 1.02/1.23  (zenon_X17 != (skc63))
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X108))
% 1.02/1.23  (young (skc19) (skf21 zenon_X0 (skc19) zenon_X869))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X712))
% 1.02/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X652)))
% 1.02/1.23  (fellow (skc19) (skf11 (skc19) zenon_X0))
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X537 (skc63) zenon_X838))
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X159) != zenon_X158)
% 1.02/1.23  (-. (member (skc19) zenon_X158 zenon_X97))
% 1.02/1.23  (-. (coat (skc63) (skf23 (skc63) zenon_X636)))
% 1.02/1.23  (young (skc63) (skf19 zenon_X15 (skc63) (skc20)))
% 1.02/1.23  (young (skc63) (skf16 zenon_X8 (skc63) zenon_X97))
% 1.02/1.23  (zenon_X537 != zenon_X0)
% 1.02/1.23  (member zenon_X815 (skf16 zenon_X8 zenon_X815 zenon_X16) zenon_X16)
% 1.02/1.23  (fellow (skc63) (skf19 zenon_X15 (skc63) (skc20)))
% 1.02/1.23  (zenon_X16 != zenon_X153)
% 1.02/1.23  ((skf11 (skc19) zenon_X537) != zenon_X158)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X0) != zenon_X160)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X153))
% 1.02/1.23  (-. (hollywood_placename (skc63) zenon_X718))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X16) != zenon_X160)
% 1.02/1.23  ((skc68) != zenon_X716)
% 1.02/1.23  (fellow (skc63) (skf11 (skc63) zenon_X153))
% 1.02/1.23  (zenon_X779 != (skc19))
% 1.02/1.23  (zenon_X9 != (skc64))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X0) != zenon_X152)
% 1.02/1.23  (member (skc63) (skf23 (skc63) (skc20)) (skc20))
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) (skc20)))
% 1.02/1.23  (zenon_X769 != (skc19))
% 1.02/1.23  ((skf23 (skc19) zenon_X0) != zenon_X154)
% 1.02/1.23  (zenon_X931 != (skc63))
% 1.02/1.23  (fellow (skc19) (skf21 zenon_X108 (skc19) zenon_X789))
% 1.02/1.23  ((skf21 zenon_X537 (skc63) zenon_X838) != zenon_X152)
% 1.02/1.23  (zenon_X863 != (skc63))
% 1.02/1.23  ((skf21 zenon_X159 (skc19) zenon_X777) != zenon_X158)
% 1.02/1.23  (fellow (skc63) (skf16 zenon_X8 (skc63) zenon_X9))
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X153) != zenon_X160)
% 1.02/1.23  (zenon_X931 != (skc19))
% 1.02/1.23  (zenon_X778 != (skc19))
% 1.02/1.23  (member (skc19) (skf21 zenon_X108 (skc19) zenon_X789) zenon_X108)
% 1.02/1.23  (white (skc19) (skc27))
% 1.02/1.23  ((skf11 (skc19) zenon_X108) != zenon_X158)
% 1.02/1.23  (member (skc19) (skf19 zenon_X15 (skc19) zenon_X16) zenon_X16)
% 1.02/1.23  ((skc71) != zenon_X583)
% 1.02/1.23  (fellow (skc63) (skf21 zenon_X97 (skc63) zenon_X950))
% 1.02/1.23  ((skc63) != zenon_X24)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) (skc64)) != zenon_X152)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) zenon_X155) zenon_X155)
% 1.02/1.23  (member (skc63) (skf16 zenon_X8 (skc63) zenon_X16) zenon_X16)
% 1.02/1.23  ((skf21 zenon_X11 (skc19) zenon_X855) != zenon_X158)
% 1.02/1.23  ((skf19 zenon_X15 (skc63) (skc64)) != zenon_X3)
% 1.02/1.23  (zenon_X756 != (skc63))
% 1.02/1.23  ((skf21 zenon_X161 (skc63) zenon_X771) != zenon_X160)
% 1.02/1.23  (fellow (skc19) (skf19 zenon_X15 (skc19) zenon_X161))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc20)) != zenon_X6)
% 1.02/1.23  ((skf21 zenon_X108 (skc63) zenon_X809) != zenon_X152)
% 1.02/1.23  (member (skc19) (skf23 (skc19) zenon_X0) zenon_X0)
% 1.02/1.23  (zenon_X101 != (skc63))
% 1.02/1.23  (zenon_X859 != (skc19))
% 1.02/1.23  ((skf23 (skc19) zenon_X155) != zenon_X158)
% 1.02/1.23  (-. (group (skc63) zenon_X682))
% 1.02/1.23  ((skf19 zenon_X15 (skc63) zenon_X16) != zenon_X152)
% 1.02/1.23  ((skf21 (skc64) (skc19) zenon_X201) != zenon_X154)
% 1.02/1.23  (member (skc19) (skf16 zenon_X8 (skc19) (skc20)) (skc20))
% 1.02/1.23  (zenon_X17 != (skc19))
% 1.02/1.23  ((skf19 zenon_X15 (skc19) zenon_X659) != zenon_X154)
% 1.02/1.23  (member (skc63) (skf21 zenon_X0 (skc63) zenon_X870) zenon_X0)
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X108) zenon_X108)
% 1.02/1.23  (-. (group (skc63) zenon_X691))
% 1.02/1.23  ((skf11 (skc19) zenon_X155) != zenon_X158)
% 1.02/1.23  ((skf19 zenon_X15 (skc19) (skc64)) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) (skc20)) != zenon_X6)
% 1.02/1.23  ((skc24) != zenon_X557)
% 1.02/1.23  ((skc64) != zenon_X616)
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X16) zenon_X16)
% 1.02/1.23  (fellow (skc63) (skf23 (skc63) zenon_X108))
% 1.02/1.23  ((skf21 zenon_X153 (skc19) zenon_X842) != zenon_X154)
% 1.02/1.23  (zenon_X16 != zenon_X537)
% 1.02/1.23  (zenon_X97 != zenon_X153)
% 1.02/1.23  ((skf11 (skc19) zenon_X161) != zenon_X158)
% 1.02/1.23  ((skc20) != zenon_X155)
% 1.02/1.23  (-. (frontseat (skc63) (skc70)))
% 1.02/1.23  (member zenon_X1 (skf11 zenon_X1 zenon_X0) zenon_X0)
% 1.02/1.23  ((skf23 (skc19) zenon_X97) != zenon_X158)
% 1.02/1.23  (zenon_X937 != (skc19))
% 1.02/1.23  (member (skc63) (skf21 zenon_X11 (skc63) zenon_X764) zenon_X11)
% 1.02/1.23  (chevy (skc19) (skc27))
% 1.02/1.23  (zenon_X948 != (skc63))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) zenon_X0) zenon_X0)
% 1.02/1.23  (young (skc19) (skf19 zenon_X15 (skc19) zenon_X537))
% 1.02/1.23  (member (skc63) (skf19 zenon_X15 (skc63) (skc64)) (skc64))
% 1.02/1.23  (fellow (skc19) (skf16 zenon_X8 (skc19) zenon_X9))
% 1.02/1.23  ((skc68) != zenon_X724)
% 1.02/1.23  ((skf16 zenon_X8 (skc63) zenon_X537) != zenon_X152)
% 1.02/1.23  (-. (member (skc19) zenon_X154 zenon_X537))
% 1.02/1.23  ((skf21 zenon_X155 (skc19) zenon_X893) != zenon_X158)
% 1.02/1.23  ((skf16 zenon_X8 (skc19) zenon_X161) != zenon_X158)
% 1.02/1.23  (member zenon_X878 (skf19 zenon_X15 zenon_X878 zenon_X659) zenon_X659)
% 1.02/1.23  ((skf11 (skc19) zenon_X9) != zenon_X158)
% 1.02/1.23  (zenon_X815 != (skc19))
% 1.02/1.23  (member zenon_X948 (skf21 zenon_X97 zenon_X948 zenon_X949) zenon_X97)
% 1.02/1.23  (-. (member (skc63) zenon_X152 zenon_X9))
% 1.02/1.23  (zenon_X867 != (skc63))
% 1.02/1.23  (event (skc19) (skc23))
% 1.02/1.23  *)
% 1.02/1.23  (* NO-PROOF *)
% 1.02/1.23  % SZS status GaveUp
% 1.02/1.23  Number of rewrites on terms: 0
% 1.02/1.23  Number of rewrites on props: 0
% 1.02/1.23  nodes searched: 19360
% 1.02/1.23  max branch formulas: 3003
% 1.02/1.23  proof nodes created: 1304
% 1.02/1.23  formulas created: 66476
% 1.02/1.23  
%------------------------------------------------------------------------------