↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n006.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:06 EDT 2024

% Result   : Unknown 1.19s 1.38s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.10  % Problem  : NLP005-1 : TPTP v8.2.0. Released v2.4.0.
% 0.02/0.10  % Command  : run_zenon_modulo %d %s
% 0.09/0.30  % Computer : n006.cluster.edu
% 0.09/0.30  % Model    : x86_64 x86_64
% 0.09/0.30  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30  % Memory   : 8042.1875MB
% 0.09/0.30  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30  % CPULimit : 300
% 0.09/0.30  % WCLimit  : 300
% 0.09/0.30  % DateTime : Sat Jun 22 22:42:54 EDT 2024
% 0.09/0.30  % CPUTime  : 
% 1.19/1.38  Zenon error: exhausted search space without finding a proof
% 1.19/1.38  (* Current branch:
% 1.19/1.38  ((skc24) != zenon_X269)
% 1.19/1.38  ((skc16) != zenon_X143)
% 1.19/1.38  ((skc24) != zenon_X235)
% 1.19/1.38  ((skc23) != zenon_X249)
% 1.19/1.38  (chevy (skc27))
% 1.19/1.38  ((skc15) != zenon_X223)
% 1.19/1.38  ((skc15) != zenon_X260)
% 1.19/1.38  (-. (young zenon_X337))
% 1.19/1.38  (-. (young zenon_X264))
% 1.19/1.38  ((skc16) != zenon_X322)
% 1.19/1.38  ((skc16) != zenon_X377)
% 1.19/1.38  ((skc29) != (skc25))
% 1.19/1.38  (-. (young zenon_X253))
% 1.19/1.38  ((skc16) != (skc15))
% 1.19/1.38  ((skc15) != zenon_X145)
% 1.19/1.38  (-. (old zenon_X21))
% 1.19/1.38  ((skc23) != zenon_X354)
% 1.19/1.38  ((skc15) != zenon_X284)
% 1.19/1.38  (-. (young zenon_X414))
% 1.19/1.38  ((skc15) != zenon_X287)
% 1.19/1.38  ((skc16) != zenon_X380)
% 1.19/1.38  ((skc23) != zenon_X218)
% 1.19/1.38  ((skc23) != zenon_X147)
% 1.19/1.38  ((skc16) != zenon_X239)
% 1.19/1.38  (event (skc21))
% 1.19/1.38  ((skc15) != zenon_X227)
% 1.19/1.38  ((skc18) != zenon_X106)
% 1.19/1.38  ((skc15) != zenon_X254)
% 1.19/1.38  (-. (young zenon_X239))
% 1.19/1.38  (-. (young zenon_X384))
% 1.19/1.38  ((skc24) != zenon_X141)
% 1.19/1.38  (-. (young zenon_X307))
% 1.19/1.38  ((skc24) != zenon_X195)
% 1.19/1.38  (-. (young zenon_X306))
% 1.19/1.38  ((skc15) != zenon_X329)
% 1.19/1.38  ((skc16) != zenon_X209)
% 1.19/1.38  ((skc23) != zenon_X302)
% 1.19/1.38  ((skc16) != (skc24))
% 1.19/1.38  ((skc16) != zenon_X167)
% 1.19/1.38  ((skc15) != zenon_X359)
% 1.19/1.38  ((skc23) != zenon_X317)
% 1.19/1.38  ((skc23) != zenon_X193)
% 1.19/1.38  ((skc24) != zenon_X237)
% 1.19/1.38  ((skc23) != zenon_X357)
% 1.19/1.38  (-. (in (skc24) (skc17)))
% 1.19/1.38  ((skc17) != zenon_X82)
% 1.19/1.38  ((skc23) != zenon_X264)
% 1.19/1.38  ((skc24) != zenon_X349)
% 1.19/1.38  ((skc15) != zenon_X153)
% 1.19/1.38  ((skc16) != zenon_X165)
% 1.19/1.38  (-. (fellow zenon_X169))
% 1.19/1.38  ((skc16) != zenon_X179)
% 1.19/1.38  ((skc24) != zenon_X258)
% 1.19/1.38  ((skc16) != zenon_X157)
% 1.19/1.38  ((skc23) != zenon_X252)
% 1.19/1.38  (-. (seat zenon_X97))
% 1.19/1.38  ((skc15) != zenon_X177)
% 1.19/1.38  (-. (young zenon_X262))
% 1.19/1.38  ((skc16) != zenon_X295)
% 1.19/1.38  ((skc16) != zenon_X369)
% 1.19/1.38  (-. (young zenon_X252))
% 1.19/1.38  ((skc24) != zenon_X193)
% 1.19/1.38  ((skc16) != zenon_X250)
% 1.19/1.38  ((skc24) != zenon_X310)
% 1.19/1.38  ((skc24) != zenon_X277)
% 1.19/1.38  (-. (seat zenon_X106))
% 1.19/1.38  ((skc24) != zenon_X145)
% 1.19/1.38  ((skc23) != zenon_X283)
% 1.19/1.38  ((skc24) != zenon_X305)
% 1.19/1.38  ((skc16) != zenon_X274)
% 1.19/1.38  ((skc16) != zenon_X310)
% 1.19/1.38  ((skc15) != zenon_X384)
% 1.19/1.38  (-. (young zenon_X290))
% 1.19/1.38  (-. (city zenon_X63))
% 1.19/1.38  (-. (young zenon_X310))
% 1.19/1.38  (-. (city zenon_X55))
% 1.19/1.38  (young (skc16))
% 1.19/1.38  (-. (event zenon_X37))
% 1.19/1.38  (-. (young zenon_X368))
% 1.19/1.38  ((skc15) != zenon_X269)
% 1.19/1.38  ((skc15) != zenon_X230)
% 1.19/1.38  ((skc24) != zenon_X312)
% 1.19/1.38  ((skc24) != zenon_X212)
% 1.19/1.38  ((skc24) != zenon_X137)
% 1.19/1.38  (young (skc24))
% 1.19/1.38  ((skc15) != zenon_X281)
% 1.19/1.38  ((skc15) != zenon_X367)
% 1.19/1.38  (-. (fellow zenon_X163))
% 1.19/1.38  ((skc16) != zenon_X277)
% 1.19/1.38  ((skc25) != zenon_X85)
% 1.19/1.38  ((skc15) != zenon_X157)
% 1.19/1.38  ((skc25) != zenon_X100)
% 1.19/1.38  ((skc15) != zenon_X261)
% 1.19/1.38  ((skc25) != zenon_X129)
% 1.19/1.38  ((skc15) != zenon_X342)
% 1.19/1.38  ((skc23) != zenon_X141)
% 1.19/1.38  (-. (young zenon_X309))
% 1.19/1.38  ((skc16) != zenon_X381)
% 1.19/1.38  ((skc16) != zenon_X331)
% 1.19/1.38  ((skc24) != zenon_X230)
% 1.19/1.38  ((skc24) != zenon_X346)
% 1.19/1.38  ((skc16) != zenon_X386)
% 1.19/1.38  ((skc15) != zenon_X295)
% 1.19/1.38  ((skc16) != zenon_X333)
% 1.19/1.38  ((skc23) != zenon_X175)
% 1.19/1.38  ((skc23) != zenon_X229)
% 1.19/1.38  (down (skc21) (skc20))
% 1.19/1.38  ((skc23) != zenon_X375)
% 1.19/1.38  ((skc15) != zenon_X192)
% 1.19/1.38  ((skc24) != zenon_X331)
% 1.19/1.38  ((skc15) != zenon_X200)
% 1.19/1.38  ((skc18) != zenon_X82)
% 1.19/1.38  ((skc28) != zenon_X37)
% 1.19/1.38  (-. (young zenon_X341))
% 1.19/1.38  ((skc23) != zenon_X261)
% 1.19/1.38  ((skc16) != zenon_X238)
% 1.19/1.38  ((skc29) != zenon_X51)
% 1.19/1.38  ((skc16) != zenon_X215)
% 1.19/1.38  ((skc18) != zenon_X94)
% 1.19/1.38  ((skc25) != zenon_X112)
% 1.19/1.38  ((skc23) != zenon_X299)
% 1.19/1.38  ((skc23) != zenon_X382)
% 1.19/1.38  ((skc23) != zenon_X250)
% 1.19/1.38  ((skc23) != zenon_X276)
% 1.19/1.38  ((skc25) != zenon_X82)
% 1.19/1.38  (-. (young zenon_X343))
% 1.19/1.38  ((skc24) != zenon_X181)
% 1.19/1.38  ((skc16) != zenon_X163)
% 1.19/1.38  (-. (young zenon_X214))
% 1.19/1.38  ((skc15) != zenon_X257)
% 1.19/1.38  ((skc16) != zenon_X393)
% 1.19/1.38  (-. (young zenon_X265))
% 1.19/1.38  ((skc15) != zenon_X274)
% 1.19/1.38  ((skc16) != zenon_X155)
% 1.19/1.38  ((skc16) != zenon_X278)
% 1.19/1.38  ((skc16) != zenon_X365)
% 1.19/1.38  (-. (event zenon_X32))
% 1.19/1.38  ((skc15) != zenon_X304)
% 1.19/1.38  ((skc23) != zenon_X239)
% 1.19/1.38  ((skc16) != zenon_X297)
% 1.19/1.38  ((skc24) != zenon_X177)
% 1.19/1.38  ((skc16) != zenon_X206)
% 1.19/1.38  (-. (fellow zenon_X292))
% 1.19/1.38  ((skc24) != zenon_X297)
% 1.19/1.38  (chevy (skc19))
% 1.19/1.38  ((skc24) != zenon_X340)
% 1.19/1.38  (-. (young zenon_X195))
% 1.19/1.38  (front (skc17))
% 1.19/1.38  ((skc23) != zenon_X368)
% 1.19/1.38  (-. (seat zenon_X109))
% 1.19/1.38  ((skc24) != zenon_X285)
% 1.19/1.38  ((skc15) != zenon_X393)
% 1.19/1.38  (-. (young zenon_X382))
% 1.19/1.38  ((skc23) != zenon_X123)
% 1.19/1.38  ((skc23) = (skc15))
% 1.19/1.38  ((skc15) != zenon_X247)
% 1.19/1.38  (-. (young zenon_X215))
% 1.19/1.38  ((skc18) != zenon_X129)
% 1.19/1.38  ((skc24) != zenon_X171)
% 1.19/1.38  (-. (young zenon_X308))
% 1.19/1.38  (-. (young zenon_X354))
% 1.19/1.38  ((skc16) != zenon_X337)
% 1.19/1.38  ((skc23) != zenon_X211)
% 1.19/1.38  ((skc15) != zenon_X238)
% 1.19/1.38  ((skc16) != zenon_X307)
% 1.19/1.38  ((skc15) != zenon_X310)
% 1.19/1.38  ((skc23) != zenon_X379)
% 1.19/1.38  ((skc16) != zenon_X256)
% 1.19/1.38  (-. (seat zenon_X118))
% 1.19/1.38  ((skc24) != zenon_X278)
% 1.19/1.38  ((skc23) != zenon_X414)
% 1.19/1.38  ((skc16) != zenon_X221)
% 1.19/1.38  ((skc16) != zenon_X360)
% 1.19/1.38  ((skc24) != zenon_X267)
% 1.19/1.38  ((skc15) != zenon_X366)
% 1.19/1.38  (-. (fellow zenon_X147))
% 1.19/1.38  ((skc24) != zenon_X282)
% 1.19/1.38  ((skc24) != zenon_X153)
% 1.19/1.38  ((skc24) != zenon_X261)
% 1.19/1.38  ((skc16) != zenon_X202)
% 1.19/1.38  ((skc23) != zenon_X272)
% 1.19/1.38  ((skc23) != zenon_X265)
% 1.19/1.38  (-. (young zenon_X232))
% 1.19/1.38  ((skc23) != zenon_X247)
% 1.19/1.38  ((skc16) != zenon_X267)
% 1.19/1.38  ((skc16) != zenon_X145)
% 1.19/1.38  (-. (young zenon_X212))
% 1.19/1.38  ((skc24) != zenon_X307)
% 1.19/1.38  ((skc25) != zenon_X79)
% 1.19/1.38  ((skc18) != zenon_X91)
% 1.19/1.38  (-. (young zenon_X267))
% 1.19/1.38  ((skc15) != zenon_X307)
% 1.19/1.38  ((skc23) != zenon_X342)
% 1.19/1.38  (-. (city zenon_X59))
% 1.19/1.38  ((skc24) != zenon_X224)
% 1.19/1.38  ((skc15) != zenon_X369)
% 1.19/1.38  ((skc15) != zenon_X337)
% 1.19/1.38  ((skc24) != zenon_X284)
% 1.19/1.38  (-. (young zenon_X342))
% 1.19/1.38  ((skc21) != zenon_X27)
% 1.19/1.38  ((skc24) != zenon_X286)
% 1.19/1.38  ((skc15) != zenon_X289)
% 1.19/1.38  (-. (young zenon_X223))
% 1.19/1.38  ((skc23) != zenon_X204)
% 1.19/1.38  ((skc24) != zenon_X337)
% 1.19/1.38  ((skc24) != zenon_X333)
% 1.19/1.38  ((skc16) != zenon_X224)
% 1.19/1.38  ((skc16) != zenon_X305)
% 1.19/1.38  ((skc23) != zenon_X241)
% 1.19/1.38  ((skc24) != zenon_X205)
% 1.19/1.38  (-. (seat zenon_X91))
% 1.19/1.38  ((skc16) != zenon_X303)
% 1.19/1.38  ((skc24) != zenon_X338)
% 1.19/1.38  ((skc16) != zenon_X287)
% 1.19/1.38  ((skc23) != zenon_X289)
% 1.19/1.38  ((skc22) != (skc18))
% 1.19/1.38  (in (skc23) (skc25))
% 1.19/1.38  ((skc24) != zenon_X360)
% 1.19/1.38  (-. (young zenon_X338))
% 1.19/1.38  ((skc16) != zenon_X311)
% 1.19/1.38  ((skc16) != zenon_X198)
% 1.19/1.38  ((skc24) != zenon_X215)
% 1.19/1.38  ((skc23) != zenon_X179)
% 1.19/1.38  ((skc23) != zenon_X288)
% 1.19/1.38  ((skc16) != zenon_X177)
% 1.19/1.38  ((skc16) != zenon_X362)
% 1.19/1.38  ((skc15) != zenon_X215)
% 1.19/1.38  ((skc15) != zenon_X270)
% 1.19/1.38  (-. (young zenon_X313))
% 1.19/1.38  ((skc23) != zenon_X333)
% 1.19/1.38  (old (skc19))
% 1.19/1.38  ((skc15) != zenon_X279)
% 1.19/1.38  ((skc25) != zenon_X109)
% 1.19/1.38  ((skc16) != zenon_X248)
% 1.19/1.38  ((skc22) != zenon_X47)
% 1.19/1.38  ((skc23) != zenon_X227)
% 1.19/1.38  ((skc23) != zenon_X230)
% 1.19/1.38  ((skc16) != zenon_X327)
% 1.19/1.38  ((skc16) != zenon_X358)
% 1.19/1.38  (-. (young zenon_X357))
% 1.19/1.38  ((skc15) != zenon_X214)
% 1.19/1.38  ((skc24) != zenon_X184)
% 1.19/1.38  ((skc24) != zenon_X379)
% 1.19/1.38  (-. (young zenon_X301))
% 1.19/1.38  ((skc24) != zenon_X227)
% 1.19/1.38  ((skc16) != zenon_X137)
% 1.19/1.38  (-. (young zenon_X213))
% 1.19/1.38  (-. (young zenon_X280))
% 1.19/1.38  ((skc22) != zenon_X51)
% 1.19/1.38  ((skc22) != zenon_X75)
% 1.19/1.38  ((skc15) != zenon_X163)
% 1.19/1.38  (-. (in (skc16) (skc18)))
% 1.19/1.38  ((skc24) != zenon_X274)
% 1.19/1.38  ((skc16) != zenon_X314)
% 1.19/1.38  ((skc15) != zenon_X252)
% 1.19/1.38  ((skc16) != zenon_X302)
% 1.19/1.38  (-. (young zenon_X346))
% 1.19/1.38  ((skc15) != zenon_X161)
% 1.19/1.38  (barrel (skc21) (skc19))
% 1.19/1.38  ((skc25) != zenon_X106)
% 1.19/1.38  ((skc15) != zenon_X268)
% 1.19/1.38  ((skc16) != zenon_X334)
% 1.19/1.38  ((skc24) != zenon_X299)
% 1.19/1.38  ((skc17) != zenon_X91)
% 1.19/1.38  ((skc23) != zenon_X257)
% 1.19/1.38  ((skc24) != zenon_X357)
% 1.19/1.38  ((skc16) != zenon_X125)
% 1.19/1.38  ((skc15) != zenon_X217)
% 1.19/1.38  (-. (young zenon_X248))
% 1.19/1.38  ((skc23) != zenon_X316)
% 1.19/1.38  ((skc23) != zenon_X383)
% 1.19/1.38  ((skc24) != zenon_X362)
% 1.19/1.38  (-. (young zenon_X271))
% 1.19/1.38  ((skc24) != zenon_X358)
% 1.19/1.38  (-. (young zenon_X281))
% 1.19/1.38  ((skc23) != zenon_X305)
% 1.19/1.38  ((skc21) != zenon_X32)
% 1.19/1.38  ((skc15) != zenon_X300)
% 1.19/1.38  ((skc24) != zenon_X232)
% 1.19/1.38  (-. (young zenon_X269))
% 1.19/1.38  ((skc29) != zenon_X67)
% 1.19/1.38  (-. (young zenon_X314))
% 1.19/1.38  ((skc15) != zenon_X272)
% 1.19/1.38  ((skc23) != zenon_X284)
% 1.19/1.38  (-. (fellow zenon_X295))
% 1.19/1.38  ((skc16) != zenon_X403)
% 1.19/1.38  ((skc16) != zenon_X135)
% 1.19/1.38  ((skc16) != zenon_X190)
% 1.19/1.38  ((skc15) != zenon_X181)
% 1.19/1.38  ((skc23) != zenon_X238)
% 1.19/1.38  ((skc24) != zenon_X403)
% 1.19/1.38  (-. (young zenon_X282))
% 1.19/1.38  ((skc18) != zenon_X118)
% 1.19/1.38  ((skc16) != zenon_X212)
% 1.19/1.38  (man (skc16))
% 1.19/1.38  ((skc24) != zenon_X382)
% 1.19/1.38  ((skc15) != zenon_X149)
% 1.19/1.38  ((skc23) != zenon_X292)
% 1.19/1.38  ((skc16) != zenon_X286)
% 1.19/1.38  (-. (fellow zenon_X139))
% 1.19/1.38  ((skc15) != zenon_X258)
% 1.19/1.38  ((skc16) != zenon_X195)
% 1.19/1.38  ((skc16) != zenon_X299)
% 1.19/1.38  ((skc23) != zenon_X149)
% 1.19/1.38  ((skc23) != zenon_X327)
% 1.19/1.38  (-. (seat zenon_X82))
% 1.19/1.38  ((skc16) != zenon_X169)
% 1.19/1.38  ((skc16) != zenon_X282)
% 1.19/1.38  ((skc15) != zenon_X336)
% 1.19/1.38  ((skc24) != zenon_X253)
% 1.19/1.38  ((skc16) != zenon_X294)
% 1.19/1.38  (-. (fellow zenon_X202))
% 1.19/1.38  ((skc24) != zenon_X223)
% 1.19/1.38  (-. (young zenon_X279))
% 1.19/1.38  (-. (young zenon_X298))
% 1.19/1.38  (-. (young zenon_X319))
% 1.19/1.38  ((skc16) != zenon_X245)
% 1.19/1.38  ((skc15) != zenon_X276)
% 1.19/1.38  ((skc16) != zenon_X216)
% 1.19/1.38  ((skc24) != zenon_X366)
% 1.19/1.38  ((skc18) != zenon_X109)
% 1.19/1.38  ((skc23) != zenon_X349)
% 1.19/1.38  (man (skc24))
% 1.19/1.38  ((skc24) != zenon_X377)
% 1.19/1.38  (in (skc24) (skc25))
% 1.19/1.38  ((skc24) != zenon_X290)
% 1.19/1.38  (-. (young zenon_X300))
% 1.19/1.38  ((skc24) != zenon_X316)
% 1.19/1.38  ((skc23) != zenon_X365)
% 1.19/1.38  ((skc16) != zenon_X257)
% 1.19/1.38  ((skc16) != zenon_X218)
% 1.19/1.38  ((skc24) != zenon_X271)
% 1.19/1.38  ((skc24) != zenon_X173)
% 1.19/1.38  ((skc23) != zenon_X307)
% 1.19/1.38  ((skc23) != zenon_X145)
% 1.19/1.38  (-. (young zenon_X287))
% 1.19/1.38  ((skc15) != zenon_X396)
% 1.19/1.38  ((skc24) != zenon_X163)
% 1.19/1.38  ((skc15) != zenon_X262)
% 1.19/1.38  (-. (young zenon_X277))
% 1.19/1.38  ((skc22) != zenon_X71)
% 1.19/1.38  (-. (young zenon_X380))
% 1.19/1.38  ((skc23) != zenon_X285)
% 1.19/1.38  ((skc23) != zenon_X206)
% 1.19/1.38  ((skc15) != zenon_X216)
% 1.19/1.38  (-. (young zenon_X331))
% 1.19/1.38  ((skc24) != zenon_X213)
% 1.19/1.38  ((skc24) != zenon_X121)
% 1.19/1.38  (-. (fellow zenon_X173))
% 1.19/1.38  (-. (young zenon_X204))
% 1.19/1.38  ((skc15) != zenon_X196)
% 1.19/1.38  ((skc17) != zenon_X103)
% 1.19/1.38  ((skc15) != zenon_X187)
% 1.19/1.38  ((skc23) != zenon_X367)
% 1.19/1.38  (lonely (skc26))
% 1.19/1.38  ((skc16) != zenon_X196)
% 1.19/1.38  (-. (fellow zenon_X209))
% 1.19/1.38  (-. (young zenon_X254))
% 1.19/1.38  (-. (fellow zenon_X187))
% 1.19/1.38  ((skc16) != zenon_X319)
% 1.19/1.38  ((skc23) != zenon_X198)
% 1.19/1.38  ((skc15) != zenon_X376)
% 1.19/1.38  (-. (fellow zenon_X177))
% 1.19/1.38  ((skc23) != zenon_X359)
% 1.19/1.38  (-. (young zenon_X258))
% 1.19/1.38  ((skc16) != zenon_X270)
% 1.19/1.38  ((skc16) != zenon_X276)
% 1.19/1.38  ((skc16) != zenon_X159)
% 1.19/1.38  (-. (fellow zenon_X175))
% 1.19/1.38  ((skc15) != zenon_X305)
% 1.19/1.38  ((skc23) != zenon_X380)
% 1.19/1.38  (-. (fellow zenon_X135))
% 1.19/1.38  ((skc16) != zenon_X213)
% 1.19/1.38  ((skc23) != zenon_X294)
% 1.19/1.38  ((skc15) != zenon_X346)
% 1.19/1.38  ((skc24) != zenon_X165)
% 1.19/1.38  (-. (young zenon_X247))
% 1.19/1.38  ((skc24) != zenon_X204)
% 1.19/1.38  ((skc15) != zenon_X333)
% 1.19/1.38  ((skc15) != zenon_X299)
% 1.19/1.38  ((skc23) != zenon_X340)
% 1.19/1.38  ((skc23) != zenon_X403)
% 1.19/1.38  ((skc23) != zenon_X139)
% 1.19/1.38  ((skc16) != zenon_X204)
% 1.19/1.38  ((skc16) != zenon_X313)
% 1.19/1.38  ((skc24) != zenon_X169)
% 1.19/1.38  ((skc24) != zenon_X127)
% 1.19/1.38  ((skc24) != zenon_X327)
% 1.19/1.38  ((skc23) != zenon_X331)
% 1.19/1.38  ((skc24) != zenon_X273)
% 1.19/1.38  ((skc15) != zenon_X249)
% 1.19/1.38  ((skc24) != zenon_X303)
% 1.19/1.38  ((skc24) != zenon_X179)
% 1.19/1.38  (-. (fellow zenon_X206))
% 1.19/1.38  ((skc17) != zenon_X97)
% 1.19/1.38  ((skc15) != zenon_X165)
% 1.19/1.38  ((skc24) != zenon_X143)
% 1.19/1.38  (-. (young zenon_X401))
% 1.19/1.38  ((skc23) != zenon_X183)
% 1.19/1.38  ((skc16) != zenon_X376)
% 1.19/1.38  ((skc23) != zenon_X137)
% 1.19/1.38  ((skc16) != zenon_X244)
% 1.19/1.38  ((skc24) != zenon_X216)
% 1.19/1.38  (-. (young zenon_X381))
% 1.19/1.38  ((skc24) != zenon_X339)
% 1.19/1.38  (street (skc26))
% 1.19/1.38  ((skc16) != zenon_X220)
% 1.19/1.38  ((skc16) != zenon_X349)
% 1.19/1.38  ((skc22) != zenon_X63)
% 1.19/1.38  ((skc23) != zenon_X268)
% 1.19/1.38  (-. (in (skc16) (skc25)))
% 1.19/1.38  ((skc23) != zenon_X260)
% 1.19/1.38  ((skc24) != zenon_X155)
% 1.19/1.38  ((skc24) != zenon_X263)
% 1.19/1.38  ((skc24) != zenon_X302)
% 1.19/1.38  ((skc24) != zenon_X280)
% 1.19/1.38  ((skc15) != zenon_X328)
% 1.19/1.38  ((skc15) != zenon_X204)
% 1.19/1.38  ((skc24) != zenon_X318)
% 1.19/1.38  ((skc24) != zenon_X298)
% 1.19/1.38  ((skc17) != zenon_X100)
% 1.19/1.38  ((skc15) != zenon_X183)
% 1.19/1.38  ((skc24) != zenon_X239)
% 1.19/1.38  ((skc15) != zenon_X313)
% 1.19/1.38  ((skc24) != zenon_X187)
% 1.19/1.38  ((skc24) != zenon_X226)
% 1.19/1.38  ((skc24) != zenon_X294)
% 1.19/1.38  ((skc18) != zenon_X85)
% 1.19/1.38  (in (skc16) (skc17))
% 1.19/1.38  ((skc23) != zenon_X278)
% 1.19/1.38  ((skc15) != zenon_X173)
% 1.19/1.38  (-. (young zenon_X386))
% 1.19/1.38  (-. (young zenon_X286))
% 1.19/1.38  ((skc15) != zenon_X292)
% 1.19/1.38  ((skc16) != zenon_X290)
% 1.19/1.38  ((skc23) != zenon_X298)
% 1.19/1.38  ((skc16) != zenon_X227)
% 1.19/1.38  (-. (young zenon_X285))
% 1.19/1.38  ((skc16) != zenon_X242)
% 1.19/1.38  ((skc16) != zenon_X301)
% 1.19/1.38  (-. (young zenon_X403))
% 1.19/1.38  ((skc16) != zenon_X280)
% 1.19/1.38  ((skc17) != zenon_X94)
% 1.19/1.38  (-. (young zenon_X291))
% 1.19/1.38  ((skc16) != zenon_X414)
% 1.19/1.38  (-. (fellow zenon_X155))
% 1.19/1.38  ((skc15) != zenon_X121)
% 1.19/1.38  ((skc15) != zenon_X141)
% 1.19/1.38  (-. (young zenon_X305))
% 1.19/1.38  ((skc16) != zenon_X382)
% 1.19/1.38  ((skc23) != zenon_X318)
% 1.19/1.38  (-. (fellow zenon_X149))
% 1.19/1.38  ((skc23) != zenon_X186)
% 1.19/1.38  (-. (young zenon_X244))
% 1.19/1.38  ((skc16) != zenon_X279)
% 1.19/1.38  ((skc15) != zenon_X277)
% 1.19/1.38  ((skc16) != zenon_X383)
% 1.19/1.38  (-. (seat zenon_X100))
% 1.19/1.38  ((skc24) != zenon_X208)
% 1.19/1.38  (-. (fellow zenon_X179))
% 1.19/1.38  ((skc16) != zenon_X141)
% 1.19/1.38  ((skc16) != zenon_X343)
% 1.19/1.38  (-. (young zenon_X396))
% 1.19/1.38  ((skc23) != zenon_X360)
% 1.19/1.38  ((skc24) != zenon_X260)
% 1.19/1.38  (-. (young zenon_X186))
% 1.19/1.38  ((skc23) != zenon_X171)
% 1.19/1.38  ((skc23) != zenon_X358)
% 1.19/1.38  ((skc23) != zenon_X143)
% 1.19/1.38  ((skc15) != zenon_X381)
% 1.19/1.38  ((skc23) != zenon_X266)
% 1.19/1.38  (-. (city zenon_X75))
% 1.19/1.38  ((skc25) != zenon_X94)
% 1.19/1.38  ((skc16) != zenon_X139)
% 1.19/1.38  ((skc15) != zenon_X340)
% 1.19/1.38  ((skc15) != zenon_X127)
% 1.19/1.38  ((skc24) != zenon_X245)
% 1.19/1.38  ((skc24) != zenon_X149)
% 1.19/1.38  ((skc15) != zenon_X198)
% 1.19/1.38  ((skc16) != zenon_X253)
% 1.19/1.38  ((skc15) != zenon_X322)
% 1.19/1.38  ((skc23) != zenon_X384)
% 1.19/1.38  ((skc16) != zenon_X217)
% 1.19/1.38  ((skc15) != zenon_X240)
% 1.19/1.38  ((skc15) != zenon_X139)
% 1.19/1.38  ((skc23) != zenon_X303)
% 1.19/1.38  ((skc23) != zenon_X407)
% 1.19/1.38  ((skc16) != zenon_X265)
% 1.19/1.38  ((skc24) != zenon_X354)
% 1.19/1.38  ((skc24) != zenon_X214)
% 1.19/1.38  ((skc24) != zenon_X401)
% 1.19/1.38  ((skc23) != zenon_X310)
% 1.19/1.38  ((skc23) != zenon_X329)
% 1.19/1.38  ((skc25) != zenon_X132)
% 1.19/1.38  ((skc23) != zenon_X346)
% 1.19/1.38  (-. (seat zenon_X88))
% 1.19/1.38  ((skc24) != zenon_X159)
% 1.19/1.38  ((skc24) != zenon_X229)
% 1.19/1.38  ((skc16) != zenon_X171)
% 1.19/1.38  ((skc18) != zenon_X132)
% 1.19/1.38  ((skc24) != zenon_X322)
% 1.19/1.38  ((skc24) != zenon_X186)
% 1.19/1.38  ((skc16) != zenon_X264)
% 1.19/1.38  ((skc19) != zenon_X21)
% 1.19/1.38  ((skc15) != zenon_X259)
% 1.19/1.38  ((skc17) != zenon_X106)
% 1.19/1.38  (in (skc28) (skc29))
% 1.19/1.38  ((skc27) != zenon_X21)
% 1.19/1.38  ((skc24) != zenon_X248)
% 1.19/1.38  ((skc24) != zenon_X190)
% 1.19/1.38  ((skc15) != zenon_X280)
% 1.19/1.38  ((skc16) != zenon_X336)
% 1.19/1.38  ((skc23) != zenon_X337)
% 1.19/1.38  (-. (young zenon_X250))
% 1.19/1.38  ((skc15) != zenon_X375)
% 1.19/1.38  ((skc23) != zenon_X245)
% 1.19/1.38  ((skc15) != zenon_X184)
% 1.19/1.38  (-. (fellow zenon_X123))
% 1.19/1.38  ((skc24) != zenon_X206)
% 1.19/1.38  ((skc16) != zenon_X342)
% 1.19/1.38  ((skc23) != zenon_X235)
% 1.19/1.38  ((skc29) != zenon_X71)
% 1.19/1.38  ((skc15) != zenon_X414)
% 1.19/1.38  (-. (young zenon_X284))
% 1.19/1.38  ((skc15) != zenon_X318)
% 1.19/1.38  ((skc18) != zenon_X115)
% 1.19/1.38  ((skc24) != zenon_X287)
% 1.19/1.38  ((skc24) != zenon_X300)
% 1.19/1.38  ((skc15) != zenon_X327)
% 1.19/1.38  ((skc23) != zenon_X258)
% 1.19/1.38  ((skc16) != zenon_X306)
% 1.19/1.38  ((skc24) != zenon_X386)
% 1.19/1.38  ((skc16) != zenon_X262)
% 1.19/1.38  (-. (fellow zenon_X143))
% 1.19/1.38  ((skc24) != zenon_X295)
% 1.19/1.38  ((skc16) != zenon_X175)
% 1.19/1.38  ((skc24) != zenon_X218)
% 1.19/1.38  ((skc24) != zenon_X266)
% 1.19/1.38  (-. (young zenon_X275))
% 1.19/1.38  ((skc24) != zenon_X309)
% 1.19/1.38  (seat (skc18))
% 1.19/1.38  ((skc24) != zenon_X135)
% 1.19/1.38  ((skc23) != zenon_X251)
% 1.19/1.38  ((skc23) != zenon_X369)
% 1.19/1.38  (down (skc28) (skc26))
% 1.19/1.38  ((skc23) != zenon_X263)
% 1.19/1.38  ((skc15) != zenon_X264)
% 1.19/1.38  ((skc23) != zenon_X314)
% 1.19/1.38  ((skc15) != zenon_X211)
% 1.19/1.38  ((skc16) != zenon_X186)
% 1.19/1.38  ((skc16) != zenon_X368)
% 1.19/1.38  ((skc24) != zenon_X369)
% 1.19/1.38  ((skc15) != zenon_X251)
% 1.19/1.38  (seat (skc17))
% 1.19/1.38  (-. (young zenon_X358))
% 1.19/1.38  ((skc28) != zenon_X32)
% 1.19/1.38  ((skc23) != zenon_X336)
% 1.19/1.38  ((skc16) != zenon_X232)
% 1.19/1.38  ((skc23) != zenon_X244)
% 1.19/1.38  ((skc16) != zenon_X192)
% 1.19/1.38  ((skc16) != zenon_X254)
% 1.19/1.38  ((skc16) != zenon_X309)
% 1.19/1.38  ((skc15) != zenon_X253)
% 1.19/1.38  ((skc15) != zenon_X278)
% 1.19/1.38  (-. (young zenon_X205))
% 1.19/1.38  ((skc24) != zenon_X252)
% 1.19/1.38  ((skc23) != zenon_X271)
% 1.19/1.38  ((skc23) != zenon_X167)
% 1.19/1.38  ((skc23) != zenon_X237)
% 1.19/1.38  ((skc15) != zenon_X167)
% 1.19/1.38  (white (skc27))
% 1.19/1.38  ((skc18) != zenon_X97)
% 1.19/1.38  ((skc15) != zenon_X236)
% 1.19/1.38  ((skc23) != zenon_X381)
% 1.19/1.38  ((skc15) != zenon_X357)
% 1.19/1.38  ((skc15) != zenon_X338)
% 1.19/1.38  ((skc17) != zenon_X79)
% 1.19/1.38  ((skc15) != zenon_X288)
% 1.19/1.38  ((skc23) != zenon_X127)
% 1.19/1.38  (-. (seat zenon_X103))
% 1.19/1.38  (-. (fellow zenon_X218))
% 1.19/1.38  ((skc15) != zenon_X354)
% 1.19/1.38  ((skc16) != zenon_X184)
% 1.19/1.38  ((skc16) != zenon_X288)
% 1.19/1.38  ((skc24) != zenon_X275)
% 1.19/1.38  ((skc16) != zenon_X401)
% 1.19/1.38  ((skc15) != zenon_X266)
% 1.19/1.38  (-. (young zenon_X273))
% 1.19/1.38  ((skc24) != zenon_X221)
% 1.19/1.38  ((skc15) != zenon_X285)
% 1.19/1.38  ((skc23) != zenon_X270)
% 1.19/1.38  (-. (seat zenon_X94))
% 1.19/1.38  ((skc15) != zenon_X312)
% 1.19/1.38  ((skc15) != zenon_X283)
% 1.19/1.38  ((skc23) != zenon_X190)
% 1.19/1.38  ((skc15) != zenon_X235)
% 1.19/1.38  ((skc15) != zenon_X306)
% 1.19/1.38  ((skc15) != zenon_X297)
% 1.19/1.38  ((skc24) != zenon_X233)
% 1.19/1.38  ((skc16) != zenon_X147)
% 1.19/1.38  (lonely (skc20))
% 1.19/1.38  (-. (young zenon_X304))
% 1.19/1.38  ((skc16) != zenon_X121)
% 1.19/1.38  ((skc24) != zenon_X314)
% 1.19/1.38  ((skc24) != zenon_X383)
% 1.19/1.38  ((skc16) != zenon_X208)
% 1.19/1.38  ((skc23) != zenon_X290)
% 1.19/1.38  ((skc16) != zenon_X189)
% 1.19/1.38  ((skc24) != zenon_X236)
% 1.19/1.38  ((skc23) != zenon_X274)
% 1.19/1.38  ((skc24) != zenon_X336)
% 1.19/1.38  (-. (young zenon_X318))
% 1.19/1.38  ((skc24) != zenon_X255)
% 1.19/1.38  ((skc23) != zenon_X282)
% 1.19/1.38  ((skc23) != zenon_X151)
% 1.19/1.38  ((skc24) != zenon_X249)
% 1.19/1.38  (-. (fellow zenon_X227))
% 1.19/1.38  ((skc24) != zenon_X279)
% 1.19/1.38  ((skc15) != zenon_X169)
% 1.19/1.38  (-. (fellow zenon_X200))
% 1.19/1.38  ((skc24) != zenon_X313)
% 1.19/1.38  ((skc16) != zenon_X252)
% 1.19/1.38  ((skc15) != zenon_X407)
% 1.19/1.38  ((skc17) != zenon_X85)
% 1.19/1.38  ((skc23) != zenon_X202)
% 1.19/1.38  ((skc23) != zenon_X297)
% 1.19/1.38  (city (skc22))
% 1.19/1.38  (city (skc29))
% 1.19/1.38  ((skc16) != zenon_X312)
% 1.19/1.38  ((skc24) != zenon_X317)
% 1.19/1.38  ((skc17) != (skc25))
% 1.19/1.38  (-. (fellow zenon_X242))
% 1.19/1.38  ((skc23) != zenon_X362)
% 1.19/1.38  ((skc24) != zenon_X167)
% 1.19/1.38  (event (skc28))
% 1.19/1.38  ((skc16) != zenon_X283)
% 1.19/1.38  ((skc15) != zenon_X242)
% 1.19/1.38  (-. (young zenon_X353))
% 1.19/1.38  ((skc23) != zenon_X376)
% 1.19/1.38  (-. (young zenon_X365))
% 1.19/1.38  (-. (young zenon_X379))
% 1.19/1.38  ((skc23) != zenon_X322)
% 1.19/1.38  ((skc24) != zenon_X281)
% 1.19/1.38  (-. (young zenon_X241))
% 1.19/1.38  ((skc24) != zenon_X288)
% 1.19/1.38  ((skc16) != zenon_X226)
% 1.19/1.38  ((skc24) != zenon_X123)
% 1.19/1.38  (-. (young zenon_X268))
% 1.19/1.38  ((skc24) != zenon_X268)
% 1.19/1.38  ((skc16) != zenon_X317)
% 1.19/1.38  ((skc16) != zenon_X153)
% 1.19/1.38  ((skc23) != zenon_X286)
% 1.19/1.38  (-. (young zenon_X289))
% 1.19/1.38  ((skc23) != zenon_X215)
% 1.19/1.38  ((skc17) != zenon_X132)
% 1.19/1.38  (-. (fellow zenon_X137))
% 1.19/1.38  ((skc23) != zenon_X240)
% 1.19/1.38  ((skc24) != zenon_X283)
% 1.19/1.38  ((skc24) != zenon_X384)
% 1.19/1.38  ((skc18) != zenon_X79)
% 1.19/1.38  ((skc16) != zenon_X346)
% 1.19/1.38  (-. (young zenon_X257))
% 1.19/1.38  ((skc25) != zenon_X97)
% 1.19/1.38  (-. (fellow zenon_X145))
% 1.19/1.38  ((skc23) != zenon_X163)
% 1.19/1.38  ((skc23) != zenon_X169)
% 1.19/1.38  (-. (event zenon_X42))
% 1.19/1.38  (-. (young zenon_X316))
% 1.19/1.38  (-. (young zenon_X259))
% 1.19/1.38  ((skc23) != zenon_X300)
% 1.19/1.38  ((skc23) != zenon_X173)
% 1.19/1.38  ((skc23) != zenon_X157)
% 1.19/1.38  ((skc16) != zenon_X263)
% 1.19/1.38  ((skc18) != zenon_X112)
% 1.19/1.38  ((skc16) != zenon_X230)
% 1.19/1.38  ((skc16) != zenon_X338)
% 1.19/1.38  (-. (fellow zenon_X245))
% 1.19/1.38  ((skc16) != zenon_X289)
% 1.19/1.38  ((skc16) != zenon_X151)
% 1.19/1.38  ((skc24) != zenon_X319)
% 1.19/1.38  (-. (young zenon_X288))
% 1.19/1.38  (hollywood (skc22))
% 1.19/1.38  ((skc17) != zenon_X129)
% 1.19/1.38  ((skc16) != zenon_X357)
% 1.19/1.38  (fellow (skc24))
% 1.19/1.38  ((skc15) != zenon_X205)
% 1.19/1.38  ((skc15) != zenon_X193)
% 1.19/1.38  ((skc16) != zenon_X269)
% 1.19/1.38  (-. (fellow zenon_X161))
% 1.19/1.38  ((skc24) != zenon_X151)
% 1.19/1.38  (-. (young zenon_X333))
% 1.19/1.38  ((skc15) != zenon_X308)
% 1.19/1.38  ((skc15) != zenon_X365)
% 1.19/1.38  (-. (young zenon_X249))
% 1.19/1.38  ((skc24) != zenon_X265)
% 1.19/1.38  ((skc16) != zenon_X281)
% 1.19/1.38  ((skc29) != zenon_X63)
% 1.19/1.38  (-. (young zenon_X311))
% 1.19/1.38  (street (skc20))
% 1.19/1.38  ((skc28) != zenon_X27)
% 1.19/1.38  (-. (young zenon_X261))
% 1.19/1.38  ((skc16) != zenon_X375)
% 1.19/1.38  ((skc15) != zenon_X209)
% 1.19/1.38  ((skc23) != zenon_X277)
% 1.19/1.38  ((skc16) != zenon_X354)
% 1.19/1.38  ((skc15) != zenon_X155)
% 1.19/1.38  (-. (young zenon_X349))
% 1.19/1.38  ((skc29) != (skc18))
% 1.19/1.38  ((skc15) != zenon_X186)
% 1.19/1.38  ((skc23) != zenon_X155)
% 1.19/1.38  ((skc17) != (skc18))
% 1.19/1.38  ((skc15) != zenon_X267)
% 1.19/1.38  ((skc27) != zenon_X15)
% 1.19/1.38  ((skc23) != zenon_X255)
% 1.19/1.38  ((skc15) != zenon_X358)
% 1.19/1.38  (-. (city zenon_X71))
% 1.19/1.38  ((skc16) != zenon_X187)
% 1.19/1.38  ((skc29) != zenon_X59)
% 1.19/1.38  ((skc15) != zenon_X349)
% 1.19/1.38  ((skc15) != zenon_X362)
% 1.19/1.38  ((skc23) != zenon_X311)
% 1.19/1.38  ((skc15) != zenon_X294)
% 1.19/1.38  ((skc18) != zenon_X103)
% 1.19/1.38  ((skc23) != zenon_X209)
% 1.19/1.38  ((skc16) != zenon_X161)
% 1.19/1.38  (-. (young zenon_X299))
% 1.19/1.38  ((skc15) != zenon_X334)
% 1.19/1.38  ((skc24) != zenon_X200)
% 1.19/1.38  ((skc23) != zenon_X216)
% 1.19/1.38  (-. (young zenon_X297))
% 1.19/1.38  (-. (young zenon_X216))
% 1.19/1.38  ((skc24) != zenon_X359)
% 1.19/1.38  ((skc24) != zenon_X251)
% 1.19/1.38  ((skc24) != zenon_X368)
% 1.19/1.38  ((skc16) != zenon_X285)
% 1.19/1.38  ((skc16) != zenon_X266)
% 1.19/1.38  ((skc15) != zenon_X143)
% 1.19/1.38  ((skc23) != zenon_X269)
% 1.19/1.38  (-. (young zenon_X276))
% 1.19/1.38  ((skc23) != zenon_X280)
% 1.19/1.38  ((skc24) != zenon_X250)
% 1.19/1.38  ((skc15) != zenon_X316)
% 1.19/1.38  ((skc23) != zenon_X259)
% 1.19/1.38  ((skc24) != zenon_X381)
% 1.19/1.38  (-. (city zenon_X67))
% 1.19/1.38  (-. (event zenon_X27))
% 1.19/1.38  ((skc24) != zenon_X157)
% 1.19/1.38  (-. (young zenon_X383))
% 1.19/1.38  ((skc23) != zenon_X248)
% 1.19/1.38  ((skc23) != zenon_X343)
% 1.19/1.38  ((skc15) != zenon_X237)
% 1.19/1.38  ((skc28) != zenon_X42)
% 1.19/1.38  ((skc24) != zenon_X334)
% 1.19/1.38  (-. (young zenon_X217))
% 1.19/1.38  ((skc15) != zenon_X275)
% 1.19/1.38  ((skc23) != zenon_X224)
% 1.19/1.38  ((skc23) != zenon_X279)
% 1.19/1.38  (-. (seat zenon_X85))
% 1.19/1.38  ((skc16) != zenon_X275)
% 1.19/1.38  ((skc15) != zenon_X244)
% 1.19/1.38  ((skc16) != zenon_X258)
% 1.19/1.38  ((skc15) != zenon_X245)
% 1.19/1.38  (-. (young zenon_X312))
% 1.19/1.38  ((skc24) != zenon_X343)
% 1.19/1.38  ((skc23) != zenon_X338)
% 1.19/1.38  ((skc24) != zenon_X240)
% 1.19/1.38  (young (skc23))
% 1.19/1.38  ((skc23) != zenon_X196)
% 1.19/1.38  ((skc23) != zenon_X334)
% 1.19/1.38  ((skc24) != zenon_X393)
% 1.19/1.38  ((skc17) != zenon_X112)
% 1.19/1.38  ((skc15) != zenon_X202)
% 1.19/1.38  ((skc23) != zenon_X319)
% 1.19/1.38  ((skc15) != zenon_X302)
% 1.19/1.38  ((skc24) != zenon_X202)
% 1.19/1.38  ((skc23) != zenon_X313)
% 1.19/1.38  ((skc17) != zenon_X88)
% 1.19/1.38  ((skc29) != zenon_X47)
% 1.19/1.38  ((skc24) != zenon_X292)
% 1.19/1.38  ((skc20) != zenon_X0)
% 1.19/1.38  ((skc23) != zenon_X205)
% 1.19/1.38  ((skc15) != zenon_X286)
% 1.19/1.38  ((skc16) != zenon_X251)
% 1.19/1.38  ((skc24) != zenon_X209)
% 1.19/1.38  ((skc23) != zenon_X377)
% 1.19/1.38  (man (skc15))
% 1.19/1.38  (ssSkC0)
% 1.19/1.38  ((skc23) != zenon_X121)
% 1.19/1.38  ((skc16) != zenon_X123)
% 1.19/1.38  (-. (young zenon_X366))
% 1.19/1.38  ((skc18) != zenon_X100)
% 1.19/1.38  ((skc15) != zenon_X218)
% 1.19/1.38  ((skc15) != zenon_X282)
% 1.19/1.38  ((skc23) != zenon_X366)
% 1.19/1.38  (fellow (skc15))
% 1.19/1.38  ((skc15) != zenon_X147)
% 1.19/1.38  (seat (skc25))
% 1.19/1.38  (-. (young zenon_X322))
% 1.19/1.38  ((skc23) != zenon_X262)
% 1.19/1.38  (-. (young zenon_X317))
% 1.19/1.38  ((skc21) != zenon_X37)
% 1.19/1.38  ((skc24) != zenon_X396)
% 1.19/1.38  ((skc19) != zenon_X15)
% 1.19/1.38  (-. (fellow zenon_X198))
% 1.19/1.38  ((skc23) != zenon_X253)
% 1.19/1.38  ((skc24) != zenon_X242)
% 1.19/1.38  ((skc24) != zenon_X353)
% 1.19/1.38  ((skc16) != zenon_X240)
% 1.19/1.38  ((skc24) != zenon_X329)
% 1.19/1.38  ((skc16) != zenon_X396)
% 1.19/1.38  ((skc15) != zenon_X311)
% 1.19/1.38  (-. (fellow zenon_X121))
% 1.19/1.38  ((skc23) != zenon_X135)
% 1.19/1.38  ((skc23) != zenon_X353)
% 1.19/1.38  ((skc24) != zenon_X125)
% 1.19/1.38  ((skc16) != zenon_X359)
% 1.19/1.38  (-. (young zenon_X393))
% 1.19/1.38  (fellow (skc23))
% 1.19/1.38  (-. (fellow zenon_X193))
% 1.19/1.38  ((skc15) != zenon_X125)
% 1.19/1.38  ((skc15) != zenon_X314)
% 1.19/1.38  ((skc15) != zenon_X179)
% 1.19/1.38  ((skc23) != zenon_X236)
% 1.19/1.38  ((skc22) != zenon_X59)
% 1.19/1.38  (-. (fellow zenon_X181))
% 1.19/1.38  (way (skc26))
% 1.19/1.38  ((skc24) != zenon_X247)
% 1.19/1.38  ((skc15) != zenon_X360)
% 1.19/1.38  ((skc22) != zenon_X67)
% 1.19/1.38  ((skc15) != zenon_X256)
% 1.19/1.38  ((skc23) != zenon_X256)
% 1.19/1.38  ((skc15) != zenon_X159)
% 1.19/1.38  (-. (fellow zenon_X184))
% 1.19/1.38  ((skc15) != zenon_X298)
% 1.19/1.38  ((skc15) != zenon_X224)
% 1.19/1.38  ((skc24) != zenon_X311)
% 1.19/1.38  ((skc15) != zenon_X233)
% 1.19/1.38  ((skc16) != zenon_X271)
% 1.19/1.38  ((skc16) != zenon_X308)
% 1.19/1.38  (young (skc15))
% 1.19/1.38  ((skc15) != zenon_X250)
% 1.19/1.38  ((skc23) != zenon_X341)
% 1.19/1.38  ((skc25) != zenon_X91)
% 1.19/1.38  ((skc16) != zenon_X235)
% 1.19/1.38  ((skc24) != zenon_X183)
% 1.19/1.38  (-. (young zenon_X360))
% 1.19/1.38  (-. (seat zenon_X115))
% 1.19/1.38  (way (skc20))
% 1.19/1.38  (barrel (skc28) (skc27))
% 1.19/1.38  ((skc23) != zenon_X287)
% 1.19/1.38  (-. (young zenon_X369))
% 1.19/1.38  (-. (fellow zenon_X190))
% 1.19/1.38  (-. (fellow zenon_X230))
% 1.19/1.38  ((skc15) != zenon_X386)
% 1.19/1.38  ((skc15) != zenon_X303)
% 1.19/1.38  ((skc23) != zenon_X161)
% 1.19/1.38  ((skc16) != zenon_X183)
% 1.19/1.38  ((skc15) != zenon_X265)
% 1.19/1.38  ((skc23) != zenon_X301)
% 1.19/1.38  ((skc24) != zenon_X306)
% 1.19/1.38  ((skc16) != zenon_X236)
% 1.19/1.38  ((skc16) != zenon_X353)
% 1.19/1.38  (-. (fellow zenon_X196))
% 1.19/1.38  (-. (fellow zenon_X221))
% 1.19/1.38  ((skc23) != zenon_X165)
% 1.19/1.38  ((skc16) != zenon_X268)
% 1.19/1.38  (-. (young zenon_X283))
% 1.19/1.38  ((skc16) != zenon_X260)
% 1.19/1.38  ((skc15) != zenon_X248)
% 1.19/1.38  ((skc15) != zenon_X301)
% 1.19/1.38  ((skc23) != zenon_X208)
% 1.19/1.38  (-. (young zenon_X211))
% 1.19/1.38  ((skc24) != zenon_X161)
% 1.19/1.38  (-. (young zenon_X235))
% 1.19/1.38  ((skc15) != zenon_X175)
% 1.19/1.38  (-. (young zenon_X278))
% 1.19/1.38  ((skc18) != zenon_X88)
% 1.19/1.38  (-. (young zenon_X272))
% 1.19/1.38  ((skc15) != zenon_X331)
% 1.19/1.38  ((skc23) != zenon_X386)
% 1.19/1.38  ((skc23) != zenon_X291)
% 1.19/1.38  ((skc23) != zenon_X273)
% 1.19/1.38  ((skc16) != zenon_X181)
% 1.19/1.38  (in (skc15) (skc18))
% 1.19/1.38  ((skc23) != zenon_X233)
% 1.19/1.38  (-. (young zenon_X367))
% 1.19/1.38  ((skc16) != (skc23))
% 1.19/1.38  ((skc24) != zenon_X380)
% 1.19/1.38  ((skc24) != zenon_X147)
% 1.19/1.38  ((skc15) != zenon_X380)
% 1.19/1.38  (-. (young zenon_X255))
% 1.19/1.38  ((skc23) != zenon_X267)
% 1.19/1.38  ((skc16) != zenon_X233)
% 1.19/1.38  ((skc23) != zenon_X308)
% 1.19/1.38  ((skc16) != zenon_X304)
% 1.19/1.38  ((skc24) != zenon_X259)
% 1.19/1.38  ((skc25) != zenon_X118)
% 1.19/1.38  ((skc15) != zenon_X377)
% 1.19/1.38  ((skc23) != zenon_X181)
% 1.19/1.38  ((skc16) != zenon_X341)
% 1.19/1.38  ((skc15) != zenon_X291)
% 1.19/1.38  ((skc23) != zenon_X177)
% 1.19/1.38  (-. (in (skc15) (skc17)))
% 1.19/1.38  ((skc16) != zenon_X261)
% 1.19/1.38  (-. (young zenon_X208))
% 1.19/1.38  ((skc23) != zenon_X396)
% 1.19/1.38  ((skc24) != zenon_X270)
% 1.19/1.38  ((skc16) != zenon_X205)
% 1.19/1.38  ((skc24) != zenon_X241)
% 1.19/1.38  ((skc15) != zenon_X123)
% 1.19/1.38  (-. (young zenon_X237))
% 1.19/1.38  (-. (seat zenon_X132))
% 1.19/1.38  ((skc23) != zenon_X212)
% 1.19/1.38  ((skc23) != zenon_X221)
% 1.19/1.38  ((skc25) != zenon_X115)
% 1.19/1.38  ((skc16) != zenon_X247)
% 1.19/1.38  ((skc23) != zenon_X184)
% 1.19/1.38  ((skc24) != zenon_X308)
% 1.19/1.38  (-. (young zenon_X329))
% 1.19/1.38  ((skc23) != zenon_X189)
% 1.19/1.38  (-. (fellow zenon_X171))
% 1.19/1.38  ((skc16) != zenon_X211)
% 1.19/1.38  ((skc24) != zenon_X367)
% 1.19/1.38  ((skc23) != zenon_X242)
% 1.19/1.38  ((skc15) != zenon_X151)
% 1.19/1.38  ((skc16) != zenon_X292)
% 1.19/1.38  (dirty (skc27))
% 1.19/1.38  ((skc15) != zenon_X383)
% 1.19/1.38  (-. (young zenon_X328))
% 1.19/1.38  (-. (young zenon_X339))
% 1.19/1.38  ((skc24) != zenon_X196)
% 1.19/1.38  ((skc16) != zenon_X229)
% 1.19/1.38  ((skc23) != zenon_X281)
% 1.19/1.38  (-. (city zenon_X47))
% 1.19/1.38  (-. (fellow zenon_X141))
% 1.19/1.38  ((skc16) != zenon_X193)
% 1.19/1.38  ((skc15) != zenon_X341)
% 1.19/1.38  ((skc24) != zenon_X341)
% 1.19/1.38  (white (skc19))
% 1.19/1.38  (-. (young zenon_X236))
% 1.19/1.38  ((skc15) != zenon_X221)
% 1.19/1.38  (-. (young zenon_X251))
% 1.19/1.38  ((skc24) != zenon_X272)
% 1.19/1.38  ((skc24) != zenon_X254)
% 1.19/1.38  ((skc24) != zenon_X289)
% 1.19/1.38  ((skc15) != zenon_X213)
% 1.19/1.38  ((skc16) != zenon_X272)
% 1.19/1.38  (-. (seat zenon_X129))
% 1.19/1.38  ((skc16) != zenon_X173)
% 1.19/1.38  ((skc16) != zenon_X329)
% 1.19/1.38  ((skc16) != zenon_X407)
% 1.19/1.38  ((skc23) != zenon_X153)
% 1.19/1.38  ((skc23) != zenon_X217)
% 1.19/1.38  (hollywood (skc29))
% 1.19/1.38  (-. (fellow zenon_X153))
% 1.19/1.38  (-. (young zenon_X274))
% 1.19/1.38  (-. (young zenon_X376))
% 1.19/1.38  ((skc23) != zenon_X223)
% 1.19/1.38  ((skc23) != zenon_X226)
% 1.19/1.38  ((skc23) != zenon_X393)
% 1.19/1.38  ((skc23) != zenon_X309)
% 1.19/1.38  ((skc15) != zenon_X319)
% 1.19/1.38  (-. (young zenon_X270))
% 1.19/1.38  (-. (old zenon_X15))
% 1.19/1.38  ((skc23) != zenon_X328)
% 1.19/1.38  (furniture (skc17))
% 1.19/1.38  ((skc23) != zenon_X214)
% 1.19/1.38  ((skc25) != zenon_X88)
% 1.19/1.38  ((skc22) != (skc25))
% 1.19/1.38  ((skc23) != zenon_X295)
% 1.19/1.38  ((skc15) != zenon_X135)
% 1.19/1.38  (-. (young zenon_X183))
% 1.19/1.38  ((skc16) != zenon_X300)
% 1.19/1.38  (-. (young zenon_X260))
% 1.19/1.38  (-. (fellow zenon_X224))
% 1.19/1.38  (-. (fellow zenon_X127))
% 1.19/1.38  ((skc15) != zenon_X317)
% 1.19/1.38  ((skc24) != zenon_X257)
% 1.19/1.38  (-. (fellow zenon_X159))
% 1.19/1.38  ((skc16) != zenon_X340)
% 1.19/1.38  ((skc24) != zenon_X262)
% 1.19/1.38  ((skc15) != zenon_X195)
% 1.19/1.38  (-. (young zenon_X238))
% 1.19/1.38  (-. (fellow zenon_X125))
% 1.19/1.38  ((skc15) != zenon_X273)
% 1.19/1.38  (-. (young zenon_X303))
% 1.19/1.38  ((skc15) != zenon_X290)
% 1.19/1.38  (-. (fellow zenon_X233))
% 1.19/1.38  ((skc16) != zenon_X284)
% 1.19/1.38  (-. (young zenon_X336))
% 1.19/1.38  ((skc15) != zenon_X343)
% 1.19/1.38  ((skc26) != zenon_X0)
% 1.19/1.38  ((skc16) != zenon_X255)
% 1.19/1.38  ((skc24) != zenon_X328)
% 1.19/1.38  ((skc16) != zenon_X200)
% 1.19/1.38  ((skc15) != zenon_X309)
% 1.19/1.38  (-. (seat zenon_X79))
% 1.19/1.38  ((skc24) != zenon_X217)
% 1.19/1.38  ((skc24) != zenon_X407)
% 1.19/1.38  ((skc16) != zenon_X259)
% 1.19/1.38  (-. (city zenon_X51))
% 1.19/1.38  ((skc15) != zenon_X339)
% 1.19/1.38  ((skc23) = (skc24))
% 1.19/1.38  ((skc16) != zenon_X241)
% 1.19/1.38  (-. (young zenon_X226))
% 1.19/1.38  ((skc29) != zenon_X55)
% 1.19/1.38  ((skc16) != zenon_X127)
% 1.19/1.38  (car (skc27))
% 1.19/1.38  ((skc24) != zenon_X375)
% 1.19/1.38  ((skc24) != zenon_X198)
% 1.19/1.38  (-. (young zenon_X334))
% 1.19/1.38  (-. (young zenon_X192))
% 1.19/1.38  ((skc16) != zenon_X367)
% 1.19/1.38  ((skc15) != zenon_X379)
% 1.19/1.38  ((skc15) != zenon_X403)
% 1.19/1.38  ((skc24) != zenon_X376)
% 1.19/1.38  (-. (young zenon_X375))
% 1.19/1.38  (front (skc25))
% 1.19/1.38  ((skc21) != zenon_X42)
% 1.19/1.38  ((skc15) != zenon_X208)
% 1.19/1.38  ((skc24) != zenon_X220)
% 1.19/1.38  ((skc23) != zenon_X192)
% 1.19/1.38  (fellow (skc16))
% 1.19/1.38  (furniture (skc25))
% 1.19/1.38  ((skc16) != zenon_X249)
% 1.19/1.38  ((skc15) != zenon_X226)
% 1.19/1.38  ((skc15) != zenon_X241)
% 1.19/1.38  (-. (young zenon_X220))
% 1.19/1.38  (-. (young zenon_X294))
% 1.19/1.38  ((skc24) != zenon_X189)
% 1.19/1.38  ((skc16) != zenon_X316)
% 1.19/1.38  ((skc15) != zenon_X368)
% 1.19/1.38  ((skc15) != zenon_X401)
% 1.19/1.38  ((skc23) != zenon_X220)
% 1.19/1.38  ((skc23) != zenon_X213)
% 1.19/1.38  (in (skc21) (skc22))
% 1.19/1.38  ((skc24) != zenon_X139)
% 1.19/1.38  ((skc24) != zenon_X414)
% 1.19/1.38  ((skc24) != zenon_X244)
% 1.19/1.38  (-. (young zenon_X189))
% 1.19/1.38  ((skc23) != zenon_X254)
% 1.19/1.38  ((skc24) != zenon_X256)
% 1.19/1.38  (dirty (skc19))
% 1.19/1.38  ((skc15) != zenon_X212)
% 1.19/1.38  ((skc17) != zenon_X118)
% 1.19/1.38  ((skc15) != zenon_X190)
% 1.19/1.38  (-. (young zenon_X327))
% 1.19/1.38  (-. (young zenon_X256))
% 1.19/1.38  ((skc24) != zenon_X211)
% 1.19/1.38  ((skc29) != zenon_X75)
% 1.19/1.38  ((skc15) != zenon_X171)
% 1.19/1.38  ((skc24) != zenon_X175)
% 1.19/1.38  ((skc16) != zenon_X214)
% 1.19/1.38  ((skc23) != zenon_X339)
% 1.19/1.38  ((skc23) != zenon_X401)
% 1.19/1.38  ((skc15) != zenon_X229)
% 1.19/1.38  (-. (in (skc23) (skc17)))
% 1.19/1.38  (-. (street zenon_X0))
% 1.19/1.38  ((skc17) != zenon_X109)
% 1.19/1.38  (-. (fellow zenon_X165))
% 1.19/1.38  ((skc24) != zenon_X276)
% 1.19/1.38  ((skc15) != zenon_X239)
% 1.19/1.38  ((skc15) != zenon_X137)
% 1.19/1.38  ((skc24) != zenon_X365)
% 1.19/1.38  ((skc22) != (skc17))
% 1.19/1.38  (-. (seat zenon_X112))
% 1.19/1.38  ((skc15) != zenon_X353)
% 1.19/1.38  ((skc16) != zenon_X384)
% 1.19/1.38  ((skc22) != zenon_X55)
% 1.19/1.38  ((skc16) != zenon_X273)
% 1.19/1.38  ((skc15) != zenon_X382)
% 1.19/1.38  ((skc15) != zenon_X271)
% 1.19/1.38  ((skc23) != zenon_X159)
% 1.19/1.38  ((skc23) != zenon_X275)
% 1.19/1.38  (-. (young zenon_X302))
% 1.19/1.38  ((skc16) != zenon_X318)
% 1.19/1.38  ((skc16) != zenon_X149)
% 1.19/1.38  (old (skc27))
% 1.19/1.38  (-. (fellow zenon_X157))
% 1.19/1.38  ((skc16) != zenon_X379)
% 1.19/1.38  ((skc15) != zenon_X232)
% 1.19/1.38  ((skc24) != zenon_X304)
% 1.19/1.38  (-. (young zenon_X407))
% 1.19/1.38  ((skc17) != zenon_X115)
% 1.19/1.38  ((skc15) != zenon_X189)
% 1.19/1.38  ((skc15) != zenon_X263)
% 1.19/1.38  ((skc16) != zenon_X298)
% 1.19/1.38  ((skc29) != (skc17))
% 1.19/1.38  (-. (fellow zenon_X151))
% 1.19/1.38  ((skc15) != zenon_X206)
% 1.19/1.38  (front (skc18))
% 1.19/1.38  ((skc16) != zenon_X366)
% 1.19/1.38  ((skc23) != zenon_X187)
% 1.19/1.38  (-. (fellow zenon_X167))
% 1.19/1.38  ((skc16) != zenon_X328)
% 1.19/1.38  ((skc23) != zenon_X200)
% 1.19/1.38  ((skc15) != zenon_X220)
% 1.19/1.38  ((skc16) != zenon_X223)
% 1.19/1.38  (-. (young zenon_X229))
% 1.19/1.38  ((skc24) != zenon_X238)
% 1.19/1.38  ((skc24) != zenon_X301)
% 1.19/1.38  (-. (young zenon_X266))
% 1.19/1.38  ((skc23) != zenon_X304)
% 1.19/1.38  (-. (young zenon_X340))
% 1.19/1.38  ((skc24) != zenon_X342)
% 1.19/1.38  ((skc25) != zenon_X103)
% 1.19/1.38  ((skc15) != zenon_X255)
% 1.19/1.38  (-. (young zenon_X362))
% 1.19/1.38  (man (skc23))
% 1.19/1.38  ((skc23) != zenon_X125)
% 1.19/1.38  ((skc24) != zenon_X192)
% 1.19/1.38  ((skc23) != zenon_X195)
% 1.19/1.38  ((skc24) != zenon_X264)
% 1.19/1.38  ((skc16) != zenon_X237)
% 1.19/1.38  (car (skc19))
% 1.19/1.38  ((skc16) != zenon_X339)
% 1.19/1.38  (-. (young zenon_X263))
% 1.19/1.38  (furniture (skc18))
% 1.19/1.38  ((skc24) = (skc15))
% 1.19/1.38  ((skc16) != zenon_X291)
% 1.19/1.38  (-. (young zenon_X359))
% 1.19/1.38  ((skc23) != zenon_X232)
% 1.19/1.38  (-. (young zenon_X240))
% 1.19/1.38  ((skc23) != zenon_X306)
% 1.19/1.38  ((skc23) != zenon_X312)
% 1.19/1.38  (-. (young zenon_X377))
% 1.19/1.38  ((skc24) != zenon_X291)
% 1.19/1.38  *)
% 1.19/1.38  (* NO-PROOF *)
% 1.19/1.38  % SZS status GaveUp
% 1.19/1.38  Number of rewrites on terms: 0
% 1.19/1.38  Number of rewrites on props: 0
% 1.19/1.38  nodes searched: 10520
% 1.19/1.38  max branch formulas: 2504
% 1.19/1.38  proof nodes created: 354
% 1.19/1.38  formulas created: 37789
% 1.19/1.38  
%------------------------------------------------------------------------------