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