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