%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP127-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:34:15 EDT 2024
% Result : Satisfiable 0.61s 0.78s
% Output : Saturation 0.61s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(clause52,negated_conjecture,
agent(skc6,skc7,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c39,axiom,
( X428 != X426
| X425 != X427
| X429 != X430
| ~ agent(X428,X425,X429)
| agent(X426,X427,X430) ),
theory(equality) ).
cnf(c288,plain,
( skc6 != X455
| skc7 != X457
| skc11 != X456
| agent(X455,X457,X456) ),
inference(resolution,[status(thm)],[c39,clause52]) ).
cnf(c300,plain,
( skc6 != X459
| skc7 != X460
| agent(X459,X460,skc11) ),
inference(resolution,[status(thm)],[c288,reflexivity]) ).
cnf(c302,plain,
( skc6 != X461
| agent(X461,skc7,skc11) ),
inference(resolution,[status(thm)],[c300,reflexivity]) ).
cnf(clause51,negated_conjecture,
down(skc6,skc7,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c38,axiom,
( X416 != X414
| X413 != X415
| X417 != X418
| ~ down(X416,X413,X417)
| down(X414,X415,X418) ),
theory(equality) ).
cnf(c283,plain,
( skc6 != X451
| skc7 != X450
| skc8 != X452
| down(X451,X450,X452) ),
inference(resolution,[status(thm)],[c38,clause51]) ).
cnf(c298,plain,
( skc6 != X453
| skc7 != X454
| down(X453,X454,skc8) ),
inference(resolution,[status(thm)],[c283,reflexivity]) ).
cnf(c299,plain,
( skc6 != X458
| down(X458,skc7,skc8) ),
inference(resolution,[status(thm)],[c298,reflexivity]) ).
cnf(clause50,negated_conjecture,
in(skc6,skc7,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c37,axiom,
( X406 != X404
| X403 != X405
| X407 != X408
| ~ in(X406,X403,X407)
| in(X404,X405,X408) ),
theory(equality) ).
cnf(c279,plain,
( skc6 != X446
| skc7 != X445
| skc10 != X444
| in(X446,X445,X444) ),
inference(resolution,[status(thm)],[c37,clause50]) ).
cnf(c295,plain,
( skc6 != X447
| skc7 != X448
| in(X447,X448,skc10) ),
inference(resolution,[status(thm)],[c279,reflexivity]) ).
cnf(c296,plain,
( skc6 != X449
| in(X449,skc7,skc10) ),
inference(resolution,[status(thm)],[c295,reflexivity]) ).
cnf(clause49,negated_conjecture,
of(skc6,skc9,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c30,axiom,
( X350 != X348
| X347 != X349
| X351 != X352
| ~ of(X350,X347,X351)
| of(X348,X349,X352) ),
theory(equality) ).
cnf(c253,plain,
( skc6 != X439
| skc9 != X440
| skc10 != X438
| of(X439,X440,X438) ),
inference(resolution,[status(thm)],[c30,clause49]) ).
cnf(c292,plain,
( skc6 != X442
| skc9 != X441
| of(X442,X441,skc10) ),
inference(resolution,[status(thm)],[c253,reflexivity]) ).
cnf(c293,plain,
( skc6 != X443
| of(X443,skc9,skc10) ),
inference(resolution,[status(thm)],[c292,reflexivity]) ).
cnf(clause35,axiom,
( ~ placename(X71,X74)
| ~ of(X71,X73,X72)
| ~ placename(X71,X73)
| ~ of(X71,X74,X72)
| ~ entity(X71,X72)
| X73 = X74 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c99,plain,
( ~ placename(skc6,skc9)
| ~ of(skc6,X437,skc10)
| ~ placename(skc6,X437)
| ~ entity(skc6,skc10)
| X437 = skc9 ),
inference(resolution,[status(thm)],[clause49,clause35]) ).
cnf(clause48,negated_conjecture,
old(skc6,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(c36,axiom,
( X397 != X395
| X394 != X396
| ~ old(X397,X394)
| old(X395,X396) ),
theory(equality) ).
cnf(c275,plain,
( skc6 != X431
| skc11 != X432
| old(X431,X432) ),
inference(resolution,[status(thm)],[c36,clause48]) ).
cnf(c289,plain,
( skc6 != X433
| old(X433,skc11) ),
inference(resolution,[status(thm)],[c275,reflexivity]) ).
cnf(clause47,negated_conjecture,
dirty(skc6,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(c35,axiom,
( X387 != X385
| X384 != X386
| ~ dirty(X387,X384)
| dirty(X385,X386) ),
theory(equality) ).
cnf(c270,plain,
( skc6 != X422
| skc11 != X423
| dirty(X422,X423) ),
inference(resolution,[status(thm)],[c35,clause47]) ).
cnf(c286,plain,
( skc6 != X424
| dirty(X424,skc11) ),
inference(resolution,[status(thm)],[c270,reflexivity]) ).
cnf(clause46,negated_conjecture,
white(skc6,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c34,axiom,
( X379 != X377
| X376 != X378
| ~ white(X379,X376)
| white(X377,X378) ),
theory(equality) ).
cnf(c266,plain,
( skc6 != X420
| skc11 != X419
| white(X420,X419) ),
inference(resolution,[status(thm)],[c34,clause46]) ).
cnf(c284,plain,
( skc6 != X421
| white(X421,skc11) ),
inference(resolution,[status(thm)],[c266,reflexivity]) ).
cnf(clause44,negated_conjecture,
present(skc6,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c33,axiom,
( X370 != X368
| X367 != X369
| ~ present(X370,X367)
| present(X368,X369) ),
theory(equality) ).
cnf(c262,plain,
( skc6 != X410
| skc7 != X411
| present(X410,X411) ),
inference(resolution,[status(thm)],[c33,clause44]) ).
cnf(c281,plain,
( skc6 != X412
| present(X412,skc7) ),
inference(resolution,[status(thm)],[c262,reflexivity]) ).
cnf(clause39,negated_conjecture,
lonely(skc6,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c32,axiom,
( X360 != X358
| X357 != X359
| ~ lonely(X360,X357)
| lonely(X358,X359) ),
theory(equality) ).
cnf(c257,plain,
( skc6 != X401
| skc8 != X402
| lonely(X401,X402) ),
inference(resolution,[status(thm)],[c32,clause39]) ).
cnf(c278,plain,
( skc6 != X409
| lonely(X409,skc8) ),
inference(resolution,[status(thm)],[c257,reflexivity]) ).
cnf(clause31,axiom,
( ~ transport(X63,X64)
| instrumentality(X63,X64) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(clause37,negated_conjecture,
chevy(skc6,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(clause28,axiom,
( ~ chevy(X57,X58)
| car(X57,X58) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c73,plain,
car(skc6,skc11),
inference(resolution,[status(thm)],[clause28,clause37]) ).
cnf(clause29,axiom,
( ~ car(X59,X60)
| vehicle(X59,X60) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c77,plain,
vehicle(skc6,skc11),
inference(resolution,[status(thm)],[clause29,c73]) ).
cnf(clause30,axiom,
( ~ vehicle(X61,X62)
| transport(X61,X62) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c79,plain,
transport(skc6,skc11),
inference(resolution,[status(thm)],[clause30,c77]) ).
cnf(c80,plain,
instrumentality(skc6,skc11),
inference(resolution,[status(thm)],[c79,clause31]) ).
cnf(c29,axiom,
( X341 != X339
| X338 != X340
| ~ instrumentality(X341,X338)
| instrumentality(X339,X340) ),
theory(equality) ).
cnf(c249,plain,
( skc6 != X399
| skc11 != X398
| instrumentality(X399,X398) ),
inference(resolution,[status(thm)],[c29,c80]) ).
cnf(c276,plain,
( skc6 != X400
| instrumentality(X400,skc11) ),
inference(resolution,[status(thm)],[c249,reflexivity]) ).
cnf(c28,axiom,
( X331 != X329
| X328 != X330
| ~ transport(X331,X328)
| transport(X329,X330) ),
theory(equality) ).
cnf(c244,plain,
( skc6 != X392
| skc11 != X391
| transport(X392,X391) ),
inference(resolution,[status(thm)],[c28,c79]) ).
cnf(c273,plain,
( skc6 != X393
| transport(X393,skc11) ),
inference(resolution,[status(thm)],[c244,reflexivity]) ).
cnf(c27,axiom,
( X323 != X321
| X320 != X322
| ~ vehicle(X323,X320)
| vehicle(X321,X322) ),
theory(equality) ).
cnf(c240,plain,
( skc6 != X389
| skc11 != X388
| vehicle(X389,X388) ),
inference(resolution,[status(thm)],[c27,c77]) ).
cnf(c271,plain,
( skc6 != X390
| vehicle(X390,skc11) ),
inference(resolution,[status(thm)],[c240,reflexivity]) ).
cnf(c26,axiom,
( X314 != X312
| X311 != X313
| ~ car(X314,X311)
| car(X312,X313) ),
theory(equality) ).
cnf(c236,plain,
( skc6 != X381
| skc11 != X382
| car(X381,X382) ),
inference(resolution,[status(thm)],[c26,c73]) ).
cnf(c268,plain,
( skc6 != X383
| car(X383,skc11) ),
inference(resolution,[status(thm)],[c236,reflexivity]) ).
cnf(c25,axiom,
( X304 != X302
| X301 != X303
| ~ chevy(X304,X301)
| chevy(X302,X303) ),
theory(equality) ).
cnf(c231,plain,
( skc6 != X374
| skc11 != X375
| chevy(X374,X375) ),
inference(resolution,[status(thm)],[c25,clause37]) ).
cnf(c265,plain,
( skc6 != X380
| chevy(X380,skc11) ),
inference(resolution,[status(thm)],[c231,reflexivity]) ).
cnf(clause38,negated_conjecture,
city(skc6,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(clause26,axiom,
( ~ city(X53,X54)
| location(X53,X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c67,plain,
location(skc6,skc10),
inference(resolution,[status(thm)],[clause26,clause38]) ).
cnf(c24,axiom,
( X296 != X294
| X293 != X295
| ~ location(X296,X293)
| location(X294,X295) ),
theory(equality) ).
cnf(c227,plain,
( skc6 != X371
| skc10 != X372
| location(X371,X372) ),
inference(resolution,[status(thm)],[c24,c67]) ).
cnf(c263,plain,
( skc6 != X373
| location(X373,skc10) ),
inference(resolution,[status(thm)],[c227,reflexivity]) ).
cnf(c23,axiom,
( X287 != X285
| X284 != X286
| ~ city(X287,X284)
| city(X285,X286) ),
theory(equality) ).
cnf(c223,plain,
( skc6 != X365
| skc10 != X364
| city(X365,X364) ),
inference(resolution,[status(thm)],[c23,clause38]) ).
cnf(c260,plain,
( skc6 != X366
| city(X366,skc10) ),
inference(resolution,[status(thm)],[c223,reflexivity]) ).
cnf(clause42,negated_conjecture,
hollywood_placename(skc6,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c22,axiom,
( X277 != X275
| X274 != X276
| ~ hollywood_placename(X277,X274)
| hollywood_placename(X275,X276) ),
theory(equality) ).
cnf(c218,plain,
( skc6 != X361
| skc9 != X362
| hollywood_placename(X361,X362) ),
inference(resolution,[status(thm)],[c22,clause42]) ).
cnf(c258,plain,
( skc6 != X363
| hollywood_placename(X363,skc9) ),
inference(resolution,[status(thm)],[c218,reflexivity]) ).
cnf(clause41,negated_conjecture,
placename(skc6,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(clause18,axiom,
( ~ placename(X37,X38)
| relname(X37,X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c58,plain,
relname(skc6,skc9),
inference(resolution,[status(thm)],[clause18,clause41]) ).
cnf(clause19,axiom,
( ~ relname(X39,X40)
| relation(X39,X40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c59,plain,
relation(skc6,skc9),
inference(resolution,[status(thm)],[clause19,c58]) ).
cnf(clause20,axiom,
( ~ relation(X41,X42)
| abstraction(X41,X42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c60,plain,
abstraction(skc6,skc9),
inference(resolution,[status(thm)],[clause20,c59]) ).
cnf(clause23,axiom,
( ~ abstraction(X47,X48)
| general(X47,X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c64,plain,
general(skc6,skc9),
inference(resolution,[status(thm)],[clause23,c60]) ).
cnf(c21,axiom,
( X269 != X267
| X266 != X268
| ~ general(X269,X266)
| general(X267,X268) ),
theory(equality) ).
cnf(c214,plain,
( skc6 != X354
| skc9 != X355
| general(X354,X355) ),
inference(resolution,[status(thm)],[c21,c64]) ).
cnf(c255,plain,
( skc6 != X356
| general(X356,skc9) ),
inference(resolution,[status(thm)],[c214,reflexivity]) ).
cnf(clause22,axiom,
( ~ abstraction(X45,X46)
| nonhuman(X45,X46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c63,plain,
nonhuman(skc6,skc9),
inference(resolution,[status(thm)],[clause22,c60]) ).
cnf(c20,axiom,
( X260 != X258
| X257 != X259
| ~ nonhuman(X260,X257)
| nonhuman(X258,X259) ),
theory(equality) ).
cnf(c210,plain,
( skc6 != X346
| skc9 != X345
| nonhuman(X346,X345) ),
inference(resolution,[status(thm)],[c20,c63]) ).
cnf(c252,plain,
( skc6 != X353
| nonhuman(X353,skc9) ),
inference(resolution,[status(thm)],[c210,reflexivity]) ).
cnf(c19,axiom,
( X250 != X248
| X247 != X249
| ~ abstraction(X250,X247)
| abstraction(X248,X249) ),
theory(equality) ).
cnf(c205,plain,
( skc6 != X343
| skc9 != X342
| abstraction(X343,X342) ),
inference(resolution,[status(thm)],[c19,c60]) ).
cnf(c250,plain,
( skc6 != X344
| abstraction(X344,skc9) ),
inference(resolution,[status(thm)],[c205,reflexivity]) ).
cnf(c18,axiom,
( X242 != X240
| X239 != X241
| ~ relation(X242,X239)
| relation(X240,X241) ),
theory(equality) ).
cnf(c201,plain,
( skc6 != X336
| skc9 != X335
| relation(X336,X335) ),
inference(resolution,[status(thm)],[c18,c59]) ).
cnf(c247,plain,
( skc6 != X337
| relation(X337,skc9) ),
inference(resolution,[status(thm)],[c201,reflexivity]) ).
cnf(c17,axiom,
( X233 != X231
| X230 != X232
| ~ relname(X233,X230)
| relname(X231,X232) ),
theory(equality) ).
cnf(c197,plain,
( skc6 != X332
| skc9 != X333
| relname(X332,X333) ),
inference(resolution,[status(thm)],[c17,c58]) ).
cnf(c245,plain,
( skc6 != X334
| relname(X334,skc9) ),
inference(resolution,[status(thm)],[c197,reflexivity]) ).
cnf(c16,axiom,
( X223 != X221
| X220 != X222
| ~ placename(X223,X220)
| placename(X221,X222) ),
theory(equality) ).
cnf(c192,plain,
( skc6 != X326
| skc9 != X325
| placename(X326,X325) ),
inference(resolution,[status(thm)],[c16,clause41]) ).
cnf(c242,plain,
( skc6 != X327
| placename(X327,skc9) ),
inference(resolution,[status(thm)],[c192,reflexivity]) ).
cnf(clause16,axiom,
( ~ object(X33,X34)
| impartial(X33,X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause27,axiom,
( ~ location(X55,X56)
| object(X55,X56) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c68,plain,
object(skc6,skc10),
inference(resolution,[status(thm)],[clause27,c67]) ).
cnf(c69,plain,
impartial(skc6,skc10),
inference(resolution,[status(thm)],[c68,clause16]) ).
cnf(c15,axiom,
( X215 != X213
| X212 != X214
| ~ impartial(X215,X212)
| impartial(X213,X214) ),
theory(equality) ).
cnf(c188,plain,
( skc6 != X319
| skc10 != X318
| impartial(X319,X318) ),
inference(resolution,[status(thm)],[c15,c69]) ).
cnf(c239,plain,
( skc6 != X324
| impartial(X324,skc10) ),
inference(resolution,[status(thm)],[c188,reflexivity]) ).
cnf(clause9,axiom,
( ~ way(X19,X20)
| artifact(X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause40,negated_conjecture,
street(skc6,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(clause8,axiom,
( ~ street(X17,X18)
| way(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c47,plain,
way(skc6,skc8),
inference(resolution,[status(thm)],[clause8,clause40]) ).
cnf(c48,plain,
artifact(skc6,skc8),
inference(resolution,[status(thm)],[c47,clause9]) ).
cnf(clause10,axiom,
( ~ artifact(X21,X22)
| object(X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c49,plain,
object(skc6,skc8),
inference(resolution,[status(thm)],[clause10,c48]) ).
cnf(c56,plain,
impartial(skc6,skc8),
inference(resolution,[status(thm)],[clause16,c49]) ).
cnf(c187,plain,
( skc6 != X316
| skc8 != X315
| impartial(X316,X315) ),
inference(resolution,[status(thm)],[c15,c56]) ).
cnf(c237,plain,
( skc6 != X317
| impartial(X317,skc8) ),
inference(resolution,[status(thm)],[c187,reflexivity]) ).
cnf(clause32,axiom,
( ~ instrumentality(X65,X66)
| artifact(X65,X66) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c81,plain,
artifact(skc6,skc11),
inference(resolution,[status(thm)],[clause32,c80]) ).
cnf(c82,plain,
object(skc6,skc11),
inference(resolution,[status(thm)],[c81,clause10]) ).
cnf(c83,plain,
impartial(skc6,skc11),
inference(resolution,[status(thm)],[c82,clause16]) ).
cnf(c186,plain,
( skc6 != X309
| skc11 != X308
| impartial(X309,X308) ),
inference(resolution,[status(thm)],[c15,c83]) ).
cnf(c234,plain,
( skc6 != X310
| impartial(X310,skc11) ),
inference(resolution,[status(thm)],[c186,reflexivity]) ).
cnf(clause15,axiom,
( ~ object(X31,X32)
| nonliving(X31,X32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c86,plain,
nonliving(skc6,skc11),
inference(resolution,[status(thm)],[c82,clause15]) ).
cnf(c14,axiom,
( X206 != X204
| X203 != X205
| ~ nonliving(X206,X203)
| nonliving(X204,X205) ),
theory(equality) ).
cnf(c182,plain,
( skc6 != X305
| skc11 != X306
| nonliving(X305,X306) ),
inference(resolution,[status(thm)],[c14,c86]) ).
cnf(c232,plain,
( skc6 != X307
| nonliving(X307,skc11) ),
inference(resolution,[status(thm)],[c182,reflexivity]) ).
cnf(c55,plain,
nonliving(skc6,skc8),
inference(resolution,[status(thm)],[clause15,c49]) ).
cnf(c181,plain,
( skc6 != X298
| skc8 != X299
| nonliving(X298,X299) ),
inference(resolution,[status(thm)],[c14,c55]) ).
cnf(c229,plain,
( skc6 != X300
| nonliving(X300,skc8) ),
inference(resolution,[status(thm)],[c181,reflexivity]) ).
cnf(c72,plain,
nonliving(skc6,skc10),
inference(resolution,[status(thm)],[c68,clause15]) ).
cnf(c180,plain,
( skc6 != X291
| skc10 != X292
| nonliving(X291,X292) ),
inference(resolution,[status(thm)],[c14,c72]) ).
cnf(c226,plain,
( skc6 != X297
| nonliving(X297,skc10) ),
inference(resolution,[status(thm)],[c180,reflexivity]) ).
cnf(clause14,axiom,
( ~ entity(X29,X30)
| existent(X29,X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause11,axiom,
( ~ object(X23,X24)
| entity(X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c71,plain,
entity(skc6,skc10),
inference(resolution,[status(thm)],[c68,clause11]) ).
cnf(c75,plain,
existent(skc6,skc10),
inference(resolution,[status(thm)],[c71,clause14]) ).
cnf(c13,axiom,
( X196 != X194
| X193 != X195
| ~ existent(X196,X193)
| existent(X194,X195) ),
theory(equality) ).
cnf(c175,plain,
( skc6 != X289
| skc10 != X288
| existent(X289,X288) ),
inference(resolution,[status(thm)],[c13,c75]) ).
cnf(c224,plain,
( skc6 != X290
| existent(X290,skc10) ),
inference(resolution,[status(thm)],[c175,reflexivity]) ).
cnf(c85,plain,
entity(skc6,skc11),
inference(resolution,[status(thm)],[c82,clause11]) ).
cnf(c91,plain,
existent(skc6,skc11),
inference(resolution,[status(thm)],[c85,clause14]) ).
cnf(c174,plain,
( skc6 != X282
| skc11 != X281
| existent(X282,X281) ),
inference(resolution,[status(thm)],[c13,c91]) ).
cnf(c221,plain,
( skc6 != X283
| existent(X283,skc11) ),
inference(resolution,[status(thm)],[c174,reflexivity]) ).
cnf(c50,plain,
entity(skc6,skc8),
inference(resolution,[status(thm)],[clause11,c49]) ).
cnf(c54,plain,
existent(skc6,skc8),
inference(resolution,[status(thm)],[clause14,c50]) ).
cnf(c173,plain,
( skc6 != X279
| skc8 != X278
| existent(X279,X278) ),
inference(resolution,[status(thm)],[c13,c54]) ).
cnf(c219,plain,
( skc6 != X280
| existent(X280,skc8) ),
inference(resolution,[status(thm)],[c173,reflexivity]) ).
cnf(c12,axiom,
( X188 != X186
| X185 != X187
| ~ entity(X188,X185)
| entity(X186,X187) ),
theory(equality) ).
cnf(c169,plain,
( skc6 != X271
| skc10 != X272
| entity(X271,X272) ),
inference(resolution,[status(thm)],[c12,c71]) ).
cnf(c216,plain,
( skc6 != X273
| entity(X273,skc10) ),
inference(resolution,[status(thm)],[c169,reflexivity]) ).
cnf(c168,plain,
( skc6 != X264
| skc8 != X265
| entity(X264,X265) ),
inference(resolution,[status(thm)],[c12,c50]) ).
cnf(c213,plain,
( skc6 != X270
| entity(X270,skc8) ),
inference(resolution,[status(thm)],[c168,reflexivity]) ).
cnf(c167,plain,
( skc6 != X261
| skc11 != X262
| entity(X261,X262) ),
inference(resolution,[status(thm)],[c12,c85]) ).
cnf(c211,plain,
( skc6 != X263
| entity(X263,skc11) ),
inference(resolution,[status(thm)],[c167,reflexivity]) ).
cnf(c11,axiom,
( X179 != X177
| X176 != X178
| ~ object(X179,X176)
| object(X177,X178) ),
theory(equality) ).
cnf(c163,plain,
( skc6 != X254
| skc11 != X255
| object(X254,X255) ),
inference(resolution,[status(thm)],[c11,c82]) ).
cnf(c208,plain,
( skc6 != X256
| object(X256,skc11) ),
inference(resolution,[status(thm)],[c163,reflexivity]) ).
cnf(c162,plain,
( skc6 != X251
| skc8 != X252
| object(X251,X252) ),
inference(resolution,[status(thm)],[c11,c49]) ).
cnf(c206,plain,
( skc6 != X253
| object(X253,skc8) ),
inference(resolution,[status(thm)],[c162,reflexivity]) ).
cnf(c161,plain,
( skc6 != X244
| skc10 != X245
| object(X244,X245) ),
inference(resolution,[status(thm)],[c11,c68]) ).
cnf(c203,plain,
( skc6 != X246
| object(X246,skc10) ),
inference(resolution,[status(thm)],[c161,reflexivity]) ).
cnf(c10,axiom,
( X169 != X167
| X166 != X168
| ~ artifact(X169,X166)
| artifact(X167,X168) ),
theory(equality) ).
cnf(c156,plain,
( skc6 != X237
| skc11 != X238
| artifact(X237,X238) ),
inference(resolution,[status(thm)],[c10,c81]) ).
cnf(c200,plain,
( skc6 != X243
| artifact(X243,skc11) ),
inference(resolution,[status(thm)],[c156,reflexivity]) ).
cnf(c155,plain,
( skc6 != X234
| skc8 != X235
| artifact(X234,X235) ),
inference(resolution,[status(thm)],[c10,c48]) ).
cnf(c198,plain,
( skc6 != X236
| artifact(X236,skc8) ),
inference(resolution,[status(thm)],[c155,reflexivity]) ).
cnf(c9,axiom,
( X161 != X159
| X158 != X160
| ~ way(X161,X158)
| way(X159,X160) ),
theory(equality) ).
cnf(c151,plain,
( skc6 != X227
| skc8 != X228
| way(X227,X228) ),
inference(resolution,[status(thm)],[c9,c47]) ).
cnf(c195,plain,
( skc6 != X229
| way(X229,skc8) ),
inference(resolution,[status(thm)],[c151,reflexivity]) ).
cnf(c8,axiom,
( X152 != X150
| X149 != X151
| ~ street(X152,X149)
| street(X150,X151) ),
theory(equality) ).
cnf(c147,plain,
( skc6 != X224
| skc8 != X225
| street(X224,X225) ),
inference(resolution,[status(thm)],[c8,clause40]) ).
cnf(c193,plain,
( skc6 != X226
| street(X226,skc8) ),
inference(resolution,[status(thm)],[c147,reflexivity]) ).
cnf(clause17,axiom,
( ~ object(X35,X36)
| unisex(X35,X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c84,plain,
unisex(skc6,skc11),
inference(resolution,[status(thm)],[c82,clause17]) ).
cnf(c7,axiom,
( X142 != X140
| X139 != X141
| ~ unisex(X142,X139)
| unisex(X140,X141) ),
theory(equality) ).
cnf(c142,plain,
( skc6 != X218
| skc11 != X217
| unisex(X218,X217) ),
inference(resolution,[status(thm)],[c7,c84]) ).
cnf(c190,plain,
( skc6 != X219
| unisex(X219,skc11) ),
inference(resolution,[status(thm)],[c142,reflexivity]) ).
cnf(clause24,axiom,
( ~ abstraction(X49,X50)
| unisex(X49,X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c65,plain,
unisex(skc6,skc9),
inference(resolution,[status(thm)],[clause24,c60]) ).
cnf(c141,plain,
( skc6 != X211
| skc9 != X210
| unisex(X211,X210) ),
inference(resolution,[status(thm)],[c7,c65]) ).
cnf(c185,plain,
( skc6 != X216
| unisex(X216,skc9) ),
inference(resolution,[status(thm)],[c141,reflexivity]) ).
cnf(c70,plain,
unisex(skc6,skc10),
inference(resolution,[status(thm)],[c68,clause17]) ).
cnf(c140,plain,
( skc6 != X208
| skc10 != X207
| unisex(X208,X207) ),
inference(resolution,[status(thm)],[c7,c70]) ).
cnf(c183,plain,
( skc6 != X209
| unisex(X209,skc10) ),
inference(resolution,[status(thm)],[c140,reflexivity]) ).
cnf(clause43,negated_conjecture,
event(skc6,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(clause2,axiom,
( ~ event(X5,X6)
| eventuality(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c40,plain,
eventuality(skc6,skc7),
inference(resolution,[status(thm)],[clause2,clause43]) ).
cnf(clause7,axiom,
( ~ eventuality(X15,X16)
| unisex(X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c46,plain,
unisex(skc6,skc7),
inference(resolution,[status(thm)],[clause7,c40]) ).
cnf(c139,plain,
( skc6 != X201
| skc7 != X200
| unisex(X201,X200) ),
inference(resolution,[status(thm)],[c7,c46]) ).
cnf(c178,plain,
( skc6 != X202
| unisex(X202,skc7) ),
inference(resolution,[status(thm)],[c139,reflexivity]) ).
cnf(c57,plain,
unisex(skc6,skc8),
inference(resolution,[status(thm)],[clause17,c49]) ).
cnf(c138,plain,
( skc6 != X198
| skc8 != X197
| unisex(X198,X197) ),
inference(resolution,[status(thm)],[c7,c57]) ).
cnf(c176,plain,
( skc6 != X199
| unisex(X199,skc8) ),
inference(resolution,[status(thm)],[c138,reflexivity]) ).
cnf(clause6,axiom,
( ~ eventuality(X13,X14)
| nonexistent(X13,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c45,plain,
nonexistent(skc6,skc7),
inference(resolution,[status(thm)],[clause6,c40]) ).
cnf(c6,axiom,
( X134 != X132
| X131 != X133
| ~ nonexistent(X134,X131)
| nonexistent(X132,X133) ),
theory(equality) ).
cnf(c134,plain,
( skc6 != X191
| skc7 != X190
| nonexistent(X191,X190) ),
inference(resolution,[status(thm)],[c6,c45]) ).
cnf(c171,plain,
( skc6 != X192
| nonexistent(X192,skc7) ),
inference(resolution,[status(thm)],[c134,reflexivity]) ).
cnf(clause13,axiom,
( ~ entity(X27,X28)
| specific(X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c90,plain,
specific(skc6,skc11),
inference(resolution,[status(thm)],[c85,clause13]) ).
cnf(c5,axiom,
( X125 != X123
| X122 != X124
| ~ specific(X125,X122)
| specific(X123,X124) ),
theory(equality) ).
cnf(c130,plain,
( skc6 != X184
| skc11 != X183
| specific(X184,X183) ),
inference(resolution,[status(thm)],[c5,c90]) ).
cnf(c166,plain,
( skc6 != X189
| specific(X189,skc11) ),
inference(resolution,[status(thm)],[c130,reflexivity]) ).
cnf(c74,plain,
specific(skc6,skc10),
inference(resolution,[status(thm)],[c71,clause13]) ).
cnf(c129,plain,
( skc6 != X181
| skc10 != X180
| specific(X181,X180) ),
inference(resolution,[status(thm)],[c5,c74]) ).
cnf(c164,plain,
( skc6 != X182
| specific(X182,skc10) ),
inference(resolution,[status(thm)],[c129,reflexivity]) ).
cnf(clause5,axiom,
( ~ eventuality(X11,X12)
| specific(X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c44,plain,
specific(skc6,skc7),
inference(resolution,[status(thm)],[clause5,c40]) ).
cnf(c128,plain,
( skc6 != X174
| skc7 != X173
| specific(X174,X173) ),
inference(resolution,[status(thm)],[c5,c44]) ).
cnf(c159,plain,
( skc6 != X175
| specific(X175,skc7) ),
inference(resolution,[status(thm)],[c128,reflexivity]) ).
cnf(c53,plain,
specific(skc6,skc8),
inference(resolution,[status(thm)],[clause13,c50]) ).
cnf(c127,plain,
( skc6 != X171
| skc8 != X170
| specific(X171,X170) ),
inference(resolution,[status(thm)],[c5,c53]) ).
cnf(c157,plain,
( skc6 != X172
| specific(X172,skc8) ),
inference(resolution,[status(thm)],[c127,reflexivity]) ).
cnf(clause4,axiom,
( ~ thing(X9,X10)
| singleton(X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause12,axiom,
( ~ entity(X25,X26)
| thing(X25,X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c51,plain,
thing(skc6,skc8),
inference(resolution,[status(thm)],[c50,clause12]) ).
cnf(c52,plain,
singleton(skc6,skc8),
inference(resolution,[status(thm)],[c51,clause4]) ).
cnf(c4,axiom,
( X115 != X113
| X112 != X114
| ~ singleton(X115,X112)
| singleton(X113,X114) ),
theory(equality) ).
cnf(c122,plain,
( skc6 != X164
| skc8 != X163
| singleton(X164,X163) ),
inference(resolution,[status(thm)],[c4,c52]) ).
cnf(c153,plain,
( skc6 != X165
| singleton(X165,skc8) ),
inference(resolution,[status(thm)],[c122,reflexivity]) ).
cnf(c76,plain,
thing(skc6,skc10),
inference(resolution,[status(thm)],[c71,clause12]) ).
cnf(c78,plain,
singleton(skc6,skc10),
inference(resolution,[status(thm)],[c76,clause4]) ).
cnf(c121,plain,
( skc6 != X157
| skc10 != X156
| singleton(X157,X156) ),
inference(resolution,[status(thm)],[c4,c78]) ).
cnf(c150,plain,
( skc6 != X162
| singleton(X162,skc10) ),
inference(resolution,[status(thm)],[c121,reflexivity]) ).
cnf(clause21,axiom,
( ~ abstraction(X43,X44)
| thing(X43,X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c61,plain,
thing(skc6,skc9),
inference(resolution,[status(thm)],[clause21,c60]) ).
cnf(c62,plain,
singleton(skc6,skc9),
inference(resolution,[status(thm)],[c61,clause4]) ).
cnf(c120,plain,
( skc6 != X154
| skc9 != X153
| singleton(X154,X153) ),
inference(resolution,[status(thm)],[c4,c62]) ).
cnf(c148,plain,
( skc6 != X155
| singleton(X155,skc9) ),
inference(resolution,[status(thm)],[c120,reflexivity]) ).
cnf(c92,plain,
thing(skc6,skc11),
inference(resolution,[status(thm)],[c85,clause12]) ).
cnf(c97,plain,
singleton(skc6,skc11),
inference(resolution,[status(thm)],[c92,clause4]) ).
cnf(c119,plain,
( skc6 != X147
| skc11 != X146
| singleton(X147,X146) ),
inference(resolution,[status(thm)],[c4,c97]) ).
cnf(c145,plain,
( skc6 != X148
| singleton(X148,skc11) ),
inference(resolution,[status(thm)],[c119,reflexivity]) ).
cnf(clause3,axiom,
( ~ eventuality(X7,X8)
| thing(X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c42,plain,
thing(skc6,skc7),
inference(resolution,[status(thm)],[clause3,c40]) ).
cnf(c43,plain,
singleton(skc6,skc7),
inference(resolution,[status(thm)],[clause4,c42]) ).
cnf(c118,plain,
( skc6 != X144
| skc7 != X143
| singleton(X144,X143) ),
inference(resolution,[status(thm)],[c4,c43]) ).
cnf(c143,plain,
( skc6 != X145
| singleton(X145,skc7) ),
inference(resolution,[status(thm)],[c118,reflexivity]) ).
cnf(c3,axiom,
( X111 != X109
| X108 != X110
| ~ thing(X111,X108)
| thing(X109,X110) ),
theory(equality) ).
cnf(c117,plain,
( skc6 != X137
| skc9 != X136
| thing(X137,X136) ),
inference(resolution,[status(thm)],[c3,c61]) ).
cnf(c136,plain,
( skc6 != X138
| thing(X138,skc9) ),
inference(resolution,[status(thm)],[c117,reflexivity]) ).
cnf(c116,plain,
( skc6 != X130
| skc11 != X129
| thing(X130,X129) ),
inference(resolution,[status(thm)],[c3,c92]) ).
cnf(c133,plain,
( skc6 != X135
| thing(X135,skc11) ),
inference(resolution,[status(thm)],[c116,reflexivity]) ).
cnf(c115,plain,
( skc6 != X127
| skc7 != X126
| thing(X127,X126) ),
inference(resolution,[status(thm)],[c3,c42]) ).
cnf(c131,plain,
( skc6 != X128
| thing(X128,skc7) ),
inference(resolution,[status(thm)],[c115,reflexivity]) ).
cnf(c114,plain,
( skc6 != X120
| skc8 != X119
| thing(X120,X119) ),
inference(resolution,[status(thm)],[c3,c51]) ).
cnf(c125,plain,
( skc6 != X121
| thing(X121,skc8) ),
inference(resolution,[status(thm)],[c114,reflexivity]) ).
cnf(c113,plain,
( skc6 != X117
| skc10 != X116
| thing(X117,X116) ),
inference(resolution,[status(thm)],[c3,c76]) ).
cnf(c123,plain,
( skc6 != X118
| thing(X118,skc10) ),
inference(resolution,[status(thm)],[c113,reflexivity]) ).
cnf(c2,axiom,
( X104 != X102
| X101 != X103
| ~ eventuality(X104,X101)
| eventuality(X102,X103) ),
theory(equality) ).
cnf(c110,plain,
( skc6 != X106
| skc7 != X105
| eventuality(X106,X105) ),
inference(resolution,[status(thm)],[c2,c40]) ).
cnf(c111,plain,
( skc6 != X107
| eventuality(X107,skc7) ),
inference(resolution,[status(thm)],[c110,reflexivity]) ).
cnf(c1,axiom,
( X94 != X92
| X91 != X93
| ~ event(X94,X91)
| event(X92,X93) ),
theory(equality) ).
cnf(c105,plain,
( skc6 != X99
| skc7 != X98
| event(X99,X98) ),
inference(resolution,[status(thm)],[c1,clause43]) ).
cnf(c108,plain,
( skc6 != X100
| event(X100,skc7) ),
inference(resolution,[status(thm)],[c105,reflexivity]) ).
cnf(clause45,negated_conjecture,
barrel(skc6,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(c0,axiom,
( X90 != X88
| X87 != X89
| ~ barrel(X90,X87)
| barrel(X88,X89) ),
theory(equality) ).
cnf(c104,plain,
( skc6 != X96
| skc7 != X95
| barrel(X96,X95) ),
inference(resolution,[status(thm)],[c0,clause45]) ).
cnf(c106,plain,
( skc6 != X97
| barrel(X97,skc7) ),
inference(resolution,[status(thm)],[c104,reflexivity]) ).
cnf(c31,axiom,
( X85 != X84
| ~ actual_world(X85)
| actual_world(X84) ),
theory(equality) ).
cnf(transitivity,axiom,
( X80 != X78
| X78 != X79
| X80 = X79 ),
theory(equality) ).
cnf(symmetry,axiom,
( X76 != X75
| X75 = X76 ),
theory(equality) ).
cnf(clause34,axiom,
( ~ nonexistent(X69,X70)
| ~ existent(X69,X70) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c96,plain,
~ nonexistent(skc6,skc11),
inference(resolution,[status(thm)],[c91,clause34]) ).
cnf(clause33,axiom,
( ~ general(X67,X68)
| ~ specific(X67,X68) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c95,plain,
~ general(skc6,skc11),
inference(resolution,[status(thm)],[c90,clause33]) ).
cnf(c94,plain,
~ nonexistent(skc6,skc10),
inference(resolution,[status(thm)],[clause34,c75]) ).
cnf(c93,plain,
~ nonexistent(skc6,skc8),
inference(resolution,[status(thm)],[clause34,c54]) ).
cnf(c89,plain,
~ general(skc6,skc10),
inference(resolution,[status(thm)],[clause33,c74]) ).
cnf(c88,plain,
~ general(skc6,skc7),
inference(resolution,[status(thm)],[clause33,c44]) ).
cnf(c87,plain,
~ general(skc6,skc8),
inference(resolution,[status(thm)],[clause33,c53]) ).
cnf(clause25,axiom,
( ~ hollywood_placename(X51,X52)
| placename(X51,X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause1,axiom,
( ~ barrel(X3,X4)
| event(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause36,negated_conjecture,
actual_world(skc6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP127-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:26:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.61/0.78 % Version: 1.5
% 0.61/0.78 % SZS status Satisfiable
% 0.61/0.78 % SZS output start Saturation
% See solution above
% 0.61/0.78
% 0.61/0.78 % Initial clauses : 95
% 0.61/0.79 % Processed clauses : 286
% 0.61/0.79 % Factors computed : 2
% 0.61/0.79 % Resolvents computed: 262
% 0.61/0.79 % Tautologies deleted: 3
% 0.61/0.79 % Forward subsumed : 70
% 0.61/0.79 % Backward subsumed : 0
% 0.61/0.79 % -------- CPU Time ---------
% 0.61/0.79 % User time : 0.423 s
% 0.61/0.79 % System time : 0.017 s
% 0.61/0.79 % Total time : 0.440 s
%------------------------------------------------------------------------------