↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n002.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:28 EDT 2024

% Result   : Unknown 0.90s 1.09s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : NLP160-1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.13  % Command  : run_zenon_modulo %d %s
% 0.13/0.34  % Computer : n002.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Sat Jun 22 22:25:38 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 0.90/1.08  Zenon error: exhausted search space without finding a proof
% 0.90/1.08  (* Current branch:
% 0.90/1.08  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X9))
% 0.90/1.08  (member (skc18) (skf10 (skc18) zenon_X149) zenon_X149)
% 0.90/1.08  (zenon_X177 != (skc18))
% 0.90/1.08  (zenon_X540 != (skc18))
% 0.90/1.08  ((skf19 zenon_X15 (skc62) (skc19)) != zenon_X148)
% 0.90/1.08  ((skf21 zenon_X0 (skc62) zenon_X584) != zenon_X148)
% 0.90/1.08  (young (skc18) (skf11 (skc18) zenon_X181))
% 0.90/1.08  (-. (member (skc18) zenon_X150 zenon_X97))
% 0.90/1.08  ((skf21 (skc19) (skc18) zenon_X228) != (skf10 (skc18) zenon_X321))
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X0))
% 0.90/1.08  (-. (member (skc18) zenon_X7 (skc19)))
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X181))
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X181) != zenon_X157)
% 0.90/1.08  (fellow (skc62) (skf11 (skc62) (skc63)))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X11) != zenon_X150)
% 0.90/1.08  (zenon_X541 != (skc18))
% 0.90/1.08  ((skf21 zenon_X9 (skc18) zenon_X542) != zenon_X150)
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X198) != zenon_X148)
% 0.90/1.08  (zenon_X0 != zenon_X158)
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X11) zenon_X11)
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X0) != zenon_X157)
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X97) != zenon_X157)
% 0.90/1.08  (young (skc18) (skf10 (skc18) zenon_X106))
% 0.90/1.08  (-. (barrel (skc62) zenon_X246))
% 0.90/1.08  (zenon_X185 != (skc62))
% 0.90/1.08  ((skc21) != zenon_X382)
% 0.90/1.08  ((skf10 (skc18) zenon_X11) != zenon_X155)
% 0.90/1.08  (-. (member (skc18) zenon_X150 zenon_X158))
% 0.90/1.08  (-. (coat (skc18) (skf10 (skc18) zenon_X321)))
% 0.90/1.08  (member zenon_X502 (skf21 zenon_X16 zenon_X502 zenon_X503) zenon_X16)
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X16) zenon_X16)
% 0.90/1.08  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X97) zenon_X97)
% 0.90/1.08  ((skf10 (skc18) zenon_X16) != zenon_X150)
% 0.90/1.08  (member (skc18) (skf10 (skc18) zenon_X156) zenon_X156)
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X11) != zenon_X157)
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X198) zenon_X198)
% 0.90/1.08  ((skf11 (skc18) zenon_X181) != zenon_X150)
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) zenon_X198))
% 0.90/1.08  ((skf11 (skc18) zenon_X158) != zenon_X150)
% 0.90/1.08  (zenon_X158 != zenon_X198)
% 0.90/1.08  (-. (group (skc18) zenon_X374))
% 0.90/1.08  ((skf21 zenon_X149 (skc18) zenon_X543) != zenon_X155)
% 0.90/1.08  (old (skc18) (skc26))
% 0.90/1.08  (-. (group (skc18) zenon_X371))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X0) != zenon_X155)
% 0.90/1.08  (-. (member (skc62) zenon_X148 zenon_X149))
% 0.90/1.08  (-. (group (skc18) zenon_X382))
% 0.90/1.08  (two (skc62) (skc65))
% 0.90/1.08  (member (skc62) (skf10 (skc62) zenon_X97) zenon_X97)
% 0.90/1.08  (member zenon_X162 (skf16 zenon_X8 zenon_X162 (skc63)) (skc63))
% 0.90/1.08  (zenon_X499 != (skc18))
% 0.90/1.08  (-. (group (skc62) zenon_X946))
% 0.90/1.08  (member (skc18) (skf11 (skc18) zenon_X156) zenon_X156)
% 0.90/1.08  (young (skc18) (skf16 zenon_X8 (skc18) (skc63)))
% 0.90/1.08  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X158))
% 0.90/1.08  (present (skc18) (skc22))
% 0.90/1.08  ((skc64) != zenon_X298)
% 0.90/1.08  ((skc21) != zenon_X371)
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) (skc19)) (skc19))
% 0.90/1.08  ((skf21 zenon_X158 (skc62) zenon_X668) != zenon_X148)
% 0.90/1.08  (young (skc18) (skf11 (skc18) zenon_X151))
% 0.90/1.08  (black (skc18) (skf11 (skc18) (skc19)))
% 0.90/1.08  (-. (old (skc62) zenon_X186))
% 0.90/1.08  ((skf10 (skc18) (skc63)) != zenon_X155)
% 0.90/1.08  ((skf11 (skc18) (skc63)) != (skf11 zenon_X24 zenon_X25))
% 0.90/1.08  (-. (ssSkP0 zenon_X23 zenon_X21))
% 0.90/1.08  (member zenon_X487 (skf11 zenon_X487 zenon_X156) zenon_X156)
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X158))
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) (skc19)))
% 0.90/1.08  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X151) zenon_X151)
% 0.90/1.08  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X9))
% 0.90/1.08  ((skc67) != zenon_X940)
% 0.90/1.08  ((skc25) != zenon_X412)
% 0.90/1.08  ((skf11 (skc62) zenon_X0) != zenon_X157)
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X149) zenon_X149)
% 0.90/1.08  (zenon_X641 != (skc62))
% 0.90/1.08  ((skc24) != zenon_X387)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X149) != zenon_X155)
% 0.90/1.08  ((skf11 (skc18) (skc19)) != (skf10 (skc18) zenon_X341))
% 0.90/1.08  ((skf11 (skc62) zenon_X106) != zenon_X148)
% 0.90/1.08  ((skf11 (skc62) (skc19)) != zenon_X157)
% 0.90/1.08  ((skc26) != zenon_X220)
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X156))
% 0.90/1.08  (young (skc18) (skf19 zenon_X15 (skc18) (skc19)))
% 0.90/1.08  (member zenon_X177 (skf16 zenon_X8 zenon_X177 (skc19)) (skc19))
% 0.90/1.08  (zenon_X11 != zenon_X198)
% 0.90/1.08  ((skf21 zenon_X0 (skc18) zenon_X583) != zenon_X155)
% 0.90/1.08  ((skf11 (skc18) zenon_X16) != zenon_X155)
% 0.90/1.08  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X106) zenon_X106)
% 0.90/1.08  (zenon_X0 != zenon_X151)
% 0.90/1.08  (zenon_X170 != (skc18))
% 0.90/1.08  (zenon_X16 != zenon_X151)
% 0.90/1.08  (-. (hollywood_placename (skc18) zenon_X391))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 zenon_X198) zenon_X198)
% 0.90/1.08  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X198))
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) zenon_X156))
% 0.90/1.08  ((skf21 zenon_X106 (skc62) zenon_X640) != zenon_X157)
% 0.90/1.08  (young (skc18) (skf10 (skc18) zenon_X0))
% 0.90/1.08  (member (skc62) (skf21 zenon_X9 (skc62) zenon_X531) zenon_X9)
% 0.90/1.08  (member (skc18) (skf21 zenon_X106 (skc18) zenon_X639) zenon_X106)
% 0.90/1.08  ((skc62) != (skc18))
% 0.90/1.08  (zenon_X181 != zenon_X106)
% 0.90/1.08  (zenon_X666 != (skc18))
% 0.90/1.08  (member (skc18) (skf10 (skc18) zenon_X9) zenon_X9)
% 0.90/1.08  ((skf10 (skc18) (skc19)) != zenon_X150)
% 0.90/1.08  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X181) zenon_X181)
% 0.90/1.08  (member (skc18) (skf11 (skc18) zenon_X11) zenon_X11)
% 0.90/1.08  ((skf10 (skc18) zenon_X0) != zenon_X150)
% 0.90/1.08  (young (skc62) (skf11 (skc62) zenon_X11))
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) zenon_X106))
% 0.90/1.08  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X181))
% 0.90/1.08  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X0) zenon_X0)
% 0.90/1.08  (-. (member (skc62) zenon_X157 (skc63)))
% 0.90/1.08  ((skf21 (skc19) (skc18) zenon_X228) != zenon_X6)
% 0.90/1.08  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X16))
% 0.90/1.08  ((skf11 (skc62) zenon_X156) != zenon_X148)
% 0.90/1.08  ((skc18) != zenon_X18)
% 0.90/1.08  (lonely (skc18) (skc23))
% 0.90/1.08  (young (skc18) (skf21 zenon_X11 (skc18) zenon_X457))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 zenon_X9) zenon_X9)
% 0.90/1.08  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X0))
% 0.90/1.08  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X149))
% 0.90/1.08  ((skf21 zenon_X158 (skc62) zenon_X668) != zenon_X157)
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X106) != zenon_X155)
% 0.90/1.08  ((skf11 (skc18) (skc19)) != zenon_X5)
% 0.90/1.08  (-. (member (skc62) zenon_X157 zenon_X158))
% 0.90/1.08  (member (skc18) (skf21 (skc19) (skc18) zenon_X228) (skc19))
% 0.90/1.08  (member (skc18) (skf10 (skc18) zenon_X181) zenon_X181)
% 0.90/1.08  (ssSkP1 (skc70) (skc65) (skc62))
% 0.90/1.08  (zenon_X106 != (skc63))
% 0.90/1.08  ((skf11 (skc18) zenon_X9) != zenon_X155)
% 0.90/1.08  (-. (hollywood_placename (skc18) zenon_X403))
% 0.90/1.08  (-. (member (skc62) zenon_X157 zenon_X16))
% 0.90/1.08  (fellow (skc62) (skf10 (skc62) zenon_X0))
% 0.90/1.08  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X16))
% 0.90/1.08  (member zenon_X650 (skf21 zenon_X181 zenon_X650 zenon_X651) zenon_X181)
% 0.90/1.08  ((skc24) != zenon_X413)
% 0.90/1.08  (member zenon_X465 (skf11 zenon_X465 zenon_X149) zenon_X149)
% 0.90/1.08  (young (skc18) (skf21 zenon_X97 (skc18) zenon_X658))
% 0.90/1.08  ((skc20) != zenon_X379)
% 0.90/1.08  (zenon_X552 != (skc62))
% 0.90/1.08  (zenon_X16 != zenon_X149)
% 0.90/1.08  (-. (hollywood_placename (skc18) zenon_X399))
% 0.90/1.08  (young (skc62) (skf11 (skc62) zenon_X97))
% 0.90/1.08  (agent (skc62) (skc66) (skc70))
% 0.90/1.08  (-. (old (skc18) zenon_X220))
% 0.90/1.08  ((skf10 (skc62) zenon_X198) != zenon_X148)
% 0.90/1.08  ((skc24) != zenon_X391)
% 0.90/1.08  (member (skc62) (skf11 (skc62) (skc63)) (skc63))
% 0.90/1.08  (zenon_X571 != (skc62))
% 0.90/1.08  (street (skc18) (skc23))
% 0.90/1.08  (ssSkP0 zenon_X437 (skc62))
% 0.90/1.08  ((skf21 zenon_X151 (skc18) zenon_X578) != zenon_X155)
% 0.90/1.08  ((skf21 zenon_X198 (skc18) zenon_X569) != zenon_X155)
% 0.90/1.08  (barrel (skc62) (skc66))
% 0.90/1.08  (zenon_X539 != (skc62))
% 0.90/1.08  (zenon_X210 != (skc18))
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X156) != zenon_X157)
% 0.90/1.08  (-. (member (skc18) zenon_X150 zenon_X106))
% 0.90/1.08  (-. (member (skc18) zenon_X5 (skc19)))
% 0.90/1.08  ((skf10 (skc62) (skc19)) != zenon_X148)
% 0.90/1.08  (zenon_X97 != zenon_X9)
% 0.90/1.08  (young (skc62) (skf21 zenon_X9 (skc62) zenon_X531))
% 0.90/1.08  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X151))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X198) != zenon_X150)
% 0.90/1.08  (-. (member (skc18) zenon_X6 (skc19)))
% 0.90/1.08  (young (skc62) (skf11 (skc62) zenon_X0))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 zenon_X181) zenon_X181)
% 0.90/1.08  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X158))
% 0.90/1.08  ((skf10 (skc62) zenon_X151) != zenon_X148)
% 0.90/1.08  (zenon_X181 != zenon_X156)
% 0.90/1.08  ((skc21) != zenon_X365)
% 0.90/1.08  (-. (member (skc18) zenon_X155 zenon_X151))
% 0.90/1.08  ((skf21 zenon_X11 (skc18) zenon_X457) != zenon_X155)
% 0.90/1.08  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X198))
% 0.90/1.08  (coat (skc18) (skf11 (skc18) (skc19)))
% 0.90/1.08  (zenon_X11 != zenon_X9)
% 0.90/1.08  ((skf11 (skc62) (skc19)) != zenon_X148)
% 0.90/1.08  ((skf10 (skc62) (skc63)) != zenon_X4)
% 0.90/1.08  (fellow (skc62) (skf10 (skc62) zenon_X198))
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X198) != zenon_X157)
% 0.90/1.08  (zenon_X508 != (skc62))
% 0.90/1.08  (member (skc62) (skf10 (skc62) zenon_X151) zenon_X151)
% 0.90/1.08  ((skf21 zenon_X151 (skc62) zenon_X579) != zenon_X148)
% 0.90/1.08  (zenon_X571 != (skc18))
% 0.90/1.08  ((skf10 (skc18) zenon_X158) != zenon_X150)
% 0.90/1.08  (fellow (skc62) (skf11 (skc62) zenon_X16))
% 0.90/1.08  (member zenon_X10 (skf16 zenon_X8 zenon_X10 zenon_X9) zenon_X9)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X158) != zenon_X150)
% 0.90/1.08  (young (skc18) (skf11 (skc18) zenon_X156))
% 0.90/1.08  (member (skc62) (skf10 (skc62) zenon_X0) zenon_X0)
% 0.90/1.08  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X149))
% 0.90/1.08  (fellow (skc62) (skf21 zenon_X97 (skc62) zenon_X657))
% 0.90/1.08  (group (skc18) (skc20))
% 0.90/1.08  ((skf11 (skc18) zenon_X151) != zenon_X155)
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X9) zenon_X9)
% 0.90/1.08  (zenon_X17 != (skc62))
% 0.90/1.08  (zenon_X16 != zenon_X156)
% 0.90/1.08  (street (skc62) (skc67))
% 0.90/1.08  (member (skc62) (skf21 zenon_X97 (skc62) zenon_X657) zenon_X97)
% 0.90/1.08  ((skf21 zenon_X11 (skc62) zenon_X537) != zenon_X157)
% 0.90/1.08  (young (skc18) (skf21 zenon_X149 (skc18) zenon_X543))
% 0.90/1.08  (coat (skc18) (skf10 (skc18) (skc19)))
% 0.90/1.08  (-. (hollywood_placename (skc18) zenon_X395))
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X0) != zenon_X155)
% 0.90/1.08  (member zenon_X494 (skf16 zenon_X8 zenon_X494 zenon_X181) zenon_X181)
% 0.90/1.08  (member (skc62) (skf21 (skc63) (skc62) zenon_X194) (skc63))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) (skc19)) != (skf10 (skc18) zenon_X321))
% 0.90/1.08  (young (skc18) (skf10 (skc18) zenon_X11))
% 0.90/1.08  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X97))
% 0.90/1.08  (actual_world (skc62))
% 0.90/1.08  ((skf21 zenon_X106 (skc18) zenon_X639) != zenon_X150)
% 0.90/1.08  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X181))
% 0.90/1.08  (member zenon_X532 (skf19 zenon_X15 zenon_X532 zenon_X0) zenon_X0)
% 0.90/1.08  ((skf10 (skc18) (skc19)) != zenon_X5)
% 0.90/1.08  (zenon_X164 != (skc18))
% 0.90/1.08  (zenon_X474 != (skc18))
% 0.90/1.08  (young (skc62) (skf21 zenon_X181 (skc62) zenon_X652))
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X106) zenon_X106)
% 0.90/1.08  (fellow (skc18) (skf11 (skc18) zenon_X181))
% 0.90/1.08  (zenon_X9 != (skc63))
% 0.90/1.08  ((skc19) != zenon_X358)
% 0.90/1.08  (-. (coat (skc62) (skf10 (skc62) zenon_X329)))
% 0.90/1.08  (dirty (skc18) (skc26))
% 0.90/1.08  ((skc24) != zenon_X389)
% 0.90/1.08  ((skc19) != zenon_X158)
% 0.90/1.08  (-. (coat (skc62) (skf10 (skc62) zenon_X303)))
% 0.90/1.08  (zenon_X533 != (skc62))
% 0.90/1.08  ((skf10 (skc62) zenon_X181) != zenon_X148)
% 0.90/1.08  (ssSkP2 (skc64) (skc63) (skc62))
% 0.90/1.08  (young (skc18) (skf11 (skc18) zenon_X106))
% 0.90/1.08  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X158))
% 0.90/1.08  (fellow (skc62) (skf21 (skc19) (skc62) zenon_X229))
% 0.90/1.08  ((skf10 (skc62) zenon_X156) != zenon_X157)
% 0.90/1.08  ((skc62) != zenon_X139)
% 0.90/1.08  (member (skc18) (skf10 (skc18) (skc19)) (skc19))
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X9) != zenon_X150)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) (skc19)) != (skf10 (skc18) zenon_X325))
% 0.90/1.08  (-. (member (skc18) zenon_X155 zenon_X0))
% 0.90/1.08  (zenon_X465 != (skc18))
% 0.90/1.08  (member zenon_X533 (skf11 zenon_X533 zenon_X16) zenon_X16)
% 0.90/1.08  (zenon_X564 != (skc62))
% 0.90/1.08  (zenon_X650 != (skc62))
% 0.90/1.08  (young (skc62) (skf10 (skc62) zenon_X156))
% 0.90/1.08  (member (skc18) (skf11 (skc18) zenon_X158) zenon_X158)
% 0.90/1.08  ((skf10 (skc62) zenon_X97) != zenon_X148)
% 0.90/1.08  (-. (hollywood_placename (skc18) zenon_X413))
% 0.90/1.08  (fellow (skc62) (skf21 zenon_X158 (skc62) zenon_X668))
% 0.90/1.08  (-. (group (skc18) zenon_X379))
% 0.90/1.08  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X181))
% 0.90/1.08  ((skf16 zenon_X8 (skc18) (skc19)) != (skf10 (skc18) zenon_X358))
% 0.90/1.08  (member zenon_X506 (skf16 zenon_X8 zenon_X506 zenon_X151) zenon_X151)
% 0.90/1.08  (member (skc62) (skf21 zenon_X0 (skc62) zenon_X584) zenon_X0)
% 0.90/1.08  (zenon_X102 != (skc62))
% 0.90/1.08  ((skf11 (skc18) (skc19)) != (skf10 (skc18) zenon_X358))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) (skc63)) != zenon_X150)
% 0.90/1.08  (-. (member (skc18) zenon_X150 zenon_X0))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 zenon_X106) zenon_X106)
% 0.90/1.08  (fellow (skc62) (skf11 (skc62) zenon_X11))
% 0.90/1.08  (young (skc18) (skf11 (skc18) zenon_X0))
% 0.90/1.08  ((skf16 zenon_X8 (skc18) (skc63)) != zenon_X150)
% 0.90/1.08  (zenon_X0 != (skc19))
% 0.90/1.08  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X16))
% 0.90/1.08  (zenon_X198 != zenon_X156)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) (skc63)) != zenon_X157)
% 0.90/1.08  (member zenon_X474 (skf19 zenon_X15 zenon_X474 zenon_X158) zenon_X158)
% 0.90/1.08  (member (skc18) (skf11 (skc18) (skc63)) (skc63))
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X181) zenon_X181)
% 0.90/1.08  (member (skc62) (skf10 (skc62) zenon_X9) zenon_X9)
% 0.90/1.08  ((skc25) != (skc26))
% 0.90/1.08  (-. (street (skc18) zenon_X307))
% 0.90/1.08  (zenon_X453 != (skc62))
% 0.90/1.08  (of (skc62) (skc68) (skc69))
% 0.90/1.08  (zenon_X185 != (skc18))
% 0.90/1.08  ((skf10 (skc18) zenon_X106) != zenon_X150)
% 0.90/1.08  (member zenon_X164 (skf21 (skc19) zenon_X164 zenon_X165) (skc19))
% 0.90/1.08  ((skc20) != zenon_X371)
% 0.90/1.08  ((skf21 zenon_X149 (skc62) zenon_X538) != zenon_X148)
% 0.90/1.08  (young (skc62) (skf21 zenon_X149 (skc62) zenon_X538))
% 0.90/1.08  (-. (member (skc18) zenon_X155 zenon_X149))
% 0.90/1.08  ((skc66) != zenon_X246)
% 0.90/1.08  (-. (actual_world zenon_X139))
% 0.90/1.08  (member (skc62) (skf11 (skc62) zenon_X149) zenon_X149)
% 0.90/1.08  (young (skc18) (skf21 zenon_X151 (skc18) zenon_X578))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) (skc19)) != (skf10 (skc18) zenon_X358))
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) (skc19)) (skc19))
% 0.90/1.08  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X158))
% 0.90/1.08  (zenon_X539 != (skc18))
% 0.90/1.08  (in (skc62) (skc66) (skc69))
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X0) != zenon_X148)
% 0.90/1.08  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X106))
% 0.90/1.08  ((skf21 (skc63) (skc18) zenon_X211) != zenon_X150)
% 0.90/1.08  (zenon_X16 != zenon_X106)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) (skc19)) != (skf10 (skc18) zenon_X321))
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X181) zenon_X181)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X97) != zenon_X148)
% 0.90/1.08  (member (skc62) (skf10 (skc62) zenon_X156) zenon_X156)
% 0.90/1.08  (-. (coat (skc18) (skf10 (skc18) zenon_X325)))
% 0.90/1.08  ((skf21 zenon_X106 (skc18) zenon_X639) != zenon_X155)
% 0.90/1.08  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X158))
% 0.90/1.08  ((skc66) != zenon_X933)
% 0.90/1.08  ((skf11 (skc62) zenon_X16) != zenon_X157)
% 0.90/1.08  (-. (member (skc62) zenon_X4 (skc63)))
% 0.90/1.08  (nonreflexive zenon_X49 (skf17 zenon_X49 zenon_X55 zenon_X53))
% 0.90/1.08  ((skf16 zenon_X8 (skc18) (skc19)) != zenon_X6)
% 0.90/1.08  (-. (barrel (skc18) zenon_X233))
% 0.90/1.08  (present (skc62) (skc66))
% 0.90/1.08  (fellow (skc62) (skf11 (skc62) zenon_X156))
% 0.90/1.08  ((skf10 (skc62) (skc19)) != zenon_X157)
% 0.90/1.08  (zenon_X106 != zenon_X151)
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X97) zenon_X97)
% 0.90/1.08  ((skf11 (skc18) zenon_X149) != zenon_X150)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) (skc63)) != zenon_X3)
% 0.90/1.08  ((skc63) != zenon_X285)
% 0.90/1.08  (zenon_X9 != zenon_X151)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) (skc63)) != zenon_X4)
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X97) zenon_X97)
% 0.90/1.08  ((skf21 zenon_X151 (skc18) zenon_X578) != zenon_X150)
% 0.90/1.08  ((skf21 zenon_X0 (skc18) zenon_X583) != zenon_X150)
% 0.90/1.08  ((skc20) != zenon_X290)
% 0.90/1.08  (chevy (skc62) (skc70))
% 0.90/1.08  (-. (member (skc18) zenon_X150 (skc63)))
% 0.90/1.08  ((skf11 (skc62) zenon_X151) != zenon_X157)
% 0.90/1.08  (member (skc18) (skf21 (skc63) (skc18) zenon_X211) (skc63))
% 0.90/1.08  (zenon_X13 != (skc62))
% 0.90/1.08  ((skf11 (skc18) zenon_X156) != zenon_X155)
% 0.90/1.08  (member (skc62) (skf10 (skc62) zenon_X16) zenon_X16)
% 0.90/1.08  ((skf11 (skc62) zenon_X9) != zenon_X148)
% 0.90/1.08  (member (skc62) (skf11 (skc62) zenon_X181) zenon_X181)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X181) != zenon_X155)
% 0.90/1.08  (fellow (skc62) (skf21 zenon_X9 (skc62) zenon_X531))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X9) != zenon_X150)
% 0.90/1.08  (-. (coat (skc18) (skf10 (skc18) zenon_X358)))
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X97) != zenon_X148)
% 0.90/1.08  (member zenon_X551 (skf11 zenon_X551 zenon_X181) zenon_X181)
% 0.90/1.08  (fellow (skc62) (skf21 zenon_X16 (skc62) zenon_X515))
% 0.90/1.08  ((skf10 (skc18) zenon_X151) != zenon_X155)
% 0.90/1.08  (member zenon_X508 (skf21 zenon_X156 zenon_X508 zenon_X509) zenon_X156)
% 0.90/1.08  (-. (member (skc18) zenon_X150 zenon_X198))
% 0.90/1.08  (coat (skc18) (skf19 zenon_X15 (skc18) (skc19)))
% 0.90/1.08  (fellow (skc18) (skf11 (skc18) zenon_X156))
% 0.90/1.08  ((skf10 (skc18) (skc19)) != (skf10 (skc18) zenon_X325))
% 0.90/1.08  (-. (member (skc18) zenon_X155 zenon_X106))
% 0.90/1.08  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X156))
% 0.90/1.08  (event (skc62) (skc66))
% 0.90/1.08  ((skf10 (skc62) zenon_X97) != zenon_X157)
% 0.90/1.08  (-. (member (skc62) zenon_X2 (skc63)))
% 0.90/1.08  (-. (member (skc18) zenon_X155 zenon_X181))
% 0.90/1.08  (fellow (skc18) (skf11 (skc18) zenon_X16))
% 0.90/1.08  (young (skc62) (skf21 zenon_X0 (skc62) zenon_X584))
% 0.90/1.08  (zenon_X0 != zenon_X11)
% 0.90/1.08  (young (skc62) (skf10 (skc62) zenon_X0))
% 0.90/1.08  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X16))
% 0.90/1.08  (zenon_X498 != (skc18))
% 0.90/1.08  (zenon_X9 != (skc19))
% 0.90/1.08  (young (skc18) (skf11 (skc18) (skc63)))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X156) != zenon_X155)
% 0.90/1.08  (young (skc62) (skf21 zenon_X11 (skc62) zenon_X537))
% 0.90/1.08  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X106))
% 0.90/1.08  (fellow (skc62) (skf11 (skc62) zenon_X181))
% 0.90/1.08  (zenon_X158 != zenon_X106)
% 0.90/1.08  ((skf10 (skc62) zenon_X149) != zenon_X148)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X106) != zenon_X150)
% 0.90/1.08  (member zenon_X629 (skf16 zenon_X8 zenon_X629 zenon_X198) zenon_X198)
% 0.90/1.08  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X156))
% 0.90/1.08  (zenon_X181 != zenon_X11)
% 0.90/1.08  ((skc63) != zenon_X946)
% 0.90/1.08  ((skf11 (skc62) zenon_X181) != zenon_X157)
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X151) zenon_X151)
% 0.90/1.08  (young (skc62) (skf11 (skc62) zenon_X198))
% 0.90/1.08  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X156))
% 0.90/1.08  (member (skc18) (skf21 zenon_X9 (skc18) zenon_X542) zenon_X9)
% 0.90/1.08  (group (skc62) (skc63))
% 0.90/1.08  (zenon_X511 != (skc62))
% 0.90/1.08  (fellow (skc62) (skf10 (skc62) zenon_X181))
% 0.90/1.08  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X9))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X156) != zenon_X150)
% 0.90/1.08  (fellow (skc62) (skf10 (skc62) zenon_X158))
% 0.90/1.08  ((skf11 (skc62) zenon_X0) != zenon_X148)
% 0.90/1.08  (-. (member (skc62) zenon_X157 zenon_X11))
% 0.90/1.08  (zenon_X16 != zenon_X11)
% 0.90/1.08  ((skf11 (skc62) zenon_X11) != zenon_X157)
% 0.90/1.08  (member zenon_X641 (skf11 zenon_X641 zenon_X97) zenon_X97)
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X16) != zenon_X157)
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X0) != zenon_X150)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X0) != zenon_X150)
% 0.90/1.08  (-. (member (skc62) zenon_X148 zenon_X11))
% 0.90/1.08  (fellow (skc62) (skf10 (skc62) zenon_X149))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) (skc19)) != zenon_X6)
% 0.90/1.08  (-. (member (skc18) zenon_X150 zenon_X181))
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X149) zenon_X149)
% 0.90/1.08  (zenon_X599 != (skc62))
% 0.90/1.08  ((skc18) != zenon_X130)
% 0.90/1.08  (zenon_X9 != zenon_X158)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X158) != zenon_X148)
% 0.90/1.08  (-. (coat (skc62) (skf10 (skc62) zenon_X317)))
% 0.90/1.08  ((skf10 (skc62) zenon_X106) != zenon_X148)
% 0.90/1.08  (young (skc62) (skf21 zenon_X156 (skc62) zenon_X616))
% 0.90/1.08  (zenon_X637 != (skc18))
% 0.90/1.08  (-. (member (skc62) zenon_X3 (skc63)))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X181) != zenon_X150)
% 0.90/1.08  (zenon_X655 != (skc18))
% 0.90/1.08  (member zenon_X535 (skf21 zenon_X149 zenon_X535 zenon_X536) zenon_X149)
% 0.90/1.08  (zenon_X453 != (skc18))
% 0.90/1.08  (young (skc62) (skf21 zenon_X106 (skc62) zenon_X640))
% 0.90/1.08  (dirty (skc62) (skc70))
% 0.90/1.08  ((skc63) != zenon_X151)
% 0.90/1.08  (member (skc18) (skf21 zenon_X151 (skc18) zenon_X578) zenon_X151)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X198) != zenon_X157)
% 0.90/1.08  ((skc24) != zenon_X403)
% 0.90/1.08  (member zenon_X637 (skf21 zenon_X106 zenon_X637 zenon_X638) zenon_X106)
% 0.90/1.08  (-. (member (skc62) zenon_X157 zenon_X198))
% 0.90/1.08  ((skf16 zenon_X8 (skc18) zenon_X198) != zenon_X150)
% 0.90/1.08  (fellow (skc18) (skf21 zenon_X97 (skc18) zenon_X658))
% 0.90/1.08  (group (skc62) (skc65))
% 0.90/1.08  (zenon_X612 != (skc18))
% 0.90/1.08  ((skc63) != zenon_X149)
% 0.90/1.08  (zenon_X487 != (skc18))
% 0.90/1.08  (down (skc18) (skc22) (skc23))
% 0.90/1.08  (young (skc62) (skf19 zenon_X15 (skc62) (skc63)))
% 0.90/1.08  (member zenon_X210 (skf11 zenon_X210 (skc63)) (skc63))
% 0.90/1.08  ((skf11 (skc62) zenon_X149) != zenon_X148)
% 0.90/1.08  (member zenon_X550 (skf19 zenon_X15 zenon_X550 zenon_X11) zenon_X11)
% 0.90/1.08  (member zenon_X505 (skf11 zenon_X505 zenon_X11) zenon_X11)
% 0.90/1.08  ((skf10 (skc62) zenon_X158) != zenon_X148)
% 0.90/1.08  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X158))
% 0.90/1.08  (zenon_X9 != zenon_X198)
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) zenon_X9))
% 0.90/1.08  ((skf21 zenon_X151 (skc62) zenon_X579) != zenon_X157)
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X16) zenon_X16)
% 0.90/1.08  (zenon_X532 != (skc18))
% 0.90/1.08  ((skc19) != zenon_X156)
% 0.90/1.08  ((skc19) != zenon_X382)
% 0.90/1.08  ((skf11 (skc62) zenon_X97) != zenon_X148)
% 0.90/1.08  ((skc21) != zenon_X290)
% 0.90/1.08  ((skf21 (skc19) (skc18) zenon_X228) != zenon_X7)
% 0.90/1.08  ((skf10 (skc18) zenon_X156) != zenon_X155)
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X0) zenon_X0)
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X106))
% 0.90/1.08  ((skf21 zenon_X11 (skc18) zenon_X457) != zenon_X150)
% 0.90/1.08  (zenon_X535 != (skc18))
% 0.90/1.08  ((skf16 zenon_X8 (skc62) (skc63)) != zenon_X148)
% 0.90/1.08  ((skc23) != zenon_X307)
% 0.90/1.08  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X11))
% 0.90/1.08  ((skf21 zenon_X16 (skc62) zenon_X515) != zenon_X148)
% 0.90/1.08  (young (skc62) (skf21 zenon_X158 (skc62) zenon_X668))
% 0.90/1.08  ((skf21 zenon_X97 (skc62) zenon_X657) != zenon_X157)
% 0.90/1.08  ((skf10 (skc18) zenon_X198) != zenon_X150)
% 0.90/1.08  (-. (member (skc62) zenon_X148 (skc19)))
% 0.90/1.08  (-. (member (skc62) zenon_X148 zenon_X198))
% 0.90/1.08  ((skf11 (skc18) (skc19)) != (skf10 (skc18) zenon_X350))
% 0.90/1.08  (fellow (skc62) (skf11 (skc62) (skc19)))
% 0.90/1.08  ((skf16 zenon_X8 (skc62) zenon_X181) != zenon_X148)
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X158) zenon_X158)
% 0.90/1.08  (-. (fellow zenon_X24 (skf11 zenon_X24 (skc63))))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 zenon_X16) zenon_X16)
% 0.90/1.08  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X11))
% 0.90/1.08  (zenon_X17 != (skc18))
% 0.90/1.08  (white (skc62) (skc70))
% 0.90/1.08  (fellow (skc18) (skf21 zenon_X16 (skc18) zenon_X504))
% 0.90/1.08  (zenon_X16 != (skc63))
% 0.90/1.08  ((skc70) != zenon_X202)
% 0.90/1.08  (member (skc18) (skf10 (skc18) zenon_X0) zenon_X0)
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X106) zenon_X106)
% 0.90/1.08  ((skf16 zenon_X8 (skc18) (skc19)) != zenon_X7)
% 0.90/1.08  ((skc19) != zenon_X371)
% 0.90/1.08  (ssSkP1 zenon_X78 zenon_X81 zenon_X76)
% 0.90/1.08  ((skf10 (skc18) zenon_X106) != zenon_X155)
% 0.90/1.08  (zenon_X552 != (skc18))
% 0.90/1.08  ((skf10 (skc62) zenon_X181) != zenon_X157)
% 0.90/1.08  (young (skc18) (skf10 (skc18) (skc19)))
% 0.90/1.08  ((skc19) != zenon_X379)
% 0.90/1.08  ((skf19 zenon_X15 (skc18) (skc19)) != zenon_X150)
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X97) != zenon_X157)
% 0.90/1.08  (member zenon_X169 (skf19 zenon_X15 zenon_X169 (skc19)) (skc19))
% 0.90/1.08  ((skc20) != zenon_X382)
% 0.90/1.08  (-. (coat (skc62) (skf10 (skc62) zenon_X959)))
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X198) zenon_X198)
% 0.90/1.08  (young (skc62) (skf11 (skc62) (skc63)))
% 0.90/1.08  ((skc24) != zenon_X407)
% 0.90/1.08  (member zenon_X552 (skf16 zenon_X8 zenon_X552 zenon_X0) zenon_X0)
% 0.90/1.08  (zenon_X106 != zenon_X156)
% 0.90/1.08  (zenon_X494 != (skc18))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 (skc19)) (skc19))
% 0.90/1.08  ((skf21 (skc19) (skc18) zenon_X228) != zenon_X5)
% 0.90/1.08  (coat (skc18) (skf16 zenon_X8 (skc18) (skc19)))
% 0.90/1.08  (member zenon_X511 (skf19 zenon_X15 zenon_X511 zenon_X149) zenon_X149)
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 zenon_X149) zenon_X149)
% 0.90/1.08  ((skf10 (skc18) zenon_X11) != zenon_X150)
% 0.90/1.08  (lonely (skc62) (skc67))
% 0.90/1.08  (zenon_X97 != (skc63))
% 0.90/1.08  (-. (member (skc62) zenon_X157 zenon_X181))
% 0.90/1.08  (zenon_X0 != zenon_X9)
% 0.90/1.08  (member (skc62) (skf21 zenon_X181 (skc62) zenon_X652) zenon_X181)
% 0.90/1.08  (zenon_X97 != zenon_X158)
% 0.90/1.08  ((skf21 zenon_X156 (skc18) zenon_X510) != zenon_X155)
% 0.90/1.08  (old (skc62) (skc70))
% 0.90/1.08  (zenon_X97 != zenon_X151)
% 0.90/1.08  (member zenon_X167 (skf21 (skc63) zenon_X167 zenon_X168) (skc63))
% 0.90/1.08  ((skf19 zenon_X15 (skc18) zenon_X151) != zenon_X155)
% 0.90/1.08  ((skf21 zenon_X156 (skc18) zenon_X510) != zenon_X150)
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) zenon_X0))
% 0.90/1.08  (black (skc18) (skf10 (skc18) (skc19)))
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X158) zenon_X158)
% 0.90/1.08  (young (skc18) (skf10 (skc18) zenon_X151))
% 0.90/1.08  (zenon_X506 != (skc62))
% 0.90/1.08  ((skf11 (skc18) zenon_X9) != zenon_X150)
% 0.90/1.08  (young (skc18) (skf10 (skc18) (skc63)))
% 0.90/1.08  (zenon_X551 != (skc18))
% 0.90/1.08  (fellow (skc62) (skf21 zenon_X156 (skc62) zenon_X616))
% 0.90/1.08  ((skf10 (skc62) zenon_X198) != zenon_X157)
% 0.90/1.08  (-. (member (skc62) zenon_X157 zenon_X106))
% 0.90/1.08  ((skf10 (skc18) zenon_X149) != zenon_X155)
% 0.90/1.08  (young (skc62) (skf10 (skc62) zenon_X158))
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X106) != zenon_X157)
% 0.90/1.08  (-. (member (skc62) zenon_X148 zenon_X106))
% 0.90/1.08  (fellow (skc18) (skf10 (skc18) zenon_X149))
% 0.90/1.08  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X9) zenon_X9)
% 0.90/1.08  (black (skc18) (skf21 (skc19) (skc18) zenon_X228))
% 0.90/1.08  (member zenon_X102 (skf10 zenon_X102 (skc63)) (skc63))
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) (skc19)))
% 0.90/1.08  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X9))
% 0.90/1.08  ((skf19 zenon_X15 (skc62) zenon_X16) != zenon_X148)
% 0.90/1.08  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X151) zenon_X151)
% 0.90/1.08  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X151))
% 0.90/1.08  (zenon_X102 != (skc18))
% 0.90/1.08  ((skf11 (skc18) zenon_X198) != zenon_X150)
% 0.90/1.08  (zenon_X494 != (skc62))
% 0.90/1.08  (member zenon_X520 (skf16 zenon_X8 zenon_X520 zenon_X156) zenon_X156)
% 0.90/1.08  (zenon_X550 != (skc62))
% 0.90/1.08  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X181) zenon_X181)
% 0.90/1.08  (fellow (skc62) (skf10 (skc62) zenon_X106))
% 0.90/1.08  (group (skc18) (skc21))
% 0.90/1.08  (-. (coat (skc62) (skf10 (skc62) zenon_X333)))
% 0.90/1.08  (young (skc18) (skf21 zenon_X16 (skc18) zenon_X504))
% 0.90/1.08  ((skc23) != zenon_X273)
% 0.90/1.08  (-. (group (skc18) zenon_X368))
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X0) zenon_X0)
% 0.90/1.09  (event zenon_X63 (skf17 zenon_X63 zenon_X69 zenon_X67))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X0) != zenon_X148)
% 0.90/1.09  (zenon_X637 != (skc62))
% 0.90/1.09  ((skf21 zenon_X97 (skc18) zenon_X658) != zenon_X155)
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X9))
% 0.90/1.09  (zenon_X508 != (skc18))
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X156))
% 0.90/1.09  (zenon_X10 != (skc18))
% 0.90/1.09  ((skc20) != zenon_X374)
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X151))
% 0.90/1.09  (zenon_X93 != (skc62))
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) (skc63)))
% 0.90/1.09  ((skf11 (skc18) (skc19)) != (skf10 (skc18) zenon_X325))
% 0.90/1.09  (zenon_X106 != zenon_X149)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc19)) != zenon_X150)
% 0.90/1.09  (young (skc18) (skf21 (skc63) (skc18) zenon_X211))
% 0.90/1.09  (of (skc18) (skc24) (skc25))
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X151 (skc18) zenon_X578))
% 0.90/1.09  (-. (member (skc62) zenon_X157 zenon_X156))
% 0.90/1.09  ((skf11 (skc18) (skc19)) != (skf10 (skc18) zenon_X321))
% 0.90/1.09  (zenon_X11 != (skc19))
% 0.90/1.09  (-. (coat (skc62) (skf10 (skc62) zenon_X951)))
% 0.90/1.09  ((skf21 (skc63) (skc62) zenon_X194) != zenon_X148)
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X198) zenon_X198)
% 0.90/1.09  (member zenon_X571 (skf11 zenon_X571 zenon_X106) zenon_X106)
% 0.90/1.09  (young (skc18) (skf21 zenon_X9 (skc18) zenon_X542))
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X198))
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X151))
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) (skc19)))
% 0.90/1.09  (member (skc18) (skf21 zenon_X0 (skc18) zenon_X583) zenon_X0)
% 0.90/1.09  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X156) zenon_X156)
% 0.90/1.09  ((skc19) != zenon_X374)
% 0.90/1.09  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X151) zenon_X151)
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X16))
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X158))
% 0.90/1.09  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X16) zenon_X16)
% 0.90/1.09  (member (skc18) (skf21 zenon_X198 (skc18) zenon_X569) zenon_X198)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X158) != zenon_X155)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X156) != zenon_X148)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X151) != zenon_X148)
% 0.90/1.09  ((skf11 (skc18) (skc63)) != (skf11 zenon_X24 (skc19)))
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X11))
% 0.90/1.09  (member zenon_X541 (skf19 zenon_X15 zenon_X541 zenon_X106) zenon_X106)
% 0.90/1.09  ((skf21 (skc63) (skc62) zenon_X194) != zenon_X2)
% 0.90/1.09  ((skf10 (skc62) zenon_X9) != zenon_X148)
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X106 (skc62) zenon_X640))
% 0.90/1.09  ((skc62) != zenon_X18)
% 0.90/1.09  (zenon_X164 != (skc62))
% 0.90/1.09  ((skc63) != zenon_X158)
% 0.90/1.09  ((skc63) != zenon_X25)
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X198))
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X16))
% 0.90/1.09  ((skf21 zenon_X11 (skc62) zenon_X537) != zenon_X148)
% 0.90/1.09  (member (skc62) (skf10 (skc62) (skc19)) (skc19))
% 0.90/1.09  ((skf11 (skc18) zenon_X97) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X198 (skc18) zenon_X569))
% 0.90/1.09  (city (skc62) (skc69))
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X156) zenon_X156)
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X16) zenon_X16)
% 0.90/1.09  (zenon_X500 != (skc18))
% 0.90/1.09  (zenon_X576 != (skc18))
% 0.90/1.09  ((skc62) != zenon_X24)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc63)) != zenon_X155)
% 0.90/1.09  (-. (fellow zenon_X24 (skf11 zenon_X24 (skc19))))
% 0.90/1.09  (zenon_X540 != (skc62))
% 0.90/1.09  ((skf10 (skc18) (skc63)) != zenon_X150)
% 0.90/1.09  ((skc25) != zenon_X409)
% 0.90/1.09  ((skf21 zenon_X97 (skc62) zenon_X657) != zenon_X148)
% 0.90/1.09  (member (skc18) (skf10 (skc18) (skc63)) (skc63))
% 0.90/1.09  (zenon_X642 != (skc18))
% 0.90/1.09  ((skf21 zenon_X198 (skc62) zenon_X570) != zenon_X148)
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X9))
% 0.90/1.09  ((skf11 (skc62) (skc63)) != zenon_X157)
% 0.90/1.09  ((skc19) != zenon_X350)
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X11))
% 0.90/1.09  ((skf21 (skc63) (skc62) zenon_X194) != zenon_X157)
% 0.90/1.09  (member (skc18) (skf21 zenon_X149 (skc18) zenon_X543) zenon_X149)
% 0.90/1.09  ((skc24) != zenon_X395)
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X16) zenon_X16)
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X97))
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X97))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != zenon_X155)
% 0.90/1.09  (young (skc18) (skf21 zenon_X181 (skc18) zenon_X653))
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X397))
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != (skf10 (skc18) zenon_X325))
% 0.90/1.09  (-. (coat (skc18) (skf10 (skc18) zenon_X341)))
% 0.90/1.09  (zenon_X16 != (skc19))
% 0.90/1.09  (member zenon_X516 (skf11 zenon_X516 zenon_X198) zenon_X198)
% 0.90/1.09  (zenon_X198 != (skc63))
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X16) zenon_X16)
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X149))
% 0.90/1.09  (zenon_X576 != (skc62))
% 0.90/1.09  ((skf11 (skc62) zenon_X151) != zenon_X148)
% 0.90/1.09  ((skf11 (skc18) zenon_X156) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) (skc63)))
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X156 (skc18) zenon_X510))
% 0.90/1.09  (state zenon_X27 (skf13 zenon_X27 zenon_X31 zenon_X32))
% 0.90/1.09  (member (skc62) (skf21 (skc19) (skc62) zenon_X229) (skc19))
% 0.90/1.09  (fellow (skc62) (skf21 (skc63) (skc62) zenon_X194))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X149) != zenon_X148)
% 0.90/1.09  ((skf10 (skc18) (skc19)) != (skf10 (skc18) zenon_X321))
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X158))
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X158))
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X151) zenon_X151)
% 0.90/1.09  (zenon_X97 != zenon_X11)
% 0.90/1.09  (zenon_X505 != (skc62))
% 0.90/1.09  ((skf21 zenon_X198 (skc18) zenon_X569) != zenon_X150)
% 0.90/1.09  ((skf11 (skc62) zenon_X9) != zenon_X157)
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X16))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) (skc19)) != zenon_X157)
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X11))
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X156) zenon_X156)
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X106))
% 0.90/1.09  ((skf11 (skc62) zenon_X198) != zenon_X148)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X0))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X16) != zenon_X155)
% 0.90/1.09  (member zenon_X564 (skf21 zenon_X198 zenon_X564 zenon_X565) zenon_X198)
% 0.90/1.09  (young (skc62) (skf21 zenon_X97 (skc62) zenon_X657))
% 0.90/1.09  ((skf16 zenon_X8 (skc62) (skc63)) != zenon_X3)
% 0.90/1.09  (-. (member (skc62) zenon_X157 zenon_X9))
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) (skc19)))
% 0.90/1.09  (wear zenon_X42 (skf17 zenon_X42 zenon_X48 zenon_X46))
% 0.90/1.09  (zenon_X198 != (skc19))
% 0.90/1.09  ((skf10 (skc18) (skc19)) != (skf10 (skc18) zenon_X358))
% 0.90/1.09  (zenon_X162 != (skc18))
% 0.90/1.09  ((skf21 zenon_X156 (skc62) zenon_X616) != zenon_X148)
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X407))
% 0.90/1.09  ((skf11 (skc18) zenon_X0) != zenon_X150)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X158))
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != (skf10 (skc18) zenon_X341))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X151) != zenon_X150)
% 0.90/1.09  ((skf10 (skc62) zenon_X11) != zenon_X148)
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) zenon_X9))
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X16))
% 0.90/1.09  (member zenon_X599 (skf19 zenon_X15 zenon_X599 zenon_X97) zenon_X97)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X198))
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X106))
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X158))
% 0.90/1.09  ((skc18) != zenon_X21)
% 0.90/1.09  ((skc24) != zenon_X401)
% 0.90/1.09  (two (skc18) (skc21))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X9) != zenon_X148)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc19)) != (skf10 (skc18) zenon_X350))
% 0.90/1.09  ((skf21 zenon_X198 (skc62) zenon_X570) != zenon_X157)
% 0.90/1.09  ((skc24) != zenon_X385)
% 0.90/1.09  (young (skc62) (skf21 (skc19) (skc62) zenon_X229))
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X149) zenon_X149)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X9))
% 0.90/1.09  (member (skc18) (skf21 zenon_X158 (skc18) zenon_X669) zenon_X158)
% 0.90/1.09  (zenon_X162 != (skc62))
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X198))
% 0.90/1.09  ((skf11 (skc18) zenon_X181) != zenon_X155)
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X97))
% 0.90/1.09  ((skf11 (skc62) zenon_X198) != zenon_X157)
% 0.90/1.09  (member (skc62) (skf21 zenon_X156 (skc62) zenon_X616) zenon_X156)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) (skc63)) != zenon_X4)
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != (skf10 (skc18) zenon_X350))
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) (skc19)) (skc19))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X156) != zenon_X150)
% 0.90/1.09  ((skf10 (skc18) (skc19)) != zenon_X155)
% 0.90/1.09  (member zenon_X585 (skf16 zenon_X8 zenon_X585 zenon_X158) zenon_X158)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X149) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf21 (skc19) (skc18) zenon_X228))
% 0.90/1.09  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X106) zenon_X106)
% 0.90/1.09  ((skc65) != zenon_X946)
% 0.90/1.09  ((skc67) != zenon_X267)
% 0.90/1.09  (zenon_X541 != (skc62))
% 0.90/1.09  (member zenon_X539 (skf19 zenon_X15 zenon_X539 zenon_X198) zenon_X198)
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X11))
% 0.90/1.09  (zenon_X177 != (skc62))
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X198 (skc62) zenon_X570))
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X181) zenon_X181)
% 0.90/1.09  ((skf10 (skc62) zenon_X151) != zenon_X157)
% 0.90/1.09  ((skf11 (skc62) (skc19)) != (skf11 zenon_X24 (skc19)))
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X198))
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X198))
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != (skf10 (skc18) zenon_X358))
% 0.90/1.09  (zenon_X532 != (skc62))
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X0))
% 0.90/1.09  ((skc62) != zenon_X21)
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X0))
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X158))
% 0.90/1.09  (-. (ssSkP0 zenon_X20 zenon_X18))
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X198) zenon_X198)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X158) != zenon_X157)
% 0.90/1.09  (ssSkP0 (skc65) (skc62))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X106) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) zenon_X181))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc19)) != zenon_X155)
% 0.90/1.09  ((skf10 (skc62) zenon_X9) != zenon_X157)
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X149 (skc62) zenon_X538))
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X16))
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) zenon_X156))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X198) != zenon_X155)
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X11))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X97))
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X151 (skc62) zenon_X579))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != (skf10 (skc18) zenon_X354))
% 0.90/1.09  ((skf21 zenon_X149 (skc62) zenon_X538) != zenon_X157)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X11))
% 0.90/1.09  (zenon_X198 != zenon_X151)
% 0.90/1.09  ((skf10 (skc62) zenon_X11) != zenon_X157)
% 0.90/1.09  ((skc19) != zenon_X368)
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X181))
% 0.90/1.09  (agent zenon_X70 (skf17 zenon_X70 zenon_X71 zenon_X75) zenon_X71)
% 0.90/1.09  (-. (actual_world zenon_X130))
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X16) != zenon_X148)
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) (skc63)))
% 0.90/1.09  (young (skc18) (skf21 zenon_X0 (skc18) zenon_X583))
% 0.90/1.09  ((skf11 (skc18) zenon_X0) != zenon_X155)
% 0.90/1.09  (-. (member (skc18) zenon_X150 zenon_X9))
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X16))
% 0.90/1.09  (member (skc62) (skf21 zenon_X151 (skc62) zenon_X579) zenon_X151)
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X97))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc19)) != zenon_X5)
% 0.90/1.09  (barrel (skc18) (skc22))
% 0.90/1.09  (member zenon_X93 (skf23 zenon_X93 zenon_X97) zenon_X97)
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X151) zenon_X151)
% 0.90/1.09  (member zenon_X17 (skf19 zenon_X15 zenon_X17 zenon_X16) zenon_X16)
% 0.90/1.09  ((skc20) != zenon_X368)
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) (skc63)))
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X181))
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X97))
% 0.90/1.09  (member (skc62) (skf10 (skc62) zenon_X11) zenon_X11)
% 0.90/1.09  ((skf11 (skc18) zenon_X106) != zenon_X150)
% 0.90/1.09  (member (skc18) (skf21 zenon_X16 (skc18) zenon_X504) zenon_X16)
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) (skc19)))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X16) != zenon_X157)
% 0.90/1.09  (ssSkP0 zenon_X442 (skc18))
% 0.90/1.09  ((skf21 zenon_X16 (skc62) zenon_X515) != zenon_X157)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X156))
% 0.90/1.09  (in (skc18) (skc22) (skc25))
% 0.90/1.09  ((skc20) != zenon_X365)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != (skf10 (skc18) zenon_X325))
% 0.90/1.09  (-. (member (skc62) zenon_X157 zenon_X97))
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X106) zenon_X106)
% 0.90/1.09  (young (skc62) (skf21 zenon_X16 (skc62) zenon_X515))
% 0.90/1.09  ((skf21 (skc63) (skc62) zenon_X194) != zenon_X4)
% 0.90/1.09  (group (skc18) (skc19))
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != zenon_X155)
% 0.90/1.09  (-. (member (skc62) zenon_X157 zenon_X0))
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X9) zenon_X9)
% 0.90/1.09  ((skf11 (skc18) (skc19)) != zenon_X150)
% 0.90/1.09  (zenon_X599 != (skc18))
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X9))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X9) != zenon_X155)
% 0.90/1.09  (in zenon_X33 (skf12 zenon_X34 zenon_X33 zenon_X36) zenon_X36)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X198))
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X0 (skc62) zenon_X584))
% 0.90/1.09  (zenon_X106 != (skc19))
% 0.90/1.09  (cheap (skc18) (skf10 (skc18) (skc19)))
% 0.90/1.09  ((skc22) != zenon_X233)
% 0.90/1.09  ((skf21 zenon_X0 (skc62) zenon_X584) != zenon_X157)
% 0.90/1.09  ((skc65) != zenon_X285)
% 0.90/1.09  (zenon_X97 != zenon_X198)
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X97) zenon_X97)
% 0.90/1.09  ((skf10 (skc18) (skc19)) != (skf10 (skc18) zenon_X354))
% 0.90/1.09  ((skc19) != zenon_X365)
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X158) zenon_X158)
% 0.90/1.09  (zenon_X520 != (skc62))
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X198) zenon_X198)
% 0.90/1.09  ((skf11 (skc18) zenon_X11) != zenon_X155)
% 0.90/1.09  (zenon_X167 != (skc18))
% 0.90/1.09  ((skf10 (skc62) (skc63)) != zenon_X2)
% 0.90/1.09  (member (skc62) (skf10 (skc62) zenon_X149) zenon_X149)
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) (skc63)))
% 0.90/1.09  ((skf21 (skc19) (skc62) zenon_X229) != zenon_X157)
% 0.90/1.09  (member zenon_X473 (skf11 zenon_X473 zenon_X151) zenon_X151)
% 0.90/1.09  (city (skc18) (skc25))
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X149) != zenon_X148)
% 0.90/1.09  (zenon_X16 != zenon_X198)
% 0.90/1.09  ((skf10 (skc62) zenon_X0) != zenon_X157)
% 0.90/1.09  (-. (old (skc18) zenon_X212))
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X0) zenon_X0)
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X11) zenon_X11)
% 0.90/1.09  (member zenon_X642 (skf19 zenon_X15 zenon_X642 zenon_X156) zenon_X156)
% 0.90/1.09  ((skf11 (skc18) (skc19)) != zenon_X6)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X9) != zenon_X148)
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) (skc63)))
% 0.90/1.09  ((skc24) != zenon_X377)
% 0.90/1.09  ((skf10 (skc18) zenon_X9) != zenon_X150)
% 0.90/1.09  (zenon_X181 != zenon_X149)
% 0.90/1.09  (-. (member (skc18) zenon_X150 zenon_X11))
% 0.90/1.09  (zenon_X16 != zenon_X9)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X11) != zenon_X148)
% 0.90/1.09  ((skf11 (skc18) (skc19)) != zenon_X7)
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X106) zenon_X106)
% 0.90/1.09  (placename (skc62) (skc68))
% 0.90/1.09  ((skf21 zenon_X16 (skc18) zenon_X504) != zenon_X155)
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X387))
% 0.90/1.09  (member (skc62) (skf21 zenon_X198 (skc62) zenon_X570) zenon_X198)
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X9))
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X149))
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) zenon_X9) zenon_X9)
% 0.90/1.09  (-. (city (skc18) zenon_X412))
% 0.90/1.09  (zenon_X553 != (skc18))
% 0.90/1.09  ((skf21 zenon_X106 (skc62) zenon_X640) != zenon_X148)
% 0.90/1.09  ((skc24) != zenon_X393)
% 0.90/1.09  ((skc65) != zenon_X120)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != zenon_X7)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) (skc63)) != zenon_X148)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X9) != zenon_X155)
% 0.90/1.09  (zenon_X198 != zenon_X106)
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X181))
% 0.90/1.09  (zenon_X170 != (skc62))
% 0.90/1.09  (-. (coat (skc62) (skf10 (skc62) zenon_X955)))
% 0.90/1.09  (zenon_X0 != zenon_X156)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X149))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X11) != zenon_X148)
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X0) zenon_X0)
% 0.90/1.09  (member zenon_X540 (skf11 zenon_X540 zenon_X158) zenon_X158)
% 0.90/1.09  ((skc64) != zenon_X946)
% 0.90/1.09  (zenon_X93 != (skc18))
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) zenon_X16))
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X158 (skc18) zenon_X669))
% 0.90/1.09  (member zenon_X13 (skf21 zenon_X11 zenon_X13 zenon_X14) zenon_X11)
% 0.90/1.09  ((skf21 zenon_X149 (skc18) zenon_X543) != zenon_X150)
% 0.90/1.09  (group (skc62) (skc64))
% 0.90/1.09  (-. (coat (skc18) (skf10 (skc18) zenon_X350)))
% 0.90/1.09  (member (skc18) (skf21 zenon_X11 (skc18) zenon_X457) zenon_X11)
% 0.90/1.09  (member zenon_X102 (skf10 zenon_X102 zenon_X158) zenon_X158)
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X151))
% 0.90/1.09  ((skf11 (skc62) (skc19)) != (skf11 zenon_X24 zenon_X25))
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X97) zenon_X97)
% 0.90/1.09  (cheap (skc18) (skf11 (skc18) (skc19)))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc19)) != (skf10 (skc18) zenon_X341))
% 0.90/1.09  (zenon_X181 != zenon_X16)
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) zenon_X11))
% 0.90/1.09  (-. (member (skc18) zenon_X150 zenon_X16))
% 0.90/1.09  (-. (member (skc62) zenon_X157 zenon_X149))
% 0.90/1.09  ((skf11 (skc62) zenon_X158) != zenon_X148)
% 0.90/1.09  (zenon_X581 != (skc18))
% 0.90/1.09  (zenon_X210 != (skc62))
% 0.90/1.09  ((skf11 (skc18) zenon_X106) != zenon_X155)
% 0.90/1.09  (zenon_X97 != zenon_X149)
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X149))
% 0.90/1.09  (member (skc62) (skf10 (skc62) zenon_X106) zenon_X106)
% 0.90/1.09  ((skc18) != zenon_X24)
% 0.90/1.09  ((skc70) != zenon_X186)
% 0.90/1.09  (zenon_X0 != (skc63))
% 0.90/1.09  (zenon_X149 != zenon_X198)
% 0.90/1.09  (-. (city (skc18) zenon_X409))
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) zenon_X151))
% 0.90/1.09  (zenon_X9 != zenon_X156)
% 0.90/1.09  (-. (member (skc18) zenon_X155 (skc63)))
% 0.90/1.09  (zenon_X641 != (skc18))
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X149))
% 0.90/1.09  ((skf10 (skc62) (skc63)) != zenon_X157)
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X9))
% 0.90/1.09  (member (skc62) (skf11 (skc62) (skc19)) (skc19))
% 0.90/1.09  ((skc26) != zenon_X212)
% 0.90/1.09  ((skf10 (skc18) zenon_X181) != zenon_X150)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X106))
% 0.90/1.09  (zenon_X506 != (skc18))
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X385))
% 0.90/1.09  (zenon_X9 != zenon_X106)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X106) != zenon_X148)
% 0.90/1.09  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X97) zenon_X97)
% 0.90/1.09  (zenon_X529 != (skc62))
% 0.90/1.09  ((skc20) != zenon_X345)
% 0.90/1.09  (member (skc62) (skf10 (skc62) (skc63)) (skc63))
% 0.90/1.09  (-. (street (skc62) zenon_X940))
% 0.90/1.09  (-. (member (skc18) zenon_X150 zenon_X149))
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X106))
% 0.90/1.09  (zenon_X181 != (skc63))
% 0.90/1.09  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X0) zenon_X0)
% 0.90/1.09  (member zenon_X500 (skf11 zenon_X500 zenon_X9) zenon_X9)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X198) != zenon_X148)
% 0.90/1.09  ((skf10 (skc18) zenon_X97) != zenon_X150)
% 0.90/1.09  ((skf10 (skc18) (skc19)) != (skf10 (skc18) zenon_X350))
% 0.90/1.09  ((skf21 zenon_X181 (skc18) zenon_X653) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X11))
% 0.90/1.09  (member (skc18) (skf19 zenon_X15 (skc18) (skc63)) (skc63))
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X106) zenon_X106)
% 0.90/1.09  ((skf11 (skc62) (skc63)) != zenon_X2)
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) (skc63)) (skc63))
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X158) zenon_X158)
% 0.90/1.09  (young (skc18) (skf21 zenon_X158 (skc18) zenon_X669))
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X106))
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X9 (skc18) zenon_X542))
% 0.90/1.09  ((skf11 (skc18) (skc63)) != (skf11 zenon_X24 (skc63)))
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X97))
% 0.90/1.09  (ssSkC0)
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X9))
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) zenon_X97))
% 0.90/1.09  (zenon_X473 != (skc18))
% 0.90/1.09  (member zenon_X595 (skf19 zenon_X15 zenon_X595 zenon_X181) zenon_X181)
% 0.90/1.09  (placename (skc18) (skc24))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X151) != zenon_X157)
% 0.90/1.09  (-. (group (skc18) zenon_X345))
% 0.90/1.09  ((skf11 (skc62) zenon_X149) != zenon_X157)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X106))
% 0.90/1.09  (member (skc62) (skf10 (skc62) zenon_X181) zenon_X181)
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X410))
% 0.90/1.09  ((skf11 (skc18) (skc19)) != (skf10 (skc18) zenon_X354))
% 0.90/1.09  ((skf10 (skc62) (skc63)) != zenon_X148)
% 0.90/1.09  (zenon_X502 != (skc62))
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) (skc63)))
% 0.90/1.09  ((skc19) != zenon_X354)
% 0.90/1.09  (zenon_X465 != (skc62))
% 0.90/1.09  (zenon_X97 != (skc19))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) (skc63)) != zenon_X2)
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X151))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X11) != zenon_X157)
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) zenon_X158))
% 0.90/1.09  (zenon_X0 != zenon_X198)
% 0.90/1.09  (zenon_X473 != (skc62))
% 0.90/1.09  (zenon_X149 != zenon_X151)
% 0.90/1.09  ((skc62) != zenon_X130)
% 0.90/1.09  ((skf10 (skc18) (skc19)) != zenon_X6)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) (skc63)) != zenon_X157)
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X0))
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X149))
% 0.90/1.09  ((skf21 (skc63) (skc62) zenon_X194) != zenon_X3)
% 0.90/1.09  ((skc19) != zenon_X151)
% 0.90/1.09  ((skf10 (skc18) zenon_X181) != zenon_X155)
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X97))
% 0.90/1.09  (-. (coat (skc18) (skf10 (skc18) zenon_X354)))
% 0.90/1.09  (-. (member (skc62) zenon_X157 (skc19)))
% 0.90/1.09  ((skf10 (skc18) (skc19)) != zenon_X7)
% 0.90/1.09  ((skf10 (skc18) zenon_X9) != zenon_X155)
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X97) zenon_X97)
% 0.90/1.09  (zenon_X97 != zenon_X156)
% 0.90/1.09  ((skf21 (skc63) (skc18) zenon_X211) != zenon_X155)
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X198))
% 0.90/1.09  ((skf11 (skc62) (skc63)) != zenon_X4)
% 0.90/1.09  (young (skc18) (skf21 (skc19) (skc18) zenon_X228))
% 0.90/1.09  ((skf11 (skc18) zenon_X16) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf21 (skc63) (skc18) zenon_X211))
% 0.90/1.09  (zenon_X655 != (skc62))
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X156))
% 0.90/1.09  ((skf10 (skc62) zenon_X16) != zenon_X148)
% 0.90/1.09  (zenon_X650 != (skc18))
% 0.90/1.09  (zenon_X156 != zenon_X151)
% 0.90/1.09  (member (skc62) (skf10 (skc62) zenon_X158) zenon_X158)
% 0.90/1.09  (zenon_X499 != (skc62))
% 0.90/1.09  (zenon_X581 != (skc62))
% 0.90/1.09  (zenon_X529 != (skc18))
% 0.90/1.09  ((skf11 (skc18) zenon_X151) != zenon_X150)
% 0.90/1.09  (zenon_X595 != (skc18))
% 0.90/1.09  (present zenon_X56 (skf17 zenon_X56 zenon_X62 zenon_X60))
% 0.90/1.09  (zenon_X181 != (skc19))
% 0.90/1.09  (zenon_X13 != (skc18))
% 0.90/1.09  (zenon_X505 != (skc18))
% 0.90/1.09  ((skf11 (skc62) zenon_X16) != zenon_X148)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X11) != zenon_X155)
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X389))
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X11) zenon_X11)
% 0.90/1.09  (-. (member (skc62) zenon_X157 zenon_X151))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X11) != zenon_X155)
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X97))
% 0.90/1.09  (zenon_X0 != zenon_X16)
% 0.90/1.09  ((skf21 zenon_X181 (skc62) zenon_X652) != zenon_X157)
% 0.90/1.09  ((skf21 (skc19) (skc62) zenon_X229) != zenon_X148)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X151) != zenon_X148)
% 0.90/1.09  (zenon_X11 != zenon_X151)
% 0.90/1.09  (zenon_X612 != (skc62))
% 0.90/1.09  (cheap (skc18) (skf21 (skc19) (skc18) zenon_X228))
% 0.90/1.09  (coat (skc18) (skf21 (skc19) (skc18) zenon_X228))
% 0.90/1.09  (-. (coat (skc62) (skf10 (skc62) zenon_X313)))
% 0.90/1.09  (zenon_X158 != zenon_X156)
% 0.90/1.09  (member zenon_X679 (skf16 zenon_X8 zenon_X679 zenon_X106) zenon_X106)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X158) != zenon_X148)
% 0.90/1.09  (zenon_X585 != (skc62))
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X198))
% 0.90/1.09  ((skf21 zenon_X181 (skc62) zenon_X652) != zenon_X148)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X9))
% 0.90/1.09  (member zenon_X581 (skf21 zenon_X0 zenon_X581 zenon_X582) zenon_X0)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X97))
% 0.90/1.09  (young (skc62) (skf10 (skc62) (skc63)))
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X181))
% 0.90/1.09  (cheap (skc18) (skf19 zenon_X15 (skc18) (skc19)))
% 0.90/1.09  ((skc19) != zenon_X341)
% 0.90/1.09  (zenon_X533 != (skc18))
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) (skc63)))
% 0.90/1.09  (member zenon_X185 (skf11 zenon_X185 (skc19)) (skc19))
% 0.90/1.09  (zenon_X181 != zenon_X97)
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X16))
% 0.90/1.09  (zenon_X11 != zenon_X149)
% 0.90/1.09  ((skf21 zenon_X156 (skc62) zenon_X616) != zenon_X157)
% 0.90/1.09  (zenon_X511 != (skc18))
% 0.90/1.09  (be zenon_X37 (skf13 zenon_X37 zenon_X41 zenon_X38) zenon_X38 (skf12 zenon_X38 zenon_X37 zenon_X41))
% 0.90/1.09  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X156) zenon_X156)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X158) != zenon_X150)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != (skf10 (skc18) zenon_X350))
% 0.90/1.09  ((skf11 (skc18) zenon_X198) != zenon_X155)
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) (skc19)))
% 0.90/1.09  (zenon_X11 != zenon_X158)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X151))
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X9) zenon_X9)
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != (skf10 (skc18) zenon_X354))
% 0.90/1.09  ((skf11 (skc62) zenon_X97) != zenon_X157)
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X151))
% 0.90/1.09  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X11) zenon_X11)
% 0.90/1.09  (young (skc18) (skf21 zenon_X156 (skc18) zenon_X510))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X9) != zenon_X157)
% 0.90/1.09  (actual_world (skc18))
% 0.90/1.09  ((skf10 (skc62) zenon_X0) != zenon_X148)
% 0.90/1.09  (member (skc18) (skf16 zenon_X8 (skc18) (skc63)) (skc63))
% 0.90/1.09  (member zenon_X453 (skf16 zenon_X8 zenon_X453 zenon_X149) zenon_X149)
% 0.90/1.09  (young (skc18) (skf11 (skc18) (skc19)))
% 0.90/1.09  (zenon_X11 != zenon_X106)
% 0.90/1.09  ((skf11 (skc62) zenon_X158) != zenon_X157)
% 0.90/1.09  (-. (fellow zenon_X24 (skf11 zenon_X24 zenon_X25)))
% 0.90/1.09  (zenon_X521 != (skc62))
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X377))
% 0.90/1.09  (zenon_X0 != zenon_X97)
% 0.90/1.09  ((skf21 zenon_X9 (skc62) zenon_X531) != zenon_X157)
% 0.90/1.09  (member zenon_X612 (skf19 zenon_X15 zenon_X612 zenon_X9) zenon_X9)
% 0.90/1.09  (-. (member (skc18) zenon_X155 (skc19)))
% 0.90/1.09  ((skf21 (skc19) (skc18) zenon_X228) != zenon_X150)
% 0.90/1.09  ((skc63) != (skc19))
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X11 (skc62) zenon_X537))
% 0.90/1.09  (-. (barrel (skc62) zenon_X933))
% 0.90/1.09  (zenon_X149 != zenon_X156)
% 0.90/1.09  (member zenon_X576 (skf21 zenon_X151 zenon_X576 zenon_X577) zenon_X151)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X181) != zenon_X157)
% 0.90/1.09  (young (skc62) (skf10 (skc62) zenon_X11))
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X106))
% 0.90/1.09  ((skf10 (skc18) zenon_X158) != zenon_X155)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != zenon_X5)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X9) != zenon_X157)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X16))
% 0.90/1.09  ((skc21) != zenon_X345)
% 0.90/1.09  (zenon_X169 != (skc18))
% 0.90/1.09  ((skf21 zenon_X16 (skc18) zenon_X504) != zenon_X150)
% 0.90/1.09  ((skf10 (skc18) zenon_X97) != zenon_X155)
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) (skc63)) (skc63))
% 0.90/1.09  ((skc21) != zenon_X374)
% 0.90/1.09  (member (skc62) (skf21 zenon_X106 (skc62) zenon_X640) zenon_X106)
% 0.90/1.09  (young (skc62) (skf21 (skc63) (skc62) zenon_X194))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X97) != zenon_X155)
% 0.90/1.09  ((skf21 zenon_X158 (skc18) zenon_X669) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X0))
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X158))
% 0.90/1.09  ((skf11 (skc62) (skc63)) != zenon_X3)
% 0.90/1.09  ((skf10 (skc18) zenon_X151) != zenon_X150)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X97) != zenon_X155)
% 0.90/1.09  (-. (group (skc18) zenon_X290))
% 0.90/1.09  ((skf21 zenon_X158 (skc18) zenon_X669) != zenon_X155)
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X156))
% 0.90/1.09  (zenon_X0 != zenon_X106)
% 0.90/1.09  ((skf11 (skc62) zenon_X156) != zenon_X157)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X9))
% 0.90/1.09  ((skf16 zenon_X8 (skc62) (skc19)) != zenon_X148)
% 0.90/1.09  (-. (two zenon_X121 zenon_X120))
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X393))
% 0.90/1.09  ((skf10 (skc62) zenon_X106) != zenon_X157)
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X158))
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X0))
% 0.90/1.09  ((skf10 (skc62) zenon_X156) != zenon_X148)
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X151))
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X151))
% 0.90/1.09  (-. (member (skc18) zenon_X155 zenon_X198))
% 0.90/1.09  (zenon_X474 != (skc62))
% 0.90/1.09  (ssSkP2 (skc20) (skc19) (skc18))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X149))
% 0.90/1.09  ((skc19) != zenon_X345)
% 0.90/1.09  (white (skc18) (skc26))
% 0.90/1.09  (zenon_X9 != zenon_X149)
% 0.90/1.09  (member (skc62) (skf19 zenon_X15 (skc62) (skc19)) (skc19))
% 0.90/1.09  (member (skc18) (skf11 (skc18) (skc19)) (skc19))
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X156))
% 0.90/1.09  ((skf11 (skc18) zenon_X158) != zenon_X155)
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) zenon_X151))
% 0.90/1.09  (zenon_X169 != (skc62))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X156) != zenon_X155)
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) (skc19)))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X106))
% 0.90/1.09  (member (skc62) (skf21 zenon_X158 (skc62) zenon_X668) zenon_X158)
% 0.90/1.09  (-. (frontseat (skc18) (skc26)))
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X198) zenon_X198)
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X11))
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) (skc19)))
% 0.90/1.09  ((skc64) != zenon_X285)
% 0.90/1.09  ((skc65) != zenon_X298)
% 0.90/1.09  (zenon_X520 != (skc18))
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X181 (skc18) zenon_X653))
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X106))
% 0.90/1.09  (member (skc62) (skf21 zenon_X11 (skc62) zenon_X537) zenon_X11)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X156) != zenon_X157)
% 0.90/1.09  (zenon_X595 != (skc62))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X9))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X151) != zenon_X150)
% 0.90/1.09  (zenon_X550 != (skc18))
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X97))
% 0.90/1.09  ((skf10 (skc18) zenon_X156) != zenon_X150)
% 0.90/1.09  (zenon_X11 != (skc63))
% 0.90/1.09  (hollywood_placename (skc18) (skc24))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X16) != zenon_X155)
% 0.90/1.09  ((skc66) != zenon_X253)
% 0.90/1.09  (-. (group (skc62) zenon_X285))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X158) != zenon_X157)
% 0.90/1.09  (zenon_X1 != (skc18))
% 0.90/1.09  (ssSkP0 (skc21) (skc18))
% 0.90/1.09  ((skf11 (skc18) (skc63)) != zenon_X150)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X181))
% 0.90/1.09  (zenon_X97 != zenon_X106)
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X16) zenon_X16)
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X106 (skc18) zenon_X639))
% 0.90/1.09  (zenon_X181 != zenon_X158)
% 0.90/1.09  ((skf10 (skc18) zenon_X16) != zenon_X155)
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X0))
% 0.90/1.09  (member zenon_X102 (skf10 zenon_X102 zenon_X97) zenon_X97)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X198) != zenon_X155)
% 0.90/1.09  (hollywood_placename (skc62) (skc68))
% 0.90/1.09  (-. (group (skc18) zenon_X365))
% 0.90/1.09  ((skc19) != zenon_X325)
% 0.90/1.09  (zenon_X516 != (skc62))
% 0.90/1.09  ((skf11 (skc18) (skc19)) != zenon_X155)
% 0.90/1.09  (member zenon_X529 (skf21 zenon_X9 zenon_X529 zenon_X530) zenon_X9)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X156))
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X11) zenon_X11)
% 0.90/1.09  (-. (street (skc62) zenon_X267))
% 0.90/1.09  (young (skc62) (skf21 zenon_X151 (skc62) zenon_X579))
% 0.90/1.09  (-. (member (skc18) zenon_X150 (skc19)))
% 0.90/1.09  (zenon_X553 != (skc62))
% 0.90/1.09  (zenon_X167 != (skc62))
% 0.90/1.09  ((skf21 zenon_X97 (skc18) zenon_X658) != zenon_X150)
% 0.90/1.09  ((skc24) != zenon_X405)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) (skc63)) != zenon_X2)
% 0.90/1.09  (zenon_X500 != (skc62))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X16) != zenon_X150)
% 0.90/1.09  (member (skc62) (skf10 (skc62) zenon_X198) zenon_X198)
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X149))
% 0.90/1.09  ((skf11 (skc18) zenon_X149) != zenon_X155)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X149) != zenon_X157)
% 0.90/1.09  (zenon_X181 != zenon_X9)
% 0.90/1.09  ((skf10 (skc62) zenon_X16) != zenon_X157)
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X0 (skc18) zenon_X583))
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X149))
% 0.90/1.09  ((skc24) != zenon_X397)
% 0.90/1.09  (black (skc18) (skf19 zenon_X15 (skc18) (skc19)))
% 0.90/1.09  ((skf11 (skc18) zenon_X11) != zenon_X150)
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X11) zenon_X11)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X149) != zenon_X150)
% 0.90/1.09  ((skf10 (skc62) zenon_X149) != zenon_X157)
% 0.90/1.09  (frontseat (skc62) (skc70))
% 0.90/1.09  (member zenon_X499 (skf16 zenon_X8 zenon_X499 zenon_X11) zenon_X11)
% 0.90/1.09  (member zenon_X655 (skf21 zenon_X97 zenon_X655 zenon_X656) zenon_X97)
% 0.90/1.09  (-. (old (skc62) zenon_X202))
% 0.90/1.09  ((skf11 (skc62) zenon_X181) != zenon_X148)
% 0.90/1.09  (zenon_X516 != (skc18))
% 0.90/1.09  (zenon_X1 != (skc62))
% 0.90/1.09  (frontseat (skc18) (skc25))
% 0.90/1.09  (-. (barrel (skc62) zenon_X253))
% 0.90/1.09  ((skf10 (skc62) (skc63)) != zenon_X3)
% 0.90/1.09  (fellow (skc62) (skf11 (skc62) zenon_X149))
% 0.90/1.09  ((skc19) != zenon_X290)
% 0.90/1.09  (-. (group (skc62) zenon_X298))
% 0.90/1.09  (young (skc62) (skf19 zenon_X15 (skc62) zenon_X149))
% 0.90/1.09  ((skf11 (skc62) (skc63)) != zenon_X148)
% 0.90/1.09  (member (skc18) (skf11 (skc18) zenon_X198) zenon_X198)
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X11))
% 0.90/1.09  (zenon_X181 != zenon_X0)
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X97))
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X97))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) (skc19)) != (skf10 (skc18) zenon_X341))
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X151) zenon_X151)
% 0.90/1.09  (fellow (skc18) (skf16 zenon_X8 (skc18) zenon_X0))
% 0.90/1.09  (member zenon_X102 (skf10 zenon_X102 zenon_X156) zenon_X156)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X106) != zenon_X157)
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X181))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X11) != zenon_X150)
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X151))
% 0.90/1.09  (young (skc62) (skf10 (skc62) (skc19)))
% 0.90/1.09  (member zenon_X521 (skf19 zenon_X15 zenon_X521 zenon_X151) zenon_X151)
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X9) zenon_X9)
% 0.90/1.09  (zenon_X0 != zenon_X149)
% 0.90/1.09  (young (skc18) (skf16 zenon_X8 (skc18) zenon_X198))
% 0.90/1.09  (-. (street (skc62) zenon_X279))
% 0.90/1.09  (member (skc62) (skf21 zenon_X16 (skc62) zenon_X515) zenon_X16)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X106) != zenon_X148)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc19)) != (skf10 (skc18) zenon_X354))
% 0.90/1.09  (-. (barrel (skc18) zenon_X260))
% 0.90/1.09  ((skf16 zenon_X8 (skc62) (skc19)) != zenon_X157)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X181) != zenon_X155)
% 0.90/1.09  (member (skc62) (skf11 (skc62) zenon_X156) zenon_X156)
% 0.90/1.09  (young (skc18) (skf11 (skc18) zenon_X149))
% 0.90/1.09  ((skc21) != zenon_X120)
% 0.90/1.09  (member (skc18) (skf10 (skc18) zenon_X158) zenon_X158)
% 0.90/1.09  (fellow (skc18) (skf11 (skc18) zenon_X9))
% 0.90/1.09  (ssSkP2 zenon_X89 zenon_X91 zenon_X87)
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X151))
% 0.90/1.09  ((skc21) != zenon_X379)
% 0.90/1.09  (zenon_X97 != zenon_X16)
% 0.90/1.09  (cheap (skc18) (skf16 zenon_X8 (skc18) (skc19)))
% 0.90/1.09  (member zenon_X170 (skf19 zenon_X15 zenon_X170 (skc63)) (skc63))
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X0) != zenon_X157)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X149) != zenon_X157)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X181) != zenon_X148)
% 0.90/1.09  (patient zenon_X82 (skf17 zenon_X82 zenon_X83 zenon_X85) zenon_X85)
% 0.90/1.09  (zenon_X181 != zenon_X198)
% 0.90/1.09  (zenon_X181 != zenon_X151)
% 0.90/1.09  ((skf19 zenon_X15 (skc62) zenon_X156) != zenon_X148)
% 0.90/1.09  (-. (street (skc18) zenon_X273))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X151) != zenon_X155)
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X97))
% 0.90/1.09  ((skc19) != zenon_X149)
% 0.90/1.09  (zenon_X679 != (skc18))
% 0.90/1.09  ((skf21 zenon_X9 (skc62) zenon_X531) != zenon_X148)
% 0.90/1.09  (fellow (skc62) (skf16 zenon_X8 (skc62) zenon_X16))
% 0.90/1.09  ((skf10 (skc62) zenon_X158) != zenon_X157)
% 0.90/1.09  (event (skc18) (skc22))
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) zenon_X97))
% 0.90/1.09  (member (skc62) (skf16 zenon_X8 (skc62) zenon_X149) zenon_X149)
% 0.90/1.09  (down (skc62) (skc66) (skc67))
% 0.90/1.09  (agent (skc18) (skc22) (skc26))
% 0.90/1.09  ((skf11 (skc18) (skc63)) != zenon_X155)
% 0.90/1.09  (member zenon_X553 (skf16 zenon_X8 zenon_X553 zenon_X16) zenon_X16)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X198))
% 0.90/1.09  (-. (coat (skc62) (skf10 (skc62) zenon_X337)))
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X149) != zenon_X155)
% 0.90/1.09  ((skf21 zenon_X9 (skc18) zenon_X542) != zenon_X155)
% 0.90/1.09  (member (skc18) (skf16 zenon_X8 (skc18) zenon_X158) zenon_X158)
% 0.90/1.09  (zenon_X11 != zenon_X156)
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X401))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X156))
% 0.90/1.09  (ssSkP1 (skc25) (skc21) (skc18))
% 0.90/1.09  ((skc18) != zenon_X139)
% 0.90/1.09  ((skc22) != zenon_X260)
% 0.90/1.09  ((skf19 zenon_X15 (skc18) zenon_X97) != zenon_X150)
% 0.90/1.09  (member (skc18) (skf19 zenon_X15 (skc18) zenon_X149) zenon_X149)
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X11 (skc18) zenon_X457))
% 0.90/1.09  ((skf11 (skc62) zenon_X106) != zenon_X157)
% 0.90/1.09  (zenon_X16 != zenon_X158)
% 0.90/1.09  ((skf10 (skc18) zenon_X198) != zenon_X155)
% 0.90/1.09  (member (skc62) (skf21 zenon_X149 (skc62) zenon_X538) zenon_X149)
% 0.90/1.09  (young (skc62) (skf21 zenon_X198 (skc62) zenon_X570))
% 0.90/1.09  (-. (member (skc18) zenon_X150 zenon_X156))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X97) != zenon_X150)
% 0.90/1.09  ((skf10 (skc18) (skc19)) != (skf10 (skc18) zenon_X341))
% 0.90/1.09  (zenon_X521 != (skc18))
% 0.90/1.09  ((skf10 (skc18) zenon_X149) != zenon_X150)
% 0.90/1.09  (chevy (skc18) (skc26))
% 0.90/1.09  (zenon_X502 != (skc18))
% 0.90/1.09  (zenon_X551 != (skc62))
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) zenon_X16))
% 0.90/1.09  (-. (member (skc62) zenon_X148 zenon_X9))
% 0.90/1.09  ((skf21 zenon_X181 (skc18) zenon_X653) != zenon_X155)
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) (skc19)))
% 0.90/1.09  (zenon_X564 != (skc18))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) zenon_X16))
% 0.90/1.09  (young (skc62) (skf11 (skc62) (skc19)))
% 0.90/1.09  (zenon_X666 != (skc62))
% 0.90/1.09  (zenon_X629 != (skc62))
% 0.90/1.09  (fellow (skc18) (skf10 (skc18) zenon_X11))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X106) != zenon_X155)
% 0.90/1.09  ((skc19) != zenon_X25)
% 0.90/1.09  (fellow (skc62) (skf10 (skc62) (skc63)))
% 0.90/1.09  ((skf11 (skc62) zenon_X11) != zenon_X148)
% 0.90/1.09  (young (skc18) (skf19 zenon_X15 (skc18) zenon_X0))
% 0.90/1.09  ((skc26) != zenon_X186)
% 0.90/1.09  ((skf16 zenon_X8 (skc62) zenon_X151) != zenon_X157)
% 0.90/1.09  (member zenon_X102 (skf10 zenon_X102 zenon_X11) zenon_X11)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X158) != zenon_X155)
% 0.90/1.09  ((skc21) != zenon_X368)
% 0.90/1.09  ((skc63) != zenon_X156)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X181) != zenon_X150)
% 0.90/1.09  (young (skc18) (skf21 zenon_X198 (skc18) zenon_X569))
% 0.90/1.09  (zenon_X149 != zenon_X158)
% 0.90/1.09  ((skc67) != zenon_X279)
% 0.90/1.09  ((skf10 (skc18) zenon_X0) != zenon_X155)
% 0.90/1.09  ((skc19) != zenon_X321)
% 0.90/1.09  ((skc24) != zenon_X399)
% 0.90/1.09  ((skf16 zenon_X8 (skc18) zenon_X16) != zenon_X150)
% 0.90/1.09  (member (skc18) (skf21 zenon_X97 (skc18) zenon_X658) zenon_X97)
% 0.90/1.09  (zenon_X535 != (skc62))
% 0.90/1.09  (member zenon_X666 (skf21 zenon_X158 zenon_X666 zenon_X667) zenon_X158)
% 0.90/1.09  (member zenon_X1 (skf11 zenon_X1 zenon_X0) zenon_X0)
% 0.90/1.09  (zenon_X498 != (skc62))
% 0.90/1.09  (zenon_X10 != (skc62))
% 0.90/1.09  (fellow (skc62) (skf19 zenon_X15 (skc62) (skc19)))
% 0.90/1.09  (fellow (skc18) (skf21 zenon_X149 (skc18) zenon_X543))
% 0.90/1.09  (black (skc18) (skf16 zenon_X8 (skc18) (skc19)))
% 0.90/1.09  (-. (member (skc18) zenon_X150 zenon_X151))
% 0.90/1.09  (zenon_X585 != (skc18))
% 0.90/1.09  (young (skc18) (skf21 zenon_X106 (skc18) zenon_X639))
% 0.90/1.09  (zenon_X151 != zenon_X158)
% 0.90/1.09  (member zenon_X102 (skf10 zenon_X102 zenon_X0) zenon_X0)
% 0.90/1.09  (-. (member (skc62) zenon_X148 (skc63)))
% 0.90/1.09  (zenon_X629 != (skc18))
% 0.90/1.09  ((skf11 (skc18) zenon_X97) != zenon_X155)
% 0.90/1.09  (zenon_X679 != (skc62))
% 0.90/1.09  (young (skc18) (skf10 (skc18) zenon_X181))
% 0.90/1.09  (fellow (skc18) (skf19 zenon_X15 (skc18) zenon_X181))
% 0.90/1.09  (-. (hollywood_placename (skc18) zenon_X405))
% 0.90/1.09  (member (skc18) (skf21 zenon_X156 (skc18) zenon_X510) zenon_X156)
% 0.90/1.09  (young (skc62) (skf11 (skc62) zenon_X151))
% 0.90/1.09  ((skc24) != zenon_X410)
% 0.90/1.09  (member (skc18) (skf21 zenon_X181 (skc18) zenon_X653) zenon_X181)
% 0.90/1.09  (zenon_X642 != (skc62))
% 0.90/1.09  (young (skc62) (skf16 zenon_X8 (skc62) zenon_X156))
% 0.90/1.09  ((skf16 zenon_X8 (skc18) (skc63)) != zenon_X155)
% 0.90/1.09  (member zenon_X498 (skf16 zenon_X8 zenon_X498 zenon_X97) zenon_X97)
% 0.90/1.09  (zenon_X487 != (skc62))
% 0.90/1.09  (member zenon_X102 (skf10 zenon_X102 zenon_X151) zenon_X151)
% 0.90/1.09  (fellow (skc62) (skf21 zenon_X181 (skc62) zenon_X652))
% 0.90/1.09  ((skc63) != zenon_X298)
% 0.90/1.09  *)
% 0.90/1.09  (* NO-PROOF *)
% 0.90/1.09  % SZS status GaveUp
% 0.90/1.09  Number of rewrites on terms: 0
% 0.90/1.09  Number of rewrites on props: 0
% 0.90/1.09  nodes searched: 17588
% 0.90/1.09  max branch formulas: 3063
% 0.90/1.09  proof nodes created: 815
% 0.90/1.09  formulas created: 53603
% 0.90/1.09  
%------------------------------------------------------------------------------