%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP158-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:28 EDT 2024
% Result : Satisfiable 0.97s 1.14s
% Output : Saturation 0.97s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause86,negated_conjecture,
( ssSkP0(X203,X202)
| member(X202,skf8(X202,X203),X203) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
cnf(clause84,negated_conjecture,
down(skc5,skc6,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
cnf(clause83,negated_conjecture,
in(skc5,skc6,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
cnf(clause81,negated_conjecture,
of(skc5,skc9,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
cnf(clause82,negated_conjecture,
agent(skc5,skc6,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
cnf(clause88,negated_conjecture,
( ~ city(X269,X271)
| ~ street(X269,X271)
| ~ lonely(X269,X271)
| ~ down(X269,X272,X271)
| ~ in(X269,X272,X271)
| ~ placename(X269,X270)
| ~ hollywood_placename(X269,X270)
| ~ of(X269,X270,X271)
| ~ event(X269,X272)
| ~ present(X269,X272)
| ~ barrel(X269,X272)
| ~ agent(X269,X272,X267)
| ~ old(X269,X267)
| ~ dirty(X269,X267)
| ~ white(X269,X267)
| ~ chevy(X269,X267)
| ~ group(X269,X268)
| ~ two(X269,X268)
| ~ ssSkP0(X268,X269)
| ~ actual_world(X269)
| member(X269,skf5(X269,X268),X268) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
cnf(c168,plain,
( ~ city(skc5,X848)
| ~ street(skc5,X848)
| ~ lonely(skc5,X848)
| ~ down(skc5,skc6,X848)
| ~ in(skc5,skc6,X848)
| ~ placename(skc5,X849)
| ~ hollywood_placename(skc5,X849)
| ~ of(skc5,X849,X848)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X850)
| ~ two(skc5,X850)
| ~ ssSkP0(X850,skc5)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X850),X850) ),
inference(resolution,[status(thm)],[clause88,clause82]) ).
cnf(c386,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ down(skc5,skc6,skc8)
| ~ in(skc5,skc6,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1158)
| ~ two(skc5,X1158)
| ~ ssSkP0(X1158,skc5)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1158),X1158) ),
inference(resolution,[status(thm)],[c168,clause81]) ).
cnf(c467,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ down(skc5,skc6,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1311)
| ~ two(skc5,X1311)
| ~ ssSkP0(X1311,skc5)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1311),X1311) ),
inference(resolution,[status(thm)],[c386,clause83]) ).
cnf(c503,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1321)
| ~ two(skc5,X1321)
| ~ ssSkP0(X1321,skc5)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1321),X1321) ),
inference(resolution,[status(thm)],[c467,clause84]) ).
cnf(c518,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1350)
| ~ two(skc5,X1350)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1350),X1350)
| member(skc5,skf8(skc5,X1350),X1350) ),
inference(resolution,[status(thm)],[c503,clause86]) ).
cnf(clause49,axiom,
( ~ seat(X100,X99)
| furniture(X100,X99) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(clause48,axiom,
( ~ frontseat(X98,X97)
| seat(X98,X97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(clause85,negated_conjecture,
( ssSkP0(X132,X131)
| frontseat(X131,skf8(X131,X133)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
cnf(c126,plain,
( ssSkP0(X134,X136)
| seat(X136,skf8(X136,X135)) ),
inference(resolution,[status(thm)],[clause85,clause48]) ).
cnf(c127,plain,
( ssSkP0(X141,X139)
| furniture(X139,skf8(X139,X140)) ),
inference(resolution,[status(thm)],[c126,clause49]) ).
cnf(c519,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1349)
| ~ two(skc5,X1349)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1349),X1349)
| furniture(skc5,skf8(skc5,X1348)) ),
inference(resolution,[status(thm)],[c503,c127]) ).
cnf(clause30,axiom,
( ~ instrumentality(X62,X61)
| artifact(X62,X61) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause50,axiom,
( ~ furniture(X102,X101)
| instrumentality(X102,X101) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c128,plain,
( ssSkP0(X144,X142)
| instrumentality(X142,skf8(X142,X143)) ),
inference(resolution,[status(thm)],[c127,clause50]) ).
cnf(c129,plain,
( ssSkP0(X147,X146)
| artifact(X146,skf8(X146,X145)) ),
inference(resolution,[status(thm)],[c128,clause30]) ).
cnf(c517,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1346)
| ~ two(skc5,X1346)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1346),X1346)
| artifact(skc5,skf8(skc5,X1347)) ),
inference(resolution,[status(thm)],[c503,c129]) ).
cnf(clause7,axiom,
( ~ thing(X16,X15)
| singleton(X16,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause6,axiom,
( ~ entity(X14,X13)
| thing(X14,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(clause32,axiom,
( ~ object(X66,X65)
| entity(X66,X65) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(clause31,axiom,
( ~ artifact(X64,X63)
| object(X64,X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c130,plain,
( ssSkP0(X148,X149)
| object(X149,skf8(X149,X150)) ),
inference(resolution,[status(thm)],[c129,clause31]) ).
cnf(c134,plain,
( ssSkP0(X163,X162)
| entity(X162,skf8(X162,X164)) ),
inference(resolution,[status(thm)],[c130,clause32]) ).
cnf(c137,plain,
( ssSkP0(X174,X175)
| thing(X175,skf8(X175,X176)) ),
inference(resolution,[status(thm)],[c134,clause6]) ).
cnf(c140,plain,
( ssSkP0(X185,X184)
| singleton(X184,skf8(X184,X183)) ),
inference(resolution,[status(thm)],[c137,clause7]) ).
cnf(c516,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1344)
| ~ two(skc5,X1344)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1344),X1344)
| singleton(skc5,skf8(skc5,X1345)) ),
inference(resolution,[status(thm)],[c503,c140]) ).
cnf(c515,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1342)
| ~ two(skc5,X1342)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1342),X1342)
| frontseat(skc5,skf8(skc5,X1343)) ),
inference(resolution,[status(thm)],[c503,clause85]) ).
cnf(c514,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1341)
| ~ two(skc5,X1341)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1341),X1341)
| instrumentality(skc5,skf8(skc5,X1340)) ),
inference(resolution,[status(thm)],[c503,c128]) ).
cnf(clause35,axiom,
( ~ object(X72,X71)
| unisex(X72,X71) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c133,plain,
( ssSkP0(X159,X161)
| unisex(X161,skf8(X161,X160)) ),
inference(resolution,[status(thm)],[c130,clause35]) ).
cnf(c513,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1338)
| ~ two(skc5,X1338)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1338),X1338)
| unisex(skc5,skf8(skc5,X1339)) ),
inference(resolution,[status(thm)],[c503,c133]) ).
cnf(clause9,axiom,
( ~ entity(X20,X19)
| existent(X20,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c138,plain,
( ssSkP0(X177,X179)
| existent(X179,skf8(X179,X178)) ),
inference(resolution,[status(thm)],[c134,clause9]) ).
cnf(c512,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1337)
| ~ two(skc5,X1337)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1337),X1337)
| existent(skc5,skf8(skc5,X1336)) ),
inference(resolution,[status(thm)],[c503,c138]) ).
cnf(c511,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1334)
| ~ two(skc5,X1334)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1334),X1334)
| object(skc5,skf8(skc5,X1335)) ),
inference(resolution,[status(thm)],[c503,c130]) ).
cnf(clause33,axiom,
( ~ object(X68,X67)
| nonliving(X68,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c132,plain,
( ssSkP0(X156,X158)
| nonliving(X158,skf8(X158,X157)) ),
inference(resolution,[status(thm)],[c130,clause33]) ).
cnf(c510,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1333)
| ~ two(skc5,X1333)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1333),X1333)
| nonliving(skc5,skf8(skc5,X1332)) ),
inference(resolution,[status(thm)],[c503,c132]) ).
cnf(c509,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1331)
| ~ two(skc5,X1331)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1331),X1331)
| thing(skc5,skf8(skc5,X1330)) ),
inference(resolution,[status(thm)],[c503,c137]) ).
cnf(c508,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1329)
| ~ two(skc5,X1329)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1329),X1329)
| seat(skc5,skf8(skc5,X1328)) ),
inference(resolution,[status(thm)],[c503,c126]) ).
cnf(c507,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1326)
| ~ two(skc5,X1326)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1326),X1326)
| entity(skc5,skf8(skc5,X1327)) ),
inference(resolution,[status(thm)],[c503,c134]) ).
cnf(clause34,axiom,
( ~ object(X70,X69)
| impartial(X70,X69) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c131,plain,
( ssSkP0(X151,X153)
| impartial(X153,skf8(X153,X152)) ),
inference(resolution,[status(thm)],[c130,clause34]) ).
cnf(c506,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1325)
| ~ two(skc5,X1325)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1325),X1325)
| impartial(skc5,skf8(skc5,X1324)) ),
inference(resolution,[status(thm)],[c503,c131]) ).
cnf(clause8,axiom,
( ~ entity(X18,X17)
| specific(X18,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c139,plain,
( ssSkP0(X180,X182)
| specific(X182,skf8(X182,X181)) ),
inference(resolution,[status(thm)],[c134,clause8]) ).
cnf(c505,plain,
( ~ city(skc5,skc8)
| ~ street(skc5,skc8)
| ~ lonely(skc5,skc8)
| ~ placename(skc5,skc9)
| ~ hollywood_placename(skc5,skc9)
| ~ event(skc5,skc6)
| ~ present(skc5,skc6)
| ~ barrel(skc5,skc6)
| ~ old(skc5,skc7)
| ~ dirty(skc5,skc7)
| ~ white(skc5,skc7)
| ~ chevy(skc5,skc7)
| ~ group(skc5,X1322)
| ~ two(skc5,X1322)
| ~ actual_world(skc5)
| member(skc5,skf5(skc5,X1322),X1322)
| specific(skc5,skf8(skc5,X1323)) ),
inference(resolution,[status(thm)],[c503,c139]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X313 != X316
| X315 != X311
| X314 != X312
| X317 != X318
| skf13(X313,X315,X314,X317) = skf13(X316,X311,X312,X318) ),
theory(equality) ).
cnf(c193,plain,
( X946 != X943
| X949 != X944
| X948 != X945
| skf13(X946,X949,X948,X947) = skf13(X943,X944,X945,X947) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c413,plain,
( X1293 != X1289
| X1290 != X1288
| skf13(X1293,X1290,X1291,X1292) = skf13(X1289,X1288,X1291,X1292) ),
inference(resolution,[status(thm)],[c193,reflexivity]) ).
cnf(c500,plain,
( X1312 != X1316
| skf13(X1312,X1314,X1313,X1315) = skf13(X1316,X1314,X1313,X1315) ),
inference(resolution,[status(thm)],[c413,reflexivity]) ).
cnf(c499,plain,
( X1306 != X1304
| skf13(X1306,X1306,X1305,X1307) = skf13(X1304,X1304,X1305,X1307) ),
inference(factor,[status(thm)],[c413]) ).
cnf(c412,plain,
( X1286 != X1283
| X1287 != X1284
| skf13(X1286,X1287,X1287,X1285) = skf13(X1283,X1284,X1284,X1285) ),
inference(factor,[status(thm)],[c193]) ).
cnf(c411,plain,
( X1270 != X1267
| X1268 != X1266
| skf13(X1270,X1268,X1270,X1269) = skf13(X1267,X1266,X1267,X1269) ),
inference(factor,[status(thm)],[c193]) ).
cnf(c494,plain,
( X1279 != X1277
| skf13(X1279,X1276,X1279,X1278) = skf13(X1277,X1276,X1277,X1278) ),
inference(resolution,[status(thm)],[c411,reflexivity]) ).
cnf(c493,plain,
( X1271 != X1273
| skf13(X1271,X1271,X1271,X1272) = skf13(X1273,X1273,X1273,X1272) ),
inference(factor,[status(thm)],[c411]) ).
cnf(c191,plain,
( X901 != X898
| X903 != X899
| X902 != X900
| skf13(X901,X903,X902,X903) = skf13(X898,X899,X900,X899) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c400,plain,
( X1224 != X1225
| X1226 != X1228
| skf13(X1224,X1226,X1227,X1226) = skf13(X1225,X1228,X1227,X1228) ),
inference(resolution,[status(thm)],[c191,reflexivity]) ).
cnf(c399,plain,
( X1208 != X1211
| X1210 != X1209
| skf13(X1208,X1210,X1210,X1210) = skf13(X1211,X1209,X1209,X1209) ),
inference(factor,[status(thm)],[c191]) ).
cnf(c398,plain,
( X1206 != X1205
| X1204 != X1207
| skf13(X1206,X1204,X1206,X1204) = skf13(X1205,X1207,X1205,X1207) ),
inference(factor,[status(thm)],[c191]) ).
cnf(c190,plain,
( X876 != X873
| X877 != X872
| X875 != X874
| skf13(X876,X877,X875,X876) = skf13(X873,X872,X874,X873) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c393,plain,
( X1191 != X1190
| X1189 != X1187
| skf13(X1191,X1189,X1188,X1191) = skf13(X1190,X1187,X1188,X1190) ),
inference(resolution,[status(thm)],[c190,reflexivity]) ).
cnf(c477,plain,
( X1198 != X1199
| skf13(X1198,X1200,X1197,X1198) = skf13(X1199,X1200,X1197,X1199) ),
inference(resolution,[status(thm)],[c393,reflexivity]) ).
cnf(c476,plain,
( X1194 != X1193
| skf13(X1194,X1194,X1192,X1194) = skf13(X1193,X1193,X1192,X1193) ),
inference(factor,[status(thm)],[c393]) ).
cnf(c391,plain,
( X1167 != X1166
| X1164 != X1165
| skf13(X1167,X1164,X1167,X1167) = skf13(X1166,X1165,X1166,X1166) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c470,plain,
( X1175 != X1176
| skf13(X1175,X1177,X1175,X1175) = skf13(X1176,X1177,X1176,X1176) ),
inference(resolution,[status(thm)],[c391,reflexivity]) ).
cnf(c392,plain,
( X1174 != X1172
| X1173 != X1171
| skf13(X1174,X1173,X1173,X1174) = skf13(X1172,X1171,X1171,X1172) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c469,plain,
( X1168 != X1169
| skf13(X1168,X1168,X1168,X1168) = skf13(X1169,X1169,X1169,X1169) ),
inference(factor,[status(thm)],[c391]) ).
cnf(c5,axiom,
( X362 != X365
| X364 != X360
| X363 != X361
| ~ member(X362,X364,X363)
| member(X365,X360,X361) ),
theory(equality) ).
cnf(c209,plain,
( X968 != X970
| skf8(X968,X969) != X972
| X969 != X971
| member(X970,X972,X971)
| ssSkP0(X969,X968) ),
inference(resolution,[status(thm)],[c5,clause86]) ).
cnf(c417,plain,
( X1153 != X1154
| X1151 != X1152
| member(X1154,skf8(X1153,X1151),X1152)
| ssSkP0(X1151,X1153) ),
inference(resolution,[status(thm)],[c209,reflexivity]) ).
cnf(c465,plain,
( X1160 != X1159
| member(X1159,skf8(X1160,X1161),X1161)
| ssSkP0(X1161,X1160) ),
inference(resolution,[status(thm)],[c417,reflexivity]) ).
cnf(c464,plain,
( X1156 != X1155
| member(X1155,skf8(X1156,X1156),X1155)
| ssSkP0(X1156,X1156) ),
inference(factor,[status(thm)],[c417]) ).
cnf(c63,axiom,
( X739 != X742
| X741 != X737
| X740 != X738
| ~ down(X739,X741,X740)
| down(X742,X737,X738) ),
theory(equality) ).
cnf(c367,plain,
( skc5 != X1145
| skc6 != X1144
| skc8 != X1143
| down(X1145,X1144,X1143) ),
inference(resolution,[status(thm)],[c63,clause84]) ).
cnf(c461,plain,
( skc5 != X1146
| skc6 != X1147
| down(X1146,X1147,skc8) ),
inference(resolution,[status(thm)],[c367,reflexivity]) ).
cnf(c462,plain,
( skc5 != X1150
| down(X1150,skc6,skc8) ),
inference(resolution,[status(thm)],[c461,reflexivity]) ).
cnf(c62,axiom,
( X714 != X717
| X716 != X712
| X715 != X713
| ~ in(X714,X716,X715)
| in(X717,X712,X713) ),
theory(equality) ).
cnf(c363,plain,
( skc5 != X1137
| skc6 != X1139
| skc8 != X1138
| in(X1137,X1139,X1138) ),
inference(resolution,[status(thm)],[c62,clause83]) ).
cnf(c458,plain,
( skc5 != X1141
| skc6 != X1140
| in(X1141,X1140,skc8) ),
inference(resolution,[status(thm)],[c363,reflexivity]) ).
cnf(c459,plain,
( skc5 != X1142
| in(X1142,skc6,skc8) ),
inference(resolution,[status(thm)],[c458,reflexivity]) ).
cnf(c61,axiom,
( X688 != X691
| X690 != X686
| X689 != X687
| ~ agent(X688,X690,X689)
| agent(X691,X686,X687) ),
theory(equality) ).
cnf(c359,plain,
( skc5 != X1127
| skc6 != X1126
| skc7 != X1128
| agent(X1127,X1126,X1128) ),
inference(resolution,[status(thm)],[c61,clause82]) ).
cnf(c454,plain,
( skc5 != X1135
| skc6 != X1134
| agent(X1135,X1134,skc7) ),
inference(resolution,[status(thm)],[c359,reflexivity]) ).
cnf(c456,plain,
( skc5 != X1136
| agent(X1136,skc6,skc7) ),
inference(resolution,[status(thm)],[c454,reflexivity]) ).
cnf(c64,axiom,
( X684 != X682
| X685 != X683
| ~ ssSkP0(X684,X685)
| ssSkP0(X682,X683) ),
theory(equality) ).
cnf(c357,plain,
( X1113 != X1110
| X1111 != X1112
| ssSkP0(X1110,X1112)
| member(X1111,skf8(X1111,X1113),X1113) ),
inference(resolution,[status(thm)],[c64,clause86]) ).
cnf(c451,plain,
( X1131 != X1130
| ssSkP0(X1130,X1129)
| member(X1129,skf8(X1129,X1131),X1131) ),
inference(resolution,[status(thm)],[c357,reflexivity]) ).
cnf(c450,plain,
( X1123 != X1124
| ssSkP0(X1124,X1124)
| member(X1123,skf8(X1123,X1123),X1123) ),
inference(factor,[status(thm)],[c357]) ).
cnf(c358,plain,
( X1107 != X1105
| X1108 != X1109
| ssSkP0(X1105,X1109)
| furniture(X1108,skf8(X1108,X1106)) ),
inference(resolution,[status(thm)],[c64,c127]) ).
cnf(c448,plain,
( X1114 != X1116
| ssSkP0(X1116,X1116)
| furniture(X1114,skf8(X1114,X1115)) ),
inference(factor,[status(thm)],[c358]) ).
cnf(c356,plain,
( X1090 != X1087
| X1089 != X1091
| ssSkP0(X1087,X1091)
| artifact(X1089,skf8(X1089,X1088)) ),
inference(resolution,[status(thm)],[c64,c129]) ).
cnf(c445,plain,
( X1097 != X1098
| ssSkP0(X1098,X1098)
| artifact(X1097,skf8(X1097,X1096)) ),
inference(factor,[status(thm)],[c356]) ).
cnf(c355,plain,
( X1069 != X1068
| X1070 != X1072
| ssSkP0(X1068,X1072)
| singleton(X1070,skf8(X1070,X1071)) ),
inference(resolution,[status(thm)],[c64,c140]) ).
cnf(c441,plain,
( X1084 != X1082
| ssSkP0(X1082,X1082)
| singleton(X1084,skf8(X1084,X1083)) ),
inference(factor,[status(thm)],[c355]) ).
cnf(c354,plain,
( X1063 != X1064
| X1065 != X1067
| ssSkP0(X1064,X1067)
| frontseat(X1065,skf8(X1065,X1066)) ),
inference(resolution,[status(thm)],[c64,clause85]) ).
cnf(c439,plain,
( X1073 != X1074
| ssSkP0(X1074,X1074)
| frontseat(X1073,skf8(X1073,X1075)) ),
inference(factor,[status(thm)],[c354]) ).
cnf(c353,plain,
( X1047 != X1045
| X1046 != X1049
| ssSkP0(X1045,X1049)
| instrumentality(X1046,skf8(X1046,X1048)) ),
inference(resolution,[status(thm)],[c64,c128]) ).
cnf(c436,plain,
( X1054 != X1056
| ssSkP0(X1056,X1056)
| instrumentality(X1054,skf8(X1054,X1055)) ),
inference(factor,[status(thm)],[c353]) ).
cnf(c352,plain,
( X1027 != X1026
| X1029 != X1028
| ssSkP0(X1026,X1028)
| unisex(X1029,skf8(X1029,X1030)) ),
inference(resolution,[status(thm)],[c64,c133]) ).
cnf(c432,plain,
( X1040 != X1042
| ssSkP0(X1042,X1042)
| unisex(X1040,skf8(X1040,X1041)) ),
inference(factor,[status(thm)],[c352]) ).
cnf(c351,plain,
( X1024 != X1021
| X1023 != X1025
| ssSkP0(X1021,X1025)
| existent(X1023,skf8(X1023,X1022)) ),
inference(resolution,[status(thm)],[c64,c138]) ).
cnf(c430,plain,
( X1033 != X1032
| ssSkP0(X1032,X1032)
| existent(X1033,skf8(X1033,X1031)) ),
inference(factor,[status(thm)],[c351]) ).
cnf(c350,plain,
( X1010 != X1007
| X1009 != X1011
| ssSkP0(X1007,X1011)
| object(X1009,skf8(X1009,X1008)) ),
inference(resolution,[status(thm)],[c64,c130]) ).
cnf(c427,plain,
( X1013 != X1014
| ssSkP0(X1014,X1014)
| object(X1013,skf8(X1013,X1012)) ),
inference(factor,[status(thm)],[c350]) ).
cnf(c55,axiom,
( X663 != X666
| X665 != X661
| X664 != X662
| ~ of(X663,X665,X664)
| of(X666,X661,X662) ),
theory(equality) ).
cnf(c336,plain,
( skc5 != X993
| skc9 != X992
| skc8 != X994
| of(X993,X992,X994) ),
inference(resolution,[status(thm)],[c55,clause81]) ).
cnf(c423,plain,
( skc5 != X1004
| skc9 != X1005
| of(X1004,X1005,skc8) ),
inference(resolution,[status(thm)],[c336,reflexivity]) ).
cnf(c425,plain,
( skc5 != X1006
| of(X1006,skc9,skc8) ),
inference(resolution,[status(thm)],[c423,reflexivity]) ).
cnf(c349,plain,
( X988 != X987
| X990 != X991
| ssSkP0(X987,X991)
| nonliving(X990,skf8(X990,X989)) ),
inference(resolution,[status(thm)],[c64,c132]) ).
cnf(c421,plain,
( X997 != X995
| ssSkP0(X995,X995)
| nonliving(X997,skf8(X997,X996)) ),
inference(factor,[status(thm)],[c349]) ).
cnf(c348,plain,
( X974 != X973
| X977 != X976
| ssSkP0(X973,X976)
| thing(X977,skf8(X977,X975)) ),
inference(resolution,[status(thm)],[c64,c137]) ).
cnf(c418,plain,
( X978 != X980
| ssSkP0(X980,X980)
| thing(X978,skf8(X978,X979)) ),
inference(factor,[status(thm)],[c348]) ).
cnf(c347,plain,
( X957 != X954
| X956 != X958
| ssSkP0(X954,X958)
| seat(X956,skf8(X956,X955)) ),
inference(resolution,[status(thm)],[c64,c126]) ).
cnf(c414,plain,
( X959 != X961
| ssSkP0(X961,X961)
| seat(X959,skf8(X959,X960)) ),
inference(factor,[status(thm)],[c347]) ).
cnf(c346,plain,
( X934 != X933
| X935 != X937
| ssSkP0(X933,X937)
| entity(X935,skf8(X935,X936)) ),
inference(resolution,[status(thm)],[c64,c134]) ).
cnf(c408,plain,
( X938 != X940
| ssSkP0(X940,X940)
| entity(X938,skf8(X938,X939)) ),
inference(factor,[status(thm)],[c346]) ).
cnf(c192,plain,
( X924 != X921
| X926 != X922
| X925 != X923
| skf13(X924,X926,X925,X925) = skf13(X921,X922,X923,X923) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c345,plain,
( X915 != X913
| X916 != X917
| ssSkP0(X913,X917)
| impartial(X916,skf8(X916,X914)) ),
inference(resolution,[status(thm)],[c64,c131]) ).
cnf(c402,plain,
( X920 != X918
| ssSkP0(X918,X918)
| impartial(X920,skf8(X920,X919)) ),
inference(factor,[status(thm)],[c345]) ).
cnf(c344,plain,
( X896 != X893
| X895 != X897
| ssSkP0(X893,X897)
| specific(X895,skf8(X895,X894)) ),
inference(resolution,[status(thm)],[c64,c139]) ).
cnf(c396,plain,
( X904 != X905
| ssSkP0(X905,X905)
| specific(X904,skf8(X904,X906)) ),
inference(factor,[status(thm)],[c344]) ).
cnf(c51,axiom,
( X627 != X625
| X628 != X626
| ~ furniture(X627,X628)
| furniture(X625,X626) ),
theory(equality) ).
cnf(c327,plain,
( X884 != X885
| skf8(X884,X881) != X883
| furniture(X885,X883)
| ssSkP0(X882,X884) ),
inference(resolution,[status(thm)],[c51,c127]) ).
cnf(c394,plain,
( X889 != X887
| furniture(X887,skf8(X889,X888))
| ssSkP0(X886,X889) ),
inference(resolution,[status(thm)],[c327,reflexivity]) ).
cnf(c50,axiom,
( X623 != X621
| X624 != X622
| ~ seat(X623,X624)
| seat(X621,X622) ),
theory(equality) ).
cnf(c326,plain,
( X866 != X863
| skf8(X866,X864) != X865
| seat(X863,X865)
| ssSkP0(X867,X866) ),
inference(resolution,[status(thm)],[c50,c126]) ).
cnf(c389,plain,
( X869 != X871
| seat(X871,skf8(X869,X870))
| ssSkP0(X868,X869) ),
inference(resolution,[status(thm)],[c326,reflexivity]) ).
cnf(c49,axiom,
( X616 != X614
| X617 != X615
| ~ frontseat(X616,X617)
| frontseat(X614,X615) ),
theory(equality) ).
cnf(c323,plain,
( X852 != X854
| skf8(X852,X853) != X855
| frontseat(X854,X855)
| ssSkP0(X851,X852) ),
inference(resolution,[status(thm)],[c49,clause85]) ).
cnf(c387,plain,
( X858 != X857
| frontseat(X857,skf8(X858,X859))
| ssSkP0(X856,X858) ),
inference(resolution,[status(thm)],[c323,reflexivity]) ).
cnf(c37,axiom,
( X526 != X524
| X527 != X525
| ~ nonliving(X526,X527)
| nonliving(X524,X525) ),
theory(equality) ).
cnf(c281,plain,
( X837 != X840
| skf8(X837,X838) != X839
| nonliving(X840,X839)
| ssSkP0(X836,X837) ),
inference(resolution,[status(thm)],[c37,c132]) ).
cnf(c384,plain,
( X843 != X841
| nonliving(X841,skf8(X843,X842))
| ssSkP0(X844,X843) ),
inference(resolution,[status(thm)],[c281,reflexivity]) ).
cnf(clause67,axiom,
( ~ placename(X246,X245)
| ~ of(X246,X247,X248)
| ~ placename(X246,X247)
| ~ of(X246,X245,X248)
| ~ entity(X246,X248)
| X247 = X245 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
cnf(c156,plain,
( ~ placename(skc5,skc9)
| ~ of(skc5,X832,skc8)
| ~ placename(skc5,X832)
| ~ entity(skc5,skc8)
| X832 = skc9 ),
inference(resolution,[status(thm)],[clause67,clause81]) ).
cnf(c36,axiom,
( X518 != X516
| X519 != X517
| ~ object(X518,X519)
| object(X516,X517) ),
theory(equality) ).
cnf(c276,plain,
( X826 != X824
| skf8(X826,X823) != X825
| object(X824,X825)
| ssSkP0(X827,X826) ),
inference(resolution,[status(thm)],[c36,c130]) ).
cnf(c381,plain,
( X829 != X828
| object(X828,skf8(X829,X830))
| ssSkP0(X831,X829) ),
inference(resolution,[status(thm)],[c276,reflexivity]) ).
cnf(c35,axiom,
( X512 != X510
| X513 != X511
| ~ artifact(X512,X513)
| artifact(X510,X511) ),
theory(equality) ).
cnf(c271,plain,
( X813 != X811
| skf8(X813,X812) != X814
| artifact(X811,X814)
| ssSkP0(X815,X813) ),
inference(resolution,[status(thm)],[c35,c129]) ).
cnf(c379,plain,
( X818 != X817
| artifact(X817,skf8(X818,X819))
| ssSkP0(X816,X818) ),
inference(resolution,[status(thm)],[c271,reflexivity]) ).
cnf(clause65,axiom,
( ~ member(X209,X208,X210)
| ~ member(X209,X211,X210)
| two(X209,X210)
| member(X209,skf13(X208,X211,X210,X209),X210)
| X208 = X211 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
cnf(c148,plain,
( ~ member(X809,X808,X810)
| two(X809,X810)
| member(X809,skf13(X808,skf8(X809,X810),X810,X809),X810)
| X808 = skf8(X809,X810)
| ssSkP0(X810,X809) ),
inference(resolution,[status(thm)],[clause65,clause86]) ).
cnf(c34,axiom,
( X505 != X503
| X506 != X504
| ~ instrumentality(X505,X506)
| instrumentality(X503,X504) ),
theory(equality) ).
cnf(c268,plain,
( X797 != X800
| skf8(X797,X799) != X796
| instrumentality(X800,X796)
| ssSkP0(X798,X797) ),
inference(resolution,[status(thm)],[c34,c128]) ).
cnf(c376,plain,
( X804 != X802
| instrumentality(X802,skf8(X804,X801))
| ssSkP0(X803,X804) ),
inference(resolution,[status(thm)],[c268,reflexivity]) ).
cnf(c27,axiom,
( X447 != X445
| X448 != X446
| ~ unisex(X447,X448)
| unisex(X445,X446) ),
theory(equality) ).
cnf(c239,plain,
( X782 != X784
| skf8(X782,X785) != X783
| unisex(X784,X783)
| ssSkP0(X781,X782) ),
inference(resolution,[status(thm)],[c27,c133]) ).
cnf(c374,plain,
( X791 != X792
| unisex(X792,skf8(X791,X790))
| ssSkP0(X789,X791) ),
inference(resolution,[status(thm)],[c239,reflexivity]) ).
cnf(c15,axiom,
( X383 != X381
| X384 != X382
| ~ impartial(X383,X384)
| impartial(X381,X382) ),
theory(equality) ).
cnf(c221,plain,
( X772 != X773
| skf8(X772,X771) != X769
| impartial(X773,X769)
| ssSkP0(X770,X772) ),
inference(resolution,[status(thm)],[c15,c131]) ).
cnf(c372,plain,
( X776 != X777
| impartial(X777,skf8(X776,X775))
| ssSkP0(X774,X776) ),
inference(resolution,[status(thm)],[c221,reflexivity]) ).
cnf(clause63,axiom,
( ~ member(X172,X171,X173)
| ~ two(X172,X173)
| X171 = skf10(X173,X172)
| X171 = skf12(X173,X172) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
cnf(c144,plain,
( ssSkP0(X764,X765)
| ~ two(X765,X764)
| skf8(X765,X764) = skf10(X764,X765)
| skf8(X765,X764) = skf12(X764,X765) ),
inference(resolution,[status(thm)],[clause86,clause63]) ).
cnf(c14,axiom,
( X374 != X372
| X375 != X373
| ~ existent(X374,X375)
| existent(X372,X373) ),
theory(equality) ).
cnf(c216,plain,
( X756 != X757
| skf8(X756,X755) != X758
| existent(X757,X758)
| ssSkP0(X759,X756) ),
inference(resolution,[status(thm)],[c14,c138]) ).
cnf(c370,plain,
( X760 != X761
| existent(X761,skf8(X760,X763))
| ssSkP0(X762,X760) ),
inference(resolution,[status(thm)],[c216,reflexivity]) ).
cnf(c13,axiom,
( X358 != X356
| X359 != X357
| ~ specific(X358,X359)
| specific(X356,X357) ),
theory(equality) ).
cnf(c206,plain,
( X745 != X746
| skf8(X745,X744) != X743
| specific(X746,X743)
| ssSkP0(X747,X745) ),
inference(resolution,[status(thm)],[c13,c139]) ).
cnf(c368,plain,
( X751 != X748
| specific(X748,skf8(X751,X749))
| ssSkP0(X750,X751) ),
inference(resolution,[status(thm)],[c206,reflexivity]) ).
cnf(c12,axiom,
( X286 != X284
| X287 != X285
| ~ singleton(X286,X287)
| singleton(X284,X285) ),
theory(equality) ).
cnf(c174,plain,
( X728 != X725
| skf8(X728,X729) != X727
| singleton(X725,X727)
| ssSkP0(X726,X728) ),
inference(resolution,[status(thm)],[c12,c140]) ).
cnf(c365,plain,
( X730 != X733
| singleton(X733,skf8(X730,X732))
| ssSkP0(X731,X730) ),
inference(resolution,[status(thm)],[c174,reflexivity]) ).
cnf(c11,axiom,
( X252 != X250
| X253 != X251
| ~ thing(X252,X253)
| thing(X250,X251) ),
theory(equality) ).
cnf(c158,plain,
( X711 != X707
| skf8(X711,X710) != X709
| thing(X707,X709)
| ssSkP0(X708,X711) ),
inference(resolution,[status(thm)],[c11,c137]) ).
cnf(c362,plain,
( X721 != X720
| thing(X720,skf8(X721,X718))
| ssSkP0(X719,X721) ),
inference(resolution,[status(thm)],[c158,reflexivity]) ).
cnf(c10,axiom,
( X238 != X236
| X239 != X237
| ~ entity(X238,X239)
| entity(X236,X237) ),
theory(equality) ).
cnf(c149,plain,
( X697 != X698
| skf8(X697,X699) != X696
| entity(X698,X696)
| ssSkP0(X695,X697) ),
inference(resolution,[status(thm)],[c10,c134]) ).
cnf(c360,plain,
( X700 != X702
| entity(X702,skf8(X700,X703))
| ssSkP0(X701,X700) ),
inference(resolution,[status(thm)],[c149,reflexivity]) ).
cnf(clause78,negated_conjecture,
lonely(skc5,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
cnf(c60,axiom,
( X677 != X675
| X678 != X676
| ~ lonely(X677,X678)
| lonely(X675,X676) ),
theory(equality) ).
cnf(c341,plain,
( skc5 != X679
| skc8 != X680
| lonely(X679,X680) ),
inference(resolution,[status(thm)],[c60,clause78]) ).
cnf(c342,plain,
( skc5 != X681
| lonely(X681,skc8) ),
inference(resolution,[status(thm)],[c341,reflexivity]) ).
cnf(clause76,negated_conjecture,
present(skc5,skc6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
cnf(c59,axiom,
( X670 != X668
| X671 != X669
| ~ present(X670,X671)
| present(X668,X669) ),
theory(equality) ).
cnf(c338,plain,
( skc5 != X672
| skc6 != X673
| present(X672,X673) ),
inference(resolution,[status(thm)],[c59,clause76]) ).
cnf(c339,plain,
( skc5 != X674
| present(X674,skc6) ),
inference(resolution,[status(thm)],[c338,reflexivity]) ).
cnf(clause73,negated_conjecture,
dirty(skc5,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
cnf(c58,axiom,
( X657 != X655
| X658 != X656
| ~ dirty(X657,X658)
| dirty(X655,X656) ),
theory(equality) ).
cnf(c334,plain,
( skc5 != X660
| skc7 != X659
| dirty(X660,X659) ),
inference(resolution,[status(thm)],[c58,clause73]) ).
cnf(c335,plain,
( skc5 != X667
| dirty(X667,skc7) ),
inference(resolution,[status(thm)],[c334,reflexivity]) ).
cnf(clause72,negated_conjecture,
white(skc5,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
cnf(c57,axiom,
( X642 != X640
| X643 != X641
| ~ white(X642,X643)
| white(X640,X641) ),
theory(equality) ).
cnf(c331,plain,
( skc5 != X653
| skc7 != X652
| white(X653,X652) ),
inference(resolution,[status(thm)],[c57,clause72]) ).
cnf(c332,plain,
( skc5 != X654
| white(X654,skc7) ),
inference(resolution,[status(thm)],[c331,reflexivity]) ).
cnf(c54,axiom,
( X646 != X649
| X648 != X644
| X647 != X645
| X650 != X651
| ~ be(X646,X648,X647,X650)
| be(X649,X644,X645,X651) ),
theory(equality) ).
cnf(c53,axiom,
( X638 != X636
| X639 != X637
| ~ young(X638,X639)
| young(X636,X637) ),
theory(equality) ).
cnf(clause74,negated_conjecture,
old(skc5,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
cnf(c52,axiom,
( X631 != X629
| X632 != X630
| ~ old(X631,X632)
| old(X629,X630) ),
theory(equality) ).
cnf(c328,plain,
( skc5 != X634
| skc7 != X633
| old(X634,X633) ),
inference(resolution,[status(thm)],[c52,clause74]) ).
cnf(c329,plain,
( skc5 != X635
| old(X635,skc7) ),
inference(resolution,[status(thm)],[c328,reflexivity]) ).
cnf(clause80,negated_conjecture,
city(skc5,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
cnf(clause46,axiom,
( ~ city(X94,X93)
| location(X94,X93) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c106,plain,
location(skc5,skc8),
inference(resolution,[status(thm)],[clause46,clause80]) ).
cnf(c48,axiom,
( X612 != X610
| X613 != X611
| ~ location(X612,X613)
| location(X610,X611) ),
theory(equality) ).
cnf(c322,plain,
( skc5 != X618
| skc8 != X619
| location(X618,X619) ),
inference(resolution,[status(thm)],[c48,c106]) ).
cnf(c324,plain,
( skc5 != X620
| location(X620,skc8) ),
inference(resolution,[status(thm)],[c322,reflexivity]) ).
cnf(c47,axiom,
( X605 != X603
| X606 != X604
| ~ city(X605,X606)
| city(X603,X604) ),
theory(equality) ).
cnf(c319,plain,
( skc5 != X608
| skc8 != X607
| city(X608,X607) ),
inference(resolution,[status(thm)],[c47,clause80]) ).
cnf(c320,plain,
( skc5 != X609
| city(X609,skc8) ),
inference(resolution,[status(thm)],[c319,reflexivity]) ).
cnf(clause69,negated_conjecture,
hollywood_placename(skc5,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
cnf(c46,axiom,
( X595 != X593
| X596 != X594
| ~ hollywood_placename(X595,X596)
| hollywood_placename(X593,X594) ),
theory(equality) ).
cnf(c314,plain,
( skc5 != X600
| skc9 != X601
| hollywood_placename(X600,X601) ),
inference(resolution,[status(thm)],[c46,clause69]) ).
cnf(c317,plain,
( skc5 != X602
| hollywood_placename(X602,skc9) ),
inference(resolution,[status(thm)],[c314,reflexivity]) ).
cnf(clause70,negated_conjecture,
placename(skc5,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
cnf(clause38,axiom,
( ~ placename(X78,X77)
| relname(X78,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c93,plain,
relname(skc5,skc9),
inference(resolution,[status(thm)],[clause38,clause70]) ).
cnf(clause39,axiom,
( ~ relname(X80,X79)
| relation(X80,X79) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c98,plain,
relation(skc5,skc9),
inference(resolution,[status(thm)],[clause39,c93]) ).
cnf(clause40,axiom,
( ~ relation(X82,X81)
| abstraction(X82,X81) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c99,plain,
abstraction(skc5,skc9),
inference(resolution,[status(thm)],[clause40,c98]) ).
cnf(clause43,axiom,
( ~ abstraction(X88,X87)
| general(X88,X87) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c103,plain,
general(skc5,skc9),
inference(resolution,[status(thm)],[clause43,c99]) ).
cnf(c45,axiom,
( X591 != X589
| X592 != X590
| ~ general(X591,X592)
| general(X589,X590) ),
theory(equality) ).
cnf(c313,plain,
( skc5 != X598
| skc9 != X597
| general(X598,X597) ),
inference(resolution,[status(thm)],[c45,c103]) ).
cnf(c315,plain,
( skc5 != X599
| general(X599,skc9) ),
inference(resolution,[status(thm)],[c313,reflexivity]) ).
cnf(clause42,axiom,
( ~ abstraction(X86,X85)
| nonhuman(X86,X85) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c102,plain,
nonhuman(skc5,skc9),
inference(resolution,[status(thm)],[clause42,c99]) ).
cnf(c44,axiom,
( X584 != X582
| X585 != X583
| ~ nonhuman(X584,X585)
| nonhuman(X582,X583) ),
theory(equality) ).
cnf(c310,plain,
( skc5 != X586
| skc9 != X587
| nonhuman(X586,X587) ),
inference(resolution,[status(thm)],[c44,c102]) ).
cnf(c311,plain,
( skc5 != X588
| nonhuman(X588,skc9) ),
inference(resolution,[status(thm)],[c310,reflexivity]) ).
cnf(c43,axiom,
( X574 != X572
| X575 != X573
| ~ abstraction(X574,X575)
| abstraction(X572,X573) ),
theory(equality) ).
cnf(c305,plain,
( skc5 != X579
| skc9 != X580
| abstraction(X579,X580) ),
inference(resolution,[status(thm)],[c43,c99]) ).
cnf(c308,plain,
( skc5 != X581
| abstraction(X581,skc9) ),
inference(resolution,[status(thm)],[c305,reflexivity]) ).
cnf(c42,axiom,
( X570 != X568
| X571 != X569
| ~ relation(X570,X571)
| relation(X568,X569) ),
theory(equality) ).
cnf(c304,plain,
( skc5 != X576
| skc9 != X577
| relation(X576,X577) ),
inference(resolution,[status(thm)],[c42,c98]) ).
cnf(c306,plain,
( skc5 != X578
| relation(X578,skc9) ),
inference(resolution,[status(thm)],[c304,reflexivity]) ).
cnf(c41,axiom,
( X563 != X561
| X564 != X562
| ~ relname(X563,X564)
| relname(X561,X562) ),
theory(equality) ).
cnf(c301,plain,
( skc5 != X566
| skc9 != X565
| relname(X566,X565) ),
inference(resolution,[status(thm)],[c41,c93]) ).
cnf(c302,plain,
( skc5 != X567
| relname(X567,skc9) ),
inference(resolution,[status(thm)],[c301,reflexivity]) ).
cnf(c40,axiom,
( X553 != X551
| X554 != X552
| ~ placename(X553,X554)
| placename(X551,X552) ),
theory(equality) ).
cnf(c296,plain,
( skc5 != X558
| skc9 != X559
| placename(X558,X559) ),
inference(resolution,[status(thm)],[c40,clause70]) ).
cnf(c299,plain,
( skc5 != X560
| placename(X560,skc9) ),
inference(resolution,[status(thm)],[c296,reflexivity]) ).
cnf(clause79,negated_conjecture,
street(skc5,skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
cnf(clause36,axiom,
( ~ street(X74,X73)
| way(X74,X73) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c86,plain,
way(skc5,skc8),
inference(resolution,[status(thm)],[clause36,clause79]) ).
cnf(c39,axiom,
( X545 != X543
| X546 != X544
| ~ way(X545,X546)
| way(X543,X544) ),
theory(equality) ).
cnf(c292,plain,
( skc5 != X556
| skc8 != X555
| way(X556,X555) ),
inference(resolution,[status(thm)],[c39,c86]) ).
cnf(c297,plain,
( skc5 != X557
| way(X557,skc8) ),
inference(resolution,[status(thm)],[c292,reflexivity]) ).
cnf(c38,axiom,
( X536 != X534
| X537 != X535
| ~ street(X536,X537)
| street(X534,X535) ),
theory(equality) ).
cnf(c288,plain,
( skc5 != X548
| skc8 != X549
| street(X548,X549) ),
inference(resolution,[status(thm)],[c38,clause79]) ).
cnf(c294,plain,
( skc5 != X550
| street(X550,skc8) ),
inference(resolution,[status(thm)],[c288,reflexivity]) ).
cnf(clause37,axiom,
( ~ way(X76,X75)
| artifact(X76,X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c87,plain,
artifact(skc5,skc8),
inference(resolution,[status(thm)],[c86,clause37]) ).
cnf(c88,plain,
object(skc5,skc8),
inference(resolution,[status(thm)],[c87,clause31]) ).
cnf(c90,plain,
nonliving(skc5,skc8),
inference(resolution,[status(thm)],[c88,clause33]) ).
cnf(c283,plain,
( skc5 != X542
| skc8 != X541
| nonliving(X542,X541) ),
inference(resolution,[status(thm)],[c37,c90]) ).
cnf(c291,plain,
( skc5 != X547
| nonliving(X547,skc8) ),
inference(resolution,[status(thm)],[c283,reflexivity]) ).
cnf(clause27,axiom,
( ~ car(X56,X55)
| vehicle(X56,X55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause71,negated_conjecture,
chevy(skc5,skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
cnf(clause26,axiom,
( ~ chevy(X54,X53)
| car(X54,X53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c72,plain,
car(skc5,skc7),
inference(resolution,[status(thm)],[clause26,clause71]) ).
cnf(c73,plain,
vehicle(skc5,skc7),
inference(resolution,[status(thm)],[c72,clause27]) ).
cnf(clause28,axiom,
( ~ vehicle(X58,X57)
| transport(X58,X57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c74,plain,
transport(skc5,skc7),
inference(resolution,[status(thm)],[clause28,c73]) ).
cnf(clause29,axiom,
( ~ transport(X60,X59)
| instrumentality(X60,X59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c75,plain,
instrumentality(skc5,skc7),
inference(resolution,[status(thm)],[clause29,c74]) ).
cnf(c76,plain,
artifact(skc5,skc7),
inference(resolution,[status(thm)],[c75,clause30]) ).
cnf(c77,plain,
object(skc5,skc7),
inference(resolution,[status(thm)],[clause31,c76]) ).
cnf(c79,plain,
nonliving(skc5,skc7),
inference(resolution,[status(thm)],[clause33,c77]) ).
cnf(c282,plain,
( skc5 != X539
| skc7 != X538
| nonliving(X539,X538) ),
inference(resolution,[status(thm)],[c37,c79]) ).
cnf(c289,plain,
( skc5 != X540
| nonliving(X540,skc7) ),
inference(resolution,[status(thm)],[c282,reflexivity]) ).
cnf(c277,plain,
( skc5 != X532
| skc7 != X531
| object(X532,X531) ),
inference(resolution,[status(thm)],[c36,c77]) ).
cnf(c286,plain,
( skc5 != X533
| object(X533,skc7) ),
inference(resolution,[status(thm)],[c277,reflexivity]) ).
cnf(c275,plain,
( skc5 != X529
| skc8 != X528
| object(X529,X528) ),
inference(resolution,[status(thm)],[c36,c88]) ).
cnf(c284,plain,
( skc5 != X530
| object(X530,skc8) ),
inference(resolution,[status(thm)],[c275,reflexivity]) ).
cnf(c273,plain,
( skc5 != X522
| skc8 != X521
| artifact(X522,X521) ),
inference(resolution,[status(thm)],[c35,c87]) ).
cnf(c279,plain,
( skc5 != X523
| artifact(X523,skc8) ),
inference(resolution,[status(thm)],[c273,reflexivity]) ).
cnf(c272,plain,
( skc5 != X515
| skc7 != X514
| artifact(X515,X514) ),
inference(resolution,[status(thm)],[c35,c76]) ).
cnf(c274,plain,
( skc5 != X520
| artifact(X520,skc7) ),
inference(resolution,[status(thm)],[c272,reflexivity]) ).
cnf(c267,plain,
( skc5 != X507
| skc7 != X508
| instrumentality(X507,X508) ),
inference(resolution,[status(thm)],[c34,c75]) ).
cnf(c269,plain,
( skc5 != X509
| instrumentality(X509,skc7) ),
inference(resolution,[status(thm)],[c267,reflexivity]) ).
cnf(c33,axiom,
( X497 != X495
| X498 != X496
| ~ transport(X497,X498)
| transport(X495,X496) ),
theory(equality) ).
cnf(c263,plain,
( skc5 != X500
| skc7 != X501
| transport(X500,X501) ),
inference(resolution,[status(thm)],[c33,c74]) ).
cnf(c265,plain,
( skc5 != X502
| transport(X502,skc7) ),
inference(resolution,[status(thm)],[c263,reflexivity]) ).
cnf(c32,axiom,
( X488 != X486
| X489 != X487
| ~ vehicle(X488,X489)
| vehicle(X486,X487) ),
theory(equality) ).
cnf(c259,plain,
( skc5 != X494
| skc7 != X493
| vehicle(X494,X493) ),
inference(resolution,[status(thm)],[c32,c73]) ).
cnf(c262,plain,
( skc5 != X499
| vehicle(X499,skc7) ),
inference(resolution,[status(thm)],[c259,reflexivity]) ).
cnf(c31,axiom,
( X478 != X476
| X479 != X477
| ~ car(X478,X479)
| car(X476,X477) ),
theory(equality) ).
cnf(c254,plain,
( skc5 != X491
| skc7 != X490
| car(X491,X490) ),
inference(resolution,[status(thm)],[c31,c72]) ).
cnf(c260,plain,
( skc5 != X492
| car(X492,skc7) ),
inference(resolution,[status(thm)],[c254,reflexivity]) ).
cnf(c30,axiom,
( X470 != X468
| X471 != X469
| ~ chevy(X470,X471)
| chevy(X468,X469) ),
theory(equality) ).
cnf(c250,plain,
( skc5 != X484
| skc7 != X483
| chevy(X484,X483) ),
inference(resolution,[status(thm)],[c30,clause71]) ).
cnf(c257,plain,
( skc5 != X485
| chevy(X485,skc7) ),
inference(resolution,[status(thm)],[c250,reflexivity]) ).
cnf(clause75,negated_conjecture,
barrel(skc5,skc6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
cnf(c29,axiom,
( X461 != X459
| X462 != X460
| ~ barrel(X461,X462)
| barrel(X459,X460) ),
theory(equality) ).
cnf(c246,plain,
( skc5 != X481
| skc6 != X480
| barrel(X481,X480) ),
inference(resolution,[status(thm)],[c29,clause75]) ).
cnf(c255,plain,
( skc5 != X482
| barrel(X482,skc6) ),
inference(resolution,[status(thm)],[c246,reflexivity]) ).
cnf(clause77,negated_conjecture,
event(skc5,skc6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
cnf(c28,axiom,
( X451 != X449
| X452 != X450
| ~ event(X451,X452)
| event(X449,X450) ),
theory(equality) ).
cnf(c241,plain,
( skc5 != X473
| skc6 != X474
| event(X473,X474) ),
inference(resolution,[status(thm)],[c28,clause77]) ).
cnf(c252,plain,
( skc5 != X475
| event(X475,skc6) ),
inference(resolution,[status(thm)],[c241,reflexivity]) ).
cnf(clause44,axiom,
( ~ abstraction(X90,X89)
| unisex(X90,X89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c104,plain,
unisex(skc5,skc9),
inference(resolution,[status(thm)],[clause44,c99]) ).
cnf(c240,plain,
( skc5 != X467
| skc9 != X466
| unisex(X467,X466) ),
inference(resolution,[status(thm)],[c27,c104]) ).
cnf(c249,plain,
( skc5 != X472
| unisex(X472,skc9) ),
inference(resolution,[status(thm)],[c240,reflexivity]) ).
cnf(c91,plain,
unisex(skc5,skc8),
inference(resolution,[status(thm)],[c88,clause35]) ).
cnf(c238,plain,
( skc5 != X464
| skc8 != X463
| unisex(X464,X463) ),
inference(resolution,[status(thm)],[c27,c91]) ).
cnf(c247,plain,
( skc5 != X465
| unisex(X465,skc8) ),
inference(resolution,[status(thm)],[c238,reflexivity]) ).
cnf(clause22,axiom,
( ~ eventuality(X46,X45)
| unisex(X46,X45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause24,axiom,
( ~ event(X50,X49)
| eventuality(X50,X49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c65,plain,
eventuality(skc5,skc6),
inference(resolution,[status(thm)],[clause24,clause77]) ).
cnf(c67,plain,
unisex(skc5,skc6),
inference(resolution,[status(thm)],[c65,clause22]) ).
cnf(c237,plain,
( skc5 != X457
| skc6 != X456
| unisex(X457,X456) ),
inference(resolution,[status(thm)],[c27,c67]) ).
cnf(c244,plain,
( skc5 != X458
| unisex(X458,skc6) ),
inference(resolution,[status(thm)],[c237,reflexivity]) ).
cnf(c85,plain,
unisex(skc5,skc7),
inference(resolution,[status(thm)],[clause35,c77]) ).
cnf(c236,plain,
( skc5 != X454
| skc7 != X453
| unisex(X454,X453) ),
inference(resolution,[status(thm)],[c27,c85]) ).
cnf(c242,plain,
( skc5 != X455
| unisex(X455,skc7) ),
inference(resolution,[status(thm)],[c236,reflexivity]) ).
cnf(clause21,axiom,
( ~ eventuality(X44,X43)
| nonexistent(X44,X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c68,plain,
nonexistent(skc5,skc6),
inference(resolution,[status(thm)],[c65,clause21]) ).
cnf(c26,axiom,
( X440 != X438
| X441 != X439
| ~ nonexistent(X440,X441)
| nonexistent(X438,X439) ),
theory(equality) ).
cnf(c233,plain,
( skc5 != X443
| skc6 != X442
| nonexistent(X443,X442) ),
inference(resolution,[status(thm)],[c26,c68]) ).
cnf(c234,plain,
( skc5 != X444
| nonexistent(X444,skc6) ),
inference(resolution,[status(thm)],[c233,reflexivity]) ).
cnf(c25,axiom,
( X433 != X431
| X434 != X432
| ~ eventuality(X433,X434)
| eventuality(X431,X432) ),
theory(equality) ).
cnf(c230,plain,
( skc5 != X436
| skc6 != X435
| eventuality(X436,X435) ),
inference(resolution,[status(thm)],[c25,c65]) ).
cnf(c231,plain,
( skc5 != X437
| eventuality(X437,skc6) ),
inference(resolution,[status(thm)],[c230,reflexivity]) ).
cnf(c24,axiom,
( X429 != X427
| X430 != X428
| ~ state(X429,X430)
| state(X427,X428) ),
theory(equality) ).
cnf(c23,axiom,
( X425 != X423
| X426 != X424
| ~ two(X425,X426)
| two(X423,X424) ),
theory(equality) ).
cnf(c22,axiom,
( X421 != X419
| X422 != X420
| ~ multiple(X421,X422)
| multiple(X419,X420) ),
theory(equality) ).
cnf(c21,axiom,
( X417 != X415
| X418 != X416
| ~ set(X417,X418)
| set(X415,X416) ),
theory(equality) ).
cnf(c20,axiom,
( X413 != X411
| X414 != X412
| ~ group(X413,X414)
| group(X411,X412) ),
theory(equality) ).
cnf(c19,axiom,
( X409 != X407
| X410 != X408
| ~ male(X409,X410)
| male(X407,X408) ),
theory(equality) ).
cnf(c18,axiom,
( X405 != X403
| X406 != X404
| ~ animate(X405,X406)
| animate(X403,X404) ),
theory(equality) ).
cnf(c17,axiom,
( X401 != X399
| X402 != X400
| ~ human(X401,X402)
| human(X399,X400) ),
theory(equality) ).
cnf(c84,plain,
impartial(skc5,skc7),
inference(resolution,[status(thm)],[clause34,c77]) ).
cnf(c222,plain,
( skc5 != X396
| skc7 != X397
| impartial(X396,X397) ),
inference(resolution,[status(thm)],[c15,c84]) ).
cnf(c228,plain,
( skc5 != X398
| impartial(X398,skc7) ),
inference(resolution,[status(thm)],[c222,reflexivity]) ).
cnf(c89,plain,
impartial(skc5,skc8),
inference(resolution,[status(thm)],[c88,clause34]) ).
cnf(c220,plain,
( skc5 != X393
| skc8 != X394
| impartial(X393,X394) ),
inference(resolution,[status(thm)],[c15,c89]) ).
cnf(c226,plain,
( skc5 != X395
| impartial(X395,skc8) ),
inference(resolution,[status(thm)],[c220,reflexivity]) ).
cnf(c16,axiom,
( X391 != X389
| X392 != X390
| ~ living(X391,X392)
| living(X389,X390) ),
theory(equality) ).
cnf(c78,plain,
entity(skc5,skc7),
inference(resolution,[status(thm)],[clause32,c77]) ).
cnf(c81,plain,
existent(skc5,skc7),
inference(resolution,[status(thm)],[c78,clause9]) ).
cnf(c215,plain,
( skc5 != X387
| skc7 != X386
| existent(X387,X386) ),
inference(resolution,[status(thm)],[c14,c81]) ).
cnf(c224,plain,
( skc5 != X388
| existent(X388,skc7) ),
inference(resolution,[status(thm)],[c215,reflexivity]) ).
cnf(c92,plain,
entity(skc5,skc8),
inference(resolution,[status(thm)],[c88,clause32]) ).
cnf(c95,plain,
existent(skc5,skc8),
inference(resolution,[status(thm)],[c92,clause9]) ).
cnf(c214,plain,
( skc5 != X380
| skc8 != X379
| existent(X380,X379) ),
inference(resolution,[status(thm)],[c14,c95]) ).
cnf(c219,plain,
( skc5 != X385
| existent(X385,skc8) ),
inference(resolution,[status(thm)],[c214,reflexivity]) ).
cnf(c96,plain,
specific(skc5,skc8),
inference(resolution,[status(thm)],[c92,clause8]) ).
cnf(c208,plain,
( skc5 != X376
| skc8 != X377
| specific(X376,X377) ),
inference(resolution,[status(thm)],[c13,c96]) ).
cnf(c217,plain,
( skc5 != X378
| specific(X378,skc8) ),
inference(resolution,[status(thm)],[c208,reflexivity]) ).
cnf(clause20,axiom,
( ~ eventuality(X42,X41)
| specific(X42,X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c69,plain,
specific(skc5,skc6),
inference(resolution,[status(thm)],[c65,clause20]) ).
cnf(c207,plain,
( skc5 != X369
| skc6 != X370
| specific(X369,X370) ),
inference(resolution,[status(thm)],[c13,c69]) ).
cnf(c212,plain,
( skc5 != X371
| specific(X371,skc6) ),
inference(resolution,[status(thm)],[c207,reflexivity]) ).
cnf(c82,plain,
specific(skc5,skc7),
inference(resolution,[status(thm)],[c78,clause8]) ).
cnf(c205,plain,
( skc5 != X366
| skc7 != X367
| specific(X366,X367) ),
inference(resolution,[status(thm)],[c13,c82]) ).
cnf(c210,plain,
( skc5 != X368
| specific(X368,skc7) ),
inference(resolution,[status(thm)],[c205,reflexivity]) ).
cnf(c4,axiom,
( X346 != X344
| X347 != X345
| skf5(X346,X347) = skf5(X344,X345) ),
theory(equality) ).
cnf(c202,plain,
( X352 != X351
| skf5(X352,X353) = skf5(X351,X353) ),
inference(resolution,[status(thm)],[c4,reflexivity]) ).
cnf(c201,plain,
( X349 != X348
| skf5(X349,X349) = skf5(X348,X348) ),
inference(factor,[status(thm)],[c4]) ).
cnf(c3,axiom,
( X332 != X330
| X333 != X331
| skf8(X332,X333) = skf8(X330,X331) ),
theory(equality) ).
cnf(c198,plain,
( X341 != X340
| skf8(X341,X339) = skf8(X340,X339) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c197,plain,
( X336 != X337
| skf8(X336,X336) = skf8(X337,X337) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c1,axiom,
( X303 != X301
| X304 != X302
| skf10(X303,X304) = skf10(X301,X302) ),
theory(equality) ).
cnf(c186,plain,
( X327 != X328
| skf10(X327,X329) = skf10(X328,X329) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c185,plain,
( X324 != X325
| skf10(X324,X324) = skf10(X325,X325) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c0,axiom,
( X295 != X293
| X296 != X294
| skf12(X295,X296) = skf12(X293,X294) ),
theory(equality) ).
cnf(c181,plain,
( X320 != X321
| skf12(X320,X319) = skf12(X321,X319) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c180,plain,
( X308 != X309
| skf12(X308,X308) = skf12(X309,X309) ),
inference(factor,[status(thm)],[c0]) ).
cnf(clause41,axiom,
( ~ abstraction(X84,X83)
| thing(X84,X83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c100,plain,
thing(skc5,skc9),
inference(resolution,[status(thm)],[clause41,c99]) ).
cnf(c101,plain,
singleton(skc5,skc9),
inference(resolution,[status(thm)],[c100,clause7]) ).
cnf(c176,plain,
( skc5 != X306
| skc9 != X305
| singleton(X306,X305) ),
inference(resolution,[status(thm)],[c12,c101]) ).
cnf(c187,plain,
( skc5 != X307
| singleton(X307,skc9) ),
inference(resolution,[status(thm)],[c176,reflexivity]) ).
cnf(clause19,axiom,
( ~ eventuality(X40,X39)
| thing(X40,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c66,plain,
thing(skc5,skc6),
inference(resolution,[status(thm)],[c65,clause19]) ).
cnf(c70,plain,
singleton(skc5,skc6),
inference(resolution,[status(thm)],[c66,clause7]) ).
cnf(c175,plain,
( skc5 != X299
| skc6 != X298
| singleton(X299,X298) ),
inference(resolution,[status(thm)],[c12,c70]) ).
cnf(c183,plain,
( skc5 != X300
| singleton(X300,skc6) ),
inference(resolution,[status(thm)],[c175,reflexivity]) ).
cnf(c80,plain,
thing(skc5,skc7),
inference(resolution,[status(thm)],[c78,clause6]) ).
cnf(c83,plain,
singleton(skc5,skc7),
inference(resolution,[status(thm)],[c80,clause7]) ).
cnf(c173,plain,
( skc5 != X292
| skc7 != X291
| singleton(X292,X291) ),
inference(resolution,[status(thm)],[c12,c83]) ).
cnf(c179,plain,
( skc5 != X297
| singleton(X297,skc7) ),
inference(resolution,[status(thm)],[c173,reflexivity]) ).
cnf(c94,plain,
thing(skc5,skc8),
inference(resolution,[status(thm)],[c92,clause6]) ).
cnf(c97,plain,
singleton(skc5,skc8),
inference(resolution,[status(thm)],[c94,clause7]) ).
cnf(c172,plain,
( skc5 != X289
| skc8 != X288
| singleton(X289,X288) ),
inference(resolution,[status(thm)],[c12,c97]) ).
cnf(c177,plain,
( skc5 != X290
| singleton(X290,skc8) ),
inference(resolution,[status(thm)],[c172,reflexivity]) ).
cnf(clause89,negated_conjecture,
( ~ city(X280,X282)
| ~ street(X280,X282)
| ~ lonely(X280,X282)
| ~ down(X280,X283,X282)
| ~ in(X280,X283,X282)
| ~ placename(X280,X281)
| ~ hollywood_placename(X280,X281)
| ~ of(X280,X281,X282)
| ~ event(X280,X283)
| ~ present(X280,X283)
| ~ barrel(X280,X283)
| ~ agent(X280,X283,X277)
| ~ old(X280,X277)
| ~ dirty(X280,X277)
| ~ white(X280,X277)
| ~ chevy(X280,X277)
| ~ young(X280,skf5(X280,X279))
| ~ fellow(X280,skf5(X280,X279))
| ~ group(X280,X278)
| ~ two(X280,X278)
| ~ ssSkP0(X278,X280)
| ~ actual_world(X280) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
cnf(c162,plain,
( skc5 != X275
| skc6 != X274
| thing(X275,X274) ),
inference(resolution,[status(thm)],[c11,c66]) ).
cnf(c170,plain,
( skc5 != X276
| thing(X276,skc6) ),
inference(resolution,[status(thm)],[c162,reflexivity]) ).
cnf(c161,plain,
( skc5 != X266
| skc7 != X265
| thing(X266,X265) ),
inference(resolution,[status(thm)],[c11,c80]) ).
cnf(c167,plain,
( skc5 != X273
| thing(X273,skc7) ),
inference(resolution,[status(thm)],[c161,reflexivity]) ).
cnf(c160,plain,
( skc5 != X263
| skc8 != X262
| thing(X263,X262) ),
inference(resolution,[status(thm)],[c11,c94]) ).
cnf(c165,plain,
( skc5 != X264
| thing(X264,skc8) ),
inference(resolution,[status(thm)],[c160,reflexivity]) ).
cnf(clause87,negated_conjecture,
( ~ in(X258,X260,skf8(X258,X261))
| ~ be(X258,X259,skf8(X258,X261),X260)
| ~ state(X258,X259)
| ssSkP0(X257,X258) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
cnf(c159,plain,
( skc5 != X255
| skc9 != X254
| thing(X255,X254) ),
inference(resolution,[status(thm)],[c11,c100]) ).
cnf(c163,plain,
( skc5 != X256
| thing(X256,skc9) ),
inference(resolution,[status(thm)],[c159,reflexivity]) ).
cnf(c151,plain,
( skc5 != X244
| skc7 != X243
| entity(X244,X243) ),
inference(resolution,[status(thm)],[c10,c78]) ).
cnf(c154,plain,
( skc5 != X249
| entity(X249,skc7) ),
inference(resolution,[status(thm)],[c151,reflexivity]) ).
cnf(c150,plain,
( skc5 != X241
| skc8 != X240
| entity(X241,X240) ),
inference(resolution,[status(thm)],[c10,c92]) ).
cnf(c152,plain,
( skc5 != X242
| entity(X242,skc8) ),
inference(resolution,[status(thm)],[c150,reflexivity]) ).
cnf(clause66,axiom,
( skf13(X232,X234,X235,X233) != X234
| ~ member(X230,X232,X231)
| ~ member(X230,X234,X231)
| two(X230,X231)
| X232 = X234 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
cnf(c9,axiom,
( X228 != X226
| X229 != X227
| ~ organism(X228,X229)
| organism(X226,X227) ),
theory(equality) ).
cnf(c8,axiom,
( X224 != X222
| X225 != X223
| ~ human_person(X224,X225)
| human_person(X222,X223) ),
theory(equality) ).
cnf(c7,axiom,
( X220 != X218
| X221 != X219
| ~ man(X220,X221)
| man(X218,X219) ),
theory(equality) ).
cnf(c6,axiom,
( X216 != X214
| X217 != X215
| ~ fellow(X216,X217)
| fellow(X214,X215) ),
theory(equality) ).
cnf(transitivity,axiom,
( X206 != X204
| X204 != X205
| X206 = X205 ),
theory(equality) ).
cnf(clause54,axiom,
( ~ multiple(X110,X109)
| ~ singleton(X110,X109) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(c143,plain,
( ssSkP0(X199,X201)
| ~ multiple(X201,skf8(X201,X200)) ),
inference(resolution,[status(thm)],[c140,clause54]) ).
cnf(clause53,axiom,
( ~ general(X108,X107)
| ~ specific(X108,X107) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
cnf(c142,plain,
( ssSkP0(X196,X197)
| ~ general(X197,skf8(X197,X198)) ),
inference(resolution,[status(thm)],[c139,clause53]) ).
cnf(clause64,axiom,
( skf13(X192,X194,X195,X193) != X192
| ~ member(X189,X192,X191)
| ~ member(X189,X190,X191)
| two(X189,X191)
| X192 = X190 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
cnf(clause57,axiom,
( ~ nonexistent(X116,X115)
| ~ existent(X116,X115) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c141,plain,
( ssSkP0(X188,X186)
| ~ nonexistent(X186,skf8(X186,X187)) ),
inference(resolution,[status(thm)],[c138,clause57]) ).
cnf(clause52,axiom,
( ~ male(X106,X105)
| ~ unisex(X106,X105) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c136,plain,
( ssSkP0(X168,X170)
| ~ male(X170,skf8(X170,X169)) ),
inference(resolution,[status(thm)],[c133,clause52]) ).
cnf(clause55,axiom,
( ~ living(X112,X111)
| ~ nonliving(X112,X111) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(c135,plain,
( ssSkP0(X166,X167)
| ~ living(X167,skf8(X167,X165)) ),
inference(resolution,[status(thm)],[c132,clause55]) ).
cnf(clause62,axiom,
( skf12(X155,X154) != skf10(X155,X154)
| ~ two(X154,X155) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
cnf(clause61,axiom,
( ~ two(X138,X137)
| member(X138,skf10(X137,X138),X137) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
cnf(c56,axiom,
( X129 != X128
| ~ actual_world(X129)
| actual_world(X128) ),
theory(equality) ).
cnf(clause60,axiom,
( ~ two(X126,X125)
| member(X126,skf12(X125,X126),X125) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
cnf(symmetry,axiom,
( X124 != X123
| X123 = X124 ),
theory(equality) ).
cnf(clause59,axiom,
( ~ be(X120,X119,X121,X122)
| X121 = X122 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(clause58,axiom,
( ~ nonliving(X118,X117)
| ~ animate(X118,X117) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
cnf(c123,plain,
~ nonexistent(skc5,skc7),
inference(resolution,[status(thm)],[clause57,c81]) ).
cnf(c122,plain,
~ nonexistent(skc5,skc8),
inference(resolution,[status(thm)],[clause57,c95]) ).
cnf(clause56,axiom,
( ~ human(X114,X113)
| ~ nonhuman(X114,X113) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(c121,plain,
~ human(skc5,skc9),
inference(resolution,[status(thm)],[clause56,c102]) ).
cnf(c120,plain,
~ living(skc5,skc8),
inference(resolution,[status(thm)],[clause55,c90]) ).
cnf(c119,plain,
~ living(skc5,skc7),
inference(resolution,[status(thm)],[clause55,c79]) ).
cnf(c118,plain,
~ multiple(skc5,skc7),
inference(resolution,[status(thm)],[clause54,c83]) ).
cnf(c117,plain,
~ multiple(skc5,skc9),
inference(resolution,[status(thm)],[clause54,c101]) ).
cnf(c116,plain,
~ multiple(skc5,skc8),
inference(resolution,[status(thm)],[clause54,c97]) ).
cnf(c115,plain,
~ multiple(skc5,skc6),
inference(resolution,[status(thm)],[clause54,c70]) ).
cnf(c114,plain,
~ general(skc5,skc8),
inference(resolution,[status(thm)],[clause53,c96]) ).
cnf(c113,plain,
~ general(skc5,skc6),
inference(resolution,[status(thm)],[clause53,c69]) ).
cnf(c112,plain,
~ general(skc5,skc7),
inference(resolution,[status(thm)],[clause53,c82]) ).
cnf(c111,plain,
~ male(skc5,skc6),
inference(resolution,[status(thm)],[clause52,c67]) ).
cnf(c110,plain,
~ male(skc5,skc9),
inference(resolution,[status(thm)],[clause52,c104]) ).
cnf(c109,plain,
~ male(skc5,skc7),
inference(resolution,[status(thm)],[clause52,c85]) ).
cnf(c108,plain,
~ male(skc5,skc8),
inference(resolution,[status(thm)],[clause52,c91]) ).
cnf(clause51,axiom,
( ~ old(X104,X103)
| ~ young(X104,X103) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(clause47,axiom,
( ~ location(X96,X95)
| object(X96,X95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(clause45,axiom,
( ~ hollywood_placename(X92,X91)
| placename(X92,X91) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(clause25,axiom,
( ~ barrel(X52,X51)
| event(X52,X51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause23,axiom,
( ~ state(X48,X47)
| event(X48,X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause18,axiom,
( ~ state(X38,X37)
| eventuality(X38,X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause17,axiom,
( ~ two(X36,X35)
| group(X36,X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause16,axiom,
( ~ set(X34,X33)
| multiple(X34,X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause15,axiom,
( ~ group(X32,X31)
| set(X32,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause14,axiom,
( ~ man(X30,X29)
| male(X30,X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,axiom,
( ~ human_person(X28,X27)
| animate(X28,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause12,axiom,
( ~ human_person(X26,X25)
| human(X26,X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause11,axiom,
( ~ organism(X24,X23)
| living(X24,X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,axiom,
( ~ organism(X22,X21)
| impartial(X22,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause5,axiom,
( ~ organism(X12,X11)
| entity(X12,X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(clause4,axiom,
( ~ human_person(X10,X9)
| organism(X10,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause3,axiom,
( ~ man(X8,X7)
| human_person(X8,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause2,axiom,
( ~ fellow(X6,X5)
| man(X6,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,axiom,
~ member(X4,X3,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause68,negated_conjecture,
actual_world(skc5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP158-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 : n024.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:39:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.97/1.14 % Version: 1.5
% 0.97/1.14 % SZS status Satisfiable
% 0.97/1.14 % SZS output start Saturation
% See solution above
% 0.97/1.15
% 0.97/1.15 % Initial clauses : 157
% 0.97/1.15 % Processed clauses : 469
% 0.97/1.15 % Factors computed : 44
% 0.97/1.15 % Resolvents computed: 411
% 0.97/1.15 % Tautologies deleted: 3
% 0.97/1.15 % Forward subsumed : 140
% 0.97/1.15 % Backward subsumed : 10
% 0.97/1.15 % -------- CPU Time ---------
% 0.97/1.15 % User time : 0.790 s
% 0.97/1.15 % System time : 0.014 s
% 0.97/1.15 % Total time : 0.804 s
%------------------------------------------------------------------------------