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