↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n009.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:23 EDT 2024

% Result   : Unknown 3.67s 3.93s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10  % Problem  : NLP125-1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.10  % Command  : run_zenon_modulo %d %s
% 0.10/0.30  % Computer : n009.cluster.edu
% 0.10/0.30  % Model    : x86_64 x86_64
% 0.10/0.30  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30  % Memory   : 8042.1875MB
% 0.10/0.30  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30  % CPULimit : 300
% 0.10/0.30  % WCLimit  : 300
% 0.10/0.30  % DateTime : Sat Jun 22 23:11:53 EDT 2024
% 0.10/0.30  % CPUTime  : 
% 3.67/3.92  Zenon error: exhausted search space without finding a proof
% 3.67/3.92  (* Current branch:
% 3.67/3.92  (zenon_X54 != zenon_X68)
% 3.67/3.92  (specific zenon_X60 (skc7))
% 3.67/3.92  ((skc6) != zenon_X104)
% 3.67/3.92  (-. (artifact zenon_X64 zenon_X239))
% 3.67/3.92  ((skc7) != zenon_X71)
% 3.67/3.92  ((skc7) != zenon_X244)
% 3.67/3.92  (zenon_X60 != zenon_X26)
% 3.67/3.92  (singleton zenon_X6 (skc8))
% 3.67/3.92  ((skc7) != zenon_X371)
% 3.67/3.92  (artifact zenon_X20 (skc7))
% 3.67/3.92  (object zenon_X60 (skc7))
% 3.67/3.92  (-. (hollywood_placename zenon_X24 zenon_X182))
% 3.67/3.92  (-. (city zenon_X18 zenon_X312))
% 3.67/3.92  (transport zenon_X24 (skc7))
% 3.67/3.92  ((skc8) != zenon_X355)
% 3.67/3.92  (-. (entity zenon_X54 zenon_X508))
% 3.67/3.92  (-. (entity zenon_X26 (skc7)))
% 3.67/3.92  (zenon_X0 != zenon_X64)
% 3.67/3.92  ((skc8) != zenon_X351)
% 3.67/3.92  ((skc8) != zenon_X100)
% 3.67/3.92  (-. (city zenon_X20 zenon_X345))
% 3.67/3.92  (zenon_X20 != zenon_X68)
% 3.67/3.92  (zenon_X26 != zenon_X52)
% 3.67/3.92  (-. (entity zenon_X58 zenon_X526))
% 3.67/3.92  (unisex zenon_X12 (skc6))
% 3.67/3.92  ((skc6) != zenon_X249)
% 3.67/3.92  ((skc8) != zenon_X102)
% 3.67/3.92  ((skc8) != zenon_X154)
% 3.67/3.92  (-. (artifact zenon_X54 zenon_X480))
% 3.67/3.92  (artifact zenon_X64 (skc7))
% 3.67/3.92  (-. (chevy zenon_X20 zenon_X528))
% 3.67/3.92  (-. (city zenon_X16 zenon_X437))
% 3.67/3.92  (zenon_X64 != zenon_X26)
% 3.67/3.92  (-. (way zenon_X8 (skc8)))
% 3.67/3.92  (-. (placename zenon_X0 (skc9)))
% 3.67/3.92  ((skc7) != zenon_X210)
% 3.67/3.92  (-. (transport zenon_X26 zenon_X436))
% 3.67/3.92  (down (skc5) (skc6) (skc8))
% 3.67/3.92  (-. (entity zenon_X26 zenon_X353))
% 3.67/3.92  ((skc7) != zenon_X360)
% 3.67/3.92  ((skc8) != zenon_X257)
% 3.67/3.92  ((skc6) != zenon_X109)
% 3.67/3.92  ((skc8) != zenon_X134)
% 3.67/3.92  ((skc7) != zenon_X79)
% 3.67/3.92  (object zenon_X50 (skc8))
% 3.67/3.92  (-. (eventuality zenon_X12 zenon_X13))
% 3.67/3.92  ((skc7) != zenon_X163)
% 3.67/3.92  (specific zenon_X0 (skc7))
% 3.67/3.92  (-. (hollywood_placename zenon_X8 zenon_X168))
% 3.67/3.92  (-. (transport zenon_X14 zenon_X438))
% 3.67/3.92  (-. (placename zenon_X52 zenon_X152))
% 3.67/3.92  (-. (placename zenon_X50 (skc9)))
% 3.67/3.92  (artifact zenon_X0 (skc7))
% 3.67/3.92  (-. (car zenon_X14 zenon_X525))
% 3.67/3.92  ((skc6) != zenon_X5)
% 3.67/3.92  (-. (artifact zenon_X48 zenon_X231))
% 3.67/3.92  ((skc7) != zenon_X410)
% 3.67/3.92  (specific zenon_X24 (skc8))
% 3.67/3.92  (-. (way zenon_X64 zenon_X257))
% 3.67/3.92  (-. (general zenon_X0 (skc7)))
% 3.67/3.92  (-. (abstraction zenon_X42 zenon_X43))
% 3.67/3.92  ((skc8) != zenon_X174)
% 3.67/3.92  (eventuality (skc5) (skc6))
% 3.67/3.92  (artifact zenon_X62 (skc7))
% 3.67/3.92  (-. (event zenon_X20 zenon_X279))
% 3.67/3.92  (of (skc5) (skc9) (skc8))
% 3.67/3.92  ((skc8) != zenon_X73)
% 3.67/3.92  (zenon_X52 != zenon_X68)
% 3.67/3.92  ((skc5) != zenon_X24)
% 3.67/3.92  ((skc7) != zenon_X33)
% 3.67/3.92  (-. (entity zenon_X68 zenon_X155))
% 3.67/3.92  (-. (placename zenon_X62 zenon_X189))
% 3.67/3.92  (-. (car zenon_X56 zenon_X57))
% 3.67/3.92  (-. (event zenon_X2 zenon_X3))
% 3.67/3.92  (-. (entity zenon_X60 zenon_X439))
% 3.67/3.92  (-. (object zenon_X62 (skc8)))
% 3.67/3.92  (-. (event zenon_X24 zenon_X164))
% 3.67/3.92  ((skc7) != zenon_X374)
% 3.67/3.92  ((skc8) != zenon_X173)
% 3.67/3.92  (-. (way zenon_X2 zenon_X295))
% 3.67/3.92  (zenon_X26 != zenon_X14)
% 3.67/3.92  ((skc7) != zenon_X29)
% 3.67/3.92  (-. (object zenon_X68 (skc8)))
% 3.67/3.92  ((skc9) != zenon_X43)
% 3.67/3.92  (-. (hollywood_placename zenon_X54 zenon_X475))
% 3.67/3.92  (existent zenon_X64 (skc7))
% 3.67/3.92  ((skc7) != zenon_X455)
% 3.67/3.92  (entity zenon_X14 (skc8))
% 3.67/3.92  (-. (instrumentality zenon_X24 zenon_X300))
% 3.67/3.92  (-. (general zenon_X18 (skc6)))
% 3.67/3.92  ((skc8) != zenon_X21)
% 3.67/3.92  ((skc8) != zenon_X96)
% 3.67/3.92  ((skc7) != zenon_X120)
% 3.67/3.92  (-. (street zenon_X0 zenon_X339))
% 3.67/3.92  (-. (existent zenon_X20 zenon_X74))
% 3.67/3.92  (-. (general zenon_X16 (skc8)))
% 3.67/3.92  (zenon_X48 != zenon_X50)
% 3.67/3.92  (-. (eventuality zenon_X14 zenon_X359))
% 3.67/3.92  (-. (artifact zenon_X18 zenon_X19))
% 3.67/3.92  ((skc6) != zenon_X245)
% 3.67/3.92  (-. (entity zenon_X50 zenon_X242))
% 3.67/3.92  (zenon_X48 != zenon_X66)
% 3.67/3.92  (in (skc5) (skc6) (skc8))
% 3.67/3.92  (object zenon_X62 (skc7))
% 3.67/3.92  (existent zenon_X26 (skc8))
% 3.67/3.92  (-. (event zenon_X20 (skc6)))
% 3.67/3.92  (-. (transport zenon_X26 (skc7)))
% 3.67/3.92  (-. (city zenon_X60 zenon_X419))
% 3.67/3.92  (zenon_X50 != zenon_X2)
% 3.67/3.92  ((skc7) != zenon_X351)
% 3.67/3.92  (artifact (skc5) (skc8))
% 3.67/3.92  ((skc6) != zenon_X279)
% 3.67/3.92  (specific zenon_X16 (skc7))
% 3.67/3.92  (-. (chevy zenon_X48 zenon_X509))
% 3.67/3.92  (-. (specific zenon_X20 (skc6)))
% 3.67/3.92  ((skc7) != zenon_X21)
% 3.67/3.92  (zenon_X62 != zenon_X68)
% 3.67/3.92  (zenon_X50 != zenon_X20)
% 3.67/3.92  ((skc7) != zenon_X336)
% 3.67/3.92  (zenon_X60 != zenon_X2)
% 3.67/3.92  (-. (entity zenon_X66 zenon_X237))
% 3.67/3.92  (zenon_X24 != zenon_X60)
% 3.67/3.92  (specific zenon_X54 (skc7))
% 3.67/3.92  (-. (barrel zenon_X66 zenon_X198))
% 3.67/3.92  (-. (entity zenon_X24 zenon_X264))
% 3.67/3.92  (-. (artifact zenon_X68 zenon_X120))
% 3.67/3.92  (-. (general zenon_X64 (skc7)))
% 3.67/3.92  (-. (street zenon_X48 zenon_X321))
% 3.67/3.92  ((skc7) != zenon_X288)
% 3.67/3.92  (actual_world (skc5))
% 3.67/3.92  (-. (way zenon_X16 zenon_X17))
% 3.67/3.92  (-. (way zenon_X60 (skc8)))
% 3.67/3.92  ((skc8) != zenon_X243)
% 3.67/3.92  (-. (nonexistent zenon_X14 (skc8)))
% 3.67/3.92  (thing zenon_X22 (skc8))
% 3.67/3.92  (-. (entity zenon_X64 (skc8)))
% 3.67/3.92  (-. (event zenon_X62 zenon_X362))
% 3.67/3.92  (artifact zenon_X16 (skc8))
% 3.67/3.92  (-. (placename zenon_X48 zenon_X144))
% 3.67/3.92  (zenon_X62 != zenon_X52)
% 3.67/3.92  (existent zenon_X52 (skc8))
% 3.67/3.92  ((skc7) != zenon_X206)
% 3.67/3.92  (hollywood_placename (skc5) (skc9))
% 3.67/3.92  (-. (eventuality zenon_X56 zenon_X524))
% 3.67/3.92  (-. (artifact zenon_X50 zenon_X304))
% 3.67/3.92  (zenon_X54 != zenon_X26)
% 3.67/3.92  (-. (transport zenon_X50 zenon_X430))
% 3.67/3.92  ((skc8) != zenon_X92)
% 3.67/3.92  (-. (barrel zenon_X54 zenon_X497))
% 3.67/3.92  ((skc9) != zenon_X200)
% 3.67/3.92  (zenon_X64 != zenon_X68)
% 3.67/3.92  ((skc8) != zenon_X127)
% 3.67/3.92  (-. (hollywood_placename zenon_X56 zenon_X478))
% 3.67/3.92  (specific zenon_X52 (skc8))
% 3.67/3.92  (-. (placename (skc5) zenon_X86))
% 3.67/3.92  (-. (nonexistent zenon_X50 (skc8)))
% 3.67/3.92  (existent zenon_X62 (skc7))
% 3.67/3.92  ((skc8) != zenon_X388)
% 3.67/3.92  (-. (entity zenon_X22 zenon_X23))
% 3.67/3.92  ((skc7) != zenon_X287)
% 3.67/3.92  ((skc7) != zenon_X307)
% 3.67/3.92  (-. (entity zenon_X18 zenon_X333))
% 3.67/3.92  (-. (specific zenon_X24 (skc6)))
% 3.67/3.92  ((skc9) != zenon_X123)
% 3.67/3.92  (-. (location zenon_X8 zenon_X289))
% 3.67/3.92  (-. (transport zenon_X60 zenon_X61))
% 3.67/3.92  ((skc8) != zenon_X51)
% 3.67/3.92  (-. (entity zenon_X60 zenon_X343))
% 3.67/3.92  ((skc8) != zenon_X369)
% 3.67/3.92  (zenon_X62 != zenon_X24)
% 3.67/3.92  (-. (general zenon_X20 (skc8)))
% 3.67/3.92  (entity zenon_X62 (skc7))
% 3.67/3.92  (zenon_X50 != zenon_X24)
% 3.67/3.92  (-. (location zenon_X56 zenon_X489))
% 3.67/3.92  (location (skc5) (skc8))
% 3.67/3.92  (specific zenon_X66 (skc7))
% 3.67/3.92  (zenon_X2 != zenon_X64)
% 3.67/3.92  ((skc7) != zenon_X320)
% 3.67/3.92  (transport zenon_X48 (skc7))
% 3.67/3.92  (-. (hollywood_placename (skc5) zenon_X160))
% 3.67/3.92  (-. (entity zenon_X20 zenon_X80))
% 3.67/3.92  ((skc8) != zenon_X149)
% 3.67/3.92  (-. (general zenon_X0 (skc6)))
% 3.67/3.92  ((skc8) != zenon_X116)
% 3.67/3.92  (-. (instrumentality zenon_X20 zenon_X310))
% 3.67/3.92  ((skc8) != zenon_X339)
% 3.67/3.92  (zenon_X20 != zenon_X56)
% 3.67/3.92  (zenon_X56 != zenon_X2)
% 3.67/3.92  (-. (barrel zenon_X0 zenon_X1))
% 3.67/3.92  (-. (entity zenon_X18 zenon_X124))
% 3.67/3.92  (-. (entity zenon_X62 zenon_X306))
% 3.67/3.92  ((skc8) != zenon_X236)
% 3.67/3.92  (-. (object zenon_X56 (skc8)))
% 3.67/3.92  (zenon_X58 != zenon_X52)
% 3.67/3.92  ((skc6) != zenon_X236)
% 3.67/3.92  (-. (entity (skc5) zenon_X89))
% 3.67/3.92  ((skc6) != zenon_X253)
% 3.67/3.92  ((skc8) != zenon_X214)
% 3.67/3.92  ((skc8) != zenon_X444)
% 3.67/3.92  (-. (street zenon_X58 zenon_X448))
% 3.67/3.92  (car zenon_X54 (skc7))
% 3.67/3.92  (zenon_X0 != zenon_X26)
% 3.67/3.92  (zenon_X60 != zenon_X52)
% 3.67/3.92  (existent zenon_X24 (skc8))
% 3.67/3.92  (-. (location zenon_X64 zenon_X247))
% 3.67/3.92  (-. (vehicle (skc5) zenon_X288))
% 3.67/3.92  (-. (vehicle zenon_X52 zenon_X405))
% 3.67/3.92  (-. (barrel zenon_X14 zenon_X392))
% 3.67/3.92  (-. (hollywood_placename zenon_X26 zenon_X316))
% 3.67/3.92  (-. (nonexistent zenon_X0 (skc7)))
% 3.67/3.92  ((skc8) != zenon_X89)
% 3.67/3.92  (-. (barrel zenon_X8 zenon_X207))
% 3.67/3.92  ((skc5) != zenon_X66)
% 3.67/3.92  (-. (barrel zenon_X60 zenon_X396))
% 3.67/3.92  ((skc9) != zenon_X160)
% 3.67/3.92  ((skc7) != zenon_X447)
% 3.67/3.92  (zenon_X16 != zenon_X60)
% 3.67/3.92  (-. (entity zenon_X20 zenon_X76))
% 3.67/3.92  (-. (general zenon_X48 (skc7)))
% 3.67/3.92  (zenon_X18 != zenon_X2)
% 3.67/3.92  (zenon_X16 != zenon_X14)
% 3.67/3.92  ((skc7) != zenon_X125)
% 3.67/3.92  (-. (event zenon_X26 zenon_X402))
% 3.67/3.92  (zenon_X48 != zenon_X60)
% 3.67/3.92  (-. (object zenon_X54 zenon_X496))
% 3.67/3.92  (-. (chevy (skc5) zenon_X455))
% 3.67/3.92  (thing zenon_X4 (skc6))
% 3.67/3.92  (specific zenon_X24 (skc7))
% 3.67/3.92  ((skc8) != zenon_X124)
% 3.67/3.92  ((skc7) != zenon_X239)
% 3.67/3.92  ((skc7) != zenon_X372)
% 3.67/3.92  (zenon_X14 != zenon_X64)
% 3.67/3.92  (object zenon_X48 (skc7))
% 3.67/3.92  (-. (entity zenon_X0 zenon_X174))
% 3.67/3.92  (-. (way zenon_X8 zenon_X228))
% 3.67/3.92  (-. (city zenon_X62 zenon_X420))
% 3.67/3.92  ((skc7) != zenon_X440)
% 3.67/3.92  (street (skc5) (skc8))
% 3.67/3.92  (-. (entity zenon_X16 zenon_X381))
% 3.67/3.92  (-. (abstraction zenon_X44 zenon_X45))
% 3.67/3.92  (zenon_X26 != zenon_X68)
% 3.67/3.92  ((skc8) != zenon_X169)
% 3.67/3.92  (-. (street zenon_X64 zenon_X375))
% 3.67/3.92  (-. (car zenon_X24 zenon_X513))
% 3.67/3.92  (-. (entity zenon_X68 zenon_X71))
% 3.67/3.92  ((skc7) != zenon_X27)
% 3.67/3.92  ((skc9) != zenon_X168)
% 3.67/3.92  ((skc7) != zenon_X234)
% 3.67/3.92  ((skc9) != zenon_X7)
% 3.67/3.92  (impartial zenon_X30 (skc7))
% 3.67/3.92  ((skc8) != zenon_X142)
% 3.67/3.92  (-. (location zenon_X2 (skc8)))
% 3.67/3.92  (-. (barrel zenon_X56 zenon_X463))
% 3.67/3.92  (-. (entity zenon_X56 zenon_X444))
% 3.67/3.92  (-. (existent zenon_X52 (skc7)))
% 3.67/3.92  (-. (location zenon_X24 zenon_X248))
% 3.67/3.92  (nonexistent zenon_X10 (skc6))
% 3.67/3.92  (-. (nonexistent zenon_X20 (skc7)))
% 3.67/3.92  ((skc7) != zenon_X201)
% 3.67/3.92  (zenon_X18 != zenon_X54)
% 3.67/3.92  ((skc8) != zenon_X113)
% 3.67/3.92  (entity zenon_X66 (skc7))
% 3.67/3.92  (-. (entity zenon_X60 zenon_X414))
% 3.67/3.92  (zenon_X16 != zenon_X54)
% 3.67/3.92  (-. (eventuality zenon_X54 zenon_X519))
% 3.67/3.92  (-. (object zenon_X54 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X105)
% 3.67/3.92  (-. (location zenon_X52 zenon_X53))
% 3.67/3.92  ((skc6) != zenon_X7)
% 3.67/3.92  (artifact zenon_X50 (skc8))
% 3.67/3.92  (-. (way zenon_X14 zenon_X391))
% 3.67/3.92  (zenon_X2 != zenon_X68)
% 3.67/3.92  ((skc7) != zenon_X153)
% 3.67/3.92  ((skc7) != zenon_X157)
% 3.67/3.92  ((skc5) != zenon_X16)
% 3.67/3.92  (-. (existent zenon_X16 zenon_X117))
% 3.67/3.92  ((skc9) != zenon_X37)
% 3.67/3.92  (zenon_X58 != zenon_X2)
% 3.67/3.92  (-. (vehicle zenon_X52 (skc7)))
% 3.67/3.92  ((skc7) != zenon_X91)
% 3.67/3.92  (-. (artifact zenon_X24 zenon_X244))
% 3.67/3.92  (-. (hollywood_placename zenon_X14 zenon_X361))
% 3.67/3.92  (specific (skc5) (skc8))
% 3.67/3.92  (zenon_X26 != zenon_X2)
% 3.67/3.92  ((skc8) != zenon_X320)
% 3.67/3.92  (-. (event zenon_X56 zenon_X531))
% 3.67/3.92  (-. (existent zenon_X50 (skc7)))
% 3.67/3.92  (zenon_X62 != zenon_X2)
% 3.67/3.92  (-. (entity zenon_X50 zenon_X221))
% 3.67/3.92  (-. (nonexistent zenon_X24 (skc8)))
% 3.67/3.92  (-. (eventuality zenon_X68 zenon_X253))
% 3.67/3.92  ((skc8) != zenon_X101)
% 3.67/3.92  (zenon_X24 != zenon_X68)
% 3.67/3.92  (-. (object zenon_X14 zenon_X355))
% 3.67/3.92  ((skc8) != zenon_X65)
% 3.67/3.92  (-. (general zenon_X18 (skc7)))
% 3.67/3.92  (-. (general (skc5) (skc8)))
% 3.67/3.92  (-. (instrumentality zenon_X26 (skc7)))
% 3.67/3.92  (-. (event zenon_X48 (skc6)))
% 3.67/3.92  (-. (instrumentality zenon_X50 zenon_X390))
% 3.67/3.92  ((skc8) != zenon_X190)
% 3.67/3.92  ((skc7) != zenon_X227)
% 3.67/3.92  (-. (artifact zenon_X56 zenon_X486))
% 3.67/3.92  (-. (artifact zenon_X2 zenon_X337))
% 3.67/3.92  (-. (object zenon_X68 zenon_X116))
% 3.67/3.92  ((skc7) != zenon_X513)
% 3.67/3.92  (-. (nonexistent (skc5) (skc8)))
% 3.67/3.92  (-. (existent zenon_X2 (skc8)))
% 3.67/3.92  (existent zenon_X16 (skc7))
% 3.67/3.92  (-. (specific (skc5) zenon_X96))
% 3.67/3.92  (-. (specific zenon_X64 (skc8)))
% 3.67/3.92  (-. (vehicle zenon_X68 (skc7)))
% 3.67/3.92  (object zenon_X56 (skc7))
% 3.67/3.92  (zenon_X8 != zenon_X62)
% 3.67/3.92  (-. (entity zenon_X60 zenon_X415))
% 3.67/3.92  (object zenon_X14 (skc8))
% 3.67/3.92  (zenon_X52 != zenon_X64)
% 3.67/3.92  ((skc7) != zenon_X400)
% 3.67/3.92  ((skc7) != zenon_X218)
% 3.67/3.92  (object zenon_X54 (skc7))
% 3.67/3.92  (event zenon_X0 (skc6))
% 3.67/3.92  (-. (object zenon_X26 (skc7)))
% 3.67/3.92  (zenon_X18 != zenon_X50)
% 3.67/3.92  (singleton zenon_X6 (skc9))
% 3.67/3.92  (specific zenon_X14 (skc8))
% 3.67/3.92  (zenon_X48 != zenon_X14)
% 3.67/3.92  ((skc9) != zenon_X86)
% 3.67/3.92  (-. (instrumentality zenon_X8 zenon_X330))
% 3.67/3.92  (general zenon_X44 (skc9))
% 3.67/3.92  (-. (street zenon_X20 zenon_X347))
% 3.67/3.92  (entity zenon_X54 (skc7))
% 3.67/3.92  ((skc7) != zenon_X275)
% 3.67/3.92  ((skc7) != zenon_X255)
% 3.67/3.92  (zenon_X8 != zenon_X20)
% 3.67/3.92  (-. (eventuality zenon_X16 zenon_X220))
% 3.67/3.92  (zenon_X24 != zenon_X64)
% 3.67/3.92  (-. (transport zenon_X2 zenon_X378))
% 3.67/3.92  ((skc7) != zenon_X81)
% 3.67/3.92  ((skc7) != zenon_X119)
% 3.67/3.92  (-. (specific zenon_X26 (skc7)))
% 3.67/3.92  (instrumentality zenon_X24 (skc7))
% 3.67/3.92  (-. (object zenon_X66 zenon_X75))
% 3.67/3.92  ((skc7) != zenon_X197)
% 3.67/3.92  (-. (city zenon_X64 zenon_X303))
% 3.67/3.92  ((skc8) != zenon_X112)
% 3.67/3.92  (placename zenon_X8 (skc9))
% 3.67/3.92  ((skc8) != zenon_X133)
% 3.67/3.92  (-. (relname zenon_X36 zenon_X37))
% 3.67/3.92  ((skc5) != zenon_X62)
% 3.67/3.92  ((skc8) != zenon_X125)
% 3.67/3.92  (specific zenon_X18 (skc7))
% 3.67/3.92  (-. (chevy zenon_X2 zenon_X510))
% 3.67/3.92  (-. (location zenon_X66 zenon_X93))
% 3.67/3.92  (zenon_X2 != zenon_X24)
% 3.67/3.92  ((skc8) != zenon_X71)
% 3.67/3.92  ((skc5) != zenon_X20)
% 3.67/3.92  (zenon_X24 != zenon_X52)
% 3.67/3.92  (-. (entity zenon_X62 zenon_X432))
% 3.67/3.92  (zenon_X48 != zenon_X68)
% 3.67/3.92  ((skc7) != zenon_X85)
% 3.67/3.92  (-. (placename zenon_X60 zenon_X342))
% 3.67/3.92  (transport zenon_X20 (skc7))
% 3.67/3.92  (-. (event zenon_X66 zenon_X195))
% 3.67/3.92  (zenon_X66 != zenon_X2)
% 3.67/3.92  ((skc6) != zenon_X293)
% 3.67/3.92  (zenon_X8 != zenon_X48)
% 3.67/3.92  (-. (placename zenon_X58 zenon_X286))
% 3.67/3.92  ((skc7) != zenon_X149)
% 3.67/3.92  (zenon_X18 != zenon_X62)
% 3.67/3.92  (-. (nonexistent zenon_X16 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X517)
% 3.67/3.92  (-. (nonexistent (skc5) (skc7)))
% 3.67/3.92  (-. (general zenon_X18 (skc8)))
% 3.67/3.92  ((skc5) != zenon_X56)
% 3.67/3.92  (-. (artifact zenon_X60 zenon_X418))
% 3.67/3.92  (zenon_X56 != zenon_X50)
% 3.67/3.92  ((skc8) != zenon_X496)
% 3.67/3.92  ((skc8) != zenon_X27)
% 3.67/3.92  (-. (chevy zenon_X68 zenon_X459))
% 3.67/3.92  (-. (vehicle zenon_X16 zenon_X484))
% 3.67/3.92  ((skc7) != zenon_X67)
% 3.67/3.92  (-. (object zenon_X28 zenon_X29))
% 3.67/3.92  (zenon_X16 != zenon_X66)
% 3.67/3.92  ((skc9) != zenon_X263)
% 3.67/3.92  (-. (event zenon_X52 zenon_X384))
% 3.67/3.92  (zenon_X52 != zenon_X54)
% 3.67/3.92  ((skc8) != zenon_X178)
% 3.67/3.92  (specific zenon_X56 (skc7))
% 3.67/3.92  (-. (nonexistent zenon_X52 (skc8)))
% 3.67/3.92  (vehicle (skc5) (skc7))
% 3.67/3.92  (zenon_X14 != zenon_X52)
% 3.67/3.92  (zenon_X8 != zenon_X66)
% 3.67/3.92  (-. (event zenon_X24 (skc6)))
% 3.67/3.92  (-. (entity zenon_X58 zenon_X287))
% 3.67/3.92  (zenon_X56 != zenon_X52)
% 3.67/3.92  (-. (chevy zenon_X16 zenon_X498))
% 3.67/3.92  ((skc8) != zenon_X474)
% 3.67/3.92  (-. (specific zenon_X18 zenon_X236))
% 3.67/3.92  (-. (location zenon_X18 zenon_X393))
% 3.67/3.92  (-. (vehicle zenon_X18 zenon_X527))
% 3.67/3.92  (placename (skc5) (skc9))
% 3.67/3.92  ((skc8) != zenon_X139)
% 3.67/3.92  ((skc8) != zenon_X105)
% 3.67/3.92  ((skc8) != zenon_X343)
% 3.67/3.92  (-. (transport zenon_X68 zenon_X277))
% 3.67/3.92  (zenon_X8 != zenon_X58)
% 3.67/3.92  ((skc7) != zenon_X137)
% 3.67/3.92  (-. (object zenon_X52 zenon_X112))
% 3.67/3.92  (specific zenon_X50 (skc8))
% 3.67/3.92  (-. (street zenon_X68 zenon_X382))
% 3.67/3.92  (zenon_X50 != zenon_X64)
% 3.67/3.92  (-. (location zenon_X48 zenon_X323))
% 3.67/3.92  (-. (barrel zenon_X26 zenon_X301))
% 3.67/3.92  ((skc7) != zenon_X280)
% 3.67/3.92  (-. (existent zenon_X66 zenon_X67))
% 3.67/3.92  ((skc7) != zenon_X72)
% 3.67/3.92  (-. (entity zenon_X58 (skc8)))
% 3.67/3.92  (-. (entity zenon_X56 (skc8)))
% 3.67/3.92  ((skc8) != zenon_X231)
% 3.67/3.92  ((skc6) != zenon_X132)
% 3.67/3.92  (-. (specific zenon_X50 zenon_X243))
% 3.67/3.92  (chevy (skc5) (skc7))
% 3.67/3.92  ((skc5) != zenon_X2)
% 3.67/3.92  (-. (transport zenon_X0 zenon_X386))
% 3.67/3.92  (zenon_X18 != zenon_X52)
% 3.67/3.92  (eventuality zenon_X50 (skc6))
% 3.67/3.92  (eventuality zenon_X16 (skc6))
% 3.67/3.92  (zenon_X14 != zenon_X60)
% 3.67/3.92  (zenon_X16 != zenon_X26)
% 3.67/3.92  (vehicle zenon_X24 (skc7))
% 3.67/3.92  (artifact zenon_X48 (skc7))
% 3.67/3.92  (-. (nonexistent zenon_X24 (skc7)))
% 3.67/3.92  (-. (object zenon_X26 zenon_X184))
% 3.67/3.92  (-. (entity zenon_X48 zenon_X133))
% 3.67/3.92  (-. (way zenon_X48 zenon_X222))
% 3.67/3.92  (-. (specific zenon_X26 zenon_X245))
% 3.67/3.92  (-. (object zenon_X50 zenon_X256))
% 3.67/3.92  (object zenon_X24 (skc7))
% 3.67/3.92  (-. (location zenon_X58 zenon_X412))
% 3.67/3.92  (zenon_X18 != zenon_X66)
% 3.67/3.92  ((skc7) != zenon_X25)
% 3.67/3.92  (-. (existent zenon_X50 zenon_X119))
% 3.67/3.92  ((skc5) != zenon_X48)
% 3.67/3.92  (-. (entity zenon_X54 zenon_X512))
% 3.67/3.92  (-. (entity zenon_X62 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X118)
% 3.67/3.92  (-. (city zenon_X0 zenon_X406))
% 3.67/3.92  (artifact zenon_X14 (skc8))
% 3.67/3.92  ((skc7) != zenon_X416)
% 3.67/3.92  (transport zenon_X58 (skc7))
% 3.67/3.92  (-. (specific zenon_X2 (skc7)))
% 3.67/3.92  ((skc7) != zenon_X154)
% 3.67/3.92  (-. (general zenon_X50 (skc6)))
% 3.67/3.92  ((skc7) != zenon_X343)
% 3.67/3.92  (specific zenon_X18 (skc8))
% 3.67/3.92  (-. (transport zenon_X52 (skc7)))
% 3.67/3.92  ((skc7) != zenon_X283)
% 3.67/3.92  (-. (entity zenon_X54 (skc8)))
% 3.67/3.92  (zenon_X50 != zenon_X68)
% 3.67/3.92  ((skc8) != zenon_X162)
% 3.67/3.92  (singleton zenon_X6 (skc7))
% 3.67/3.92  (-. (placename zenon_X64 zenon_X251))
% 3.67/3.92  (-. (entity zenon_X68 (skc7)))
% 3.67/3.92  (-. (general zenon_X52 (skc8)))
% 3.67/3.92  (entity zenon_X18 (skc7))
% 3.67/3.92  ((skc7) != zenon_X132)
% 3.67/3.92  ((skc8) != zenon_X67)
% 3.67/3.92  (-. (eventuality zenon_X52 zenon_X223))
% 3.67/3.92  (unisex zenon_X46 (skc9))
% 3.67/3.92  ((skc6) != zenon_X164)
% 3.67/3.92  ((skc7) != zenon_X306)
% 3.67/3.92  (-. (entity zenon_X66 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X297)
% 3.67/3.92  (-. (general zenon_X24 (skc7)))
% 3.67/3.92  ((skc8) != zenon_X383)
% 3.67/3.92  ((skc5) != zenon_X18)
% 3.67/3.92  (-. (entity zenon_X24 zenon_X25))
% 3.67/3.92  (-. (hollywood_placename zenon_X66 zenon_X158))
% 3.67/3.92  ((skc5) != zenon_X60)
% 3.67/3.92  (-. (transport zenon_X20 zenon_X372))
% 3.67/3.92  (-. (barrel zenon_X64 zenon_X103))
% 3.67/3.92  (-. (general zenon_X14 (skc6)))
% 3.67/3.92  (-. (general zenon_X50 (skc8)))
% 3.67/3.92  (-. (way zenon_X68 (skc8)))
% 3.67/3.92  (-. (specific zenon_X52 (skc6)))
% 3.67/3.92  (-. (event zenon_X14 zenon_X366))
% 3.67/3.92  (-. (existent zenon_X48 zenon_X215))
% 3.67/3.92  ((skc6) != zenon_X9)
% 3.67/3.92  ((skc7) != zenon_X192)
% 3.67/3.92  ((skc7) != zenon_X298)
% 3.67/3.92  (existent zenon_X26 (skc7))
% 3.67/3.92  (-. (entity zenon_X52 zenon_X153))
% 3.67/3.92  (-. (eventuality zenon_X4 zenon_X5))
% 3.67/3.92  (zenon_X52 != zenon_X66)
% 3.67/3.92  (-. (eventuality zenon_X0 zenon_X193))
% 3.67/3.92  (-. (existent zenon_X68 (skc7)))
% 3.67/3.92  ((skc6) != zenon_X193)
% 3.67/3.92  (zenon_X18 != zenon_X26)
% 3.67/3.92  (-. (eventuality zenon_X58 zenon_X514))
% 3.67/3.92  ((skc9) != zenon_X148)
% 3.67/3.92  (-. (eventuality zenon_X48 zenon_X167))
% 3.67/3.92  ((skc6) != zenon_X1)
% 3.67/3.92  ((skc6) != zenon_X3)
% 3.67/3.92  ((skc8) != zenon_X25)
% 3.67/3.92  ((skc6) != zenon_X163)
% 3.67/3.92  (zenon_X14 != zenon_X2)
% 3.67/3.92  (-. (existent zenon_X24 zenon_X214))
% 3.67/3.92  ((skc7) != zenon_X134)
% 3.67/3.92  (-. (object zenon_X2 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X116)
% 3.67/3.92  (instrumentality zenon_X18 (skc7))
% 3.67/3.92  (zenon_X20 != zenon_X64)
% 3.67/3.92  (nonliving zenon_X28 (skc8))
% 3.67/3.92  ((skc7) != zenon_X139)
% 3.67/3.92  (-. (barrel zenon_X62 zenon_X309))
% 3.67/3.92  (specific zenon_X50 (skc6))
% 3.67/3.92  ((skc8) != zenon_X391)
% 3.67/3.92  ((skc7) != zenon_X444)
% 3.67/3.92  (-. (object zenon_X0 zenon_X192))
% 3.67/3.92  (-. (existent zenon_X2 zenon_X267))
% 3.67/3.92  (event (skc5) (skc6))
% 3.67/3.92  (zenon_X18 != zenon_X14)
% 3.67/3.92  ((skc8) != zenon_X93)
% 3.67/3.92  ((skc8) != zenon_X132)
% 3.67/3.92  (transport zenon_X18 (skc7))
% 3.67/3.92  (-. (car zenon_X2 zenon_X517))
% 3.67/3.92  (lonely (skc5) (skc8))
% 3.67/3.92  ((skc7) != zenon_X214)
% 3.67/3.92  (-. (city zenon_X24 zenon_X363))
% 3.67/3.92  (-. (entity zenon_X20 zenon_X79))
% 3.67/3.92  (zenon_X8 != zenon_X24)
% 3.67/3.92  (-. (street zenon_X62 zenon_X354))
% 3.67/3.92  (-. (entity zenon_X48 zenon_X149))
% 3.67/3.92  ((skc8) != zenon_X29)
% 3.67/3.92  (-. (hollywood_placename zenon_X18 zenon_X281))
% 3.67/3.92  ((skc7) != zenon_X202)
% 3.67/3.92  ((skc6) != zenon_X284)
% 3.67/3.92  ((skc7) != zenon_X405)
% 3.67/3.92  ((skc7) != zenon_X59)
% 3.67/3.92  ((skc8) != zenon_X248)
% 3.67/3.92  (zenon_X24 != zenon_X56)
% 3.67/3.92  (-. (specific zenon_X64 (skc6)))
% 3.67/3.92  ((skc7) != zenon_X302)
% 3.67/3.92  (-. (general zenon_X0 (skc8)))
% 3.67/3.92  (entity zenon_X50 (skc8))
% 3.67/3.92  (-. (existent zenon_X68 zenon_X115))
% 3.67/3.92  (-. (city (skc5) zenon_X131))
% 3.67/3.92  (-. (placename zenon_X54 zenon_X453))
% 3.67/3.92  (-. (specific zenon_X68 zenon_X325))
% 3.67/3.92  (-. (car zenon_X50 zenon_X503))
% 3.67/3.92  ((skc7) != zenon_X74)
% 3.67/3.92  (-. (location zenon_X68 (skc8)))
% 3.67/3.92  (-. (specific zenon_X14 (skc7)))
% 3.67/3.92  (-. (placename zenon_X24 zenon_X263))
% 3.67/3.92  (-. (vehicle zenon_X8 zenon_X297))
% 3.67/3.92  ((skc6) != zenon_X359)
% 3.67/3.92  (-. (entity zenon_X24 zenon_X434))
% 3.67/3.92  (zenon_X18 != zenon_X68)
% 3.67/3.92  (-. (barrel zenon_X68 zenon_X329))
% 3.67/3.92  (-. (chevy zenon_X24 zenon_X511))
% 3.67/3.92  ((skc7) != zenon_X107)
% 3.67/3.92  (-. (existent (skc5) zenon_X85))
% 3.67/3.92  (-. (car zenon_X48 zenon_X488))
% 3.67/3.92  (object zenon_X0 (skc8))
% 3.67/3.92  ((skc7) != zenon_X414)
% 3.67/3.92  (-. (street zenon_X54 zenon_X506))
% 3.67/3.92  (-. (location zenon_X2 zenon_X388))
% 3.67/3.92  (transport (skc5) (skc7))
% 3.67/3.92  (-. (entity zenon_X56 zenon_X541))
% 3.67/3.92  (zenon_X24 != zenon_X58)
% 3.67/3.92  (-. (chevy zenon_X14 zenon_X493))
% 3.67/3.92  (-. (placename zenon_X18 zenon_X123))
% 3.67/3.92  (instrumentality zenon_X20 (skc7))
% 3.67/3.92  (-. (street zenon_X60 zenon_X441))
% 3.67/3.92  ((skc8) != zenon_X334)
% 3.67/3.92  (-. (entity zenon_X8 zenon_X331))
% 3.67/3.92  (object zenon_X52 (skc8))
% 3.67/3.92  ((skc7) != zenon_X147)
% 3.67/3.92  ((skc6) != zenon_X99)
% 3.67/3.92  ((skc8) != zenon_X275)
% 3.67/3.92  (-. (vehicle zenon_X26 zenon_X521))
% 3.67/3.92  (instrumentality zenon_X60 (skc7))
% 3.67/3.92  (-. (object zenon_X2 (skc7)))
% 3.67/3.92  ((skc8) != zenon_X244)
% 3.67/3.92  (-. (street zenon_X66 zenon_X141))
% 3.67/3.92  (zenon_X14 != zenon_X8)
% 3.67/3.92  (zenon_X16 != zenon_X50)
% 3.67/3.92  (-. (artifact zenon_X68 (skc7)))
% 3.67/3.92  (-. (hollywood_placename zenon_X0 zenon_X180))
% 3.67/3.92  ((skc7) != zenon_X480)
% 3.67/3.92  (zenon_X50 != zenon_X66)
% 3.67/3.92  (existent zenon_X66 (skc7))
% 3.67/3.92  (-. (object zenon_X64 zenon_X134))
% 3.67/3.92  (-. (event zenon_X54 zenon_X530))
% 3.67/3.92  (-. (artifact zenon_X20 zenon_X292))
% 3.67/3.92  (-. (specific zenon_X2 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X260)
% 3.67/3.92  (-. (event zenon_X48 zenon_X233))
% 3.67/3.92  (-. (entity zenon_X14 zenon_X340))
% 3.67/3.92  (-. (artifact zenon_X62 zenon_X431))
% 3.67/3.92  (-. (chevy zenon_X0 zenon_X504))
% 3.67/3.92  (zenon_X0 != zenon_X68)
% 3.67/3.92  (-. (entity zenon_X54 zenon_X454))
% 3.67/3.92  ((skc7) != zenon_X496)
% 3.67/3.92  (object zenon_X24 (skc8))
% 3.67/3.92  ((skc6) != zenon_X334)
% 3.67/3.92  (-. (placename zenon_X52 (skc9)))
% 3.67/3.92  (-. (street zenon_X52 zenon_X364))
% 3.67/3.92  (artifact zenon_X18 (skc7))
% 3.67/3.92  (-. (event zenon_X64 zenon_X95))
% 3.67/3.92  (-. (instrumentality zenon_X2 zenon_X294))
% 3.67/3.92  (zenon_X48 != zenon_X58)
% 3.67/3.92  ((skc6) != zenon_X230)
% 3.67/3.92  (-. (artifact (skc5) zenon_X125))
% 3.67/3.92  (-. (way zenon_X68 zenon_X169))
% 3.67/3.92  (zenon_X16 != zenon_X62)
% 3.67/3.92  (-. (specific zenon_X52 (skc7)))
% 3.67/3.92  ((skc9) != zenon_X35)
% 3.67/3.92  (zenon_X62 != zenon_X64)
% 3.67/3.92  (-. (eventuality zenon_X18 zenon_X230))
% 3.67/3.92  (zenon_X16 != zenon_X56)
% 3.67/3.92  (-. (nonexistent zenon_X48 (skc8)))
% 3.67/3.92  ((skc5) != zenon_X64)
% 3.67/3.92  (-. (object zenon_X20 zenon_X21))
% 3.67/3.92  (zenon_X16 != zenon_X68)
% 3.67/3.92  (-. (entity zenon_X0 zenon_X320))
% 3.67/3.92  ((skc7) != zenon_X104)
% 3.67/3.92  (-. (existent zenon_X68 (skc8)))
% 3.67/3.92  (-. (entity zenon_X2 zenon_X335))
% 3.67/3.92  ((skc6) != zenon_X96)
% 3.67/3.92  (artifact zenon_X48 (skc8))
% 3.67/3.92  (-. (existent zenon_X52 zenon_X91))
% 3.67/3.92  (-. (way zenon_X64 (skc8)))
% 3.67/3.92  ((skc8) != zenon_X76)
% 3.67/3.92  (-. (placename zenon_X56 zenon_X443))
% 3.67/3.92  (-. (general zenon_X62 (skc6)))
% 3.67/3.92  (nonhuman zenon_X42 (skc9))
% 3.67/3.92  (specific (skc5) (skc6))
% 3.67/3.92  (entity (skc5) (skc7))
% 3.67/3.92  (object zenon_X18 (skc7))
% 3.67/3.92  (-. (hollywood_placename zenon_X50 zenon_X313))
% 3.67/3.92  (-. (city zenon_X48 zenon_X232))
% 3.67/3.92  (existent zenon_X58 (skc7))
% 3.67/3.92  ((skc7) != zenon_X181)
% 3.67/3.92  (-. (chevy zenon_X26 zenon_X522))
% 3.67/3.92  ((skc5) != zenon_X52)
% 3.67/3.92  (-. (eventuality zenon_X50 zenon_X249))
% 3.67/3.92  (entity zenon_X56 (skc7))
% 3.67/3.92  ((skc8) != zenon_X81)
% 3.67/3.92  (-. (way zenon_X54 zenon_X507))
% 3.67/3.92  ((skc6) != zenon_X220)
% 3.67/3.92  (-. (object zenon_X62 zenon_X197))
% 3.67/3.92  (zenon_X48 != zenon_X62)
% 3.67/3.92  (-. (car zenon_X8 (skc7)))
% 3.67/3.92  ((skc7) != zenon_X236)
% 3.67/3.92  (-. (chevy zenon_X54 zenon_X55))
% 3.67/3.92  ((skc6) != zenon_X296)
% 3.67/3.92  (-. (entity zenon_X18 zenon_X140))
% 3.67/3.92  (-. (eventuality zenon_X66 zenon_X219))
% 3.67/3.92  (-. (transport zenon_X2 (skc7)))
% 3.67/3.92  ((skc8) != zenon_X218)
% 3.67/3.92  (-. (street zenon_X56 zenon_X490))
% 3.67/3.92  (relname zenon_X34 (skc9))
% 3.67/3.92  (-. (way zenon_X52 zenon_X225))
% 3.67/3.92  ((skc6) != zenon_X223)
% 3.67/3.92  ((skc6) != zenon_X105)
% 3.67/3.92  (-. (eventuality zenon_X62 zenon_X284))
% 3.67/3.92  ((skc8) != zenon_X201)
% 3.67/3.92  ((skc7) != zenon_X215)
% 3.67/3.92  (agent (skc5) (skc6) (skc7))
% 3.67/3.92  (-. (car (skc5) zenon_X445))
% 3.67/3.92  ((skc7) != zenon_X508)
% 3.67/3.92  (zenon_X48 != zenon_X64)
% 3.67/3.92  (zenon_X0 != zenon_X20)
% 3.67/3.92  (zenon_X8 != zenon_X68)
% 3.67/3.92  (zenon_X8 != zenon_X16)
% 3.67/3.92  ((skc6) != zenon_X97)
% 3.67/3.92  ((skc7) != zenon_X173)
% 3.67/3.92  (specific zenon_X14 (skc6))
% 3.67/3.92  (-. (chevy zenon_X8 zenon_X534))
% 3.67/3.92  (entity (skc5) (skc8))
% 3.67/3.92  (-. (specific zenon_X8 (skc7)))
% 3.67/3.92  (instrumentality zenon_X0 (skc7))
% 3.67/3.92  (-. (artifact zenon_X66 (skc8)))
% 3.67/3.92  (-. (placename zenon_X14 zenon_X177))
% 3.67/3.92  (-. (transport zenon_X68 (skc7)))
% 3.67/3.92  (-. (chevy zenon_X52 zenon_X466))
% 3.67/3.92  (-. (object zenon_X64 (skc8)))
% 3.67/3.92  (-. (placename zenon_X16 (skc9)))
% 3.67/3.92  (instrumentality (skc5) (skc7))
% 3.67/3.92  (-. (city zenon_X52 zenon_X429))
% 3.67/3.92  ((skc7) != zenon_X237)
% 3.67/3.92  (-. (specific zenon_X16 zenon_X227))
% 3.67/3.92  ((skc5) != zenon_X58)
% 3.67/3.92  (-. (way zenon_X60 zenon_X401))
% 3.67/3.92  (existent zenon_X14 (skc8))
% 3.67/3.92  (-. (entity (skc5) zenon_X98))
% 3.67/3.92  ((skc8) != zenon_X79)
% 3.67/3.92  ((skc7) != zenon_X89)
% 3.67/3.92  (zenon_X16 != zenon_X58)
% 3.67/3.92  (specific zenon_X62 (skc7))
% 3.67/3.92  ((skc7) != zenon_X242)
% 3.67/3.92  ((skc8) != zenon_X91)
% 3.67/3.92  ((skc7) != zenon_X523)
% 3.67/3.92  ((skc8) != zenon_X146)
% 3.67/3.92  (-. (vehicle zenon_X50 zenon_X446))
% 3.67/3.92  (entity zenon_X16 (skc7))
% 3.67/3.92  ((skc9) != zenon_X47)
% 3.67/3.92  (-. (street zenon_X26 zenon_X246))
% 3.67/3.92  (-. (entity zenon_X68 zenon_X216))
% 3.67/3.92  ((skc6) != zenon_X13)
% 3.67/3.92  ((skc8) != zenon_X126)
% 3.67/3.92  (-. (location zenon_X20 zenon_X397))
% 3.67/3.92  (entity zenon_X20 (skc7))
% 3.67/3.92  ((skc8) != zenon_X80)
% 3.67/3.92  ((skc9) != (skc8))
% 3.67/3.92  (specific (skc5) (skc7))
% 3.67/3.92  (-. (placename zenon_X24 (skc9)))
% 3.67/3.92  ((skc8) != zenon_X153)
% 3.67/3.92  (zenon_X20 != zenon_X26)
% 3.67/3.92  ((skc7) != zenon_X76)
% 3.67/3.92  ((skc7) != zenon_X434)
% 3.67/3.92  ((skc7) != zenon_X61)
% 3.67/3.92  ((skc6) != zenon_X322)
% 3.67/3.92  ((skc7) != zenon_X407)
% 3.67/3.92  (zenon_X18 != zenon_X24)
% 3.67/3.92  (present (skc5) (skc6))
% 3.67/3.92  (-. (instrumentality (skc5) zenon_X191))
% 3.67/3.92  (zenon_X20 != zenon_X52)
% 3.67/3.92  (-. (object zenon_X58 (skc8)))
% 3.67/3.92  ((skc7) != zenon_X521)
% 3.67/3.92  ((skc7) != zenon_X63)
% 3.67/3.92  ((skc7) != zenon_X418)
% 3.67/3.92  ((skc7) != zenon_X292)
% 3.67/3.92  (-. (object zenon_X56 zenon_X474))
% 3.67/3.92  (specific zenon_X16 (skc8))
% 3.67/3.92  (existent zenon_X48 (skc7))
% 3.67/3.92  (-. (object zenon_X32 zenon_X33))
% 3.67/3.92  (zenon_X56 != zenon_X14)
% 3.67/3.92  (object (skc5) (skc7))
% 3.67/3.92  (-. (specific zenon_X20 zenon_X163))
% 3.67/3.92  ((skc8) != zenon_X115)
% 3.67/3.92  (-. (way zenon_X62 zenon_X308))
% 3.67/3.92  ((skc8) != zenon_X260)
% 3.67/3.92  (-. (barrel (skc5) zenon_X111))
% 3.67/3.92  ((skc8) != zenon_X400)
% 3.67/3.92  (-. (city zenon_X54 zenon_X467))
% 3.67/3.92  (-. (instrumentality zenon_X52 zenon_X210))
% 3.67/3.92  (instrumentality zenon_X48 (skc7))
% 3.67/3.92  (-. (entity zenon_X62 zenon_X190))
% 3.67/3.92  (zenon_X54 != zenon_X2)
% 3.67/3.92  ((skc7) != zenon_X55)
% 3.67/3.92  (zenon_X48 != zenon_X16)
% 3.67/3.92  (-. (eventuality zenon_X24 (skc6)))
% 3.67/3.92  (-. (event zenon_X0 zenon_X377))
% 3.67/3.92  (entity zenon_X48 (skc7))
% 3.67/3.92  ((skc8) != zenon_X221)
% 3.67/3.92  (zenon_X16 != zenon_X52)
% 3.67/3.92  (zenon_X50 != zenon_X60)
% 3.67/3.92  ((skc9) != zenon_X39)
% 3.67/3.92  (-. (general (skc5) (skc7)))
% 3.67/3.92  (specific zenon_X18 (skc6))
% 3.67/3.92  (-. (entity zenon_X16 zenon_X173))
% 3.67/3.92  (-. (entity zenon_X0 zenon_X202))
% 3.67/3.92  ((skc7) != zenon_X185)
% 3.67/3.92  ((skc6) != zenon_X142)
% 3.67/3.92  (existent zenon_X60 (skc7))
% 3.67/3.92  (-. (instrumentality zenon_X0 zenon_X206))
% 3.67/3.92  ((skc8) != zenon_X256)
% 3.67/3.92  (-. (specific zenon_X0 zenon_X105))
% 3.67/3.92  (-. (artifact zenon_X68 (skc8)))
% 3.67/3.92  ((skc8) != zenon_X23)
% 3.67/3.92  ((skc5) != zenon_X26)
% 3.67/3.92  ((skc8) != zenon_X379)
% 3.67/3.92  ((skc8) != zenon_X434)
% 3.67/3.92  (-. (entity zenon_X8 zenon_X110))
% 3.67/3.92  (-. (entity zenon_X26 zenon_X130))
% 3.67/3.92  ((skc5) != zenon_X54)
% 3.67/3.92  ((skc9) != zenon_X82)
% 3.67/3.92  (zenon_X0 != zenon_X8)
% 3.67/3.92  ((skc7) != zenon_X133)
% 3.67/3.92  ((skc8) != zenon_X163)
% 3.67/3.92  ((skc8) != zenon_X104)
% 3.67/3.92  (-. (placename zenon_X60 (skc9)))
% 3.67/3.92  ((skc7) != zenon_X527)
% 3.67/3.92  (-. (hollywood_placename zenon_X52 zenon_X211))
% 3.67/3.92  (entity zenon_X0 (skc8))
% 3.67/3.92  (-. (entity zenon_X8 zenon_X270))
% 3.67/3.92  ((skc8) != zenon_X370)
% 3.67/3.92  ((skc8) != zenon_X304)
% 3.67/3.92  (-. (existent zenon_X66 (skc8)))
% 3.67/3.92  (-. (placename zenon_X16 zenon_X172))
% 3.67/3.92  (object zenon_X66 (skc7))
% 3.67/3.92  (specific zenon_X64 (skc7))
% 3.67/3.92  (zenon_X16 != zenon_X2)
% 3.67/3.92  (-. (hollywood_placename zenon_X20 zenon_X94))
% 3.67/3.92  ((skc6) != zenon_X260)
% 3.67/3.92  (-. (hollywood_placename zenon_X60 zenon_X376))
% 3.67/3.92  ((skc7) != zenon_X115)
% 3.67/3.92  (-. (instrumentality zenon_X64 zenon_X291))
% 3.67/3.92  ((skc7) != zenon_X310)
% 3.67/3.92  (-. (car zenon_X68 zenon_X283))
% 3.67/3.92  (-. (entity zenon_X58 zenon_X416))
% 3.67/3.92  (-. (eventuality zenon_X20 zenon_X194))
% 3.67/3.92  ((skc8) != zenon_X454)
% 3.67/3.92  ((skc9) != zenon_X152)
% 3.67/3.92  (-. (chevy zenon_X18 zenon_X516))
% 3.67/3.92  (-. (entity zenon_X62 zenon_X336))
% 3.67/3.92  (-. (car zenon_X52 zenon_X426))
% 3.67/3.92  ((skc6) != zenon_X377)
% 3.67/3.92  (-. (entity zenon_X14 zenon_X178))
% 3.67/3.92  (existent zenon_X18 (skc8))
% 3.67/3.92  ((skc6) != (skc8))
% 3.67/3.92  ((skc6) != zenon_X194)
% 3.67/3.92  (zenon_X8 != zenon_X18)
% 3.67/3.92  ((skc8) != zenon_X15)
% 3.67/3.92  (-. (placename zenon_X20 (skc9)))
% 3.67/3.92  (-. (object zenon_X60 zenon_X371))
% 3.67/3.92  (-. (event zenon_X58 zenon_X311))
% 3.67/3.92  (-. (instrumentality zenon_X16 zenon_X350))
% 3.67/3.92  (-. (street zenon_X16 zenon_X411))
% 3.67/3.92  (-. (existent zenon_X2 (skc7)))
% 3.67/3.92  (-. (event zenon_X18 zenon_X322))
% 3.67/3.92  (zenon_X20 != zenon_X14)
% 3.67/3.92  ((skc8) != zenon_X242)
% 3.67/3.92  (-. (location zenon_X62 zenon_X423))
% 3.67/3.92  ((skc7) != zenon_X229)
% 3.67/3.92  ((skc8) != zenon_X340)
% 3.67/3.92  ((skc7) != zenon_X512)
% 3.67/3.92  (-. (entity zenon_X52 zenon_X100))
% 3.67/3.92  ((skc8) != zenon_X358)
% 3.67/3.92  (thing zenon_X22 (skc7))
% 3.67/3.92  (-. (entity zenon_X2 zenon_X157))
% 3.67/3.92  (-. (event zenon_X50 zenon_X299))
% 3.67/3.92  (-. (general zenon_X48 (skc8)))
% 3.67/3.92  (-. (instrumentality zenon_X48 zenon_X368))
% 3.67/3.92  ((skc7) != zenon_X469)
% 3.67/3.92  ((skc7) != zenon_X190)
% 3.67/3.92  (entity zenon_X48 (skc8))
% 3.67/3.92  ((skc8) != zenon_X117)
% 3.67/3.92  ((skc7) != zenon_X209)
% 3.67/3.92  (-. (object (skc5) zenon_X81))
% 3.67/3.92  (object (skc5) (skc8))
% 3.67/3.92  (entity zenon_X58 (skc7))
% 3.67/3.92  (-. (general (skc5) (skc6)))
% 3.67/3.92  (-. (eventuality zenon_X48 (skc6)))
% 3.67/3.92  (-. (entity zenon_X50 zenon_X358))
% 3.67/3.92  ((skc7) != zenon_X386)
% 3.67/3.92  (-. (location zenon_X54 zenon_X491))
% 3.67/3.92  (-. (barrel zenon_X20 zenon_X187))
% 3.67/3.92  (-. (eventuality (skc5) zenon_X97))
% 3.67/3.92  ((skc7) != zenon_X267)
% 3.67/3.92  (-. (location zenon_X16 zenon_X261))
% 3.67/3.92  (-. (entity zenon_X2 zenon_X319))
% 3.67/3.92  ((skc8) != zenon_X264)
% 3.67/3.92  ((skc8) != zenon_X401)
% 3.67/3.92  (specific zenon_X0 (skc6))
% 3.67/3.92  (old (skc5) (skc7))
% 3.67/3.92  (-. (abstraction zenon_X40 zenon_X41))
% 3.67/3.92  (impartial zenon_X30 (skc8))
% 3.67/3.92  ((skc8) != zenon_X118)
% 3.67/3.92  (zenon_X62 != zenon_X14)
% 3.67/3.92  ((skc7) != zenon_X19)
% 3.67/3.92  (-. (city zenon_X68 zenon_X170))
% 3.67/3.92  (artifact zenon_X24 (skc7))
% 3.67/3.92  (-. (way zenon_X58 zenon_X456))
% 3.67/3.92  ((skc5) != zenon_X0)
% 3.67/3.92  (zenon_X0 != zenon_X52)
% 3.67/3.92  (-. (transport zenon_X24 zenon_X440))
% 3.67/3.92  (object zenon_X48 (skc8))
% 3.67/3.92  (thing zenon_X40 (skc9))
% 3.67/3.92  (-. (general zenon_X24 (skc8)))
% 3.67/3.92  (-. (hollywood_placename zenon_X62 zenon_X290))
% 3.67/3.92  ((skc7) != zenon_X445)
% 3.67/3.92  (-. (abstraction zenon_X46 zenon_X47))
% 3.67/3.92  (entity zenon_X64 (skc7))
% 3.67/3.92  (-. (car zenon_X26 zenon_X500))
% 3.67/3.92  (-. (entity zenon_X48 zenon_X146))
% 3.67/3.92  (zenon_X18 != zenon_X58)
% 3.67/3.92  (object zenon_X58 (skc7))
% 3.67/3.92  (-. (way zenon_X56 zenon_X485))
% 3.67/3.93  (-. (specific zenon_X48 (skc6)))
% 3.67/3.93  (zenon_X18 != zenon_X64)
% 3.67/3.93  (-. (entity zenon_X14 zenon_X326))
% 3.67/3.93  (existent zenon_X20 (skc7))
% 3.67/3.93  ((skc9) != (skc6))
% 3.67/3.93  (zenon_X50 != zenon_X58)
% 3.67/3.93  (way (skc5) (skc8))
% 3.67/3.93  (-. (barrel zenon_X2 zenon_X387))
% 3.67/3.93  (-. (street zenon_X2 zenon_X338))
% 3.67/3.93  (white (skc5) (skc7))
% 3.67/3.93  (eventuality zenon_X18 (skc6))
% 3.67/3.93  (-. (hollywood_placename zenon_X58 zenon_X398))
% 3.67/3.93  (zenon_X24 != zenon_X54)
% 3.67/3.93  ((skc7) != zenon_X7)
% 3.67/3.93  (-. (transport (skc5) zenon_X344))
% 3.67/3.93  (singleton zenon_X6 (skc6))
% 3.67/3.93  (-. (entity zenon_X2 (skc7)))
% 3.67/3.93  (-. (vehicle zenon_X14 zenon_X447))
% 3.67/3.93  (-. (object zenon_X8 zenon_X217))
% 3.67/3.93  (-. (object zenon_X14 (skc7)))
% 3.67/3.93  (zenon_X8 != zenon_X60)
% 3.67/3.93  (eventuality zenon_X0 (skc6))
% 3.67/3.93  (-. (entity zenon_X68 (skc8)))
% 3.67/3.93  (-. (artifact zenon_X14 zenon_X379))
% 3.67/3.93  (-. (eventuality zenon_X26 zenon_X327))
% 3.67/3.93  ((skc7) != zenon_X96)
% 3.67/3.93  (-. (vehicle zenon_X20 zenon_X307))
% 3.67/3.93  (-. (placename zenon_X34 zenon_X35))
% 3.67/3.93  (-. (entity zenon_X66 zenon_X72))
% 3.67/3.93  (-. (existent zenon_X14 zenon_X229))
% 3.67/3.93  (-. (transport zenon_X48 zenon_X360))
% 3.67/3.93  ((skc7) != zenon_X326)
% 3.67/3.93  (zenon_X20 != zenon_X54)
% 3.67/3.93  ((skc8) != zenon_X393)
% 3.67/3.93  ((skc7) != zenon_X162)
% 3.67/3.93  (entity zenon_X60 (skc7))
% 3.67/3.93  ((skc9) != zenon_X49)
% 3.67/3.93  ((skc7) != zenon_X191)
% 3.67/3.93  (-. (hollywood_placename zenon_X2 zenon_X161))
% 3.67/3.93  (-. (barrel zenon_X50 zenon_X394))
% 3.67/3.93  (-. (specific zenon_X8 (skc8)))
% 3.67/3.93  (zenon_X18 != zenon_X56)
% 3.67/3.93  ((skc7) != zenon_X126)
% 3.67/3.93  ((skc8) != zenon_X267)
% 3.67/3.93  ((skc7) != zenon_X113)
% 3.67/3.93  (zenon_X0 != zenon_X56)
% 3.67/3.93  (-. (entity zenon_X66 zenon_X181))
% 3.67/3.93  (-. (location zenon_X66 (skc8)))
% 3.67/3.93  (-. (location zenon_X68 zenon_X165))
% 3.67/3.93  (transport zenon_X16 (skc7))
% 3.67/3.93  ((skc6) != zenon_X167)
% 3.67/3.93  (zenon_X16 != zenon_X64)
% 3.67/3.93  (-. (entity zenon_X18 zenon_X275))
% 3.67/3.93  (-. (vehicle zenon_X48 zenon_X298))
% 3.67/3.93  (-. (event zenon_X60 zenon_X433))
% 3.67/3.93  (zenon_X14 != zenon_X24)
% 3.67/3.93  (-. (placename (skc5) zenon_X82))
% 3.67/3.93  ((skc6) != zenon_X299)
% 3.67/3.93  (-. (existent zenon_X8 zenon_X282))
% 3.67/3.93  ((skc6) != zenon_X65)
% 3.67/3.93  (entity zenon_X52 (skc8))
% 3.67/3.93  (-. (hollywood_placename zenon_X68 zenon_X138))
% 3.67/3.93  (-. (vehicle zenon_X24 zenon_X523))
% 3.67/3.93  (zenon_X20 != zenon_X60)
% 3.67/3.93  ((skc7) != zenon_X277)
% 3.67/3.93  (car (skc5) (skc7))
% 3.67/3.93  (zenon_X58 != zenon_X68)
% 3.67/3.93  ((skc6) != (skc7))
% 3.67/3.93  (-. (entity zenon_X50 zenon_X370))
% 3.67/3.93  ((skc7) != zenon_X264)
% 3.67/3.93  ((skc7) != zenon_X296)
% 3.67/3.93  (-. (barrel zenon_X24 zenon_X186))
% 3.67/3.93  (zenon_X48 != zenon_X24)
% 3.67/3.93  ((skc8) != zenon_X131)
% 3.67/3.93  (zenon_X50 != zenon_X26)
% 3.67/3.93  (-. (general zenon_X8 (skc6)))
% 3.67/3.93  (-. (eventuality zenon_X52 (skc6)))
% 3.67/3.93  (vehicle zenon_X56 (skc7))
% 3.67/3.93  (zenon_X56 != zenon_X68)
% 3.67/3.93  ((skc9) != zenon_X342)
% 3.67/3.93  (zenon_X48 != zenon_X20)
% 3.67/3.93  (-. (car zenon_X2 (skc7)))
% 3.67/3.93  ((skc8) != zenon_X165)
% 3.67/3.93  (-. (nonexistent zenon_X26 (skc7)))
% 3.67/3.93  ((skc7) != zenon_X355)
% 3.67/3.93  (-. (existent zenon_X14 (skc7)))
% 3.67/3.93  (-. (event (skc5) zenon_X99))
% 3.67/3.93  (-. (entity zenon_X26 (skc8)))
% 3.67/3.93  (-. (entity zenon_X64 zenon_X252))
% 3.67/3.93  (-. (transport zenon_X8 zenon_X373))
% 3.67/3.93  (-. (relation zenon_X38 zenon_X39))
% 3.67/3.93  (existent (skc5) (skc8))
% 3.67/3.93  (-. (vehicle zenon_X8 (skc7)))
% 3.67/3.93  ((skc9) != zenon_X172)
% 3.67/3.93  (existent (skc5) (skc7))
% 3.67/3.93  (zenon_X26 != zenon_X66)
% 3.67/3.93  (-. (eventuality zenon_X64 zenon_X90))
% 3.67/3.93  (-. (specific zenon_X64 zenon_X65))
% 3.67/3.93  (object zenon_X64 (skc7))
% 3.67/3.93  (-. (nonexistent zenon_X20 (skc8)))
% 3.67/3.93  (zenon_X0 != zenon_X58)
% 3.67/3.93  (-. (artifact zenon_X26 zenon_X226))
% 3.67/3.93  (-. (barrel zenon_X48 zenon_X183))
% 3.67/3.93  (-. (barrel zenon_X58 zenon_X399))
% 3.67/3.93  (-. (car zenon_X18 zenon_X468))
% 3.67/3.93  ((skc8) != zenon_X422)
% 3.67/3.93  (-. (placename zenon_X20 zenon_X78))
% 3.67/3.93  ((skc8) != zenon_X245)
% 3.67/3.93  (-. (location zenon_X60 zenon_X424))
% 3.67/3.93  ((skc7) != zenon_X130)
% 3.67/3.93  (-. (vehicle zenon_X2 (skc7)))
% 3.67/3.93  ((skc8) != zenon_X119)
% 3.67/3.93  ((skc7) != zenon_X102)
% 3.67/3.93  (zenon_X20 != zenon_X62)
% 3.67/3.93  (-. (vehicle zenon_X50 (skc7)))
% 3.67/3.93  (-. (general zenon_X16 (skc7)))
% 3.67/3.93  ((skc6) != zenon_X111)
% 3.67/3.93  (-. (instrumentality zenon_X68 (skc7)))
% 3.67/3.93  ((skc7) != zenon_X446)
% 3.67/3.93  (-. (car zenon_X20 zenon_X461))
% 3.67/3.93  ((skc7) != zenon_X252)
% 3.67/3.93  ((skc7) != zenon_X436)
% 3.67/3.93  (-. (way (skc5) zenon_X127))
% 3.67/3.93  (-. (entity zenon_X14 (skc7)))
% 3.67/3.93  (-. (placename zenon_X48 zenon_X145))
% 3.67/3.93  (existent zenon_X56 (skc7))
% 3.67/3.93  ((skc8) != zenon_X7)
% 3.67/3.93  (-. (specific zenon_X2 zenon_X142))
% 3.67/3.93  ((skc9) != zenon_X45)
% 3.67/3.93  ((skc7) != zenon_X231)
% 3.67/3.93  (existent zenon_X24 (skc7))
% 3.67/3.93  (zenon_X16 != zenon_X20)
% 3.67/3.93  (-. (city zenon_X66 zenon_X108))
% 3.67/3.93  (-. (placename zenon_X66 (skc9)))
% 3.67/3.93  (object zenon_X20 (skc7))
% 3.67/3.93  (-. (object zenon_X2 zenon_X162))
% 3.67/3.93  (zenon_X0 != zenon_X54)
% 3.67/3.93  (zenon_X8 != zenon_X50)
% 3.67/3.93  ((skc8) != zenon_X381)
% 3.67/3.93  (specific zenon_X48 (skc7))
% 3.67/3.93  (entity zenon_X20 (skc8))
% 3.67/3.93  (relation zenon_X36 (skc9))
% 3.67/3.93  ((skc8) != zenon_X228)
% 3.67/3.93  ((skc8) != zenon_X202)
% 3.67/3.93  ((skc8) != zenon_X346)
% 3.67/3.93  ((skc7) != zenon_X259)
% 3.67/3.93  (-. (object zenon_X16 zenon_X218))
% 3.67/3.93  ((skc5) != zenon_X8)
% 3.67/3.93  (-. (general zenon_X62 (skc7)))
% 3.67/3.93  (-. (street zenon_X18 zenon_X356))
% 3.67/3.93  ((skc7) != zenon_X474)
% 3.67/3.93  ((skc8) != zenon_X197)
% 3.67/3.93  (-. (entity zenon_X24 zenon_X255))
% 3.67/3.93  (-. (entity zenon_X16 zenon_X234))
% 3.67/3.93  (existent zenon_X20 (skc8))
% 3.67/3.93  ((skc8) != zenon_X333)
% 3.67/3.93  ((skc9) != zenon_X286)
% 3.67/3.93  (-. (vehicle zenon_X14 (skc7)))
% 3.67/3.93  (zenon_X0 != zenon_X60)
% 3.67/3.93  (-. (city zenon_X26 zenon_X159))
% 3.67/3.93  (zenon_X50 != zenon_X62)
% 3.67/3.93  ((skc9) != zenon_X41)
% 3.67/3.93  (-. (object zenon_X60 (skc8)))
% 3.67/3.93  (-. (way zenon_X20 zenon_X278))
% 3.67/3.93  (zenon_X14 != zenon_X54)
% 3.67/3.93  (-. (placename zenon_X66 zenon_X136))
% 3.67/3.93  (zenon_X2 != zenon_X48)
% 3.67/3.93  (object zenon_X18 (skc8))
% 3.67/3.93  (-. (existent zenon_X0 zenon_X351))
% 3.67/3.93  ((skc8) != zenon_X74)
% 3.67/3.93  (-. (hollywood_placename zenon_X16 zenon_X208))
% 3.67/3.93  ((skc5) != zenon_X68)
% 3.67/3.93  ((skc7) != zenon_X415)
% 3.67/3.93  (-. (existent zenon_X18 zenon_X107))
% 3.67/3.93  (-. (nonexistent zenon_X18 (skc8)))
% 3.67/3.93  (barrel (skc5) (skc6))
% 3.67/3.93  (existent zenon_X18 (skc7))
% 3.67/3.93  (-. (street (skc5) zenon_X179))
% 3.67/3.93  (-. (city zenon_X56 zenon_X501))
% 3.67/3.93  ((skc6) != zenon_X233)
% 3.67/3.93  (specific zenon_X48 (skc8))
% 3.67/3.93  (-. (location zenon_X0 zenon_X383))
% 3.67/3.93  ((skc7) != zenon_X75)
% 3.67/3.93  (-. (eventuality zenon_X10 zenon_X11))
% 3.67/3.93  ((skc8) != zenon_X140)
% 3.67/3.93  (-. (placename zenon_X48 zenon_X148))
% 3.67/3.93  ((skc7) != zenon_X334)
% 3.67/3.93  (zenon_X48 != zenon_X26)
% 3.67/3.93  (-. (placename zenon_X0 zenon_X200))
% 3.67/3.93  ((skc7) != zenon_X541)
% 3.67/3.93  (zenon_X48 != zenon_X56)
% 3.67/3.93  ((skc7) != zenon_X142)
% 3.67/3.93  ((skc7) != zenon_X117)
% 3.67/3.93  (zenon_X0 != zenon_X2)
% 3.67/3.93  ((skc8) != zenon_X185)
% 3.67/3.93  ((skc7) != zenon_X378)
% 3.67/3.93  (-. (entity zenon_X52 zenon_X154))
% 3.67/3.93  (entity zenon_X18 (skc8))
% 3.67/3.93  ((skc7) != zenon_X184)
% 3.67/3.93  ((skc7) != zenon_X432)
% 3.67/3.93  (zenon_X2 != zenon_X52)
% 3.67/3.93  ((skc7) != zenon_X174)
% 3.67/3.93  (-. (location zenon_X50 zenon_X369))
% 3.67/3.93  ((skc8) != zenon_X287)
% 3.67/3.93  (zenon_X0 != zenon_X50)
% 3.67/3.93  (zenon_X16 != zenon_X24)
% 3.67/3.93  (location zenon_X50 (skc8))
% 3.67/3.93  (-. (way zenon_X50 zenon_X258))
% 3.67/3.93  ((skc7) != zenon_X368)
% 3.67/3.93  (-. (instrumentality zenon_X26 zenon_X302))
% 3.67/3.93  ((skc7) != zenon_X439)
% 3.67/3.93  (existent zenon_X0 (skc8))
% 3.67/3.93  ((skc7) != (skc8))
% 3.67/3.93  (-. (entity zenon_X56 zenon_X494))
% 3.67/3.93  ((skc8) != zenon_X72)
% 3.67/3.93  ((skc8) != zenon_X53)
% 3.67/3.93  (-. (specific zenon_X26 (skc8)))
% 3.67/3.93  (-. (nonexistent zenon_X48 (skc7)))
% 3.67/3.93  (-. (location zenon_X26 zenon_X106))
% 3.67/3.93  (-. (object zenon_X48 zenon_X113))
% 3.67/3.93  (way zenon_X0 (skc8))
% 3.67/3.93  ((skc9) != zenon_X241)
% 3.67/3.93  (-. (entity zenon_X48 zenon_X185))
% 3.67/3.93  (zenon_X14 != zenon_X58)
% 3.67/3.93  (zenon_X58 != zenon_X26)
% 3.67/3.93  (zenon_X0 != zenon_X66)
% 3.67/3.93  (zenon_X24 != zenon_X26)
% 3.67/3.93  (-. (thing zenon_X6 zenon_X7))
% 3.67/3.93  (-. (specific zenon_X8 zenon_X102))
% 3.67/3.93  (placename zenon_X48 (skc9))
% 3.67/3.93  (-. (street zenon_X24 zenon_X367))
% 3.67/3.93  (-. (object zenon_X66 (skc8)))
% 3.67/3.93  (instrumentality zenon_X16 (skc7))
% 3.67/3.93  (-. (entity zenon_X52 zenon_X346))
% 3.67/3.93  (specific zenon_X8 (skc6))
% 3.67/3.93  (specific zenon_X0 (skc8))
% 3.67/3.93  (-. (specific zenon_X24 zenon_X104))
% 3.67/3.93  (-. (location (skc5) zenon_X101))
% 3.67/3.93  ((skc8) != zenon_X130)
% 3.67/3.93  ((skc7) != zenon_X344)
% 3.67/3.93  ((skc7) != zenon_X143)
% 3.67/3.93  ((skc7) != zenon_X57)
% 3.67/3.93  (-. (entity zenon_X26 zenon_X27))
% 3.67/3.93  ((skc7) != zenon_X65)
% 3.67/3.93  (-. (object zenon_X30 zenon_X31))
% 3.67/3.93  (-. (artifact zenon_X66 zenon_X92))
% 3.67/3.93  (zenon_X8 != zenon_X64)
% 3.67/3.93  ((skc7) != zenon_X291)
% 3.67/3.93  (zenon_X0 != zenon_X14)
% 3.67/3.93  (-. (hollywood_placename zenon_X48 zenon_X49))
% 3.67/3.93  (zenon_X48 != zenon_X52)
% 3.67/3.93  (existent zenon_X0 (skc7))
% 3.67/3.93  (-. (way zenon_X26 zenon_X121))
% 3.67/3.93  (-. (general zenon_X14 (skc8)))
% 3.67/3.93  (-. (entity zenon_X66 zenon_X137))
% 3.67/3.93  (zenon_X54 != zenon_X8)
% 3.67/3.93  (-. (entity zenon_X16 zenon_X126))
% 3.67/3.93  (zenon_X8 != zenon_X52)
% 3.67/3.93  (-. (way zenon_X24 zenon_X265))
% 3.67/3.93  (-. (eventuality zenon_X68 (skc6)))
% 3.67/3.93  (zenon_X48 != zenon_X18)
% 3.67/3.93  ((skc8) != zenon_X98)
% 3.67/3.93  (zenon_X50 != zenon_X54)
% 3.67/3.93  ((skc7) != zenon_X526)
% 3.67/3.93  ((skc8) != zenon_X255)
% 3.67/3.93  ((skc7) != zenon_X146)
% 3.67/3.93  (zenon_X60 != zenon_X68)
% 3.67/3.93  (-. (car zenon_X68 (skc7)))
% 3.67/3.93  (-. (nonexistent zenon_X66 (skc7)))
% 3.67/3.93  ((skc5) != zenon_X50)
% 3.67/3.93  (-. (artifact zenon_X8 zenon_X315))
% 3.67/3.93  (zenon_X48 != zenon_X54)
% 3.67/3.93  (specific zenon_X62 (skc6))
% 3.67/3.93  ((skc8) != zenon_X326)
% 3.67/3.93  ((skc9) != zenon_X145)
% 3.67/3.93  (-. (entity zenon_X64 zenon_X259))
% 3.67/3.93  ((skc8) != zenon_X229)
% 3.67/3.93  (-. (specific zenon_X14 zenon_X334))
% 3.67/3.93  (-. (transport zenon_X52 zenon_X425))
% 3.67/3.93  (-. (specific zenon_X48 zenon_X132))
% 3.67/3.93  (existent zenon_X54 (skc7))
% 3.67/3.93  (zenon_X20 != zenon_X58)
% 3.67/3.93  (-. (car zenon_X8 zenon_X477))
% 3.67/3.93  (zenon_X62 != zenon_X26)
% 3.67/3.93  (zenon_X24 != zenon_X66)
% 3.67/3.93  (specific zenon_X16 (skc6))
% 3.67/3.93  ((skc7) != zenon_X454)
% 3.67/3.93  (-. (entity zenon_X60 (skc8)))
% 3.67/3.93  (-. (event zenon_X16 zenon_X293))
% 3.67/3.93  (-. (location zenon_X14 zenon_X422))
% 3.67/3.93  (-. (nonexistent zenon_X0 (skc8)))
% 3.67/3.93  ((skc7) != zenon_X431)
% 3.67/3.93  (-. (street zenon_X8 zenon_X332))
% 3.67/3.93  ((skc9) != zenon_X136)
% 3.67/3.93  (eventuality zenon_X2 (skc6))
% 3.67/3.93  (unisex zenon_X32 (skc7))
% 3.67/3.93  ((skc7) != zenon_X73)
% 3.67/3.93  ((skc6) != zenon_X11)
% 3.67/3.93  ((skc8) != zenon_X179)
% 3.67/3.93  (-. (instrumentality zenon_X68 zenon_X143))
% 3.67/3.93  ((skc8) != zenon_X192)
% 3.67/3.93  (-. (vehicle zenon_X68 zenon_X280))
% 3.67/3.93  (-. (entity zenon_X58 zenon_X407))
% 3.67/3.93  (-. (transport zenon_X18 zenon_X374))
% 3.67/3.93  (-. (entity zenon_X64 zenon_X118))
% 3.67/3.93  (zenon_X0 != zenon_X62)
% 3.67/3.93  (-. (object zenon_X68 (skc7)))
% 3.67/3.93  (-. (placename zenon_X18 (skc9)))
% 3.67/3.93  (-. (eventuality zenon_X60 zenon_X413))
% 3.67/3.93  ((skc8) != zenon_X114)
% 3.67/3.93  (-. (city zenon_X2 zenon_X421))
% 3.67/3.93  ((skc7) != zenon_X140)
% 3.67/3.93  (dirty (skc5) (skc7))
% 3.67/3.93  (-. (placename zenon_X50 zenon_X241))
% 3.67/3.93  ((skc7) != zenon_X300)
% 3.67/3.93  (zenon_X14 != zenon_X68)
% 3.67/3.93  (-. (vehicle zenon_X0 zenon_X417))
% 3.67/3.93  ((skc7) != zenon_X31)
% 3.67/3.93  (unisex zenon_X32 (skc8))
% 3.67/3.93  (-. (general zenon_X2 (skc6)))
% 3.67/3.93  ((skc9) != zenon_X144)
% 3.67/3.93  (-. (city zenon_X58 zenon_X465))
% 3.67/3.93  (entity zenon_X0 (skc7))
% 3.67/3.93  (-. (artifact zenon_X58 zenon_X476))
% 3.67/3.93  ((skc7) != zenon_X98)
% 3.67/3.93  ((skc8) != zenon_X215)
% 3.67/3.93  (-. (nonexistent zenon_X16 (skc7)))
% 3.67/3.93  (nonliving zenon_X28 (skc7))
% 3.67/3.93  ((skc9) != zenon_X78)
% 3.67/3.93  (zenon_X2 != zenon_X20)
% 3.67/3.93  ((skc8) != zenon_X234)
% 3.67/3.93  ((skc8) != zenon_X31)
% 3.67/3.93  (-. (car zenon_X16 zenon_X449))
% 3.67/3.93  ((skc8) != zenon_X147)
% 3.67/3.93  ((skc7) != zenon_X92)
% 3.67/3.93  ((skc6) != zenon_X102)
% 3.67/3.93  ((skc7) != zenon_X370)
% 3.67/3.93  (-. (entity zenon_X48 zenon_X147))
% 3.67/3.93  (-. (specific zenon_X68 (skc6)))
% 3.67/3.93  (-. (artifact zenon_X52 zenon_X314))
% 3.67/3.93  (artifact zenon_X16 (skc7))
% 3.67/3.93  (-. (vehicle zenon_X58 zenon_X59))
% 3.67/3.93  ((skc6) != zenon_X90)
% 3.67/3.93  (-. (instrumentality zenon_X62 zenon_X63))
% 3.67/3.93  (-. (city zenon_X50 zenon_X51))
% 3.67/3.93  (-. (way zenon_X66 (skc8)))
% 3.67/3.93  (way zenon_X14 (skc8))
% 3.67/3.93  (-. (way zenon_X66 zenon_X114))
% 3.67/3.93  (-. (eventuality zenon_X24 zenon_X109))
% 3.67/3.93  ((skc8) != zenon_X107)
% 3.67/3.93  (-. (barrel zenon_X52 zenon_X385))
% 3.67/3.93  ((skc7) != zenon_X124)
% 3.67/3.93  (-. (chevy zenon_X50 zenon_X492))
% 3.67/3.93  (-. (eventuality zenon_X8 zenon_X9))
% 3.67/3.93  ((skc7) != zenon_X333)
% 3.67/3.93  ((skc7) != zenon_X245)
% 3.67/3.93  (specific zenon_X58 (skc7))
% 3.67/3.93  (-. (transport zenon_X16 zenon_X410))
% 3.67/3.93  ((skc7) != zenon_X350)
% 3.67/3.93  (zenon_X56 != zenon_X26)
% 3.67/3.93  (-. (event zenon_X68 zenon_X328))
% 3.67/3.93  (zenon_X14 != zenon_X66)
% 3.67/3.93  (-. (general zenon_X16 (skc6)))
% 3.67/3.93  (-. (object zenon_X18 zenon_X139))
% 3.67/3.93  (zenon_X66 != zenon_X68)
% 3.67/3.93  (-. (nonexistent zenon_X18 (skc7)))
% 3.67/3.93  (abstraction zenon_X38 (skc9))
% 3.67/3.93  (-. (entity zenon_X0 zenon_X201))
% 3.67/3.93  (-. (general zenon_X20 (skc7)))
% 3.67/3.93  ((skc7) != zenon_X381)
% 3.67/3.93  (-. (object zenon_X58 zenon_X400))
% 3.67/3.93  (-. (eventuality zenon_X20 (skc6)))
% 3.67/3.93  (-. (instrumentality zenon_X18 zenon_X209))
% 3.67/3.93  (existent zenon_X50 (skc8))
% 3.67/3.93  ((skc8) != zenon_X33)
% 3.67/3.93  (-. (city zenon_X8 zenon_X238))
% 3.67/3.93  ((skc6) != zenon_X325)
% 3.67/3.93  (existent zenon_X48 (skc8))
% 3.67/3.93  (-. (placename zenon_X58 (skc9)))
% 3.67/3.93  ((skc6) != zenon_X243)
% 3.67/3.93  ((skc8) != zenon_X371)
% 3.67/3.93  (artifact (skc5) (skc7))
% 3.67/3.93  (entity zenon_X16 (skc8))
% 3.67/3.93  (-. (vehicle zenon_X26 (skc7)))
% 3.67/3.93  ((skc9) != zenon_X189)
% 3.67/3.93  ((skc8) != zenon_X227)
% 3.67/3.93  (zenon_X50 != zenon_X52)
% 3.67/3.93  (-. (nonexistent zenon_X26 (skc8)))
% 3.67/3.93  ((skc8) != zenon_X323)
% 3.67/3.93  (-. (specific zenon_X26 (skc6)))
% 3.67/3.93  (zenon_X0 != zenon_X48)
% 3.67/3.93  ((skc7) != zenon_X476)
% 3.67/3.93  (existent zenon_X16 (skc8))
% 3.67/3.93  (-. (specific zenon_X52 zenon_X260))
% 3.67/3.93  ((skc8) != zenon_X17)
% 3.67/3.93  ((skc7) != zenon_X494)
% 3.67/3.93  (zenon_X0 != zenon_X24)
% 3.67/3.93  ((skc8) != zenon_X19)
% 3.67/3.93  ((skc7) != zenon_X80)
% 3.67/3.93  (zenon_X56 != zenon_X8)
% 3.67/3.93  (zenon_X18 != zenon_X20)
% 3.67/3.93  ((skc7) != zenon_X23)
% 3.67/3.93  (zenon_X20 != zenon_X66)
% 3.67/3.93  ((skc5) != zenon_X14)
% 3.67/3.93  (-. (car zenon_X0 zenon_X462))
% 3.67/3.93  (-. (instrumentality zenon_X14 zenon_X348))
% 3.67/3.93  ((skc8) != zenon_X222)
% 3.67/3.93  ((skc9) != (skc7))
% 3.67/3.93  ((skc7) != zenon_X486)
% 3.67/3.93  ((skc8) != zenon_X120)
% 3.67/3.93  (-. (vehicle zenon_X2 zenon_X469))
% 3.67/3.93  (-. (street zenon_X14 zenon_X15))
% 3.67/3.93  (city (skc5) (skc8))
% 3.67/3.93  (-. (eventuality zenon_X64 (skc6)))
% 3.67/3.93  ((skc8) != zenon_X75)
% 3.67/3.93  (-. (existent zenon_X26 zenon_X73))
% 3.67/3.93  ((skc8) != zenon_X85)
% 3.67/3.93  ((skc7) != zenon_X477)
% 3.67/3.93  (-. (placename zenon_X62 (skc9)))
% 3.67/3.93  (-. (instrumentality zenon_X52 (skc7)))
% 3.67/3.93  (-. (hollywood_placename zenon_X64 zenon_X166))
% 3.67/3.93  ((skc6) != zenon_X227)
% 3.67/3.93  ((skc7) != zenon_X425)
% 3.67/3.93  ((skc7) != zenon_X484)
% 3.67/3.93  ((skc8) != zenon_X258)
% 3.67/3.93  (zenon_X8 != zenon_X26)
% 3.67/3.93  (zenon_X18 != zenon_X60)
% 3.67/3.93  (-. (specific zenon_X62 zenon_X296))
% 3.67/3.93  *)
% 3.67/3.93  (* NO-PROOF *)
% 3.67/3.93  % SZS status GaveUp
% 3.67/3.93  Number of rewrites on terms: 0
% 3.67/3.93  Number of rewrites on props: 0
% 3.67/3.93  nodes searched: 66815
% 3.67/3.93  max branch formulas: 2678
% 3.67/3.93  proof nodes created: 3104
% 3.67/3.93  formulas created: 83078
% 3.67/3.93  
%------------------------------------------------------------------------------