%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP255-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:53 EDT 2024
% Result : Satisfiable 4.68s 4.85s
% Output : Saturation 4.72s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause83,negated_conjecture,
accessible_world(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
cnf(clause81,negated_conjecture,
man(skc8,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
cnf(clause52,axiom,
( ~ accessible_world(X161,X162)
| ~ man(X161,X163)
| man(X162,X163) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c232,plain,
( ~ accessible_world(skc8,X258)
| man(X258,skc10) ),
inference(resolution,[status(thm)],[clause52,clause81]) ).
cnf(c331,plain,
man(skc12,skc10),
inference(resolution,[status(thm)],[c232,clause83]) ).
cnf(clause93,negated_conjecture,
( ~ man(skc12,X287)
| agent(skc12,skf2(X287),X287) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
cnf(c385,plain,
agent(skc12,skf2(skc10),skc10),
inference(resolution,[status(thm)],[clause93,c331]) ).
cnf(clause90,negated_conjecture,
( ~ man(skc12,X269)
| smoke(skc12,skf2(X270)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
cnf(c359,plain,
smoke(skc12,skf2(X271)),
inference(resolution,[status(thm)],[clause90,c331]) ).
cnf(clause91,negated_conjecture,
( ~ man(skc12,X275)
| present(skc12,skf2(X276)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
cnf(c371,plain,
present(skc12,skf2(X281)),
inference(resolution,[status(thm)],[clause91,c331]) ).
cnf(clause1,axiom,
( ~ smoke(X3,X4)
| event(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(c360,plain,
event(skc12,skf2(X272)),
inference(resolution,[status(thm)],[c359,clause1]) ).
cnf(clause88,negated_conjecture,
of(skc8,skc11,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
cnf(clause68,axiom,
( ~ accessible_world(X246,X248)
| ~ of(X246,X249,X247)
| of(X248,X249,X247) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
cnf(c324,plain,
( ~ accessible_world(skc8,X500)
| of(X500,skc11,skc10) ),
inference(resolution,[status(thm)],[clause68,clause88]) ).
cnf(c580,plain,
of(skc12,skc11,skc10),
inference(resolution,[status(thm)],[c324,clause83]) ).
cnf(clause94,negated_conjecture,
( ~ proposition(X298,X295)
| ~ accessible_world(X298,X295)
| ~ think_believe_consider(X298,X294)
| ~ present(X298,X294)
| ~ event(X298,X294)
| ~ theme(X298,X294,X295)
| ~ vincent_forename(X298,X289)
| ~ forename(X298,X289)
| ~ agent(X298,X294,X299)
| ~ man(X298,X299)
| ~ of(X298,X289,X299)
| ~ accessible_world(X298,X291)
| ~ proposition(X298,X291)
| ~ theme(X298,X296,X291)
| ~ event(X298,X296)
| ~ present(X298,X296)
| ~ think_believe_consider(X298,X296)
| ~ state(X298,X297)
| ~ of(X298,X288,X293)
| ~ vincent_forename(X298,X288)
| ~ forename(X298,X288)
| ~ man(X298,X293)
| ~ be(X298,X297,X293,X293)
| ~ agent(X298,X296,X293)
| ~ smoke(X291,X290)
| ~ present(X291,X290)
| ~ agent(X291,X290,X293)
| ~ event(X291,X290)
| ~ forename(X298,X292)
| ~ jules_forename(X298,X292)
| ~ of(X298,X292,X293)
| ~ actual_world(X298)
| man(X295,skf4(X295)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
cnf(clause89,negated_conjecture,
be(skc8,skc9,skc10,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
cnf(clause69,axiom,
( ~ accessible_world(X256,X255)
| ~ be(X256,X254,X253,X257)
| be(X255,X254,X253,X257) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
cnf(c330,plain,
( ~ accessible_world(skc8,X509)
| be(X509,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[clause69,clause89]) ).
cnf(c587,plain,
be(skc12,skc9,skc10,skc10),
inference(resolution,[status(thm)],[c330,clause83]) ).
cnf(c590,plain,
( ~ proposition(skc12,X1052)
| ~ accessible_world(skc12,X1052)
| ~ think_believe_consider(skc12,X1047)
| ~ present(skc12,X1047)
| ~ event(skc12,X1047)
| ~ theme(skc12,X1047,X1052)
| ~ vincent_forename(skc12,X1048)
| ~ forename(skc12,X1048)
| ~ agent(skc12,X1047,X1051)
| ~ man(skc12,X1051)
| ~ of(skc12,X1048,X1051)
| ~ accessible_world(skc12,X1055)
| ~ proposition(skc12,X1055)
| ~ theme(skc12,X1049,X1055)
| ~ event(skc12,X1049)
| ~ present(skc12,X1049)
| ~ think_believe_consider(skc12,X1049)
| ~ state(skc12,skc9)
| ~ of(skc12,X1054,skc10)
| ~ vincent_forename(skc12,X1054)
| ~ forename(skc12,X1054)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1049,skc10)
| ~ smoke(X1055,X1053)
| ~ present(X1055,X1053)
| ~ agent(X1055,X1053,skc10)
| ~ event(X1055,X1053)
| ~ forename(skc12,X1050)
| ~ jules_forename(skc12,X1050)
| ~ of(skc12,X1050,skc10)
| ~ actual_world(skc12)
| man(X1052,skf4(X1052)) ),
inference(resolution,[status(thm)],[c587,clause94]) ).
cnf(c924,plain,
( ~ proposition(skc12,X1376)
| ~ accessible_world(skc12,X1376)
| ~ think_believe_consider(skc12,X1372)
| ~ present(skc12,X1372)
| ~ event(skc12,X1372)
| ~ theme(skc12,X1372,X1376)
| ~ vincent_forename(skc12,X1373)
| ~ forename(skc12,X1373)
| ~ agent(skc12,X1372,X1375)
| ~ man(skc12,X1375)
| ~ of(skc12,X1373,X1375)
| ~ accessible_world(skc12,X1378)
| ~ proposition(skc12,X1378)
| ~ theme(skc12,X1377,X1378)
| ~ event(skc12,X1377)
| ~ present(skc12,X1377)
| ~ think_believe_consider(skc12,X1377)
| ~ state(skc12,skc9)
| ~ of(skc12,X1374,skc10)
| ~ vincent_forename(skc12,X1374)
| ~ forename(skc12,X1374)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1377,skc10)
| ~ smoke(X1378,X1379)
| ~ present(X1378,X1379)
| ~ agent(X1378,X1379,skc10)
| ~ event(X1378,X1379)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1376,skf4(X1376)) ),
inference(resolution,[status(thm)],[c590,c580]) ).
cnf(c1062,plain,
( ~ proposition(skc12,X1530)
| ~ accessible_world(skc12,X1530)
| ~ think_believe_consider(skc12,X1535)
| ~ present(skc12,X1535)
| ~ event(skc12,X1535)
| ~ theme(skc12,X1535,X1530)
| ~ vincent_forename(skc12,X1531)
| ~ forename(skc12,X1531)
| ~ agent(skc12,X1535,X1533)
| ~ man(skc12,X1533)
| ~ of(skc12,X1531,X1533)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1534,skc12)
| ~ event(skc12,X1534)
| ~ present(skc12,X1534)
| ~ think_believe_consider(skc12,X1534)
| ~ state(skc12,skc9)
| ~ of(skc12,X1532,skc10)
| ~ vincent_forename(skc12,X1532)
| ~ forename(skc12,X1532)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1534,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1530,skf4(X1530)) ),
inference(resolution,[status(thm)],[c924,c385]) ).
cnf(c1102,plain,
( ~ proposition(skc12,X1705)
| ~ accessible_world(skc12,X1705)
| ~ think_believe_consider(skc12,X1704)
| ~ present(skc12,X1704)
| ~ event(skc12,X1704)
| ~ theme(skc12,X1704,X1705)
| ~ vincent_forename(skc12,X1703)
| ~ forename(skc12,X1703)
| ~ agent(skc12,X1704,X1706)
| ~ man(skc12,X1706)
| ~ of(skc12,X1703,X1706)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1707,skc12)
| ~ event(skc12,X1707)
| ~ present(skc12,X1707)
| ~ think_believe_consider(skc12,X1707)
| ~ state(skc12,skc9)
| ~ of(skc12,X1708,skc10)
| ~ vincent_forename(skc12,X1708)
| ~ forename(skc12,X1708)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1707,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1705,skf4(X1705)) ),
inference(resolution,[status(thm)],[c1062,c360]) ).
cnf(c1142,plain,
( ~ proposition(skc12,X1709)
| ~ accessible_world(skc12,X1709)
| ~ think_believe_consider(skc12,X1711)
| ~ present(skc12,X1711)
| ~ event(skc12,X1711)
| ~ theme(skc12,X1711,X1709)
| ~ vincent_forename(skc12,X1713)
| ~ forename(skc12,X1713)
| ~ agent(skc12,X1711,X1710)
| ~ man(skc12,X1710)
| ~ of(skc12,X1713,X1710)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1714,skc12)
| ~ event(skc12,X1714)
| ~ present(skc12,X1714)
| ~ think_believe_consider(skc12,X1714)
| ~ state(skc12,skc9)
| ~ of(skc12,X1712,skc10)
| ~ vincent_forename(skc12,X1712)
| ~ forename(skc12,X1712)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1714,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1709,skf4(X1709)) ),
inference(resolution,[status(thm)],[c1102,c371]) ).
cnf(c1143,plain,
( ~ proposition(skc12,X1724)
| ~ accessible_world(skc12,X1724)
| ~ think_believe_consider(skc12,X1720)
| ~ present(skc12,X1720)
| ~ event(skc12,X1720)
| ~ theme(skc12,X1720,X1724)
| ~ vincent_forename(skc12,X1721)
| ~ forename(skc12,X1721)
| ~ agent(skc12,X1720,X1722)
| ~ man(skc12,X1722)
| ~ of(skc12,X1721,X1722)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1725,skc12)
| ~ event(skc12,X1725)
| ~ present(skc12,X1725)
| ~ think_believe_consider(skc12,X1725)
| ~ state(skc12,skc9)
| ~ of(skc12,X1723,skc10)
| ~ vincent_forename(skc12,X1723)
| ~ forename(skc12,X1723)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1725,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1724,skf4(X1724)) ),
inference(resolution,[status(thm)],[c1142,c359]) ).
cnf(c1145,plain,
( ~ proposition(skc12,X1747)
| ~ accessible_world(skc12,X1747)
| ~ think_believe_consider(skc12,X1749)
| ~ present(skc12,X1749)
| ~ event(skc12,X1749)
| ~ theme(skc12,X1749,X1747)
| ~ vincent_forename(skc12,X1750)
| ~ forename(skc12,X1750)
| ~ agent(skc12,X1749,X1751)
| ~ man(skc12,X1751)
| ~ of(skc12,X1750,X1751)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1748,skc10)
| ~ vincent_forename(skc12,X1748)
| ~ forename(skc12,X1748)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1747,skf4(X1747)) ),
inference(resolution,[status(thm)],[c1143,c385]) ).
cnf(c1152,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1754)
| ~ forename(skc12,X1754)
| ~ agent(skc12,skf2(skc10),X1752)
| ~ man(skc12,X1752)
| ~ of(skc12,X1754,X1752)
| ~ state(skc12,skc9)
| ~ of(skc12,X1753,skc10)
| ~ vincent_forename(skc12,X1753)
| ~ forename(skc12,X1753)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1145]) ).
cnf(c1153,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1761)
| ~ forename(skc12,X1761)
| ~ man(skc12,skc10)
| ~ of(skc12,X1761,skc10)
| ~ state(skc12,skc9)
| ~ of(skc12,X1760,skc10)
| ~ vincent_forename(skc12,X1760)
| ~ forename(skc12,X1760)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1152,c385]) ).
cnf(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
cnf(clause67,axiom,
( ~ accessible_world(X240,X242)
| ~ theme(X240,X243,X241)
| theme(X242,X243,X241) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
cnf(c320,plain,
( ~ accessible_world(skc8,X494)
| theme(X494,skc13,skc12) ),
inference(resolution,[status(thm)],[clause67,clause87]) ).
cnf(c571,plain,
theme(skc12,skc13,skc12),
inference(resolution,[status(thm)],[c320,clause83]) ).
cnf(c1144,plain,
( ~ proposition(skc12,X1727)
| ~ accessible_world(skc12,X1727)
| ~ think_believe_consider(skc12,X1728)
| ~ present(skc12,X1728)
| ~ event(skc12,X1728)
| ~ theme(skc12,X1728,X1727)
| ~ vincent_forename(skc12,X1729)
| ~ forename(skc12,X1729)
| ~ agent(skc12,X1728,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1729,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1728,skc12)
| ~ state(skc12,skc9)
| ~ of(skc12,X1726,skc10)
| ~ vincent_forename(skc12,X1726)
| ~ forename(skc12,X1726)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1727,skf4(X1727)) ),
inference(factor,[status(thm)],[c1143]) ).
cnf(c1146,plain,
( ~ proposition(skc12,X1730)
| ~ accessible_world(skc12,X1730)
| ~ think_believe_consider(skc12,X1731)
| ~ present(skc12,X1731)
| ~ event(skc12,X1731)
| ~ theme(skc12,X1731,X1730)
| ~ vincent_forename(skc12,X1732)
| ~ forename(skc12,X1732)
| ~ agent(skc12,X1731,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1732,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1731,skc12)
| ~ state(skc12,skc9)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1730,skf4(X1730)) ),
inference(factor,[status(thm)],[c1144]) ).
cnf(c1149,plain,
( ~ proposition(skc12,X1742)
| ~ accessible_world(skc12,X1742)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1742)
| ~ vincent_forename(skc12,X1741)
| ~ forename(skc12,X1741)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1741,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ state(skc12,skc9)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1742,skf4(X1742)) ),
inference(resolution,[status(thm)],[c1146,c571]) ).
cnf(c1148,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1734)
| ~ present(skc12,X1734)
| ~ event(skc12,X1734)
| ~ theme(skc12,X1734,skc12)
| ~ vincent_forename(skc12,X1733)
| ~ forename(skc12,X1733)
| ~ agent(skc12,X1734,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1733,skc10)
| ~ state(skc12,skc9)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1146]) ).
cnf(c923,plain,
( ~ proposition(skc12,X1359)
| ~ accessible_world(skc12,X1359)
| ~ think_believe_consider(skc12,X1356)
| ~ present(skc12,X1356)
| ~ event(skc12,X1356)
| ~ theme(skc12,X1356,X1359)
| ~ vincent_forename(skc12,X1357)
| ~ forename(skc12,X1357)
| ~ agent(skc12,X1356,X1358)
| ~ man(skc12,X1358)
| ~ of(skc12,X1357,X1358)
| ~ accessible_world(skc12,X1361)
| ~ proposition(skc12,X1361)
| ~ theme(skc12,X1360,X1361)
| ~ event(skc12,X1360)
| ~ present(skc12,X1360)
| ~ think_believe_consider(skc12,X1360)
| ~ state(skc12,skc9)
| ~ of(skc12,X1362,skc10)
| ~ vincent_forename(skc12,X1362)
| ~ forename(skc12,X1362)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1360,skc10)
| ~ smoke(X1361,X1363)
| ~ present(X1361,X1363)
| ~ agent(X1361,X1363,skc10)
| ~ event(X1361,X1363)
| ~ jules_forename(skc12,X1362)
| ~ actual_world(skc12)
| man(X1359,skf4(X1359)) ),
inference(factor,[status(thm)],[c590]) ).
cnf(c1054,plain,
( ~ proposition(skc12,X1513)
| ~ accessible_world(skc12,X1513)
| ~ think_believe_consider(skc12,X1514)
| ~ present(skc12,X1514)
| ~ event(skc12,X1514)
| ~ theme(skc12,X1514,X1513)
| ~ vincent_forename(skc12,X1515)
| ~ forename(skc12,X1515)
| ~ agent(skc12,X1514,X1510)
| ~ man(skc12,X1510)
| ~ of(skc12,X1515,X1510)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1511,skc12)
| ~ event(skc12,X1511)
| ~ present(skc12,X1511)
| ~ think_believe_consider(skc12,X1511)
| ~ state(skc12,skc9)
| ~ of(skc12,X1512,skc10)
| ~ vincent_forename(skc12,X1512)
| ~ forename(skc12,X1512)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1511,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ jules_forename(skc12,X1512)
| ~ actual_world(skc12)
| man(X1513,skf4(X1513)) ),
inference(resolution,[status(thm)],[c923,c385]) ).
cnf(c1097,plain,
( ~ proposition(skc12,X1651)
| ~ accessible_world(skc12,X1651)
| ~ think_believe_consider(skc12,X1650)
| ~ present(skc12,X1650)
| ~ event(skc12,X1650)
| ~ theme(skc12,X1650,X1651)
| ~ vincent_forename(skc12,X1649)
| ~ forename(skc12,X1649)
| ~ agent(skc12,X1650,X1653)
| ~ man(skc12,X1653)
| ~ of(skc12,X1649,X1653)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1654,skc12)
| ~ event(skc12,X1654)
| ~ present(skc12,X1654)
| ~ think_believe_consider(skc12,X1654)
| ~ state(skc12,skc9)
| ~ of(skc12,X1652,skc10)
| ~ vincent_forename(skc12,X1652)
| ~ forename(skc12,X1652)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1654,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ jules_forename(skc12,X1652)
| ~ actual_world(skc12)
| man(X1651,skf4(X1651)) ),
inference(resolution,[status(thm)],[c1054,c360]) ).
cnf(c1134,plain,
( ~ proposition(skc12,X1658)
| ~ accessible_world(skc12,X1658)
| ~ think_believe_consider(skc12,X1660)
| ~ present(skc12,X1660)
| ~ event(skc12,X1660)
| ~ theme(skc12,X1660,X1658)
| ~ vincent_forename(skc12,X1656)
| ~ forename(skc12,X1656)
| ~ agent(skc12,X1660,X1657)
| ~ man(skc12,X1657)
| ~ of(skc12,X1656,X1657)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1659,skc12)
| ~ event(skc12,X1659)
| ~ present(skc12,X1659)
| ~ think_believe_consider(skc12,X1659)
| ~ state(skc12,skc9)
| ~ of(skc12,X1655,skc10)
| ~ vincent_forename(skc12,X1655)
| ~ forename(skc12,X1655)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1659,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ jules_forename(skc12,X1655)
| ~ actual_world(skc12)
| man(X1658,skf4(X1658)) ),
inference(resolution,[status(thm)],[c1097,c371]) ).
cnf(c1135,plain,
( ~ proposition(skc12,X1669)
| ~ accessible_world(skc12,X1669)
| ~ think_believe_consider(skc12,X1665)
| ~ present(skc12,X1665)
| ~ event(skc12,X1665)
| ~ theme(skc12,X1665,X1669)
| ~ vincent_forename(skc12,X1666)
| ~ forename(skc12,X1666)
| ~ agent(skc12,X1665,X1667)
| ~ man(skc12,X1667)
| ~ of(skc12,X1666,X1667)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1670,skc12)
| ~ event(skc12,X1670)
| ~ present(skc12,X1670)
| ~ think_believe_consider(skc12,X1670)
| ~ state(skc12,skc9)
| ~ of(skc12,X1668,skc10)
| ~ vincent_forename(skc12,X1668)
| ~ forename(skc12,X1668)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1670,skc10)
| ~ jules_forename(skc12,X1668)
| ~ actual_world(skc12)
| man(X1669,skf4(X1669)) ),
inference(resolution,[status(thm)],[c1134,c359]) ).
cnf(c1137,plain,
( ~ proposition(skc12,X1676)
| ~ accessible_world(skc12,X1676)
| ~ think_believe_consider(skc12,X1675)
| ~ present(skc12,X1675)
| ~ event(skc12,X1675)
| ~ theme(skc12,X1675,X1676)
| ~ vincent_forename(skc12,X1677)
| ~ forename(skc12,X1677)
| ~ agent(skc12,X1675,X1679)
| ~ man(skc12,X1679)
| ~ of(skc12,X1677,X1679)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1678,skc10)
| ~ vincent_forename(skc12,X1678)
| ~ forename(skc12,X1678)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1678)
| ~ actual_world(skc12)
| man(X1676,skf4(X1676)) ),
inference(resolution,[status(thm)],[c1135,c385]) ).
cnf(c1138,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1680)
| ~ forename(skc12,X1680)
| ~ agent(skc12,skf2(skc10),X1682)
| ~ man(skc12,X1682)
| ~ of(skc12,X1680,X1682)
| ~ state(skc12,skc9)
| ~ of(skc12,X1681,skc10)
| ~ vincent_forename(skc12,X1681)
| ~ forename(skc12,X1681)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1681)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1137]) ).
cnf(c1139,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1684)
| ~ forename(skc12,X1684)
| ~ man(skc12,skc10)
| ~ of(skc12,X1684,skc10)
| ~ state(skc12,skc9)
| ~ of(skc12,X1683,skc10)
| ~ vincent_forename(skc12,X1683)
| ~ forename(skc12,X1683)
| ~ jules_forename(skc12,X1683)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1138,c385]) ).
cnf(c397,plain,
( ~ proposition(skc8,X678)
| ~ accessible_world(skc8,X678)
| ~ think_believe_consider(skc8,X673)
| ~ present(skc8,X673)
| ~ event(skc8,X673)
| ~ theme(skc8,X673,X678)
| ~ vincent_forename(skc8,X674)
| ~ forename(skc8,X674)
| ~ agent(skc8,X673,X677)
| ~ man(skc8,X677)
| ~ of(skc8,X674,X677)
| ~ accessible_world(skc8,X681)
| ~ proposition(skc8,X681)
| ~ theme(skc8,X675,X681)
| ~ event(skc8,X675)
| ~ present(skc8,X675)
| ~ think_believe_consider(skc8,X675)
| ~ state(skc8,skc9)
| ~ of(skc8,X680,skc10)
| ~ vincent_forename(skc8,X680)
| ~ forename(skc8,X680)
| ~ man(skc8,skc10)
| ~ agent(skc8,X675,skc10)
| ~ smoke(X681,X679)
| ~ present(X681,X679)
| ~ agent(X681,X679,skc10)
| ~ event(X681,X679)
| ~ forename(skc8,X676)
| ~ jules_forename(skc8,X676)
| ~ of(skc8,X676,skc10)
| ~ actual_world(skc8)
| man(X678,skf4(X678)) ),
inference(resolution,[status(thm)],[clause94,clause89]) ).
cnf(c699,plain,
( ~ proposition(skc8,X1276)
| ~ accessible_world(skc8,X1276)
| ~ think_believe_consider(skc8,X1273)
| ~ present(skc8,X1273)
| ~ event(skc8,X1273)
| ~ theme(skc8,X1273,X1276)
| ~ vincent_forename(skc8,X1275)
| ~ forename(skc8,X1275)
| ~ agent(skc8,X1273,X1278)
| ~ man(skc8,X1278)
| ~ of(skc8,X1275,X1278)
| ~ accessible_world(skc8,X1277)
| ~ proposition(skc8,X1277)
| ~ theme(skc8,X1274,X1277)
| ~ event(skc8,X1274)
| ~ present(skc8,X1274)
| ~ think_believe_consider(skc8,X1274)
| ~ state(skc8,skc9)
| ~ of(skc8,X1280,skc10)
| ~ vincent_forename(skc8,X1280)
| ~ forename(skc8,X1280)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1274,skc10)
| ~ smoke(X1277,X1279)
| ~ present(X1277,X1279)
| ~ agent(X1277,X1279,skc10)
| ~ event(X1277,X1279)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1276,skf4(X1276)) ),
inference(resolution,[status(thm)],[c397,clause88]) ).
cnf(c1037,plain,
( ~ proposition(skc8,X1463)
| ~ accessible_world(skc8,X1463)
| ~ think_believe_consider(skc8,X1467)
| ~ present(skc8,X1467)
| ~ event(skc8,X1467)
| ~ theme(skc8,X1467,X1463)
| ~ vincent_forename(skc8,X1466)
| ~ forename(skc8,X1466)
| ~ agent(skc8,X1467,X1462)
| ~ man(skc8,X1462)
| ~ of(skc8,X1466,X1462)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1464,skc12)
| ~ event(skc8,X1464)
| ~ present(skc8,X1464)
| ~ think_believe_consider(skc8,X1464)
| ~ state(skc8,skc9)
| ~ of(skc8,X1465,skc10)
| ~ vincent_forename(skc8,X1465)
| ~ forename(skc8,X1465)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1464,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1463,skf4(X1463)) ),
inference(resolution,[status(thm)],[c699,c385]) ).
cnf(c1080,plain,
( ~ proposition(skc8,X1593)
| ~ accessible_world(skc8,X1593)
| ~ think_believe_consider(skc8,X1596)
| ~ present(skc8,X1596)
| ~ event(skc8,X1596)
| ~ theme(skc8,X1596,X1593)
| ~ vincent_forename(skc8,X1591)
| ~ forename(skc8,X1591)
| ~ agent(skc8,X1596,X1594)
| ~ man(skc8,X1594)
| ~ of(skc8,X1591,X1594)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1592,skc12)
| ~ event(skc8,X1592)
| ~ present(skc8,X1592)
| ~ think_believe_consider(skc8,X1592)
| ~ state(skc8,skc9)
| ~ of(skc8,X1595,skc10)
| ~ vincent_forename(skc8,X1595)
| ~ forename(skc8,X1595)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1592,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1593,skf4(X1593)) ),
inference(resolution,[status(thm)],[c1037,c360]) ).
cnf(c1120,plain,
( ~ proposition(skc8,X1611)
| ~ accessible_world(skc8,X1611)
| ~ think_believe_consider(skc8,X1609)
| ~ present(skc8,X1609)
| ~ event(skc8,X1609)
| ~ theme(skc8,X1609,X1611)
| ~ vincent_forename(skc8,X1612)
| ~ forename(skc8,X1612)
| ~ agent(skc8,X1609,X1608)
| ~ man(skc8,X1608)
| ~ of(skc8,X1612,X1608)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1610,skc12)
| ~ event(skc8,X1610)
| ~ present(skc8,X1610)
| ~ think_believe_consider(skc8,X1610)
| ~ state(skc8,skc9)
| ~ of(skc8,X1607,skc10)
| ~ vincent_forename(skc8,X1607)
| ~ forename(skc8,X1607)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1610,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1611,skf4(X1611)) ),
inference(resolution,[status(thm)],[c1080,c371]) ).
cnf(c1122,plain,
( ~ proposition(skc8,X1615)
| ~ accessible_world(skc8,X1615)
| ~ think_believe_consider(skc8,X1614)
| ~ present(skc8,X1614)
| ~ event(skc8,X1614)
| ~ theme(skc8,X1614,X1615)
| ~ vincent_forename(skc8,X1618)
| ~ forename(skc8,X1618)
| ~ agent(skc8,X1614,X1613)
| ~ man(skc8,X1613)
| ~ of(skc8,X1618,X1613)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1616,skc12)
| ~ event(skc8,X1616)
| ~ present(skc8,X1616)
| ~ think_believe_consider(skc8,X1616)
| ~ state(skc8,skc9)
| ~ of(skc8,X1617,skc10)
| ~ vincent_forename(skc8,X1617)
| ~ forename(skc8,X1617)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1616,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1615,skf4(X1615)) ),
inference(resolution,[status(thm)],[c1120,c359]) ).
cnf(c1123,plain,
( ~ proposition(skc8,X1620)
| ~ accessible_world(skc8,X1620)
| ~ think_believe_consider(skc8,X1619)
| ~ present(skc8,X1619)
| ~ event(skc8,X1619)
| ~ theme(skc8,X1619,X1620)
| ~ vincent_forename(skc8,X1622)
| ~ forename(skc8,X1622)
| ~ agent(skc8,X1619,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1622,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1619,skc12)
| ~ state(skc8,skc9)
| ~ of(skc8,X1621,skc10)
| ~ vincent_forename(skc8,X1621)
| ~ forename(skc8,X1621)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1620,skf4(X1620)) ),
inference(factor,[status(thm)],[c1122]) ).
cnf(c1124,plain,
( ~ proposition(skc8,X1628)
| ~ accessible_world(skc8,X1628)
| ~ think_believe_consider(skc8,X1630)
| ~ present(skc8,X1630)
| ~ event(skc8,X1630)
| ~ theme(skc8,X1630,X1628)
| ~ vincent_forename(skc8,X1629)
| ~ forename(skc8,X1629)
| ~ agent(skc8,X1630,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1629,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1630,skc12)
| ~ state(skc8,skc9)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1628,skf4(X1628)) ),
inference(factor,[status(thm)],[c1123]) ).
cnf(c1128,plain,
( ~ proposition(skc8,X1635)
| ~ accessible_world(skc8,X1635)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1635)
| ~ vincent_forename(skc8,X1634)
| ~ forename(skc8,X1634)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1634,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ state(skc8,skc9)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1635,skf4(X1635)) ),
inference(resolution,[status(thm)],[c1124,clause87]) ).
cnf(c1127,plain,
( ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ think_believe_consider(skc8,X1631)
| ~ present(skc8,X1631)
| ~ event(skc8,X1631)
| ~ theme(skc8,X1631,skc12)
| ~ vincent_forename(skc8,X1632)
| ~ forename(skc8,X1632)
| ~ agent(skc8,X1631,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1632,skc10)
| ~ state(skc8,skc9)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1124]) ).
cnf(c698,plain,
( ~ proposition(skc8,X1253)
| ~ accessible_world(skc8,X1253)
| ~ think_believe_consider(skc8,X1250)
| ~ present(skc8,X1250)
| ~ event(skc8,X1250)
| ~ theme(skc8,X1250,X1253)
| ~ vincent_forename(skc8,X1252)
| ~ forename(skc8,X1252)
| ~ agent(skc8,X1250,X1255)
| ~ man(skc8,X1255)
| ~ of(skc8,X1252,X1255)
| ~ accessible_world(skc8,X1254)
| ~ proposition(skc8,X1254)
| ~ theme(skc8,X1251,X1254)
| ~ event(skc8,X1251)
| ~ present(skc8,X1251)
| ~ think_believe_consider(skc8,X1251)
| ~ state(skc8,skc9)
| ~ of(skc8,X1257,skc10)
| ~ vincent_forename(skc8,X1257)
| ~ forename(skc8,X1257)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1251,skc10)
| ~ smoke(X1254,X1256)
| ~ present(X1254,X1256)
| ~ agent(X1254,X1256,skc10)
| ~ event(X1254,X1256)
| ~ jules_forename(skc8,X1257)
| ~ actual_world(skc8)
| man(X1253,skf4(X1253)) ),
inference(factor,[status(thm)],[c397]) ).
cnf(c1029,plain,
( ~ proposition(skc8,X1427)
| ~ accessible_world(skc8,X1427)
| ~ think_believe_consider(skc8,X1424)
| ~ present(skc8,X1424)
| ~ event(skc8,X1424)
| ~ theme(skc8,X1424,X1427)
| ~ vincent_forename(skc8,X1425)
| ~ forename(skc8,X1425)
| ~ agent(skc8,X1424,X1429)
| ~ man(skc8,X1429)
| ~ of(skc8,X1425,X1429)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1428,skc12)
| ~ event(skc8,X1428)
| ~ present(skc8,X1428)
| ~ think_believe_consider(skc8,X1428)
| ~ state(skc8,skc9)
| ~ of(skc8,X1426,skc10)
| ~ vincent_forename(skc8,X1426)
| ~ forename(skc8,X1426)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1428,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ jules_forename(skc8,X1426)
| ~ actual_world(skc8)
| man(X1427,skf4(X1427)) ),
inference(resolution,[status(thm)],[c698,c385]) ).
cnf(c1071,plain,
( ~ proposition(skc8,X1568)
| ~ accessible_world(skc8,X1568)
| ~ think_believe_consider(skc8,X1573)
| ~ present(skc8,X1573)
| ~ event(skc8,X1573)
| ~ theme(skc8,X1573,X1568)
| ~ vincent_forename(skc8,X1571)
| ~ forename(skc8,X1571)
| ~ agent(skc8,X1573,X1572)
| ~ man(skc8,X1572)
| ~ of(skc8,X1571,X1572)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1569,skc12)
| ~ event(skc8,X1569)
| ~ present(skc8,X1569)
| ~ think_believe_consider(skc8,X1569)
| ~ state(skc8,skc9)
| ~ of(skc8,X1570,skc10)
| ~ vincent_forename(skc8,X1570)
| ~ forename(skc8,X1570)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1569,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ jules_forename(skc8,X1570)
| ~ actual_world(skc8)
| man(X1568,skf4(X1568)) ),
inference(resolution,[status(thm)],[c1029,c360]) ).
cnf(c1117,plain,
( ~ proposition(skc8,X1587)
| ~ accessible_world(skc8,X1587)
| ~ think_believe_consider(skc8,X1589)
| ~ present(skc8,X1589)
| ~ event(skc8,X1589)
| ~ theme(skc8,X1589,X1587)
| ~ vincent_forename(skc8,X1585)
| ~ forename(skc8,X1585)
| ~ agent(skc8,X1589,X1588)
| ~ man(skc8,X1588)
| ~ of(skc8,X1585,X1588)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1590,skc12)
| ~ event(skc8,X1590)
| ~ present(skc8,X1590)
| ~ think_believe_consider(skc8,X1590)
| ~ state(skc8,skc9)
| ~ of(skc8,X1586,skc10)
| ~ vincent_forename(skc8,X1586)
| ~ forename(skc8,X1586)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1590,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ jules_forename(skc8,X1586)
| ~ actual_world(skc8)
| man(X1587,skf4(X1587)) ),
inference(resolution,[status(thm)],[c1071,c371]) ).
cnf(c1119,plain,
( ~ proposition(skc8,X1600)
| ~ accessible_world(skc8,X1600)
| ~ think_believe_consider(skc8,X1602)
| ~ present(skc8,X1602)
| ~ event(skc8,X1602)
| ~ theme(skc8,X1602,X1600)
| ~ vincent_forename(skc8,X1599)
| ~ forename(skc8,X1599)
| ~ agent(skc8,X1602,X1598)
| ~ man(skc8,X1598)
| ~ of(skc8,X1599,X1598)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1597,skc12)
| ~ event(skc8,X1597)
| ~ present(skc8,X1597)
| ~ think_believe_consider(skc8,X1597)
| ~ state(skc8,skc9)
| ~ of(skc8,X1601,skc10)
| ~ vincent_forename(skc8,X1601)
| ~ forename(skc8,X1601)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1597,skc10)
| ~ jules_forename(skc8,X1601)
| ~ actual_world(skc8)
| man(X1600,skf4(X1600)) ),
inference(resolution,[status(thm)],[c1117,c359]) ).
cnf(c922,plain,
( ~ proposition(skc12,X1343)
| ~ accessible_world(skc12,X1343)
| ~ think_believe_consider(skc12,X1340)
| ~ present(skc12,X1340)
| ~ event(skc12,X1340)
| ~ theme(skc12,X1340,X1343)
| ~ vincent_forename(skc12,X1345)
| ~ forename(skc12,X1345)
| ~ agent(skc12,X1340,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1345,skc10)
| ~ accessible_world(skc12,X1344)
| ~ proposition(skc12,X1344)
| ~ theme(skc12,X1342,X1344)
| ~ event(skc12,X1342)
| ~ present(skc12,X1342)
| ~ think_believe_consider(skc12,X1342)
| ~ state(skc12,skc9)
| ~ of(skc12,X1341,skc10)
| ~ vincent_forename(skc12,X1341)
| ~ forename(skc12,X1341)
| ~ agent(skc12,X1342,skc10)
| ~ smoke(X1344,X1346)
| ~ present(X1344,X1346)
| ~ agent(X1344,X1346,skc10)
| ~ event(X1344,X1346)
| ~ jules_forename(skc12,X1345)
| ~ actual_world(skc12)
| man(X1343,skf4(X1343)) ),
inference(factor,[status(thm)],[c590]) ).
cnf(c1047,plain,
( ~ proposition(skc12,X1496)
| ~ accessible_world(skc12,X1496)
| ~ think_believe_consider(skc12,X1494)
| ~ present(skc12,X1494)
| ~ event(skc12,X1494)
| ~ theme(skc12,X1494,X1496)
| ~ vincent_forename(skc12,X1493)
| ~ forename(skc12,X1493)
| ~ agent(skc12,X1494,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1493,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1497,skc12)
| ~ event(skc12,X1497)
| ~ present(skc12,X1497)
| ~ think_believe_consider(skc12,X1497)
| ~ state(skc12,skc9)
| ~ of(skc12,X1495,skc10)
| ~ vincent_forename(skc12,X1495)
| ~ forename(skc12,X1495)
| ~ agent(skc12,X1497,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ jules_forename(skc12,X1493)
| ~ actual_world(skc12)
| man(X1496,skf4(X1496)) ),
inference(resolution,[status(thm)],[c922,c385]) ).
cnf(c1088,plain,
( ~ proposition(skc12,X1540)
| ~ accessible_world(skc12,X1540)
| ~ think_believe_consider(skc12,X1537)
| ~ present(skc12,X1537)
| ~ event(skc12,X1537)
| ~ theme(skc12,X1537,X1540)
| ~ vincent_forename(skc12,X1536)
| ~ forename(skc12,X1536)
| ~ agent(skc12,X1537,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1536,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1539,skc12)
| ~ event(skc12,X1539)
| ~ present(skc12,X1539)
| ~ think_believe_consider(skc12,X1539)
| ~ state(skc12,skc9)
| ~ of(skc12,X1538,skc10)
| ~ vincent_forename(skc12,X1538)
| ~ forename(skc12,X1538)
| ~ agent(skc12,X1539,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ jules_forename(skc12,X1536)
| ~ actual_world(skc12)
| man(X1540,skf4(X1540)) ),
inference(resolution,[status(thm)],[c1047,c360]) ).
cnf(c1105,plain,
( ~ proposition(skc12,X1541)
| ~ accessible_world(skc12,X1541)
| ~ think_believe_consider(skc12,X1544)
| ~ present(skc12,X1544)
| ~ event(skc12,X1544)
| ~ theme(skc12,X1544,X1541)
| ~ vincent_forename(skc12,X1542)
| ~ forename(skc12,X1542)
| ~ agent(skc12,X1544,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1542,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1543,skc12)
| ~ event(skc12,X1543)
| ~ present(skc12,X1543)
| ~ think_believe_consider(skc12,X1543)
| ~ state(skc12,skc9)
| ~ of(skc12,X1545,skc10)
| ~ vincent_forename(skc12,X1545)
| ~ forename(skc12,X1545)
| ~ agent(skc12,X1543,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ jules_forename(skc12,X1542)
| ~ actual_world(skc12)
| man(X1541,skf4(X1541)) ),
inference(resolution,[status(thm)],[c1088,c371]) ).
cnf(c1106,plain,
( ~ proposition(skc12,X1548)
| ~ accessible_world(skc12,X1548)
| ~ think_believe_consider(skc12,X1550)
| ~ present(skc12,X1550)
| ~ event(skc12,X1550)
| ~ theme(skc12,X1550,X1548)
| ~ vincent_forename(skc12,X1549)
| ~ forename(skc12,X1549)
| ~ agent(skc12,X1550,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1549,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1546,skc12)
| ~ event(skc12,X1546)
| ~ present(skc12,X1546)
| ~ think_believe_consider(skc12,X1546)
| ~ state(skc12,skc9)
| ~ of(skc12,X1547,skc10)
| ~ vincent_forename(skc12,X1547)
| ~ forename(skc12,X1547)
| ~ agent(skc12,X1546,skc10)
| ~ jules_forename(skc12,X1549)
| ~ actual_world(skc12)
| man(X1548,skf4(X1548)) ),
inference(resolution,[status(thm)],[c1105,c359]) ).
cnf(c1108,plain,
( ~ proposition(skc12,X1581)
| ~ accessible_world(skc12,X1581)
| ~ think_believe_consider(skc12,X1580)
| ~ present(skc12,X1580)
| ~ event(skc12,X1580)
| ~ theme(skc12,X1580,X1581)
| ~ vincent_forename(skc12,X1579)
| ~ forename(skc12,X1579)
| ~ agent(skc12,X1580,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1579,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1582,skc10)
| ~ vincent_forename(skc12,X1582)
| ~ forename(skc12,X1582)
| ~ jules_forename(skc12,X1579)
| ~ actual_world(skc12)
| man(X1581,skf4(X1581)) ),
inference(resolution,[status(thm)],[c1106,c385]) ).
cnf(c1107,plain,
( ~ proposition(skc12,X1552)
| ~ accessible_world(skc12,X1552)
| ~ think_believe_consider(skc12,X1554)
| ~ present(skc12,X1554)
| ~ event(skc12,X1554)
| ~ theme(skc12,X1554,X1552)
| ~ vincent_forename(skc12,X1551)
| ~ forename(skc12,X1551)
| ~ agent(skc12,X1554,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1551,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1554,skc12)
| ~ state(skc12,skc9)
| ~ of(skc12,X1553,skc10)
| ~ vincent_forename(skc12,X1553)
| ~ forename(skc12,X1553)
| ~ jules_forename(skc12,X1551)
| ~ actual_world(skc12)
| man(X1552,skf4(X1552)) ),
inference(factor,[status(thm)],[c1106]) ).
cnf(c1109,plain,
( ~ proposition(skc12,X1555)
| ~ accessible_world(skc12,X1555)
| ~ think_believe_consider(skc12,X1557)
| ~ present(skc12,X1557)
| ~ event(skc12,X1557)
| ~ theme(skc12,X1557,X1555)
| ~ vincent_forename(skc12,X1556)
| ~ forename(skc12,X1556)
| ~ agent(skc12,X1557,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1556,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1557,skc12)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1556)
| ~ actual_world(skc12)
| man(X1555,skf4(X1555)) ),
inference(factor,[status(thm)],[c1107]) ).
cnf(c1112,plain,
( ~ proposition(skc12,X1565)
| ~ accessible_world(skc12,X1565)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1565)
| ~ vincent_forename(skc12,X1566)
| ~ forename(skc12,X1566)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1566,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1566)
| ~ actual_world(skc12)
| man(X1565,skf4(X1565)) ),
inference(resolution,[status(thm)],[c1109,c571]) ).
cnf(c1116,plain,
( ~ proposition(skc12,X1567)
| ~ accessible_world(skc12,X1567)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1567)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1567,skf4(X1567)) ),
inference(resolution,[status(thm)],[c1112,c580]) ).
cnf(c1111,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1562)
| ~ present(skc12,X1562)
| ~ event(skc12,X1562)
| ~ theme(skc12,X1562,skc12)
| ~ vincent_forename(skc12,X1563)
| ~ forename(skc12,X1563)
| ~ agent(skc12,X1562,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1563,skc10)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1563)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1109]) ).
cnf(c1114,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1564)
| ~ present(skc12,X1564)
| ~ event(skc12,X1564)
| ~ theme(skc12,X1564,skc12)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ agent(skc12,X1564,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1111,c580]) ).
cnf(c1115,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1114,c385]) ).
cnf(c1060,plain,
( ~ proposition(skc12,X1419)
| ~ accessible_world(skc12,X1419)
| ~ think_believe_consider(skc12,X1422)
| ~ present(skc12,X1422)
| ~ event(skc12,X1422)
| ~ theme(skc12,X1422,X1419)
| ~ vincent_forename(skc12,X1420)
| ~ forename(skc12,X1420)
| ~ agent(skc12,X1422,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1420,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1423,skc12)
| ~ event(skc12,X1423)
| ~ present(skc12,X1423)
| ~ think_believe_consider(skc12,X1423)
| ~ state(skc12,skc9)
| ~ of(skc12,X1421,skc10)
| ~ vincent_forename(skc12,X1421)
| ~ forename(skc12,X1421)
| ~ agent(skc12,X1423,skc10)
| ~ smoke(skc12,X1422)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1419,skf4(X1419)) ),
inference(factor,[status(thm)],[c924]) ).
cnf(c1070,plain,
( ~ proposition(skc12,X1559)
| ~ accessible_world(skc12,X1559)
| ~ think_believe_consider(skc12,X1558)
| ~ present(skc12,X1558)
| ~ event(skc12,X1558)
| ~ theme(skc12,X1558,X1559)
| ~ vincent_forename(skc12,X1560)
| ~ forename(skc12,X1560)
| ~ agent(skc12,X1558,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1560,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1561,skc10)
| ~ vincent_forename(skc12,X1561)
| ~ forename(skc12,X1561)
| ~ smoke(skc12,X1558)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1559,skf4(X1559)) ),
inference(resolution,[status(thm)],[c1060,c385]) ).
cnf(c697,plain,
( ~ proposition(skc8,X1245)
| ~ accessible_world(skc8,X1245)
| ~ think_believe_consider(skc8,X1243)
| ~ present(skc8,X1243)
| ~ event(skc8,X1243)
| ~ theme(skc8,X1243,X1245)
| ~ vincent_forename(skc8,X1248)
| ~ forename(skc8,X1248)
| ~ agent(skc8,X1243,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1248,skc10)
| ~ accessible_world(skc8,X1246)
| ~ proposition(skc8,X1246)
| ~ theme(skc8,X1244,X1246)
| ~ event(skc8,X1244)
| ~ present(skc8,X1244)
| ~ think_believe_consider(skc8,X1244)
| ~ state(skc8,skc9)
| ~ of(skc8,X1249,skc10)
| ~ vincent_forename(skc8,X1249)
| ~ forename(skc8,X1249)
| ~ agent(skc8,X1244,skc10)
| ~ smoke(X1246,X1247)
| ~ present(X1246,X1247)
| ~ agent(X1246,X1247,skc10)
| ~ event(X1246,X1247)
| ~ jules_forename(skc8,X1248)
| ~ actual_world(skc8)
| man(X1245,skf4(X1245)) ),
inference(factor,[status(thm)],[c397]) ).
cnf(c1026,plain,
( ~ proposition(skc8,X1398)
| ~ accessible_world(skc8,X1398)
| ~ think_believe_consider(skc8,X1401)
| ~ present(skc8,X1401)
| ~ event(skc8,X1401)
| ~ theme(skc8,X1401,X1398)
| ~ vincent_forename(skc8,X1399)
| ~ forename(skc8,X1399)
| ~ agent(skc8,X1401,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1399,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1402,skc12)
| ~ event(skc8,X1402)
| ~ present(skc8,X1402)
| ~ think_believe_consider(skc8,X1402)
| ~ state(skc8,skc9)
| ~ of(skc8,X1400,skc10)
| ~ vincent_forename(skc8,X1400)
| ~ forename(skc8,X1400)
| ~ agent(skc8,X1402,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ jules_forename(skc8,X1399)
| ~ actual_world(skc8)
| man(X1398,skf4(X1398)) ),
inference(resolution,[status(thm)],[c697,c385]) ).
cnf(c1065,plain,
( ~ proposition(skc8,X1480)
| ~ accessible_world(skc8,X1480)
| ~ think_believe_consider(skc8,X1479)
| ~ present(skc8,X1479)
| ~ event(skc8,X1479)
| ~ theme(skc8,X1479,X1480)
| ~ vincent_forename(skc8,X1481)
| ~ forename(skc8,X1481)
| ~ agent(skc8,X1479,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1481,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1478,skc12)
| ~ event(skc8,X1478)
| ~ present(skc8,X1478)
| ~ think_believe_consider(skc8,X1478)
| ~ state(skc8,skc9)
| ~ of(skc8,X1482,skc10)
| ~ vincent_forename(skc8,X1482)
| ~ forename(skc8,X1482)
| ~ agent(skc8,X1478,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ jules_forename(skc8,X1481)
| ~ actual_world(skc8)
| man(X1480,skf4(X1480)) ),
inference(resolution,[status(thm)],[c1026,c360]) ).
cnf(c1083,plain,
( ~ proposition(skc8,X1483)
| ~ accessible_world(skc8,X1483)
| ~ think_believe_consider(skc8,X1487)
| ~ present(skc8,X1487)
| ~ event(skc8,X1487)
| ~ theme(skc8,X1487,X1483)
| ~ vincent_forename(skc8,X1486)
| ~ forename(skc8,X1486)
| ~ agent(skc8,X1487,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1486,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1484,skc12)
| ~ event(skc8,X1484)
| ~ present(skc8,X1484)
| ~ think_believe_consider(skc8,X1484)
| ~ state(skc8,skc9)
| ~ of(skc8,X1485,skc10)
| ~ vincent_forename(skc8,X1485)
| ~ forename(skc8,X1485)
| ~ agent(skc8,X1484,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ jules_forename(skc8,X1486)
| ~ actual_world(skc8)
| man(X1483,skf4(X1483)) ),
inference(resolution,[status(thm)],[c1065,c371]) ).
cnf(c1084,plain,
( ~ proposition(skc8,X1491)
| ~ accessible_world(skc8,X1491)
| ~ think_believe_consider(skc8,X1488)
| ~ present(skc8,X1488)
| ~ event(skc8,X1488)
| ~ theme(skc8,X1488,X1491)
| ~ vincent_forename(skc8,X1492)
| ~ forename(skc8,X1492)
| ~ agent(skc8,X1488,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1492,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1490,skc12)
| ~ event(skc8,X1490)
| ~ present(skc8,X1490)
| ~ think_believe_consider(skc8,X1490)
| ~ state(skc8,skc9)
| ~ of(skc8,X1489,skc10)
| ~ vincent_forename(skc8,X1489)
| ~ forename(skc8,X1489)
| ~ agent(skc8,X1490,skc10)
| ~ jules_forename(skc8,X1492)
| ~ actual_world(skc8)
| man(X1491,skf4(X1491)) ),
inference(resolution,[status(thm)],[c1083,c359]) ).
cnf(c1085,plain,
( ~ proposition(skc8,X1499)
| ~ accessible_world(skc8,X1499)
| ~ think_believe_consider(skc8,X1500)
| ~ present(skc8,X1500)
| ~ event(skc8,X1500)
| ~ theme(skc8,X1500,X1499)
| ~ vincent_forename(skc8,X1498)
| ~ forename(skc8,X1498)
| ~ agent(skc8,X1500,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1498,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1500,skc12)
| ~ state(skc8,skc9)
| ~ of(skc8,X1501,skc10)
| ~ vincent_forename(skc8,X1501)
| ~ forename(skc8,X1501)
| ~ jules_forename(skc8,X1498)
| ~ actual_world(skc8)
| man(X1499,skf4(X1499)) ),
inference(factor,[status(thm)],[c1084]) ).
cnf(c1089,plain,
( ~ proposition(skc8,X1502)
| ~ accessible_world(skc8,X1502)
| ~ think_believe_consider(skc8,X1503)
| ~ present(skc8,X1503)
| ~ event(skc8,X1503)
| ~ theme(skc8,X1503,X1502)
| ~ vincent_forename(skc8,X1504)
| ~ forename(skc8,X1504)
| ~ agent(skc8,X1503,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1504,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1503,skc12)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1504)
| ~ actual_world(skc8)
| man(X1502,skf4(X1502)) ),
inference(factor,[status(thm)],[c1085]) ).
cnf(c1092,plain,
( ~ proposition(skc8,X1508)
| ~ accessible_world(skc8,X1508)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1508)
| ~ vincent_forename(skc8,X1509)
| ~ forename(skc8,X1509)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1509,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1509)
| ~ actual_world(skc8)
| man(X1508,skf4(X1508)) ),
inference(resolution,[status(thm)],[c1089,clause87]) ).
cnf(c1094,plain,
( ~ proposition(skc8,X1516)
| ~ accessible_world(skc8,X1516)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1516)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc8,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1516,skf4(X1516)) ),
inference(resolution,[status(thm)],[c1092,clause88]) ).
cnf(c1091,plain,
( ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ think_believe_consider(skc8,X1505)
| ~ present(skc8,X1505)
| ~ event(skc8,X1505)
| ~ theme(skc8,X1505,skc12)
| ~ vincent_forename(skc8,X1506)
| ~ forename(skc8,X1506)
| ~ agent(skc8,X1505,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1506,skc10)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1506)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1089]) ).
cnf(c1093,plain,
( ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ think_believe_consider(skc8,X1507)
| ~ present(skc8,X1507)
| ~ event(skc8,X1507)
| ~ theme(skc8,X1507,skc12)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ agent(skc8,X1507,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1091,clause88]) ).
cnf(c1036,plain,
( ~ proposition(skc8,X1443)
| ~ accessible_world(skc8,X1443)
| ~ think_believe_consider(skc8,X1446)
| ~ present(skc8,X1446)
| ~ event(skc8,X1446)
| ~ theme(skc8,X1446,X1443)
| ~ vincent_forename(skc8,X1445)
| ~ forename(skc8,X1445)
| ~ agent(skc8,X1446,X1442)
| ~ man(skc8,X1442)
| ~ of(skc8,X1445,X1442)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1447,skc8)
| ~ event(skc8,X1447)
| ~ present(skc8,X1447)
| ~ think_believe_consider(skc8,X1447)
| ~ state(skc8,skc9)
| ~ of(skc8,X1444,skc10)
| ~ vincent_forename(skc8,X1444)
| ~ forename(skc8,X1444)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1447,skc10)
| ~ smoke(skc8,X1447)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1443,skf4(X1443)) ),
inference(factor,[status(thm)],[c699]) ).
cnf(clause95,negated_conjecture,
( ~ proposition(X310,X307)
| ~ accessible_world(X310,X307)
| ~ smoke(X307,X306)
| ~ present(X307,X306)
| ~ agent(X307,X306,skf4(X307))
| ~ event(X307,X306)
| ~ think_believe_consider(X310,X301)
| ~ present(X310,X301)
| ~ event(X310,X301)
| ~ theme(X310,X301,X307)
| ~ vincent_forename(X310,X312)
| ~ forename(X310,X312)
| ~ agent(X310,X301,X303)
| ~ man(X310,X303)
| ~ of(X310,X312,X303)
| ~ accessible_world(X310,X308)
| ~ proposition(X310,X308)
| ~ theme(X310,X309,X308)
| ~ event(X310,X309)
| ~ present(X310,X309)
| ~ think_believe_consider(X310,X309)
| ~ state(X310,X300)
| ~ of(X310,X305,X302)
| ~ vincent_forename(X310,X305)
| ~ forename(X310,X305)
| ~ man(X310,X302)
| ~ be(X310,X300,X302,X302)
| ~ agent(X310,X309,X302)
| ~ smoke(X308,X304)
| ~ present(X308,X304)
| ~ agent(X308,X304,X302)
| ~ event(X308,X304)
| ~ forename(X310,X311)
| ~ jules_forename(X310,X311)
| ~ of(X310,X311,X302)
| ~ actual_world(X310) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
cnf(c589,plain,
( ~ proposition(skc12,X1038)
| ~ accessible_world(skc12,X1038)
| ~ smoke(X1038,X1040)
| ~ present(X1038,X1040)
| ~ agent(X1038,X1040,skf4(X1038))
| ~ event(X1038,X1040)
| ~ think_believe_consider(skc12,X1034)
| ~ present(skc12,X1034)
| ~ event(skc12,X1034)
| ~ theme(skc12,X1034,X1038)
| ~ vincent_forename(skc12,X1032)
| ~ forename(skc12,X1032)
| ~ agent(skc12,X1034,X1039)
| ~ man(skc12,X1039)
| ~ of(skc12,X1032,X1039)
| ~ accessible_world(skc12,X1037)
| ~ proposition(skc12,X1037)
| ~ theme(skc12,X1035,X1037)
| ~ event(skc12,X1035)
| ~ present(skc12,X1035)
| ~ think_believe_consider(skc12,X1035)
| ~ state(skc12,skc9)
| ~ of(skc12,X1031,skc10)
| ~ vincent_forename(skc12,X1031)
| ~ forename(skc12,X1031)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1035,skc10)
| ~ smoke(X1037,X1036)
| ~ present(X1037,X1036)
| ~ agent(X1037,X1036,skc10)
| ~ event(X1037,X1036)
| ~ forename(skc12,X1033)
| ~ jules_forename(skc12,X1033)
| ~ of(skc12,X1033,skc10)
| ~ actual_world(skc12) ),
inference(resolution,[status(thm)],[c587,clause95]) ).
cnf(c917,plain,
( ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ smoke(skc12,X1334)
| ~ present(skc12,X1334)
| ~ agent(skc12,X1334,skf4(skc12))
| ~ event(skc12,X1334)
| ~ think_believe_consider(skc12,X1334)
| ~ theme(skc12,X1334,skc12)
| ~ vincent_forename(skc12,X1332)
| ~ forename(skc12,X1332)
| ~ man(skc12,skf4(skc12))
| ~ of(skc12,X1332,skf4(skc12))
| ~ accessible_world(skc12,X1329)
| ~ proposition(skc12,X1329)
| ~ theme(skc12,X1335,X1329)
| ~ event(skc12,X1335)
| ~ present(skc12,X1335)
| ~ think_believe_consider(skc12,X1335)
| ~ state(skc12,skc9)
| ~ of(skc12,X1331,skc10)
| ~ vincent_forename(skc12,X1331)
| ~ forename(skc12,X1331)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1335,skc10)
| ~ smoke(X1329,X1333)
| ~ present(X1329,X1333)
| ~ agent(X1329,X1333,skc10)
| ~ event(X1329,X1333)
| ~ forename(skc12,X1330)
| ~ jules_forename(skc12,X1330)
| ~ of(skc12,X1330,skc10)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c589]) ).
cnf(c1035,plain,
( ~ proposition(skc8,X1315)
| ~ accessible_world(skc8,X1315)
| ~ think_believe_consider(skc8,X1319)
| ~ present(skc8,X1319)
| ~ event(skc8,X1319)
| ~ theme(skc8,X1319,X1315)
| ~ vincent_forename(skc8,X1318)
| ~ forename(skc8,X1318)
| ~ agent(skc8,X1319,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1318,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1316,skc8)
| ~ event(skc8,X1316)
| ~ present(skc8,X1316)
| ~ think_believe_consider(skc8,X1316)
| ~ state(skc8,skc9)
| ~ of(skc8,X1317,skc10)
| ~ vincent_forename(skc8,X1317)
| ~ forename(skc8,X1317)
| ~ agent(skc8,X1316,skc10)
| ~ smoke(skc8,X1319)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1315,skf4(X1315)) ),
inference(factor,[status(thm)],[c699]) ).
cnf(c1040,plain,
( ~ proposition(skc8,X1322)
| ~ accessible_world(skc8,X1322)
| ~ think_believe_consider(skc8,X1320)
| ~ present(skc8,X1320)
| ~ event(skc8,X1320)
| ~ theme(skc8,X1320,X1322)
| ~ vincent_forename(skc8,X1321)
| ~ forename(skc8,X1321)
| ~ agent(skc8,X1320,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1321,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1320,skc8)
| ~ state(skc8,skc9)
| ~ of(skc8,X1323,skc10)
| ~ vincent_forename(skc8,X1323)
| ~ forename(skc8,X1323)
| ~ smoke(skc8,X1320)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1322,skf4(X1322)) ),
inference(factor,[status(thm)],[c1035]) ).
cnf(c1041,plain,
( ~ proposition(skc8,X1325)
| ~ accessible_world(skc8,X1325)
| ~ think_believe_consider(skc8,X1326)
| ~ present(skc8,X1326)
| ~ event(skc8,X1326)
| ~ theme(skc8,X1326,X1325)
| ~ vincent_forename(skc8,X1324)
| ~ forename(skc8,X1324)
| ~ agent(skc8,X1326,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1324,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1326,skc8)
| ~ state(skc8,skc9)
| ~ smoke(skc8,X1326)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1325,skf4(X1325)) ),
inference(factor,[status(thm)],[c1040]) ).
cnf(c1043,plain,
( ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1328)
| ~ present(skc8,X1328)
| ~ event(skc8,X1328)
| ~ theme(skc8,X1328,skc8)
| ~ vincent_forename(skc8,X1327)
| ~ forename(skc8,X1327)
| ~ agent(skc8,X1328,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1327,skc10)
| ~ state(skc8,skc9)
| ~ smoke(skc8,X1328)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1041]) ).
cnf(c405,plain,
( ~ proposition(skc8,X695)
| ~ accessible_world(skc8,X695)
| ~ smoke(X695,X697)
| ~ present(X695,X697)
| ~ agent(X695,X697,skf4(X695))
| ~ event(X695,X697)
| ~ think_believe_consider(skc8,X691)
| ~ present(skc8,X691)
| ~ event(skc8,X691)
| ~ theme(skc8,X691,X695)
| ~ vincent_forename(skc8,X689)
| ~ forename(skc8,X689)
| ~ agent(skc8,X691,X696)
| ~ man(skc8,X696)
| ~ of(skc8,X689,X696)
| ~ accessible_world(skc8,X694)
| ~ proposition(skc8,X694)
| ~ theme(skc8,X692,X694)
| ~ event(skc8,X692)
| ~ present(skc8,X692)
| ~ think_believe_consider(skc8,X692)
| ~ state(skc8,skc9)
| ~ of(skc8,X688,skc10)
| ~ vincent_forename(skc8,X688)
| ~ forename(skc8,X688)
| ~ man(skc8,skc10)
| ~ agent(skc8,X692,skc10)
| ~ smoke(X694,X693)
| ~ present(X694,X693)
| ~ agent(X694,X693,skc10)
| ~ event(X694,X693)
| ~ forename(skc8,X690)
| ~ jules_forename(skc8,X690)
| ~ of(skc8,X690,skc10)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[clause95,clause89]) ).
cnf(c704,plain,
( ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ smoke(skc8,X1309)
| ~ present(skc8,X1309)
| ~ agent(skc8,X1309,skf4(skc8))
| ~ event(skc8,X1309)
| ~ think_believe_consider(skc8,X1309)
| ~ theme(skc8,X1309,skc8)
| ~ vincent_forename(skc8,X1307)
| ~ forename(skc8,X1307)
| ~ man(skc8,skf4(skc8))
| ~ of(skc8,X1307,skf4(skc8))
| ~ accessible_world(skc8,X1305)
| ~ proposition(skc8,X1305)
| ~ theme(skc8,X1306,X1305)
| ~ event(skc8,X1306)
| ~ present(skc8,X1306)
| ~ think_believe_consider(skc8,X1306)
| ~ state(skc8,skc9)
| ~ of(skc8,X1304,skc10)
| ~ vincent_forename(skc8,X1304)
| ~ forename(skc8,X1304)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1306,skc10)
| ~ smoke(X1305,X1310)
| ~ present(X1305,X1310)
| ~ agent(X1305,X1310,skc10)
| ~ event(X1305,X1310)
| ~ forename(skc8,X1308)
| ~ jules_forename(skc8,X1308)
| ~ of(skc8,X1308,skc10)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1028,plain,
( ~ proposition(skc8,X1301)
| ~ accessible_world(skc8,X1301)
| ~ think_believe_consider(skc8,X1298)
| ~ present(skc8,X1298)
| ~ event(skc8,X1298)
| ~ theme(skc8,X1298,X1301)
| ~ vincent_forename(skc8,X1299)
| ~ forename(skc8,X1299)
| ~ agent(skc8,X1298,X1303)
| ~ man(skc8,X1303)
| ~ of(skc8,X1299,X1303)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1302,skc8)
| ~ event(skc8,X1302)
| ~ present(skc8,X1302)
| ~ think_believe_consider(skc8,X1302)
| ~ state(skc8,skc9)
| ~ of(skc8,X1300,skc10)
| ~ vincent_forename(skc8,X1300)
| ~ forename(skc8,X1300)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1302,skc10)
| ~ smoke(skc8,X1302)
| ~ jules_forename(skc8,X1300)
| ~ actual_world(skc8)
| man(X1301,skf4(X1301)) ),
inference(factor,[status(thm)],[c698]) ).
cnf(c1025,plain,
( ~ proposition(skc8,X1284)
| ~ accessible_world(skc8,X1284)
| ~ think_believe_consider(skc8,X1287)
| ~ present(skc8,X1287)
| ~ event(skc8,X1287)
| ~ theme(skc8,X1287,X1284)
| ~ vincent_forename(skc8,X1285)
| ~ forename(skc8,X1285)
| ~ agent(skc8,X1287,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1285,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1288,skc8)
| ~ event(skc8,X1288)
| ~ present(skc8,X1288)
| ~ think_believe_consider(skc8,X1288)
| ~ state(skc8,skc9)
| ~ of(skc8,X1286,skc10)
| ~ vincent_forename(skc8,X1286)
| ~ forename(skc8,X1286)
| ~ agent(skc8,X1288,skc10)
| ~ smoke(skc8,X1288)
| ~ jules_forename(skc8,X1285)
| ~ actual_world(skc8)
| man(X1284,skf4(X1284)) ),
inference(factor,[status(thm)],[c697]) ).
cnf(c1024,plain,
( ~ proposition(skc8,X1258)
| ~ accessible_world(skc8,X1258)
| ~ think_believe_consider(skc8,X1261)
| ~ present(skc8,X1261)
| ~ event(skc8,X1261)
| ~ theme(skc8,X1261,X1258)
| ~ vincent_forename(skc8,X1259)
| ~ forename(skc8,X1259)
| ~ agent(skc8,X1261,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1259,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1262,skc8)
| ~ event(skc8,X1262)
| ~ present(skc8,X1262)
| ~ think_believe_consider(skc8,X1262)
| ~ state(skc8,skc9)
| ~ of(skc8,X1260,skc10)
| ~ vincent_forename(skc8,X1260)
| ~ forename(skc8,X1260)
| ~ agent(skc8,X1262,skc10)
| ~ smoke(skc8,X1261)
| ~ jules_forename(skc8,X1259)
| ~ actual_world(skc8)
| man(X1258,skf4(X1258)) ),
inference(factor,[status(thm)],[c697]) ).
cnf(c1030,plain,
( ~ proposition(skc8,X1264)
| ~ accessible_world(skc8,X1264)
| ~ think_believe_consider(skc8,X1263)
| ~ present(skc8,X1263)
| ~ event(skc8,X1263)
| ~ theme(skc8,X1263,X1264)
| ~ vincent_forename(skc8,X1265)
| ~ forename(skc8,X1265)
| ~ agent(skc8,X1263,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1265,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1263,skc8)
| ~ state(skc8,skc9)
| ~ of(skc8,X1266,skc10)
| ~ vincent_forename(skc8,X1266)
| ~ forename(skc8,X1266)
| ~ smoke(skc8,X1263)
| ~ jules_forename(skc8,X1265)
| ~ actual_world(skc8)
| man(X1264,skf4(X1264)) ),
inference(factor,[status(thm)],[c1024]) ).
cnf(c1031,plain,
( ~ proposition(skc8,X1269)
| ~ accessible_world(skc8,X1269)
| ~ think_believe_consider(skc8,X1268)
| ~ present(skc8,X1268)
| ~ event(skc8,X1268)
| ~ theme(skc8,X1268,X1269)
| ~ vincent_forename(skc8,X1267)
| ~ forename(skc8,X1267)
| ~ agent(skc8,X1268,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1267,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1268,skc8)
| ~ state(skc8,skc9)
| ~ smoke(skc8,X1268)
| ~ jules_forename(skc8,X1267)
| ~ actual_world(skc8)
| man(X1269,skf4(X1269)) ),
inference(factor,[status(thm)],[c1030]) ).
cnf(c1033,plain,
( ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1270)
| ~ present(skc8,X1270)
| ~ event(skc8,X1270)
| ~ theme(skc8,X1270,skc8)
| ~ vincent_forename(skc8,X1271)
| ~ forename(skc8,X1271)
| ~ agent(skc8,X1270,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1271,skc10)
| ~ state(skc8,skc9)
| ~ smoke(skc8,X1270)
| ~ jules_forename(skc8,X1271)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1031]) ).
cnf(c1034,plain,
( ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1272)
| ~ present(skc8,X1272)
| ~ event(skc8,X1272)
| ~ theme(skc8,X1272,skc8)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ agent(skc8,X1272,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ smoke(skc8,X1272)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1033,clause88]) ).
cnf(clause73,negated_conjecture,
man(skc8,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
cnf(c233,plain,
( ~ accessible_world(skc8,X286)
| man(X286,skc15) ),
inference(resolution,[status(thm)],[clause52,clause73]) ).
cnf(c379,plain,
man(skc12,skc15),
inference(resolution,[status(thm)],[c233,clause83]) ).
cnf(c384,plain,
agent(skc12,skf2(skc15),skc15),
inference(resolution,[status(thm)],[clause93,c379]) ).
cnf(clause71,axiom,
( ~ proposition(X267,X266)
| ~ proposition(X267,X265)
| ~ theme(X267,X263,X266)
| ~ think_believe_consider(X267,X263)
| ~ think_believe_consider(X267,X268)
| ~ theme(X267,X268,X265)
| ~ agent(X267,X268,X264)
| ~ agent(X267,X263,X264)
| X266 = X265 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
cnf(clause86,negated_conjecture,
agent(skc8,skc13,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
cnf(clause66,axiom,
( ~ accessible_world(X233,X235)
| ~ agent(X233,X236,X234)
| agent(X235,X236,X234) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
cnf(c316,plain,
( ~ accessible_world(skc8,X493)
| agent(X493,skc13,skc15) ),
inference(resolution,[status(thm)],[clause66,clause86]) ).
cnf(c568,plain,
agent(skc12,skc13,skc15),
inference(resolution,[status(thm)],[c316,clause83]) ).
cnf(c569,plain,
( ~ proposition(skc12,X1000)
| ~ proposition(skc12,X1002)
| ~ theme(skc12,skc13,X1000)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,X1001)
| ~ theme(skc12,X1001,X1002)
| ~ agent(skc12,X1001,skc15)
| X1000 = X1002 ),
inference(resolution,[status(thm)],[c568,clause71]) ).
cnf(c896,plain,
( ~ proposition(skc12,X1242)
| ~ proposition(skc12,X1241)
| ~ theme(skc12,skc13,X1242)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1241)
| X1242 = X1241 ),
inference(resolution,[status(thm)],[c569,c384]) ).
cnf(c350,plain,
( ~ proposition(X660,X658)
| ~ proposition(X660,X656)
| ~ theme(X660,X659,X658)
| ~ think_believe_consider(X660,X659)
| ~ theme(X660,X659,X656)
| ~ agent(X660,X659,X657)
| X658 = X656 ),
inference(factor,[status(thm)],[clause71]) ).
cnf(c689,plain,
( ~ proposition(skc12,X1231)
| ~ proposition(skc12,X1230)
| ~ theme(skc12,skc13,X1231)
| ~ think_believe_consider(skc12,skc13)
| ~ theme(skc12,skc13,X1230)
| X1231 = X1230 ),
inference(resolution,[status(thm)],[c350,c568]) ).
cnf(c1021,plain,
( ~ proposition(skc12,X1234)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skc13,X1234)
| ~ think_believe_consider(skc12,skc13)
| X1234 = skc12 ),
inference(resolution,[status(thm)],[c689,c571]) ).
cnf(c686,plain,
( ~ proposition(skc8,X1200)
| ~ proposition(skc8,X1199)
| ~ theme(skc8,skc13,X1200)
| ~ think_believe_consider(skc8,skc13)
| ~ theme(skc8,skc13,X1199)
| X1200 = X1199 ),
inference(resolution,[status(thm)],[c350,clause86]) ).
cnf(c1009,plain,
( ~ proposition(skc8,X1233)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,skc13,X1233)
| ~ think_believe_consider(skc8,skc13)
| X1233 = skc12 ),
inference(resolution,[status(thm)],[c686,clause87]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c30,axiom,
( X570 != X567
| X571 != X568
| X564 != X569
| X565 != X566
| ~ be(X570,X571,X564,X565)
| be(X567,X568,X569,X566) ),
theory(equality) ).
cnf(c633,plain,
( skc12 != X1119
| skc9 != X1118
| skc10 != X1120
| skc10 != X1117
| be(X1119,X1118,X1120,X1117) ),
inference(resolution,[status(thm)],[c30,c587]) ).
cnf(c966,plain,
( skc12 != X1223
| skc9 != X1222
| skc10 != X1224
| be(X1223,X1222,X1224,skc10) ),
inference(resolution,[status(thm)],[c633,reflexivity]) ).
cnf(c688,plain,
( ~ proposition(skc12,X1221)
| ~ proposition(skc12,X1220)
| ~ theme(skc12,skf2(skc15),X1221)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1220)
| X1221 = X1220 ),
inference(resolution,[status(thm)],[c350,c384]) ).
cnf(c632,plain,
( skc8 != X1111
| skc9 != X1110
| skc10 != X1112
| skc10 != X1109
| be(X1111,X1110,X1112,X1109) ),
inference(resolution,[status(thm)],[c30,clause89]) ).
cnf(c961,plain,
( skc8 != X1217
| skc9 != X1215
| skc10 != X1216
| be(X1217,X1215,X1216,skc10) ),
inference(resolution,[status(thm)],[c632,reflexivity]) ).
cnf(c965,plain,
( skc12 != X1209
| skc9 != X1207
| skc10 != X1208
| be(X1209,X1207,X1208,X1208) ),
inference(factor,[status(thm)],[c633]) ).
cnf(c1013,plain,
( skc12 != X1212
| skc9 != X1213
| be(X1212,X1213,skc10,skc10) ),
inference(resolution,[status(thm)],[c965,reflexivity]) ).
cnf(c1015,plain,
( skc12 != X1214
| be(X1214,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1013,reflexivity]) ).
cnf(c687,plain,
( ~ proposition(skc12,X1211)
| ~ proposition(skc12,X1210)
| ~ theme(skc12,skf2(skc10),X1211)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1210)
| X1211 = X1210 ),
inference(resolution,[status(thm)],[c350,c385]) ).
cnf(c960,plain,
( skc8 != X1202
| skc9 != X1201
| skc10 != X1203
| be(X1202,X1201,X1203,X1203) ),
inference(factor,[status(thm)],[c632]) ).
cnf(c1010,plain,
( skc8 != X1205
| skc9 != X1204
| be(X1205,X1204,skc10,skc10) ),
inference(resolution,[status(thm)],[c960,reflexivity]) ).
cnf(c1011,plain,
( skc8 != X1206
| be(X1206,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1010,reflexivity]) ).
cnf(c36,axiom,
( X628 != X625
| X629 != X626
| X624 != X627
| ~ of(X628,X629,X624)
| of(X625,X626,X627) ),
theory(equality) ).
cnf(c669,plain,
( skc8 != X1193
| skc11 != X1194
| skc10 != X1192
| of(X1193,X1194,X1192) ),
inference(resolution,[status(thm)],[c36,clause88]) ).
cnf(c1004,plain,
( skc8 != X1197
| skc11 != X1196
| of(X1197,X1196,skc10) ),
inference(resolution,[status(thm)],[c669,reflexivity]) ).
cnf(c1006,plain,
( skc8 != X1198
| of(X1198,skc11,skc10) ),
inference(resolution,[status(thm)],[c1004,reflexivity]) ).
cnf(clause85,negated_conjecture,
of(skc8,skc14,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
cnf(c668,plain,
( skc8 != X1188
| skc14 != X1189
| skc15 != X1187
| of(X1188,X1189,X1187) ),
inference(resolution,[status(thm)],[c36,clause85]) ).
cnf(c1002,plain,
( skc8 != X1190
| skc14 != X1191
| of(X1190,X1191,skc15) ),
inference(resolution,[status(thm)],[c668,reflexivity]) ).
cnf(c1003,plain,
( skc8 != X1195
| of(X1195,skc14,skc15) ),
inference(resolution,[status(thm)],[c1002,reflexivity]) ).
cnf(c667,plain,
( skc12 != X1182
| skc11 != X1183
| skc10 != X1181
| of(X1182,X1183,X1181) ),
inference(resolution,[status(thm)],[c36,c580]) ).
cnf(c999,plain,
( skc12 != X1185
| skc11 != X1184
| of(X1185,X1184,skc10) ),
inference(resolution,[status(thm)],[c667,reflexivity]) ).
cnf(c1000,plain,
( skc12 != X1186
| of(X1186,skc11,skc10) ),
inference(resolution,[status(thm)],[c999,reflexivity]) ).
cnf(c323,plain,
( ~ accessible_world(skc8,X499)
| of(X499,skc14,skc15) ),
inference(resolution,[status(thm)],[clause68,clause85]) ).
cnf(c577,plain,
of(skc12,skc14,skc15),
inference(resolution,[status(thm)],[c323,clause83]) ).
cnf(c666,plain,
( skc12 != X1175
| skc14 != X1176
| skc15 != X1174
| of(X1175,X1176,X1174) ),
inference(resolution,[status(thm)],[c36,c577]) ).
cnf(c995,plain,
( skc12 != X1178
| skc14 != X1179
| of(X1178,X1179,skc15) ),
inference(resolution,[status(thm)],[c666,reflexivity]) ).
cnf(c997,plain,
( skc12 != X1180
| of(X1180,skc14,skc15) ),
inference(resolution,[status(thm)],[c995,reflexivity]) ).
cnf(c35,axiom,
( X618 != X615
| X619 != X616
| X614 != X617
| ~ theme(X618,X619,X614)
| theme(X615,X616,X617) ),
theory(equality) ).
cnf(c662,plain,
( skc8 != X1166
| skc13 != X1168
| skc12 != X1167
| theme(X1166,X1168,X1167) ),
inference(resolution,[status(thm)],[c35,clause87]) ).
cnf(c991,plain,
( skc8 != X1173
| skc13 != X1172
| theme(X1173,X1172,skc12) ),
inference(resolution,[status(thm)],[c662,reflexivity]) ).
cnf(c994,plain,
( skc8 != X1177
| theme(X1177,skc13,skc12) ),
inference(resolution,[status(thm)],[c991,reflexivity]) ).
cnf(c661,plain,
( skc12 != X1157
| skc13 != X1159
| skc12 != X1158
| theme(X1157,X1159,X1158) ),
inference(resolution,[status(thm)],[c35,c571]) ).
cnf(c986,plain,
( skc12 != X1169
| skc13 != X1170
| theme(X1169,X1170,skc12) ),
inference(resolution,[status(thm)],[c661,reflexivity]) ).
cnf(c992,plain,
( skc12 != X1171
| theme(X1171,skc13,skc12) ),
inference(resolution,[status(thm)],[c986,reflexivity]) ).
cnf(c34,axiom,
( X607 != X604
| X608 != X605
| X603 != X606
| ~ agent(X607,X608,X603)
| agent(X604,X605,X606) ),
theory(equality) ).
cnf(c657,plain,
( skc12 != X1156
| skc13 != X1155
| skc15 != X1154
| agent(X1156,X1155,X1154) ),
inference(resolution,[status(thm)],[c34,c568]) ).
cnf(c984,plain,
( skc12 != X1163
| skc13 != X1164
| agent(X1163,X1164,skc15) ),
inference(resolution,[status(thm)],[c657,reflexivity]) ).
cnf(c989,plain,
( skc12 != X1165
| agent(X1165,skc13,skc15) ),
inference(resolution,[status(thm)],[c984,reflexivity]) ).
cnf(c985,plain,
( skc12 != X1160
| skc13 != X1161
| theme(X1160,X1161,X1160) ),
inference(factor,[status(thm)],[c661]) ).
cnf(c987,plain,
( skc12 != X1162
| theme(X1162,skc13,X1162) ),
inference(resolution,[status(thm)],[c985,reflexivity]) ).
cnf(c656,plain,
( skc12 != X1150
| skf2(skc15) != X1149
| skc15 != X1148
| agent(X1150,X1149,X1148) ),
inference(resolution,[status(thm)],[c34,c384]) ).
cnf(c981,plain,
( skc12 != X1152
| skc15 != X1151
| agent(X1152,skf2(skc15),X1151) ),
inference(resolution,[status(thm)],[c656,reflexivity]) ).
cnf(c982,plain,
( skc12 != X1153
| agent(X1153,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c981,reflexivity]) ).
cnf(c655,plain,
( skc12 != X1144
| skf2(skc10) != X1143
| skc10 != X1142
| agent(X1144,X1143,X1142) ),
inference(resolution,[status(thm)],[c34,c385]) ).
cnf(c978,plain,
( skc12 != X1146
| skc10 != X1145
| agent(X1146,skf2(skc10),X1145) ),
inference(resolution,[status(thm)],[c655,reflexivity]) ).
cnf(c979,plain,
( skc12 != X1147
| agent(X1147,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c978,reflexivity]) ).
cnf(c654,plain,
( skc8 != X1138
| skc13 != X1137
| skc15 != X1136
| agent(X1138,X1137,X1136) ),
inference(resolution,[status(thm)],[c34,clause86]) ).
cnf(c975,plain,
( skc8 != X1140
| skc13 != X1139
| agent(X1140,X1139,skc15) ),
inference(resolution,[status(thm)],[c654,reflexivity]) ).
cnf(c976,plain,
( skc8 != X1141
| agent(X1141,skc13,skc15) ),
inference(resolution,[status(thm)],[c975,reflexivity]) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
cnf(c33,axiom,
( X596 != X597
| X598 != X595
| ~ think_believe_consider(X596,X598)
| think_believe_consider(X597,X595) ),
theory(equality) ).
cnf(c650,plain,
( skc8 != X1134
| skc13 != X1133
| think_believe_consider(X1134,X1133) ),
inference(resolution,[status(thm)],[c33,clause78]) ).
cnf(c973,plain,
( skc8 != X1135
| think_believe_consider(X1135,skc13) ),
inference(resolution,[status(thm)],[c650,reflexivity]) ).
cnf(c32,axiom,
( X586 != X587
| X588 != X585
| ~ present(X586,X588)
| present(X587,X585) ),
theory(equality) ).
cnf(c643,plain,
( skc12 != X1127
| skf2(X1128) != X1129
| present(X1127,X1129) ),
inference(resolution,[status(thm)],[c32,c371]) ).
cnf(c971,plain,
( skc12 != X1131
| present(X1131,skf2(X1130)) ),
inference(resolution,[status(thm)],[c643,reflexivity]) ).
cnf(clause45,axiom,
( ~ accessible_world(X119,X120)
| ~ think_believe_consider(X119,X121)
| think_believe_consider(X120,X121) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(c199,plain,
( ~ accessible_world(skc8,X202)
| think_believe_consider(X202,skc13) ),
inference(resolution,[status(thm)],[clause45,clause78]) ).
cnf(c263,plain,
think_believe_consider(skc12,skc13),
inference(resolution,[status(thm)],[c199,clause83]) ).
cnf(c649,plain,
( skc12 != X1125
| skc13 != X1124
| think_believe_consider(X1125,X1124) ),
inference(resolution,[status(thm)],[c33,c263]) ).
cnf(c969,plain,
( skc12 != X1126
| think_believe_consider(X1126,skc13) ),
inference(resolution,[status(thm)],[c649,reflexivity]) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
cnf(clause44,axiom,
( ~ accessible_world(X115,X116)
| ~ present(X115,X117)
| present(X116,X117) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c191,plain,
( ~ accessible_world(skc8,X194)
| present(X194,skc13) ),
inference(resolution,[status(thm)],[clause44,clause77]) ).
cnf(c259,plain,
present(skc12,skc13),
inference(resolution,[status(thm)],[c191,clause83]) ).
cnf(c642,plain,
( skc12 != X1121
| skc13 != X1122
| present(X1121,X1122) ),
inference(resolution,[status(thm)],[c32,c259]) ).
cnf(c967,plain,
( skc12 != X1123
| present(X1123,skc13) ),
inference(resolution,[status(thm)],[c642,reflexivity]) ).
cnf(c641,plain,
( skc8 != X1114
| skc13 != X1115
| present(X1114,X1115) ),
inference(resolution,[status(thm)],[c32,clause77]) ).
cnf(c963,plain,
( skc8 != X1116
| present(X1116,skc13) ),
inference(resolution,[status(thm)],[c641,reflexivity]) ).
cnf(c31,axiom,
( X578 != X579
| X580 != X577
| ~ accessible_world(X578,X580)
| accessible_world(X579,X577) ),
theory(equality) ).
cnf(c637,plain,
( skc8 != X1108
| skc12 != X1107
| accessible_world(X1108,X1107) ),
inference(resolution,[status(thm)],[c31,clause83]) ).
cnf(c959,plain,
( skc8 != X1113
| accessible_world(X1113,skc12) ),
inference(resolution,[status(thm)],[c637,reflexivity]) ).
cnf(clause79,negated_conjecture,
jules_forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
cnf(c29,axiom,
( X555 != X556
| X557 != X554
| ~ jules_forename(X555,X557)
| jules_forename(X556,X554) ),
theory(equality) ).
cnf(c627,plain,
( skc8 != X1104
| skc11 != X1103
| jules_forename(X1104,X1103) ),
inference(resolution,[status(thm)],[c29,clause79]) ).
cnf(c956,plain,
( skc8 != X1106
| jules_forename(X1106,skc11) ),
inference(resolution,[status(thm)],[c627,reflexivity]) ).
cnf(clause65,axiom,
( ~ accessible_world(X228,X229)
| ~ jules_forename(X228,X230)
| jules_forename(X229,X230) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
cnf(c313,plain,
( ~ accessible_world(skc8,X415)
| jules_forename(X415,skc11) ),
inference(resolution,[status(thm)],[clause65,clause79]) ).
cnf(c529,plain,
jules_forename(skc12,skc11),
inference(resolution,[status(thm)],[c313,clause83]) ).
cnf(c626,plain,
( skc12 != X1102
| skc11 != X1101
| jules_forename(X1102,X1101) ),
inference(resolution,[status(thm)],[c29,c529]) ).
cnf(c955,plain,
( skc12 != X1105
| jules_forename(X1105,skc11) ),
inference(resolution,[status(thm)],[c626,reflexivity]) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
cnf(clause64,axiom,
( ~ accessible_world(X224,X225)
| ~ vincent_forename(X224,X226)
| vincent_forename(X225,X226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
cnf(c308,plain,
( ~ accessible_world(skc8,X408)
| vincent_forename(X408,skc14) ),
inference(resolution,[status(thm)],[clause64,clause75]) ).
cnf(c520,plain,
vincent_forename(skc12,skc14),
inference(resolution,[status(thm)],[c308,clause83]) ).
cnf(c28,axiom,
( X547 != X548
| X549 != X546
| ~ vincent_forename(X547,X549)
| vincent_forename(X548,X546) ),
theory(equality) ).
cnf(c622,plain,
( skc12 != X1098
| skc14 != X1097
| vincent_forename(X1098,X1097) ),
inference(resolution,[status(thm)],[c28,c520]) ).
cnf(c952,plain,
( skc12 != X1100
| vincent_forename(X1100,skc14) ),
inference(resolution,[status(thm)],[c622,reflexivity]) ).
cnf(c621,plain,
( skc8 != X1096
| skc14 != X1095
| vincent_forename(X1096,X1095) ),
inference(resolution,[status(thm)],[c28,clause75]) ).
cnf(c951,plain,
( skc8 != X1099
| vincent_forename(X1099,skc14) ),
inference(resolution,[status(thm)],[c621,reflexivity]) ).
cnf(clause74,negated_conjecture,
forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
cnf(clause27,axiom,
( ~ forename(X55,X56)
| relname(X55,X56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c84,plain,
relname(skc8,skc14),
inference(resolution,[status(thm)],[clause27,clause74]) ).
cnf(c27,axiom,
( X538 != X539
| X540 != X537
| ~ relname(X538,X540)
| relname(X539,X537) ),
theory(equality) ).
cnf(c617,plain,
( skc8 != X1092
| skc14 != X1091
| relname(X1092,X1091) ),
inference(resolution,[status(thm)],[c27,c84]) ).
cnf(c948,plain,
( skc8 != X1094
| relname(X1094,skc14) ),
inference(resolution,[status(thm)],[c617,reflexivity]) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
cnf(clause62,axiom,
( ~ accessible_world(X216,X217)
| ~ forename(X216,X218)
| forename(X217,X218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
cnf(c292,plain,
( ~ accessible_world(skc8,X384)
| forename(X384,skc11) ),
inference(resolution,[status(thm)],[clause62,clause80]) ).
cnf(c483,plain,
forename(skc12,skc11),
inference(resolution,[status(thm)],[c292,clause83]) ).
cnf(c495,plain,
relname(skc12,skc11),
inference(resolution,[status(thm)],[c483,clause27]) ).
cnf(c616,plain,
( skc12 != X1090
| skc11 != X1089
| relname(X1090,X1089) ),
inference(resolution,[status(thm)],[c27,c495]) ).
cnf(c947,plain,
( skc12 != X1093
| relname(X1093,skc11) ),
inference(resolution,[status(thm)],[c616,reflexivity]) ).
cnf(c83,plain,
relname(skc8,skc11),
inference(resolution,[status(thm)],[clause27,clause80]) ).
cnf(c615,plain,
( skc8 != X1086
| skc11 != X1085
| relname(X1086,X1085) ),
inference(resolution,[status(thm)],[c27,c83]) ).
cnf(c944,plain,
( skc8 != X1088
| relname(X1088,skc11) ),
inference(resolution,[status(thm)],[c615,reflexivity]) ).
cnf(c293,plain,
( ~ accessible_world(skc8,X389)
| forename(X389,skc14) ),
inference(resolution,[status(thm)],[clause62,clause74]) ).
cnf(c499,plain,
forename(skc12,skc14),
inference(resolution,[status(thm)],[c293,clause83]) ).
cnf(c500,plain,
relname(skc12,skc14),
inference(resolution,[status(thm)],[c499,clause27]) ).
cnf(c614,plain,
( skc12 != X1084
| skc14 != X1083
| relname(X1084,X1083) ),
inference(resolution,[status(thm)],[c27,c500]) ).
cnf(c943,plain,
( skc12 != X1087
| relname(X1087,skc14) ),
inference(resolution,[status(thm)],[c614,reflexivity]) ).
cnf(c26,axiom,
( X528 != X529
| X530 != X527
| ~ forename(X528,X530)
| forename(X529,X527) ),
theory(equality) ).
cnf(c609,plain,
( skc8 != X1080
| skc14 != X1079
| forename(X1080,X1079) ),
inference(resolution,[status(thm)],[c26,clause74]) ).
cnf(c940,plain,
( skc8 != X1082
| forename(X1082,skc14) ),
inference(resolution,[status(thm)],[c609,reflexivity]) ).
cnf(c608,plain,
( skc12 != X1078
| skc11 != X1077
| forename(X1078,X1077) ),
inference(resolution,[status(thm)],[c26,c483]) ).
cnf(c939,plain,
( skc12 != X1081
| forename(X1081,skc11) ),
inference(resolution,[status(thm)],[c608,reflexivity]) ).
cnf(c607,plain,
( skc12 != X1074
| skc14 != X1073
| forename(X1074,X1073) ),
inference(resolution,[status(thm)],[c26,c499]) ).
cnf(c936,plain,
( skc12 != X1076
| forename(X1076,skc14) ),
inference(resolution,[status(thm)],[c607,reflexivity]) ).
cnf(c606,plain,
( skc8 != X1072
| skc11 != X1071
| forename(X1072,X1071) ),
inference(resolution,[status(thm)],[c26,clause80]) ).
cnf(c935,plain,
( skc8 != X1075
| forename(X1075,skc11) ),
inference(resolution,[status(thm)],[c606,reflexivity]) ).
cnf(clause26,axiom,
( ~ man(X53,X54)
| male(X53,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c82,plain,
male(skc8,skc15),
inference(resolution,[status(thm)],[clause26,clause73]) ).
cnf(c25,axiom,
( X520 != X521
| X522 != X519
| ~ male(X520,X522)
| male(X521,X519) ),
theory(equality) ).
cnf(c602,plain,
( skc8 != X1068
| skc15 != X1067
| male(X1068,X1067) ),
inference(resolution,[status(thm)],[c25,c82]) ).
cnf(c932,plain,
( skc8 != X1070
| male(X1070,skc15) ),
inference(resolution,[status(thm)],[c602,reflexivity]) ).
cnf(c81,plain,
male(skc8,skc10),
inference(resolution,[status(thm)],[clause26,clause81]) ).
cnf(c601,plain,
( skc8 != X1066
| skc10 != X1065
| male(X1066,X1065) ),
inference(resolution,[status(thm)],[c25,c81]) ).
cnf(c931,plain,
( skc8 != X1069
| male(X1069,skc10) ),
inference(resolution,[status(thm)],[c601,reflexivity]) ).
cnf(c381,plain,
male(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause26]) ).
cnf(c600,plain,
( skc12 != X1062
| skc15 != X1061
| male(X1062,X1061) ),
inference(resolution,[status(thm)],[c25,c381]) ).
cnf(c928,plain,
( skc12 != X1064
| male(X1064,skc15) ),
inference(resolution,[status(thm)],[c600,reflexivity]) ).
cnf(c333,plain,
male(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause26]) ).
cnf(c599,plain,
( skc12 != X1060
| skc10 != X1059
| male(X1060,X1059) ),
inference(resolution,[status(thm)],[c25,c333]) ).
cnf(c927,plain,
( skc12 != X1063
| male(X1063,skc10) ),
inference(resolution,[status(thm)],[c599,reflexivity]) ).
cnf(clause25,axiom,
( ~ human_person(X51,X52)
| animate(X51,X52) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(clause16,axiom,
( ~ man(X33,X34)
| human_person(X33,X34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c334,plain,
human_person(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause16]) ).
cnf(c340,plain,
animate(skc12,skc10),
inference(resolution,[status(thm)],[c334,clause25]) ).
cnf(c24,axiom,
( X511 != X512
| X513 != X510
| ~ animate(X511,X513)
| animate(X512,X510) ),
theory(equality) ).
cnf(c595,plain,
( skc12 != X1056
| skc10 != X1057
| animate(X1056,X1057) ),
inference(resolution,[status(thm)],[c24,c340]) ).
cnf(c925,plain,
( skc12 != X1058
| animate(X1058,skc10) ),
inference(resolution,[status(thm)],[c595,reflexivity]) ).
cnf(c60,plain,
human_person(skc8,skc15),
inference(resolution,[status(thm)],[clause16,clause73]) ).
cnf(c80,plain,
animate(skc8,skc15),
inference(resolution,[status(thm)],[clause25,c60]) ).
cnf(c594,plain,
( skc8 != X1044
| skc15 != X1045
| animate(X1044,X1045) ),
inference(resolution,[status(thm)],[c24,c80]) ).
cnf(c920,plain,
( skc8 != X1046
| animate(X1046,skc15) ),
inference(resolution,[status(thm)],[c594,reflexivity]) ).
cnf(c59,plain,
human_person(skc8,skc10),
inference(resolution,[status(thm)],[clause16,clause81]) ).
cnf(c79,plain,
animate(skc8,skc10),
inference(resolution,[status(thm)],[clause25,c59]) ).
cnf(c593,plain,
( skc8 != X1041
| skc10 != X1042
| animate(X1041,X1042) ),
inference(resolution,[status(thm)],[c24,c79]) ).
cnf(c918,plain,
( skc8 != X1043
| animate(X1043,skc10) ),
inference(resolution,[status(thm)],[c593,reflexivity]) ).
cnf(c382,plain,
human_person(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause16]) ).
cnf(c387,plain,
animate(skc12,skc15),
inference(resolution,[status(thm)],[c382,clause25]) ).
cnf(c592,plain,
( skc12 != X1028
| skc15 != X1029
| animate(X1028,X1029) ),
inference(resolution,[status(thm)],[c24,c387]) ).
cnf(c915,plain,
( skc12 != X1030
| animate(X1030,skc15) ),
inference(resolution,[status(thm)],[c592,reflexivity]) ).
cnf(clause24,axiom,
( ~ human_person(X49,X50)
| human(X49,X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c78,plain,
human(skc8,skc15),
inference(resolution,[status(thm)],[clause24,c60]) ).
cnf(c23,axiom,
( X503 != X504
| X505 != X502
| ~ human(X503,X505)
| human(X504,X502) ),
theory(equality) ).
cnf(c586,plain,
( skc8 != X1025
| skc15 != X1024
| human(X1025,X1024) ),
inference(resolution,[status(thm)],[c23,c78]) ).
cnf(c913,plain,
( skc8 != X1027
| human(X1027,skc15) ),
inference(resolution,[status(thm)],[c586,reflexivity]) ).
cnf(c588,plain,
( ~ accessible_world(skc12,X1026)
| be(X1026,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c587,clause69]) ).
cnf(c342,plain,
human(skc12,skc10),
inference(resolution,[status(thm)],[c334,clause24]) ).
cnf(c585,plain,
( skc12 != X1022
| skc10 != X1021
| human(X1022,X1021) ),
inference(resolution,[status(thm)],[c23,c342]) ).
cnf(c911,plain,
( skc12 != X1023
| human(X1023,skc10) ),
inference(resolution,[status(thm)],[c585,reflexivity]) ).
cnf(clause70,axiom,
( ~ forename(X259,X261)
| ~ of(X259,X262,X260)
| ~ forename(X259,X262)
| ~ of(X259,X261,X260)
| ~ entity(X259,X260)
| X262 = X261 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
cnf(c582,plain,
( ~ forename(skc12,skc11)
| ~ of(skc12,X1020,skc10)
| ~ forename(skc12,X1020)
| ~ entity(skc12,skc10)
| X1020 = skc11 ),
inference(resolution,[status(thm)],[c580,clause70]) ).
cnf(c389,plain,
human(skc12,skc15),
inference(resolution,[status(thm)],[c382,clause24]) ).
cnf(c584,plain,
( skc12 != X1018
| skc15 != X1017
| human(X1018,X1017) ),
inference(resolution,[status(thm)],[c23,c389]) ).
cnf(c908,plain,
( skc12 != X1019
| human(X1019,skc15) ),
inference(resolution,[status(thm)],[c584,reflexivity]) ).
cnf(c77,plain,
human(skc8,skc10),
inference(resolution,[status(thm)],[clause24,c59]) ).
cnf(c583,plain,
( skc8 != X1015
| skc10 != X1014
| human(X1015,X1014) ),
inference(resolution,[status(thm)],[c23,c77]) ).
cnf(c906,plain,
( skc8 != X1016
| human(X1016,skc10) ),
inference(resolution,[status(thm)],[c583,reflexivity]) ).
cnf(c579,plain,
( ~ forename(skc12,skc14)
| ~ of(skc12,X1013,skc15)
| ~ forename(skc12,X1013)
| ~ entity(skc12,skc15)
| X1013 = skc14 ),
inference(resolution,[status(thm)],[c577,clause70]) ).
cnf(clause23,axiom,
( ~ organism(X47,X48)
| living(X47,X48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(clause17,axiom,
( ~ human_person(X35,X36)
| organism(X35,X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c386,plain,
organism(skc12,skc15),
inference(resolution,[status(thm)],[c382,clause17]) ).
cnf(c390,plain,
living(skc12,skc15),
inference(resolution,[status(thm)],[c386,clause23]) ).
cnf(c22,axiom,
( X496 != X497
| X498 != X495
| ~ living(X496,X498)
| living(X497,X495) ),
theory(equality) ).
cnf(c576,plain,
( skc12 != X1011
| skc15 != X1010
| living(X1011,X1010) ),
inference(resolution,[status(thm)],[c22,c390]) ).
cnf(c903,plain,
( skc12 != X1012
| living(X1012,skc15) ),
inference(resolution,[status(thm)],[c576,reflexivity]) ).
cnf(c339,plain,
organism(skc12,skc10),
inference(resolution,[status(thm)],[c334,clause17]) ).
cnf(c343,plain,
living(skc12,skc10),
inference(resolution,[status(thm)],[c339,clause23]) ).
cnf(c575,plain,
( skc12 != X1008
| skc10 != X1007
| living(X1008,X1007) ),
inference(resolution,[status(thm)],[c22,c343]) ).
cnf(c901,plain,
( skc12 != X1009
| living(X1009,skc10) ),
inference(resolution,[status(thm)],[c575,reflexivity]) ).
cnf(c61,plain,
organism(skc8,skc10),
inference(resolution,[status(thm)],[clause17,c59]) ).
cnf(c76,plain,
living(skc8,skc10),
inference(resolution,[status(thm)],[clause23,c61]) ).
cnf(c574,plain,
( skc8 != X1005
| skc10 != X1004
| living(X1005,X1004) ),
inference(resolution,[status(thm)],[c22,c76]) ).
cnf(c899,plain,
( skc8 != X1006
| living(X1006,skc10) ),
inference(resolution,[status(thm)],[c574,reflexivity]) ).
cnf(c62,plain,
organism(skc8,skc15),
inference(resolution,[status(thm)],[clause17,c60]) ).
cnf(c75,plain,
living(skc8,skc15),
inference(resolution,[status(thm)],[clause23,c62]) ).
cnf(c573,plain,
( skc8 != X999
| skc15 != X998
| living(X999,X998) ),
inference(resolution,[status(thm)],[c22,c75]) ).
cnf(c895,plain,
( skc8 != X1003
| living(X1003,skc15) ),
inference(resolution,[status(thm)],[c573,reflexivity]) ).
cnf(clause22,axiom,
( ~ organism(X45,X46)
| impartial(X45,X46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c74,plain,
impartial(skc8,skc10),
inference(resolution,[status(thm)],[clause22,c61]) ).
cnf(c21,axiom,
( X488 != X489
| X490 != X487
| ~ impartial(X488,X490)
| impartial(X489,X487) ),
theory(equality) ).
cnf(c567,plain,
( skc8 != X994
| skc10 != X995
| impartial(X994,X995) ),
inference(resolution,[status(thm)],[c21,c74]) ).
cnf(c892,plain,
( skc8 != X997
| impartial(X997,skc10) ),
inference(resolution,[status(thm)],[c567,reflexivity]) ).
cnf(c73,plain,
impartial(skc8,skc15),
inference(resolution,[status(thm)],[clause22,c62]) ).
cnf(c566,plain,
( skc8 != X992
| skc15 != X993
| impartial(X992,X993) ),
inference(resolution,[status(thm)],[c21,c73]) ).
cnf(c891,plain,
( skc8 != X996
| impartial(X996,skc15) ),
inference(resolution,[status(thm)],[c566,reflexivity]) ).
cnf(c346,plain,
impartial(skc12,skc10),
inference(resolution,[status(thm)],[c339,clause22]) ).
cnf(c565,plain,
( skc12 != X988
| skc10 != X989
| impartial(X988,X989) ),
inference(resolution,[status(thm)],[c21,c346]) ).
cnf(c888,plain,
( skc12 != X991
| impartial(X991,skc10) ),
inference(resolution,[status(thm)],[c565,reflexivity]) ).
cnf(c393,plain,
impartial(skc12,skc15),
inference(resolution,[status(thm)],[c386,clause22]) ).
cnf(c564,plain,
( skc12 != X986
| skc15 != X987
| impartial(X986,X987) ),
inference(resolution,[status(thm)],[c21,c393]) ).
cnf(c887,plain,
( skc12 != X990
| impartial(X990,skc15) ),
inference(resolution,[status(thm)],[c564,reflexivity]) ).
cnf(clause21,axiom,
( ~ entity(X43,X44)
| existent(X43,X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(clause18,axiom,
( ~ organism(X37,X38)
| entity(X37,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c345,plain,
entity(skc12,skc10),
inference(resolution,[status(thm)],[c339,clause18]) ).
cnf(c355,plain,
existent(skc12,skc10),
inference(resolution,[status(thm)],[c345,clause21]) ).
cnf(c20,axiom,
( X474 != X475
| X476 != X473
| ~ existent(X474,X476)
| existent(X475,X473) ),
theory(equality) ).
cnf(c563,plain,
( skc12 != X983
| skc10 != X982
| existent(X983,X982) ),
inference(resolution,[status(thm)],[c20,c355]) ).
cnf(c884,plain,
( skc12 != X985
| existent(X985,skc10) ),
inference(resolution,[status(thm)],[c563,reflexivity]) ).
cnf(c392,plain,
entity(skc12,skc15),
inference(resolution,[status(thm)],[c386,clause18]) ).
cnf(c401,plain,
existent(skc12,skc15),
inference(resolution,[status(thm)],[c392,clause21]) ).
cnf(c562,plain,
( skc12 != X981
| skc15 != X980
| existent(X981,X980) ),
inference(resolution,[status(thm)],[c20,c401]) ).
cnf(c883,plain,
( skc12 != X984
| existent(X984,skc15) ),
inference(resolution,[status(thm)],[c562,reflexivity]) ).
cnf(c64,plain,
entity(skc8,skc10),
inference(resolution,[status(thm)],[clause18,c61]) ).
cnf(c72,plain,
existent(skc8,skc10),
inference(resolution,[status(thm)],[clause21,c64]) ).
cnf(c561,plain,
( skc8 != X977
| skc10 != X976
| existent(X977,X976) ),
inference(resolution,[status(thm)],[c20,c72]) ).
cnf(c880,plain,
( skc8 != X979
| existent(X979,skc10) ),
inference(resolution,[status(thm)],[c561,reflexivity]) ).
cnf(c63,plain,
entity(skc8,skc15),
inference(resolution,[status(thm)],[clause18,c62]) ).
cnf(c71,plain,
existent(skc8,skc15),
inference(resolution,[status(thm)],[clause21,c63]) ).
cnf(c560,plain,
( skc8 != X975
| skc15 != X974
| existent(X975,X974) ),
inference(resolution,[status(thm)],[c20,c71]) ).
cnf(c879,plain,
( skc8 != X978
| existent(X978,skc15) ),
inference(resolution,[status(thm)],[c560,reflexivity]) ).
cnf(c19,axiom,
( X462 != X463
| X464 != X461
| ~ entity(X462,X464)
| entity(X463,X461) ),
theory(equality) ).
cnf(c559,plain,
( skc12 != X971
| skc15 != X970
| entity(X971,X970) ),
inference(resolution,[status(thm)],[c19,c392]) ).
cnf(c876,plain,
( skc12 != X973
| entity(X973,skc15) ),
inference(resolution,[status(thm)],[c559,reflexivity]) ).
cnf(c558,plain,
( skc8 != X969
| skc10 != X968
| entity(X969,X968) ),
inference(resolution,[status(thm)],[c19,c64]) ).
cnf(c875,plain,
( skc8 != X972
| entity(X972,skc10) ),
inference(resolution,[status(thm)],[c558,reflexivity]) ).
cnf(c557,plain,
( skc12 != X965
| skc10 != X964
| entity(X965,X964) ),
inference(resolution,[status(thm)],[c19,c345]) ).
cnf(c872,plain,
( skc12 != X967
| entity(X967,skc10) ),
inference(resolution,[status(thm)],[c557,reflexivity]) ).
cnf(c556,plain,
( skc8 != X963
| skc15 != X962
| entity(X963,X962) ),
inference(resolution,[status(thm)],[c19,c63]) ).
cnf(c871,plain,
( skc8 != X966
| entity(X966,skc15) ),
inference(resolution,[status(thm)],[c556,reflexivity]) ).
cnf(c18,axiom,
( X453 != X454
| X455 != X452
| ~ organism(X453,X455)
| organism(X454,X452) ),
theory(equality) ).
cnf(c555,plain,
( skc8 != X958
| skc10 != X959
| organism(X958,X959) ),
inference(resolution,[status(thm)],[c18,c61]) ).
cnf(c868,plain,
( skc8 != X961
| organism(X961,skc10) ),
inference(resolution,[status(thm)],[c555,reflexivity]) ).
cnf(c554,plain,
( skc12 != X956
| skc15 != X957
| organism(X956,X957) ),
inference(resolution,[status(thm)],[c18,c386]) ).
cnf(c867,plain,
( skc12 != X960
| organism(X960,skc15) ),
inference(resolution,[status(thm)],[c554,reflexivity]) ).
cnf(c553,plain,
( skc12 != X952
| skc10 != X953
| organism(X952,X953) ),
inference(resolution,[status(thm)],[c18,c339]) ).
cnf(c864,plain,
( skc12 != X955
| organism(X955,skc10) ),
inference(resolution,[status(thm)],[c553,reflexivity]) ).
cnf(c552,plain,
( skc8 != X950
| skc15 != X951
| organism(X950,X951) ),
inference(resolution,[status(thm)],[c18,c62]) ).
cnf(c863,plain,
( skc8 != X954
| organism(X954,skc15) ),
inference(resolution,[status(thm)],[c552,reflexivity]) ).
cnf(c17,axiom,
( X444 != X445
| X446 != X443
| ~ human_person(X444,X446)
| human_person(X445,X443) ),
theory(equality) ).
cnf(c551,plain,
( skc12 != X946
| skc15 != X947
| human_person(X946,X947) ),
inference(resolution,[status(thm)],[c17,c382]) ).
cnf(c860,plain,
( skc12 != X949
| human_person(X949,skc15) ),
inference(resolution,[status(thm)],[c551,reflexivity]) ).
cnf(c550,plain,
( skc12 != X944
| skc10 != X945
| human_person(X944,X945) ),
inference(resolution,[status(thm)],[c17,c334]) ).
cnf(c859,plain,
( skc12 != X948
| human_person(X948,skc10) ),
inference(resolution,[status(thm)],[c550,reflexivity]) ).
cnf(c549,plain,
( skc8 != X941
| skc15 != X942
| human_person(X941,X942) ),
inference(resolution,[status(thm)],[c17,c60]) ).
cnf(c857,plain,
( skc8 != X943
| human_person(X943,skc15) ),
inference(resolution,[status(thm)],[c549,reflexivity]) ).
cnf(c546,plain,
( ~ proposition(skc12,X938)
| ~ proposition(skc12,X940)
| ~ theme(skc12,skf2(skc10),X938)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,X939)
| ~ theme(skc12,X939,X940)
| ~ agent(skc12,X939,skc10)
| X938 = X940 ),
inference(resolution,[status(thm)],[c385,clause71]) ).
cnf(c548,plain,
( skc8 != X935
| skc10 != X936
| human_person(X935,X936) ),
inference(resolution,[status(thm)],[c17,c59]) ).
cnf(c854,plain,
( skc8 != X937
| human_person(X937,skc10) ),
inference(resolution,[status(thm)],[c548,reflexivity]) ).
cnf(c547,plain,
( ~ accessible_world(skc12,X934)
| agent(X934,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c385,clause66]) ).
cnf(c545,plain,
( ~ accessible_world(skc12,X933)
| agent(X933,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c384,clause66]) ).
cnf(c544,plain,
( ~ proposition(skc12,X930)
| ~ proposition(skc12,X932)
| ~ theme(skc12,skf2(skc15),X930)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ think_believe_consider(skc12,X931)
| ~ theme(skc12,X931,X932)
| ~ agent(skc12,X931,skc15)
| X930 = X932 ),
inference(resolution,[status(thm)],[c384,clause71]) ).
cnf(c16,axiom,
( X437 != X438
| X439 != X436
| ~ man(X437,X439)
| man(X438,X436) ),
theory(equality) ).
cnf(c543,plain,
( skc12 != X928
| skc10 != X927
| man(X928,X927) ),
inference(resolution,[status(thm)],[c16,c331]) ).
cnf(c851,plain,
( skc12 != X929
| man(X929,skc10) ),
inference(resolution,[status(thm)],[c543,reflexivity]) ).
cnf(c542,plain,
( skc8 != X925
| skc15 != X924
| man(X925,X924) ),
inference(resolution,[status(thm)],[c16,clause73]) ).
cnf(c849,plain,
( skc8 != X926
| man(X926,skc15) ),
inference(resolution,[status(thm)],[c542,reflexivity]) ).
cnf(c541,plain,
( skc8 != X922
| skc10 != X921
| man(X922,X921) ),
inference(resolution,[status(thm)],[c16,clause81]) ).
cnf(c847,plain,
( skc8 != X923
| man(X923,skc10) ),
inference(resolution,[status(thm)],[c541,reflexivity]) ).
cnf(c540,plain,
( skc12 != X919
| skc15 != X918
| man(X919,X918) ),
inference(resolution,[status(thm)],[c16,c379]) ).
cnf(c845,plain,
( skc12 != X920
| man(X920,skc15) ),
inference(resolution,[status(thm)],[c540,reflexivity]) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
cnf(clause51,axiom,
( ~ accessible_world(X154,X155)
| ~ state(X154,X156)
| state(X155,X156) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c229,plain,
( ~ accessible_world(skc8,X252)
| state(X252,skc9) ),
inference(resolution,[status(thm)],[clause51,clause82]) ).
cnf(c326,plain,
state(skc12,skc9),
inference(resolution,[status(thm)],[c229,clause83]) ).
cnf(c15,axiom,
( X428 != X429
| X430 != X427
| ~ state(X428,X430)
| state(X429,X427) ),
theory(equality) ).
cnf(c539,plain,
( skc12 != X915
| skc9 != X916
| state(X915,X916) ),
inference(resolution,[status(thm)],[c15,c326]) ).
cnf(c843,plain,
( skc12 != X917
| state(X917,skc9) ),
inference(resolution,[status(thm)],[c539,reflexivity]) ).
cnf(c538,plain,
( skc8 != X912
| skc9 != X913
| state(X912,X913) ),
inference(resolution,[status(thm)],[c15,clause82]) ).
cnf(c841,plain,
( skc8 != X914
| state(X914,skc9) ),
inference(resolution,[status(thm)],[c538,reflexivity]) ).
cnf(clause12,axiom,
( ~ abstraction(X25,X26)
| general(X25,X26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(clause9,axiom,
( ~ relation(X19,X20)
| abstraction(X19,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause28,axiom,
( ~ relname(X57,X58)
| relation(X57,X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c85,plain,
relation(skc8,skc11),
inference(resolution,[status(thm)],[clause28,c83]) ).
cnf(clause47,axiom,
( ~ accessible_world(X132,X133)
| ~ relation(X132,X134)
| relation(X133,X134) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c207,plain,
( ~ accessible_world(skc8,X215)
| relation(X215,skc11) ),
inference(resolution,[status(thm)],[clause47,c85]) ).
cnf(c284,plain,
relation(skc12,skc11),
inference(resolution,[status(thm)],[c207,clause83]) ).
cnf(c286,plain,
abstraction(skc12,skc11),
inference(resolution,[status(thm)],[c284,clause9]) ).
cnf(c291,plain,
general(skc12,skc11),
inference(resolution,[status(thm)],[c286,clause12]) ).
cnf(c14,axiom,
( X419 != X420
| X421 != X418
| ~ general(X419,X421)
| general(X420,X418) ),
theory(equality) ).
cnf(c537,plain,
( skc12 != X909
| skc11 != X910
| general(X909,X910) ),
inference(resolution,[status(thm)],[c14,c291]) ).
cnf(c839,plain,
( skc12 != X911
| general(X911,skc11) ),
inference(resolution,[status(thm)],[c537,reflexivity]) ).
cnf(c86,plain,
relation(skc8,skc14),
inference(resolution,[status(thm)],[clause28,c84]) ).
cnf(c209,plain,
( ~ accessible_world(skc8,X223)
| relation(X223,skc14) ),
inference(resolution,[status(thm)],[clause47,c86]) ).
cnf(c300,plain,
relation(skc12,skc14),
inference(resolution,[status(thm)],[c209,clause83]) ).
cnf(c302,plain,
abstraction(skc12,skc14),
inference(resolution,[status(thm)],[c300,clause9]) ).
cnf(c307,plain,
general(skc12,skc14),
inference(resolution,[status(thm)],[c302,clause12]) ).
cnf(c536,plain,
( skc12 != X906
| skc14 != X907
| general(X906,X907) ),
inference(resolution,[status(thm)],[c14,c307]) ).
cnf(c837,plain,
( skc12 != X908
| general(X908,skc14) ),
inference(resolution,[status(thm)],[c536,reflexivity]) ).
cnf(c89,plain,
abstraction(skc8,skc14),
inference(resolution,[status(thm)],[c86,clause9]) ).
cnf(c97,plain,
general(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause12]) ).
cnf(c535,plain,
( skc8 != X901
| skc14 != X902
| general(X901,X902) ),
inference(resolution,[status(thm)],[c14,c97]) ).
cnf(c833,plain,
( skc8 != X905
| general(X905,skc14) ),
inference(resolution,[status(thm)],[c535,reflexivity]) ).
cnf(clause8,axiom,
( ~ proposition(X17,X18)
| relation(X17,X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
cnf(clause46,axiom,
( ~ accessible_world(X125,X126)
| ~ proposition(X125,X127)
| proposition(X126,X127) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(c204,plain,
( ~ accessible_world(skc8,X207)
| proposition(X207,skc12) ),
inference(resolution,[status(thm)],[clause46,clause84]) ).
cnf(c267,plain,
proposition(skc12,skc12),
inference(resolution,[status(thm)],[c204,clause83]) ).
cnf(c269,plain,
relation(skc12,skc12),
inference(resolution,[status(thm)],[c267,clause8]) ).
cnf(c271,plain,
abstraction(skc12,skc12),
inference(resolution,[status(thm)],[c269,clause9]) ).
cnf(c276,plain,
general(skc12,skc12),
inference(resolution,[status(thm)],[c271,clause12]) ).
cnf(c534,plain,
( skc12 != X899
| skc12 != X900
| general(X899,X900) ),
inference(resolution,[status(thm)],[c14,c276]) ).
cnf(c832,plain,
( skc12 != X904
| general(X904,skc12) ),
inference(resolution,[status(thm)],[c534,reflexivity]) ).
cnf(c831,plain,
( skc12 != X903
| general(X903,X903) ),
inference(factor,[status(thm)],[c534]) ).
cnf(c44,plain,
relation(skc8,skc12),
inference(resolution,[status(thm)],[clause8,clause84]) ).
cnf(c45,plain,
abstraction(skc8,skc12),
inference(resolution,[status(thm)],[clause9,c44]) ).
cnf(c49,plain,
general(skc8,skc12),
inference(resolution,[status(thm)],[clause12,c45]) ).
cnf(c533,plain,
( skc8 != X895
| skc12 != X896
| general(X895,X896) ),
inference(resolution,[status(thm)],[c14,c49]) ).
cnf(c828,plain,
( skc8 != X898
| general(X898,skc12) ),
inference(resolution,[status(thm)],[c533,reflexivity]) ).
cnf(c88,plain,
abstraction(skc8,skc11),
inference(resolution,[status(thm)],[c85,clause9]) ).
cnf(c93,plain,
general(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause12]) ).
cnf(c532,plain,
( skc8 != X893
| skc11 != X894
| general(X893,X894) ),
inference(resolution,[status(thm)],[c14,c93]) ).
cnf(c827,plain,
( skc8 != X897
| general(X897,skc11) ),
inference(resolution,[status(thm)],[c532,reflexivity]) ).
cnf(clause11,axiom,
( ~ abstraction(X23,X24)
| nonhuman(X23,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c304,plain,
nonhuman(skc12,skc14),
inference(resolution,[status(thm)],[c302,clause11]) ).
cnf(c13,axiom,
( X412 != X413
| X414 != X411
| ~ nonhuman(X412,X414)
| nonhuman(X413,X411) ),
theory(equality) ).
cnf(c528,plain,
( skc12 != X889
| skc14 != X890
| nonhuman(X889,X890) ),
inference(resolution,[status(thm)],[c13,c304]) ).
cnf(c824,plain,
( skc12 != X892
| nonhuman(X892,skc14) ),
inference(resolution,[status(thm)],[c528,reflexivity]) ).
cnf(c48,plain,
nonhuman(skc8,skc12),
inference(resolution,[status(thm)],[clause11,c45]) ).
cnf(c527,plain,
( skc8 != X887
| skc12 != X888
| nonhuman(X887,X888) ),
inference(resolution,[status(thm)],[c13,c48]) ).
cnf(c823,plain,
( skc8 != X891
| nonhuman(X891,skc12) ),
inference(resolution,[status(thm)],[c527,reflexivity]) ).
cnf(c273,plain,
nonhuman(skc12,skc12),
inference(resolution,[status(thm)],[c271,clause11]) ).
cnf(c526,plain,
( skc12 != X883
| skc12 != X884
| nonhuman(X883,X884) ),
inference(resolution,[status(thm)],[c13,c273]) ).
cnf(c820,plain,
( skc12 != X886
| nonhuman(X886,skc12) ),
inference(resolution,[status(thm)],[c526,reflexivity]) ).
cnf(c819,plain,
( skc12 != X885
| nonhuman(X885,X885) ),
inference(factor,[status(thm)],[c526]) ).
cnf(c96,plain,
nonhuman(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause11]) ).
cnf(c525,plain,
( skc8 != X880
| skc14 != X881
| nonhuman(X880,X881) ),
inference(resolution,[status(thm)],[c13,c96]) ).
cnf(c817,plain,
( skc8 != X882
| nonhuman(X882,skc14) ),
inference(resolution,[status(thm)],[c525,reflexivity]) ).
cnf(c92,plain,
nonhuman(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause11]) ).
cnf(c524,plain,
( skc8 != X877
| skc11 != X878
| nonhuman(X877,X878) ),
inference(resolution,[status(thm)],[c13,c92]) ).
cnf(c815,plain,
( skc8 != X879
| nonhuman(X879,skc11) ),
inference(resolution,[status(thm)],[c524,reflexivity]) ).
cnf(c288,plain,
nonhuman(skc12,skc11),
inference(resolution,[status(thm)],[c286,clause11]) ).
cnf(c523,plain,
( skc12 != X874
| skc11 != X875
| nonhuman(X874,X875) ),
inference(resolution,[status(thm)],[c13,c288]) ).
cnf(c813,plain,
( skc12 != X876
| nonhuman(X876,skc11) ),
inference(resolution,[status(thm)],[c523,reflexivity]) ).
cnf(c12,axiom,
( X405 != X406
| X407 != X404
| ~ abstraction(X405,X407)
| abstraction(X406,X404) ),
theory(equality) ).
cnf(c519,plain,
( skc8 != X872
| skc11 != X871
| abstraction(X872,X871) ),
inference(resolution,[status(thm)],[c12,c88]) ).
cnf(c811,plain,
( skc8 != X873
| abstraction(X873,skc11) ),
inference(resolution,[status(thm)],[c519,reflexivity]) ).
cnf(c518,plain,
( skc12 != X869
| skc14 != X868
| abstraction(X869,X868) ),
inference(resolution,[status(thm)],[c12,c302]) ).
cnf(c809,plain,
( skc12 != X870
| abstraction(X870,skc14) ),
inference(resolution,[status(thm)],[c518,reflexivity]) ).
cnf(c517,plain,
( skc8 != X866
| skc12 != X865
| abstraction(X866,X865) ),
inference(resolution,[status(thm)],[c12,c45]) ).
cnf(c807,plain,
( skc8 != X867
| abstraction(X867,skc12) ),
inference(resolution,[status(thm)],[c517,reflexivity]) ).
cnf(c516,plain,
( skc8 != X863
| skc14 != X862
| abstraction(X863,X862) ),
inference(resolution,[status(thm)],[c12,c89]) ).
cnf(c805,plain,
( skc8 != X864
| abstraction(X864,skc14) ),
inference(resolution,[status(thm)],[c516,reflexivity]) ).
cnf(c515,plain,
( skc12 != X860
| skc11 != X859
| abstraction(X860,X859) ),
inference(resolution,[status(thm)],[c12,c286]) ).
cnf(c803,plain,
( skc12 != X861
| abstraction(X861,skc11) ),
inference(resolution,[status(thm)],[c515,reflexivity]) ).
cnf(c514,plain,
( skc12 != X856
| skc12 != X855
| abstraction(X856,X855) ),
inference(resolution,[status(thm)],[c12,c271]) ).
cnf(c800,plain,
( skc12 != X858
| abstraction(X858,skc12) ),
inference(resolution,[status(thm)],[c514,reflexivity]) ).
cnf(c799,plain,
( skc12 != X857
| abstraction(X857,X857) ),
inference(factor,[status(thm)],[c514]) ).
cnf(c11,axiom,
( X398 != X399
| X400 != X397
| ~ relation(X398,X400)
| relation(X399,X397) ),
theory(equality) ).
cnf(c512,plain,
( skc8 != X850
| skc11 != X851
| relation(X850,X851) ),
inference(resolution,[status(thm)],[c11,c85]) ).
cnf(c795,plain,
( skc8 != X854
| relation(X854,skc11) ),
inference(resolution,[status(thm)],[c512,reflexivity]) ).
cnf(c511,plain,
( skc12 != X848
| skc12 != X849
| relation(X848,X849) ),
inference(resolution,[status(thm)],[c11,c269]) ).
cnf(c794,plain,
( skc12 != X853
| relation(X853,skc12) ),
inference(resolution,[status(thm)],[c511,reflexivity]) ).
cnf(c793,plain,
( skc12 != X852
| relation(X852,X852) ),
inference(factor,[status(thm)],[c511]) ).
cnf(c510,plain,
( skc12 != X844
| skc14 != X845
| relation(X844,X845) ),
inference(resolution,[status(thm)],[c11,c300]) ).
cnf(c790,plain,
( skc12 != X847
| relation(X847,skc14) ),
inference(resolution,[status(thm)],[c510,reflexivity]) ).
cnf(c509,plain,
( skc12 != X842
| skc11 != X843
| relation(X842,X843) ),
inference(resolution,[status(thm)],[c11,c284]) ).
cnf(c789,plain,
( skc12 != X846
| relation(X846,skc11) ),
inference(resolution,[status(thm)],[c509,reflexivity]) ).
cnf(c508,plain,
( skc8 != X838
| skc12 != X839
| relation(X838,X839) ),
inference(resolution,[status(thm)],[c11,c44]) ).
cnf(c786,plain,
( skc8 != X841
| relation(X841,skc12) ),
inference(resolution,[status(thm)],[c508,reflexivity]) ).
cnf(c507,plain,
( skc8 != X836
| skc14 != X837
| relation(X836,X837) ),
inference(resolution,[status(thm)],[c11,c86]) ).
cnf(c785,plain,
( skc8 != X840
| relation(X840,skc14) ),
inference(resolution,[status(thm)],[c507,reflexivity]) ).
cnf(c10,axiom,
( X391 != X392
| X393 != X390
| ~ proposition(X391,X393)
| proposition(X392,X390) ),
theory(equality) ).
cnf(c503,plain,
( skc12 != X833
| skc12 != X832
| proposition(X833,X832) ),
inference(resolution,[status(thm)],[c10,c267]) ).
cnf(c782,plain,
( skc12 != X835
| proposition(X835,skc12) ),
inference(resolution,[status(thm)],[c503,reflexivity]) ).
cnf(c781,plain,
( skc12 != X834
| proposition(X834,X834) ),
inference(factor,[status(thm)],[c503]) ).
cnf(c502,plain,
( skc8 != X830
| skc12 != X829
| proposition(X830,X829) ),
inference(resolution,[status(thm)],[c10,clause84]) ).
cnf(c779,plain,
( skc8 != X831
| proposition(X831,skc12) ),
inference(resolution,[status(thm)],[c502,reflexivity]) ).
cnf(clause7,axiom,
( ~ eventuality(X15,X16)
| unisex(X15,X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause2,axiom,
( ~ event(X5,X6)
| eventuality(X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
cnf(clause37,axiom,
( ~ accessible_world(X84,X85)
| ~ event(X84,X86)
| event(X85,X86) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c118,plain,
( ~ accessible_world(skc8,X87)
| event(X87,skc13) ),
inference(resolution,[status(thm)],[clause37,clause76]) ).
cnf(c120,plain,
event(skc12,skc13),
inference(resolution,[status(thm)],[c118,clause83]) ).
cnf(c121,plain,
eventuality(skc12,skc13),
inference(resolution,[status(thm)],[c120,clause2]) ).
cnf(c125,plain,
unisex(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause7]) ).
cnf(c9,axiom,
( X386 != X387
| X388 != X385
| ~ unisex(X386,X388)
| unisex(X387,X385) ),
theory(equality) ).
cnf(c494,plain,
( skc12 != X827
| skc13 != X826
| unisex(X827,X826) ),
inference(resolution,[status(thm)],[c9,c125]) ).
cnf(c777,plain,
( skc12 != X828
| unisex(X828,skc13) ),
inference(resolution,[status(thm)],[c494,reflexivity]) ).
cnf(c38,plain,
eventuality(skc8,skc13),
inference(resolution,[status(thm)],[clause2,clause76]) ).
cnf(c43,plain,
unisex(skc8,skc13),
inference(resolution,[status(thm)],[clause7,c38]) ).
cnf(c493,plain,
( skc8 != X824
| skc13 != X823
| unisex(X824,X823) ),
inference(resolution,[status(thm)],[c9,c43]) ).
cnf(c775,plain,
( skc8 != X825
| unisex(X825,skc13) ),
inference(resolution,[status(thm)],[c493,reflexivity]) ).
cnf(clause13,axiom,
( ~ abstraction(X27,X28)
| unisex(X27,X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c91,plain,
unisex(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause13]) ).
cnf(clause43,axiom,
( ~ accessible_world(X110,X111)
| ~ unisex(X110,X112)
| unisex(X111,X112) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c180,plain,
( ~ accessible_world(skc8,X177)
| unisex(X177,skc11) ),
inference(resolution,[status(thm)],[clause43,c91]) ).
cnf(c242,plain,
unisex(skc12,skc11),
inference(resolution,[status(thm)],[c180,clause83]) ).
cnf(c492,plain,
( skc12 != X821
| skc11 != X820
| unisex(X821,X820) ),
inference(resolution,[status(thm)],[c9,c242]) ).
cnf(c773,plain,
( skc12 != X822
| unisex(X822,skc11) ),
inference(resolution,[status(thm)],[c492,reflexivity]) ).
cnf(c50,plain,
unisex(skc8,skc12),
inference(resolution,[status(thm)],[clause13,c45]) ).
cnf(c183,plain,
( ~ accessible_world(skc8,X183)
| unisex(X183,skc12) ),
inference(resolution,[status(thm)],[clause43,c50]) ).
cnf(c251,plain,
unisex(skc12,skc12),
inference(resolution,[status(thm)],[c183,clause83]) ).
cnf(c491,plain,
( skc12 != X817
| skc12 != X816
| unisex(X817,X816) ),
inference(resolution,[status(thm)],[c9,c251]) ).
cnf(c770,plain,
( skc12 != X819
| unisex(X819,skc12) ),
inference(resolution,[status(thm)],[c491,reflexivity]) ).
cnf(c769,plain,
( skc12 != X818
| unisex(X818,X818) ),
inference(factor,[status(thm)],[c491]) ).
cnf(c490,plain,
( skc8 != X814
| skc12 != X813
| unisex(X814,X813) ),
inference(resolution,[status(thm)],[c9,c50]) ).
cnf(c767,plain,
( skc8 != X815
| unisex(X815,skc12) ),
inference(resolution,[status(thm)],[c490,reflexivity]) ).
cnf(clause14,axiom,
( ~ state(X29,X30)
| eventuality(X29,X30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c51,plain,
eventuality(skc8,skc9),
inference(resolution,[status(thm)],[clause14,clause82]) ).
cnf(c55,plain,
unisex(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause7]) ).
cnf(c489,plain,
( skc8 != X811
| skc9 != X810
| unisex(X811,X810) ),
inference(resolution,[status(thm)],[c9,c55]) ).
cnf(c765,plain,
( skc8 != X812
| unisex(X812,skc9) ),
inference(resolution,[status(thm)],[c489,reflexivity]) ).
cnf(c95,plain,
unisex(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause13]) ).
cnf(c181,plain,
( ~ accessible_world(skc8,X178)
| unisex(X178,skc14) ),
inference(resolution,[status(thm)],[clause43,c95]) ).
cnf(c245,plain,
unisex(skc12,skc14),
inference(resolution,[status(thm)],[c181,clause83]) ).
cnf(c488,plain,
( skc12 != X808
| skc14 != X807
| unisex(X808,X807) ),
inference(resolution,[status(thm)],[c9,c245]) ).
cnf(c763,plain,
( skc12 != X809
| unisex(X809,skc14) ),
inference(resolution,[status(thm)],[c488,reflexivity]) ).
cnf(c487,plain,
( skc8 != X805
| skc14 != X804
| unisex(X805,X804) ),
inference(resolution,[status(thm)],[c9,c95]) ).
cnf(c761,plain,
( skc8 != X806
| unisex(X806,skc14) ),
inference(resolution,[status(thm)],[c487,reflexivity]) ).
cnf(c486,plain,
( skc8 != X802
| skc11 != X801
| unisex(X802,X801) ),
inference(resolution,[status(thm)],[c9,c91]) ).
cnf(c759,plain,
( skc8 != X803
| unisex(X803,skc11) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(c362,plain,
eventuality(skc12,skf2(X273)),
inference(resolution,[status(thm)],[c360,clause2]) ).
cnf(c367,plain,
unisex(skc12,skf2(X278)),
inference(resolution,[status(thm)],[c362,clause7]) ).
cnf(c485,plain,
( skc12 != X796
| skf2(X797) != X795
| unisex(X796,X795) ),
inference(resolution,[status(thm)],[c9,c367]) ).
cnf(c757,plain,
( skc12 != X798
| unisex(X798,skf2(X799)) ),
inference(resolution,[status(thm)],[c485,reflexivity]) ).
cnf(clause15,axiom,
( ~ state(X31,X32)
| event(X31,X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c52,plain,
event(skc8,skc9),
inference(resolution,[status(thm)],[clause15,clause82]) ).
cnf(c119,plain,
( ~ accessible_world(skc8,X94)
| event(X94,skc9) ),
inference(resolution,[status(thm)],[clause37,c52]) ).
cnf(c141,plain,
event(skc12,skc9),
inference(resolution,[status(thm)],[c119,clause83]) ).
cnf(c142,plain,
eventuality(skc12,skc9),
inference(resolution,[status(thm)],[c141,clause2]) ).
cnf(c147,plain,
unisex(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause7]) ).
cnf(c484,plain,
( skc12 != X793
| skc9 != X792
| unisex(X793,X792) ),
inference(resolution,[status(thm)],[c9,c147]) ).
cnf(c755,plain,
( skc12 != X794
| unisex(X794,skc9) ),
inference(resolution,[status(thm)],[c484,reflexivity]) ).
cnf(clause6,axiom,
( ~ eventuality(X13,X14)
| nonexistent(X13,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c53,plain,
nonexistent(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause6]) ).
cnf(c8,axiom,
( X378 != X379
| X380 != X377
| ~ nonexistent(X378,X380)
| nonexistent(X379,X377) ),
theory(equality) ).
cnf(c481,plain,
( skc8 != X790
| skc9 != X789
| nonexistent(X790,X789) ),
inference(resolution,[status(thm)],[c8,c53]) ).
cnf(c753,plain,
( skc8 != X791
| nonexistent(X791,skc9) ),
inference(resolution,[status(thm)],[c481,reflexivity]) ).
cnf(c148,plain,
nonexistent(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause6]) ).
cnf(c480,plain,
( skc12 != X787
| skc9 != X786
| nonexistent(X787,X786) ),
inference(resolution,[status(thm)],[c8,c148]) ).
cnf(c751,plain,
( skc12 != X788
| nonexistent(X788,skc9) ),
inference(resolution,[status(thm)],[c480,reflexivity]) ).
cnf(c368,plain,
nonexistent(skc12,skf2(X279)),
inference(resolution,[status(thm)],[c362,clause6]) ).
cnf(c478,plain,
( skc12 != X782
| skf2(X780) != X781
| nonexistent(X782,X781) ),
inference(resolution,[status(thm)],[c8,c368]) ).
cnf(c749,plain,
( skc12 != X784
| nonexistent(X784,skf2(X783)) ),
inference(resolution,[status(thm)],[c478,reflexivity]) ).
cnf(c123,plain,
nonexistent(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause6]) ).
cnf(c479,plain,
( skc12 != X778
| skc13 != X777
| nonexistent(X778,X777) ),
inference(resolution,[status(thm)],[c8,c123]) ).
cnf(c747,plain,
( skc12 != X779
| nonexistent(X779,skc13) ),
inference(resolution,[status(thm)],[c479,reflexivity]) ).
cnf(c42,plain,
nonexistent(skc8,skc13),
inference(resolution,[status(thm)],[clause6,c38]) ).
cnf(c477,plain,
( skc8 != X775
| skc13 != X774
| nonexistent(X775,X774) ),
inference(resolution,[status(thm)],[c8,c42]) ).
cnf(c745,plain,
( skc8 != X776
| nonexistent(X776,skc13) ),
inference(resolution,[status(thm)],[c477,reflexivity]) ).
cnf(clause20,axiom,
( ~ entity(X41,X42)
| specific(X41,X42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c69,plain,
specific(skc8,skc15),
inference(resolution,[status(thm)],[clause20,c63]) ).
cnf(c7,axiom,
( X371 != X372
| X373 != X370
| ~ specific(X371,X373)
| specific(X372,X370) ),
theory(equality) ).
cnf(c475,plain,
( skc8 != X772
| skc15 != X771
| specific(X772,X771) ),
inference(resolution,[status(thm)],[c7,c69]) ).
cnf(c743,plain,
( skc8 != X773
| specific(X773,skc15) ),
inference(resolution,[status(thm)],[c475,reflexivity]) ).
cnf(clause5,axiom,
( ~ eventuality(X11,X12)
| specific(X11,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c126,plain,
specific(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause5]) ).
cnf(c474,plain,
( skc12 != X769
| skc13 != X768
| specific(X769,X768) ),
inference(resolution,[status(thm)],[c7,c126]) ).
cnf(c741,plain,
( skc12 != X770
| specific(X770,skc13) ),
inference(resolution,[status(thm)],[c474,reflexivity]) ).
cnf(c70,plain,
specific(skc8,skc10),
inference(resolution,[status(thm)],[clause20,c64]) ).
cnf(clause41,axiom,
( ~ accessible_world(X98,X99)
| ~ specific(X98,X100)
| specific(X99,X100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c163,plain,
( ~ accessible_world(skc8,X153)
| specific(X153,skc10) ),
inference(resolution,[status(thm)],[clause41,c70]) ).
cnf(c226,plain,
specific(skc12,skc10),
inference(resolution,[status(thm)],[c163,clause83]) ).
cnf(c473,plain,
( skc12 != X766
| skc10 != X765
| specific(X766,X765) ),
inference(resolution,[status(thm)],[c7,c226]) ).
cnf(c739,plain,
( skc12 != X767
| specific(X767,skc10) ),
inference(resolution,[status(thm)],[c473,reflexivity]) ).
cnf(c144,plain,
specific(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause5]) ).
cnf(c472,plain,
( skc12 != X763
| skc9 != X762
| specific(X763,X762) ),
inference(resolution,[status(thm)],[c7,c144]) ).
cnf(c737,plain,
( skc12 != X764
| specific(X764,skc9) ),
inference(resolution,[status(thm)],[c472,reflexivity]) ).
cnf(c41,plain,
specific(skc8,skc13),
inference(resolution,[status(thm)],[clause5,c38]) ).
cnf(c471,plain,
( skc8 != X760
| skc13 != X759
| specific(X760,X759) ),
inference(resolution,[status(thm)],[c7,c41]) ).
cnf(c735,plain,
( skc8 != X761
| specific(X761,skc13) ),
inference(resolution,[status(thm)],[c471,reflexivity]) ).
cnf(c167,plain,
( ~ accessible_world(skc8,X160)
| specific(X160,skc15) ),
inference(resolution,[status(thm)],[clause41,c69]) ).
cnf(c231,plain,
specific(skc12,skc15),
inference(resolution,[status(thm)],[c167,clause83]) ).
cnf(c470,plain,
( skc12 != X757
| skc15 != X756
| specific(X757,X756) ),
inference(resolution,[status(thm)],[c7,c231]) ).
cnf(c733,plain,
( skc12 != X758
| specific(X758,skc15) ),
inference(resolution,[status(thm)],[c470,reflexivity]) ).
cnf(c469,plain,
( skc8 != X754
| skc10 != X753
| specific(X754,X753) ),
inference(resolution,[status(thm)],[c7,c70]) ).
cnf(c731,plain,
( skc8 != X755
| specific(X755,skc10) ),
inference(resolution,[status(thm)],[c469,reflexivity]) ).
cnf(c364,plain,
specific(skc12,skf2(X274)),
inference(resolution,[status(thm)],[c362,clause5]) ).
cnf(c468,plain,
( skc12 != X748
| skf2(X749) != X747
| specific(X748,X747) ),
inference(resolution,[status(thm)],[c7,c364]) ).
cnf(c729,plain,
( skc12 != X751
| specific(X751,skf2(X750)) ),
inference(resolution,[status(thm)],[c468,reflexivity]) ).
cnf(c56,plain,
specific(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause5]) ).
cnf(c467,plain,
( skc8 != X745
| skc9 != X744
| specific(X745,X744) ),
inference(resolution,[status(thm)],[c7,c56]) ).
cnf(c727,plain,
( skc8 != X746
| specific(X746,skc9) ),
inference(resolution,[status(thm)],[c467,reflexivity]) ).
cnf(clause4,axiom,
( ~ thing(X9,X10)
| singleton(X9,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause3,axiom,
( ~ eventuality(X7,X8)
| thing(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c366,plain,
thing(skc12,skf2(X277)),
inference(resolution,[status(thm)],[c362,clause3]) ).
cnf(c372,plain,
singleton(skc12,skf2(X284)),
inference(resolution,[status(thm)],[c366,clause4]) ).
cnf(c6,axiom,
( X363 != X364
| X365 != X362
| ~ singleton(X363,X365)
| singleton(X364,X362) ),
theory(equality) ).
cnf(c459,plain,
( skc12 != X740
| skf2(X739) != X738
| singleton(X740,X738) ),
inference(resolution,[status(thm)],[c6,c372]) ).
cnf(c725,plain,
( skc12 != X742
| singleton(X742,skf2(X741)) ),
inference(resolution,[status(thm)],[c459,reflexivity]) ).
cnf(c124,plain,
thing(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause3]) ).
cnf(c127,plain,
singleton(skc12,skc13),
inference(resolution,[status(thm)],[c124,clause4]) ).
cnf(c464,plain,
( skc12 != X736
| skc13 != X735
| singleton(X736,X735) ),
inference(resolution,[status(thm)],[c6,c127]) ).
cnf(c723,plain,
( skc12 != X737
| singleton(X737,skc13) ),
inference(resolution,[status(thm)],[c464,reflexivity]) ).
cnf(c5,axiom,
( X356 != X357
| X358 != X355
| ~ thing(X356,X358)
| thing(X357,X355) ),
theory(equality) ).
cnf(c447,plain,
( skc12 != X729
| skf2(X731) != X730
| thing(X729,X730) ),
inference(resolution,[status(thm)],[c5,c366]) ).
cnf(c721,plain,
( skc12 != X733
| thing(X733,skf2(X732)) ),
inference(resolution,[status(thm)],[c447,reflexivity]) ).
cnf(clause10,axiom,
( ~ abstraction(X21,X22)
| thing(X21,X22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c94,plain,
thing(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause10]) ).
cnf(c100,plain,
singleton(skc8,skc14),
inference(resolution,[status(thm)],[c94,clause4]) ).
cnf(c463,plain,
( skc8 != X727
| skc14 != X726
| singleton(X727,X726) ),
inference(resolution,[status(thm)],[c6,c100]) ).
cnf(c719,plain,
( skc8 != X728
| singleton(X728,skc14) ),
inference(resolution,[status(thm)],[c463,reflexivity]) ).
cnf(c4,axiom,
( X349 != X350
| X351 != X348
| ~ eventuality(X349,X351)
| eventuality(X350,X348) ),
theory(equality) ).
cnf(c428,plain,
( skc12 != X719
| skf2(X721) != X720
| eventuality(X719,X720) ),
inference(resolution,[status(thm)],[c4,c362]) ).
cnf(c717,plain,
( skc12 != X723
| eventuality(X723,skf2(X724)) ),
inference(resolution,[status(thm)],[c428,reflexivity]) ).
cnf(c3,axiom,
( X342 != X343
| X344 != X341
| ~ event(X342,X344)
| event(X343,X341) ),
theory(equality) ).
cnf(c422,plain,
( skc12 != X713
| skf2(X712) != X714
| event(X713,X714) ),
inference(resolution,[status(thm)],[c3,c360]) ).
cnf(c713,plain,
( skc12 != X717
| event(X717,skf2(X718)) ),
inference(resolution,[status(thm)],[c422,reflexivity]) ).
cnf(c46,plain,
thing(skc8,skc12),
inference(resolution,[status(thm)],[clause10,c45]) ).
cnf(clause39,axiom,
( ~ accessible_world(X91,X92)
| ~ thing(X91,X93)
| thing(X92,X93) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c136,plain,
( ~ accessible_world(skc8,X114)
| thing(X114,skc12) ),
inference(resolution,[status(thm)],[clause39,c46]) ).
cnf(c190,plain,
thing(skc12,skc12),
inference(resolution,[status(thm)],[c136,clause83]) ).
cnf(c192,plain,
singleton(skc12,skc12),
inference(resolution,[status(thm)],[c190,clause4]) ).
cnf(c462,plain,
( skc12 != X711
| skc12 != X710
| singleton(X711,X710) ),
inference(resolution,[status(thm)],[c6,c192]) ).
cnf(c712,plain,
( skc12 != X716
| singleton(X716,skc12) ),
inference(resolution,[status(thm)],[c462,reflexivity]) ).
cnf(c711,plain,
( skc12 != X715
| singleton(X715,X715) ),
inference(factor,[status(thm)],[c462]) ).
cnf(c2,axiom,
( X335 != X336
| X337 != X334
| ~ smoke(X335,X337)
| smoke(X336,X334) ),
theory(equality) ).
cnf(c416,plain,
( skc12 != X704
| skf2(X703) != X705
| smoke(X704,X705) ),
inference(resolution,[status(thm)],[c2,c359]) ).
cnf(c708,plain,
( skc12 != X707
| smoke(X707,skf2(X708)) ),
inference(resolution,[status(thm)],[c416,reflexivity]) ).
cnf(clause19,axiom,
( ~ entity(X39,X40)
| thing(X39,X40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c65,plain,
thing(skc8,skc15),
inference(resolution,[status(thm)],[clause19,c63]) ).
cnf(c67,plain,
singleton(skc8,skc15),
inference(resolution,[status(thm)],[c65,clause4]) ).
cnf(c461,plain,
( skc8 != X702
| skc15 != X701
| singleton(X702,X701) ),
inference(resolution,[status(thm)],[c6,c67]) ).
cnf(c707,plain,
( skc8 != X706
| singleton(X706,skc15) ),
inference(resolution,[status(thm)],[c461,reflexivity]) ).
cnf(c66,plain,
thing(skc8,skc10),
inference(resolution,[status(thm)],[clause19,c64]) ).
cnf(c137,plain,
( ~ accessible_world(skc8,X118)
| thing(X118,skc10) ),
inference(resolution,[status(thm)],[clause39,c66]) ).
cnf(c195,plain,
thing(skc12,skc10),
inference(resolution,[status(thm)],[c137,clause83]) ).
cnf(c196,plain,
singleton(skc12,skc10),
inference(resolution,[status(thm)],[c195,clause4]) ).
cnf(c460,plain,
( skc12 != X699
| skc10 != X698
| singleton(X699,X698) ),
inference(resolution,[status(thm)],[c6,c196]) ).
cnf(c705,plain,
( skc12 != X700
| singleton(X700,skc10) ),
inference(resolution,[status(thm)],[c460,reflexivity]) ).
cnf(c39,plain,
thing(skc8,skc13),
inference(resolution,[status(thm)],[clause3,c38]) ).
cnf(c40,plain,
singleton(skc8,skc13),
inference(resolution,[status(thm)],[clause4,c39]) ).
cnf(c458,plain,
( skc8 != X686
| skc13 != X685
| singleton(X686,X685) ),
inference(resolution,[status(thm)],[c6,c40]) ).
cnf(c702,plain,
( skc8 != X687
| singleton(X687,skc13) ),
inference(resolution,[status(thm)],[c458,reflexivity]) ).
cnf(c90,plain,
thing(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause10]) ).
cnf(c99,plain,
singleton(skc8,skc11),
inference(resolution,[status(thm)],[c90,clause4]) ).
cnf(c457,plain,
( skc8 != X683
| skc11 != X682
| singleton(X683,X682) ),
inference(resolution,[status(thm)],[c6,c99]) ).
cnf(c700,plain,
( skc8 != X684
| singleton(X684,skc11) ),
inference(resolution,[status(thm)],[c457,reflexivity]) ).
cnf(c68,plain,
singleton(skc8,skc10),
inference(resolution,[status(thm)],[c66,clause4]) ).
cnf(c456,plain,
( skc8 != X671
| skc10 != X670
| singleton(X671,X670) ),
inference(resolution,[status(thm)],[c6,c68]) ).
cnf(c695,plain,
( skc8 != X672
| singleton(X672,skc10) ),
inference(resolution,[status(thm)],[c456,reflexivity]) ).
cnf(c47,plain,
singleton(skc8,skc12),
inference(resolution,[status(thm)],[c46,clause4]) ).
cnf(c455,plain,
( skc8 != X665
| skc12 != X664
| singleton(X665,X664) ),
inference(resolution,[status(thm)],[c6,c47]) ).
cnf(c692,plain,
( skc8 != X669
| singleton(X669,skc12) ),
inference(resolution,[status(thm)],[c455,reflexivity]) ).
cnf(c351,plain,
( ~ proposition(skc8,X666)
| ~ proposition(skc8,X668)
| ~ theme(skc8,skc13,X666)
| ~ think_believe_consider(skc8,skc13)
| ~ think_believe_consider(skc8,X667)
| ~ theme(skc8,X667,X668)
| ~ agent(skc8,X667,skc15)
| X666 = X668 ),
inference(resolution,[status(thm)],[clause71,clause86]) ).
cnf(c133,plain,
( ~ accessible_world(skc8,X108)
| thing(X108,skc15) ),
inference(resolution,[status(thm)],[clause39,c65]) ).
cnf(c174,plain,
thing(skc12,skc15),
inference(resolution,[status(thm)],[c133,clause83]) ).
cnf(c175,plain,
singleton(skc12,skc15),
inference(resolution,[status(thm)],[c174,clause4]) ).
cnf(c454,plain,
( skc12 != X662
| skc15 != X661
| singleton(X662,X661) ),
inference(resolution,[status(thm)],[c6,c175]) ).
cnf(c690,plain,
( skc12 != X663
| singleton(X663,skc15) ),
inference(resolution,[status(thm)],[c454,reflexivity]) ).
cnf(c134,plain,
( ~ accessible_world(skc8,X109)
| thing(X109,skc11) ),
inference(resolution,[status(thm)],[clause39,c90]) ).
cnf(c178,plain,
thing(skc12,skc11),
inference(resolution,[status(thm)],[c134,clause83]) ).
cnf(c186,plain,
singleton(skc12,skc11),
inference(resolution,[status(thm)],[c178,clause4]) ).
cnf(c453,plain,
( skc12 != X654
| skc11 != X653
| singleton(X654,X653) ),
inference(resolution,[status(thm)],[c6,c186]) ).
cnf(c684,plain,
( skc12 != X655
| singleton(X655,skc11) ),
inference(resolution,[status(thm)],[c453,reflexivity]) ).
cnf(c140,plain,
( ~ accessible_world(skc8,X124)
| thing(X124,skc14) ),
inference(resolution,[status(thm)],[clause39,c94]) ).
cnf(c201,plain,
thing(skc12,skc14),
inference(resolution,[status(thm)],[c140,clause83]) ).
cnf(c202,plain,
singleton(skc12,skc14),
inference(resolution,[status(thm)],[c201,clause4]) ).
cnf(c452,plain,
( skc12 != X651
| skc14 != X650
| singleton(X651,X650) ),
inference(resolution,[status(thm)],[c6,c202]) ).
cnf(c682,plain,
( skc12 != X652
| singleton(X652,skc14) ),
inference(resolution,[status(thm)],[c452,reflexivity]) ).
cnf(c338,plain,
( ~ forename(skc8,skc11)
| ~ of(skc8,X649,skc10)
| ~ forename(skc8,X649)
| ~ entity(skc8,skc10)
| X649 = skc11 ),
inference(resolution,[status(thm)],[clause70,clause88]) ).
cnf(c146,plain,
thing(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause3]) ).
cnf(c150,plain,
singleton(skc12,skc9),
inference(resolution,[status(thm)],[c146,clause4]) ).
cnf(c451,plain,
( skc12 != X647
| skc9 != X646
| singleton(X647,X646) ),
inference(resolution,[status(thm)],[c6,c150]) ).
cnf(c679,plain,
( skc12 != X648
| singleton(X648,skc9) ),
inference(resolution,[status(thm)],[c451,reflexivity]) ).
cnf(c54,plain,
thing(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause3]) ).
cnf(c58,plain,
singleton(skc8,skc9),
inference(resolution,[status(thm)],[c54,clause4]) ).
cnf(c450,plain,
( skc8 != X643
| skc9 != X642
| singleton(X643,X642) ),
inference(resolution,[status(thm)],[c6,c58]) ).
cnf(c676,plain,
( skc8 != X645
| singleton(X645,skc9) ),
inference(resolution,[status(thm)],[c450,reflexivity]) ).
cnf(c337,plain,
( ~ forename(skc8,skc14)
| ~ of(skc8,X644,skc15)
| ~ forename(skc8,X644)
| ~ entity(skc8,skc15)
| X644 = skc14 ),
inference(resolution,[status(thm)],[clause70,clause85]) ).
cnf(c446,plain,
( skc8 != X639
| skc14 != X640
| thing(X639,X640) ),
inference(resolution,[status(thm)],[c5,c94]) ).
cnf(c674,plain,
( skc8 != X641
| thing(X641,skc14) ),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c445,plain,
( skc8 != X633
| skc13 != X634
| thing(X633,X634) ),
inference(resolution,[status(thm)],[c5,c39]) ).
cnf(c672,plain,
( skc8 != X635
| thing(X635,skc13) ),
inference(resolution,[status(thm)],[c445,reflexivity]) ).
cnf(c444,plain,
( skc12 != X630
| skc11 != X631
| thing(X630,X631) ),
inference(resolution,[status(thm)],[c5,c178]) ).
cnf(c670,plain,
( skc12 != X632
| thing(X632,skc11) ),
inference(resolution,[status(thm)],[c444,reflexivity]) ).
cnf(c443,plain,
( skc12 != X621
| skc15 != X622
| thing(X621,X622) ),
inference(resolution,[status(thm)],[c5,c174]) ).
cnf(c664,plain,
( skc12 != X623
| thing(X623,skc15) ),
inference(resolution,[status(thm)],[c443,reflexivity]) ).
cnf(c442,plain,
( skc12 != X612
| skc13 != X613
| thing(X612,X613) ),
inference(resolution,[status(thm)],[c5,c124]) ).
cnf(c660,plain,
( skc12 != X620
| thing(X620,skc13) ),
inference(resolution,[status(thm)],[c442,reflexivity]) ).
cnf(c441,plain,
( skc8 != X609
| skc10 != X610
| thing(X609,X610) ),
inference(resolution,[status(thm)],[c5,c66]) ).
cnf(c658,plain,
( skc8 != X611
| thing(X611,skc10) ),
inference(resolution,[status(thm)],[c441,reflexivity]) ).
cnf(c440,plain,
( skc8 != X600
| skc12 != X601
| thing(X600,X601) ),
inference(resolution,[status(thm)],[c5,c46]) ).
cnf(c652,plain,
( skc8 != X602
| thing(X602,skc12) ),
inference(resolution,[status(thm)],[c440,reflexivity]) ).
cnf(c439,plain,
( skc12 != X592
| skc12 != X593
| thing(X592,X593) ),
inference(resolution,[status(thm)],[c5,c190]) ).
cnf(c647,plain,
( skc12 != X599
| thing(X599,skc12) ),
inference(resolution,[status(thm)],[c439,reflexivity]) ).
cnf(c646,plain,
( skc12 != X594
| thing(X594,X594) ),
inference(factor,[status(thm)],[c439]) ).
cnf(c438,plain,
( skc12 != X589
| skc10 != X590
| thing(X589,X590) ),
inference(resolution,[status(thm)],[c5,c195]) ).
cnf(c644,plain,
( skc12 != X591
| thing(X591,skc10) ),
inference(resolution,[status(thm)],[c438,reflexivity]) ).
cnf(c437,plain,
( skc8 != X582
| skc9 != X583
| thing(X582,X583) ),
inference(resolution,[status(thm)],[c5,c54]) ).
cnf(c639,plain,
( skc8 != X584
| thing(X584,skc9) ),
inference(resolution,[status(thm)],[c437,reflexivity]) ).
cnf(c436,plain,
( skc8 != X575
| skc11 != X576
| thing(X575,X576) ),
inference(resolution,[status(thm)],[c5,c90]) ).
cnf(c636,plain,
( skc8 != X581
| thing(X581,skc11) ),
inference(resolution,[status(thm)],[c436,reflexivity]) ).
cnf(c435,plain,
( skc12 != X572
| skc14 != X573
| thing(X572,X573) ),
inference(resolution,[status(thm)],[c5,c201]) ).
cnf(c634,plain,
( skc12 != X574
| thing(X574,skc14) ),
inference(resolution,[status(thm)],[c435,reflexivity]) ).
cnf(c434,plain,
( skc8 != X561
| skc15 != X562
| thing(X561,X562) ),
inference(resolution,[status(thm)],[c5,c65]) ).
cnf(c630,plain,
( skc8 != X563
| thing(X563,skc15) ),
inference(resolution,[status(thm)],[c434,reflexivity]) ).
cnf(c433,plain,
( skc12 != X558
| skc9 != X559
| thing(X558,X559) ),
inference(resolution,[status(thm)],[c5,c146]) ).
cnf(c628,plain,
( skc12 != X560
| thing(X560,skc9) ),
inference(resolution,[status(thm)],[c433,reflexivity]) ).
cnf(c430,plain,
( skc8 != X551
| skc9 != X552
| eventuality(X551,X552) ),
inference(resolution,[status(thm)],[c4,c51]) ).
cnf(c624,plain,
( skc8 != X553
| eventuality(X553,skc9) ),
inference(resolution,[status(thm)],[c430,reflexivity]) ).
cnf(c429,plain,
( skc12 != X544
| skc9 != X545
| eventuality(X544,X545) ),
inference(resolution,[status(thm)],[c4,c142]) ).
cnf(c620,plain,
( skc12 != X550
| eventuality(X550,skc9) ),
inference(resolution,[status(thm)],[c429,reflexivity]) ).
cnf(c427,plain,
( skc8 != X541
| skc13 != X542
| eventuality(X541,X542) ),
inference(resolution,[status(thm)],[c4,c38]) ).
cnf(c618,plain,
( skc8 != X543
| eventuality(X543,skc13) ),
inference(resolution,[status(thm)],[c427,reflexivity]) ).
cnf(c426,plain,
( skc12 != X534
| skc13 != X535
| eventuality(X534,X535) ),
inference(resolution,[status(thm)],[c4,c121]) ).
cnf(c612,plain,
( skc12 != X536
| eventuality(X536,skc13) ),
inference(resolution,[status(thm)],[c426,reflexivity]) ).
cnf(c423,plain,
( skc12 != X531
| skc13 != X532
| event(X531,X532) ),
inference(resolution,[status(thm)],[c3,c120]) ).
cnf(c610,plain,
( skc12 != X533
| event(X533,skc13) ),
inference(resolution,[status(thm)],[c423,reflexivity]) ).
cnf(c421,plain,
( skc8 != X524
| skc13 != X525
| event(X524,X525) ),
inference(resolution,[status(thm)],[c3,clause76]) ).
cnf(c604,plain,
( skc8 != X526
| event(X526,skc13) ),
inference(resolution,[status(thm)],[c421,reflexivity]) ).
cnf(c420,plain,
( skc12 != X517
| skc9 != X518
| event(X517,X518) ),
inference(resolution,[status(thm)],[c3,c141]) ).
cnf(c598,plain,
( skc12 != X523
| event(X523,skc9) ),
inference(resolution,[status(thm)],[c420,reflexivity]) ).
cnf(c419,plain,
( skc8 != X514
| skc9 != X515
| event(X514,X515) ),
inference(resolution,[status(thm)],[c3,c52]) ).
cnf(c596,plain,
( skc8 != X516
| event(X516,skc9) ),
inference(resolution,[status(thm)],[c419,reflexivity]) ).
cnf(c581,plain,
( ~ accessible_world(skc12,X508)
| of(X508,skc11,skc10) ),
inference(resolution,[status(thm)],[c580,clause68]) ).
cnf(c578,plain,
( ~ accessible_world(skc12,X507)
| of(X507,skc14,skc15) ),
inference(resolution,[status(thm)],[c577,clause68]) ).
cnf(c572,plain,
( ~ accessible_world(skc12,X506)
| theme(X506,skc13,skc12) ),
inference(resolution,[status(thm)],[c571,clause67]) ).
cnf(c570,plain,
( ~ accessible_world(skc12,X501)
| agent(X501,skc13,skc15) ),
inference(resolution,[status(thm)],[c568,clause66]) ).
cnf(clause40,axiom,
( ~ accessible_world(X95,X96)
| ~ singleton(X95,X97)
| singleton(X96,X97) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c378,plain,
( ~ accessible_world(skc12,X491)
| singleton(X491,skf2(X492)) ),
inference(resolution,[status(thm)],[c372,clause40]) ).
cnf(c377,plain,
( ~ accessible_world(skc12,X486)
| present(X486,skf2(X485)) ),
inference(resolution,[status(thm)],[c371,clause44]) ).
cnf(clause42,axiom,
( ~ accessible_world(X105,X106)
| ~ nonexistent(X105,X107)
| nonexistent(X106,X107) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c376,plain,
( ~ accessible_world(skc12,X483)
| nonexistent(X483,skf2(X484)) ),
inference(resolution,[status(thm)],[c368,clause42]) ).
cnf(c374,plain,
( ~ accessible_world(skc12,X482)
| unisex(X482,skf2(X481)) ),
inference(resolution,[status(thm)],[c367,clause43]) ).
cnf(c373,plain,
( ~ accessible_world(skc12,X480)
| thing(X480,skf2(X479)) ),
inference(resolution,[status(thm)],[c366,clause39]) ).
cnf(c369,plain,
( ~ accessible_world(skc12,X477)
| specific(X477,skf2(X478)) ),
inference(resolution,[status(thm)],[c364,clause41]) ).
cnf(clause38,axiom,
( ~ accessible_world(X88,X89)
| ~ eventuality(X88,X90)
| eventuality(X89,X90) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c365,plain,
( ~ accessible_world(skc12,X471)
| eventuality(X471,skf2(X472)) ),
inference(resolution,[status(thm)],[c362,clause38]) ).
cnf(c363,plain,
( ~ accessible_world(skc12,X470)
| event(X470,skf2(X469)) ),
inference(resolution,[status(thm)],[c360,clause37]) ).
cnf(clause36,axiom,
( ~ accessible_world(X77,X78)
| ~ smoke(X77,X79)
| smoke(X78,X79) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c361,plain,
( ~ accessible_world(skc12,X468)
| smoke(X468,skf2(X467)) ),
inference(resolution,[status(thm)],[c359,clause36]) ).
cnf(c530,plain,
( ~ accessible_world(skc12,X466)
| jules_forename(X466,skc11) ),
inference(resolution,[status(thm)],[c529,clause65]) ).
cnf(c522,plain,
( ~ accessible_world(skc12,X465)
| vincent_forename(X465,skc14) ),
inference(resolution,[status(thm)],[c520,clause64]) ).
cnf(clause63,axiom,
( ~ accessible_world(X220,X221)
| ~ relname(X220,X222)
| relname(X221,X222) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
cnf(c504,plain,
( ~ accessible_world(skc12,X460)
| relname(X460,skc14) ),
inference(resolution,[status(thm)],[c500,clause63]) ).
cnf(c501,plain,
( ~ accessible_world(skc12,X459)
| forename(X459,skc14) ),
inference(resolution,[status(thm)],[c499,clause62]) ).
cnf(c497,plain,
( ~ accessible_world(skc12,X458)
| relname(X458,skc11) ),
inference(resolution,[status(thm)],[c495,clause63]) ).
cnf(c496,plain,
( ~ accessible_world(skc12,X457)
| forename(X457,skc11) ),
inference(resolution,[status(thm)],[c483,clause62]) ).
cnf(clause56,axiom,
( ~ accessible_world(X184,X185)
| ~ existent(X184,X186)
| existent(X185,X186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
cnf(c404,plain,
( ~ accessible_world(skc12,X456)
| existent(X456,skc15) ),
inference(resolution,[status(thm)],[c401,clause56]) ).
cnf(clause57,axiom,
( ~ accessible_world(X189,X190)
| ~ impartial(X189,X191)
| impartial(X190,X191) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
cnf(c402,plain,
( ~ accessible_world(skc12,X451)
| impartial(X451,skc15) ),
inference(resolution,[status(thm)],[c393,clause57]) ).
cnf(clause55,axiom,
( ~ accessible_world(X179,X180)
| ~ entity(X179,X181)
| entity(X180,X181) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
cnf(c400,plain,
( ~ accessible_world(skc12,X450)
| entity(X450,skc15) ),
inference(resolution,[status(thm)],[c392,clause55]) ).
cnf(clause58,axiom,
( ~ accessible_world(X196,X197)
| ~ living(X196,X198)
| living(X197,X198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
cnf(c396,plain,
( ~ accessible_world(skc12,X449)
| living(X449,skc15) ),
inference(resolution,[status(thm)],[c390,clause58]) ).
cnf(clause59,axiom,
( ~ accessible_world(X203,X204)
| ~ human(X203,X205)
| human(X204,X205) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
cnf(c395,plain,
( ~ accessible_world(skc12,X448)
| human(X448,skc15) ),
inference(resolution,[status(thm)],[c389,clause59]) ).
cnf(clause60,axiom,
( ~ accessible_world(X208,X209)
| ~ animate(X208,X210)
| animate(X209,X210) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
cnf(c394,plain,
( ~ accessible_world(skc12,X447)
| animate(X447,skc15) ),
inference(resolution,[status(thm)],[c387,clause60]) ).
cnf(clause54,axiom,
( ~ accessible_world(X173,X174)
| ~ organism(X173,X175)
| organism(X174,X175) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
cnf(c391,plain,
( ~ accessible_world(skc12,X442)
| organism(X442,skc15) ),
inference(resolution,[status(thm)],[c386,clause54]) ).
cnf(clause53,axiom,
( ~ accessible_world(X167,X168)
| ~ human_person(X167,X169)
| human_person(X168,X169) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(c388,plain,
( ~ accessible_world(skc12,X441)
| human_person(X441,skc15) ),
inference(resolution,[status(thm)],[c382,clause53]) ).
cnf(clause61,axiom,
( ~ accessible_world(X211,X212)
| ~ male(X211,X213)
| male(X212,X213) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
cnf(c383,plain,
( ~ accessible_world(skc12,X440)
| male(X440,skc15) ),
inference(resolution,[status(thm)],[c381,clause61]) ).
cnf(c380,plain,
( ~ accessible_world(skc12,X435)
| man(X435,skc15) ),
inference(resolution,[status(thm)],[c379,clause52]) ).
cnf(c358,plain,
( ~ accessible_world(skc12,X434)
| existent(X434,skc10) ),
inference(resolution,[status(thm)],[c355,clause56]) ).
cnf(c356,plain,
( ~ accessible_world(skc12,X433)
| impartial(X433,skc10) ),
inference(resolution,[status(thm)],[c346,clause57]) ).
cnf(c354,plain,
( ~ accessible_world(skc12,X432)
| entity(X432,skc10) ),
inference(resolution,[status(thm)],[c345,clause55]) ).
cnf(c349,plain,
( ~ accessible_world(skc12,X431)
| living(X431,skc10) ),
inference(resolution,[status(thm)],[c343,clause58]) ).
cnf(c348,plain,
( ~ accessible_world(skc12,X426)
| human(X426,skc10) ),
inference(resolution,[status(thm)],[c342,clause59]) ).
cnf(c347,plain,
( ~ accessible_world(skc12,X425)
| animate(X425,skc10) ),
inference(resolution,[status(thm)],[c340,clause60]) ).
cnf(c344,plain,
( ~ accessible_world(skc12,X424)
| organism(X424,skc10) ),
inference(resolution,[status(thm)],[c339,clause54]) ).
cnf(c341,plain,
( ~ accessible_world(skc12,X423)
| human_person(X423,skc10) ),
inference(resolution,[status(thm)],[c334,clause53]) ).
cnf(c335,plain,
( ~ accessible_world(skc12,X422)
| male(X422,skc10) ),
inference(resolution,[status(thm)],[c333,clause61]) ).
cnf(c332,plain,
( ~ accessible_world(skc12,X417)
| man(X417,skc10) ),
inference(resolution,[status(thm)],[c331,clause52]) ).
cnf(c327,plain,
( ~ accessible_world(skc12,X416)
| state(X416,skc9) ),
inference(resolution,[status(thm)],[c326,clause51]) ).
cnf(clause50,axiom,
( ~ accessible_world(X149,X150)
| ~ general(X149,X151)
| general(X150,X151) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c311,plain,
( ~ accessible_world(skc12,X410)
| general(X410,skc14) ),
inference(resolution,[status(thm)],[c307,clause50]) ).
cnf(clause49,axiom,
( ~ accessible_world(X143,X144)
| ~ nonhuman(X143,X145)
| nonhuman(X144,X145) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c309,plain,
( ~ accessible_world(skc12,X409)
| nonhuman(X409,skc14) ),
inference(resolution,[status(thm)],[c304,clause49]) ).
cnf(clause48,axiom,
( ~ accessible_world(X137,X138)
| ~ abstraction(X137,X139)
| abstraction(X138,X139) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(c306,plain,
( ~ accessible_world(skc12,X403)
| abstraction(X403,skc14) ),
inference(resolution,[status(thm)],[c302,clause48]) ).
cnf(c301,plain,
( ~ accessible_world(skc12,X402)
| relation(X402,skc14) ),
inference(resolution,[status(thm)],[c300,clause47]) ).
cnf(c299,plain,
( ~ accessible_world(skc8,X401)
| relname(X401,skc14) ),
inference(resolution,[status(thm)],[clause63,c84]) ).
cnf(c298,plain,
( ~ accessible_world(skc8,X396)
| relname(X396,skc11) ),
inference(resolution,[status(thm)],[clause63,c83]) ).
cnf(c296,plain,
( ~ accessible_world(skc12,X395)
| general(X395,skc11) ),
inference(resolution,[status(thm)],[c291,clause50]) ).
cnf(c294,plain,
( ~ accessible_world(skc12,X394)
| nonhuman(X394,skc11) ),
inference(resolution,[status(thm)],[c288,clause49]) ).
cnf(c290,plain,
( ~ accessible_world(skc12,X383)
| abstraction(X383,skc11) ),
inference(resolution,[status(thm)],[c286,clause48]) ).
cnf(c285,plain,
( ~ accessible_world(skc12,X382)
| relation(X382,skc11) ),
inference(resolution,[status(thm)],[c284,clause47]) ).
cnf(c283,plain,
( ~ accessible_world(skc8,X381)
| male(X381,skc15) ),
inference(resolution,[status(thm)],[clause61,c82]) ).
cnf(c282,plain,
( ~ accessible_world(skc8,X376)
| male(X376,skc10) ),
inference(resolution,[status(thm)],[clause61,c81]) ).
cnf(c281,plain,
( ~ accessible_world(skc12,X375)
| general(X375,skc12) ),
inference(resolution,[status(thm)],[c276,clause50]) ).
cnf(c279,plain,
( ~ accessible_world(skc12,X374)
| nonhuman(X374,skc12) ),
inference(resolution,[status(thm)],[c273,clause49]) ).
cnf(c278,plain,
( ~ accessible_world(skc8,X369)
| animate(X369,skc15) ),
inference(resolution,[status(thm)],[clause60,c80]) ).
cnf(c277,plain,
( ~ accessible_world(skc8,X368)
| animate(X368,skc10) ),
inference(resolution,[status(thm)],[clause60,c79]) ).
cnf(c275,plain,
( ~ accessible_world(skc12,X367)
| abstraction(X367,skc12) ),
inference(resolution,[status(thm)],[c271,clause48]) ).
cnf(c270,plain,
( ~ accessible_world(skc12,X366)
| relation(X366,skc12) ),
inference(resolution,[status(thm)],[c269,clause47]) ).
cnf(c268,plain,
( ~ accessible_world(skc12,X361)
| proposition(X361,skc12) ),
inference(resolution,[status(thm)],[c267,clause46]) ).
cnf(c266,plain,
( ~ accessible_world(skc8,X360)
| human(X360,skc15) ),
inference(resolution,[status(thm)],[clause59,c78]) ).
cnf(c265,plain,
( ~ accessible_world(skc8,X359)
| human(X359,skc10) ),
inference(resolution,[status(thm)],[clause59,c77]) ).
cnf(c264,plain,
( ~ accessible_world(skc12,X354)
| think_believe_consider(X354,skc13) ),
inference(resolution,[status(thm)],[c263,clause45]) ).
cnf(c262,plain,
( ~ accessible_world(skc8,X353)
| living(X353,skc10) ),
inference(resolution,[status(thm)],[clause58,c76]) ).
cnf(c261,plain,
( ~ accessible_world(skc8,X352)
| living(X352,skc15) ),
inference(resolution,[status(thm)],[clause58,c75]) ).
cnf(c260,plain,
( ~ accessible_world(skc12,X347)
| present(X347,skc13) ),
inference(resolution,[status(thm)],[c259,clause44]) ).
cnf(c258,plain,
( ~ accessible_world(skc8,X346)
| impartial(X346,skc10) ),
inference(resolution,[status(thm)],[clause57,c74]) ).
cnf(c257,plain,
( ~ accessible_world(skc8,X345)
| impartial(X345,skc15) ),
inference(resolution,[status(thm)],[clause57,c73]) ).
cnf(c254,plain,
( ~ accessible_world(skc12,X340)
| unisex(X340,skc12) ),
inference(resolution,[status(thm)],[c251,clause43]) ).
cnf(c253,plain,
( ~ accessible_world(skc8,X339)
| existent(X339,skc10) ),
inference(resolution,[status(thm)],[clause56,c72]) ).
cnf(c252,plain,
( ~ accessible_world(skc8,X338)
| existent(X338,skc15) ),
inference(resolution,[status(thm)],[clause56,c71]) ).
cnf(c248,plain,
( ~ accessible_world(skc12,X333)
| unisex(X333,skc14) ),
inference(resolution,[status(thm)],[c245,clause43]) ).
cnf(c247,plain,
( ~ accessible_world(skc8,X332)
| entity(X332,skc10) ),
inference(resolution,[status(thm)],[clause55,c64]) ).
cnf(c1,axiom,
( X329 != X330
| skf4(X329) = skf4(X330) ),
theory(equality) ).
cnf(c246,plain,
( ~ accessible_world(skc8,X328)
| entity(X328,skc15) ),
inference(resolution,[status(thm)],[clause55,c63]) ).
cnf(c243,plain,
( ~ accessible_world(skc12,X327)
| unisex(X327,skc11) ),
inference(resolution,[status(thm)],[c242,clause43]) ).
cnf(c241,plain,
( ~ accessible_world(skc8,X326)
| organism(X326,skc10) ),
inference(resolution,[status(thm)],[clause54,c61]) ).
cnf(c0,axiom,
( X323 != X324
| skf2(X323) = skf2(X324) ),
theory(equality) ).
cnf(c240,plain,
( ~ accessible_world(skc8,X322)
| organism(X322,skc15) ),
inference(resolution,[status(thm)],[clause54,c62]) ).
cnf(transitivity,axiom,
( X317 != X318
| X318 != X316
| X317 = X316 ),
theory(equality) ).
cnf(c238,plain,
( ~ accessible_world(skc8,X315)
| human_person(X315,skc15) ),
inference(resolution,[status(thm)],[clause53,c60]) ).
cnf(c237,plain,
( ~ accessible_world(skc8,X314)
| human_person(X314,skc10) ),
inference(resolution,[status(thm)],[clause53,c59]) ).
cnf(c234,plain,
( ~ accessible_world(skc12,X313)
| specific(X313,skc15) ),
inference(resolution,[status(thm)],[c231,clause41]) ).
cnf(clause34,axiom,
( ~ nonexistent(X69,X70)
| ~ existent(X69,X70) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c403,plain,
~ nonexistent(skc12,skc15),
inference(resolution,[status(thm)],[c401,clause34]) ).
cnf(clause31,axiom,
( ~ male(X63,X64)
| ~ unisex(X63,X64) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c375,plain,
~ male(skc12,skf2(X285)),
inference(resolution,[status(thm)],[c367,clause31]) ).
cnf(clause32,axiom,
( ~ general(X65,X66)
| ~ specific(X65,X66) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c370,plain,
~ general(skc12,skf2(X280)),
inference(resolution,[status(thm)],[c364,clause32]) ).
cnf(c357,plain,
~ nonexistent(skc12,skc10),
inference(resolution,[status(thm)],[c355,clause34]) ).
cnf(c227,plain,
( ~ accessible_world(skc12,X251)
| specific(X251,skc10) ),
inference(resolution,[status(thm)],[c226,clause41]) ).
cnf(c224,plain,
( ~ accessible_world(skc8,X250)
| general(X250,skc11) ),
inference(resolution,[status(thm)],[clause50,c93]) ).
cnf(c223,plain,
( ~ accessible_world(skc8,X245)
| general(X245,skc14) ),
inference(resolution,[status(thm)],[clause50,c97]) ).
cnf(c222,plain,
( ~ accessible_world(skc8,X244)
| general(X244,skc12) ),
inference(resolution,[status(thm)],[clause50,c49]) ).
cnf(c220,plain,
( ~ accessible_world(skc8,X239)
| nonhuman(X239,skc12) ),
inference(resolution,[status(thm)],[clause49,c48]) ).
cnf(c219,plain,
( ~ accessible_world(skc8,X238)
| nonhuman(X238,skc11) ),
inference(resolution,[status(thm)],[clause49,c92]) ).
cnf(c218,plain,
( ~ accessible_world(skc8,X237)
| nonhuman(X237,skc14) ),
inference(resolution,[status(thm)],[clause49,c96]) ).
cnf(c214,plain,
( ~ accessible_world(skc8,X232)
| abstraction(X232,skc14) ),
inference(resolution,[status(thm)],[clause48,c89]) ).
cnf(c213,plain,
( ~ accessible_world(skc8,X231)
| abstraction(X231,skc11) ),
inference(resolution,[status(thm)],[clause48,c88]) ).
cnf(c212,plain,
( ~ accessible_world(skc8,X227)
| abstraction(X227,skc12) ),
inference(resolution,[status(thm)],[clause48,c45]) ).
cnf(clause33,axiom,
( ~ human(X67,X68)
| ~ nonhuman(X67,X68) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c310,plain,
~ human(skc12,skc14),
inference(resolution,[status(thm)],[c304,clause33]) ).
cnf(c208,plain,
( ~ accessible_world(skc8,X219)
| relation(X219,skc12) ),
inference(resolution,[status(thm)],[clause47,c44]) ).
cnf(c295,plain,
~ human(skc12,skc11),
inference(resolution,[status(thm)],[c288,clause33]) ).
cnf(c205,plain,
( ~ accessible_world(skc12,X214)
| singleton(X214,skc14) ),
inference(resolution,[status(thm)],[c202,clause40]) ).
cnf(c280,plain,
~ human(skc12,skc12),
inference(resolution,[status(thm)],[c273,clause33]) ).
cnf(c203,plain,
( ~ accessible_world(skc12,X206)
| thing(X206,skc14) ),
inference(resolution,[status(thm)],[c201,clause39]) ).
cnf(c198,plain,
( ~ accessible_world(skc12,X201)
| singleton(X201,skc10) ),
inference(resolution,[status(thm)],[c196,clause40]) ).
cnf(c197,plain,
( ~ accessible_world(skc12,X200)
| thing(X200,skc10) ),
inference(resolution,[status(thm)],[c195,clause39]) ).
cnf(c194,plain,
( ~ accessible_world(skc12,X199)
| singleton(X199,skc12) ),
inference(resolution,[status(thm)],[c192,clause40]) ).
cnf(c193,plain,
( ~ accessible_world(skc12,X195)
| thing(X195,skc12) ),
inference(resolution,[status(thm)],[c190,clause39]) ).
cnf(c188,plain,
( ~ accessible_world(skc12,X193)
| singleton(X193,skc11) ),
inference(resolution,[status(thm)],[c186,clause40]) ).
cnf(c187,plain,
( ~ accessible_world(skc12,X192)
| thing(X192,skc11) ),
inference(resolution,[status(thm)],[c178,clause39]) ).
cnf(c185,plain,
( ~ accessible_world(skc12,X188)
| unisex(X188,skc13) ),
inference(resolution,[status(thm)],[clause43,c125]) ).
cnf(c184,plain,
( ~ accessible_world(skc8,X187)
| unisex(X187,skc13) ),
inference(resolution,[status(thm)],[clause43,c43]) ).
cnf(c255,plain,
~ male(skc12,skc12),
inference(resolution,[status(thm)],[c251,clause31]) ).
cnf(c182,plain,
( ~ accessible_world(skc8,X182)
| unisex(X182,skc9) ),
inference(resolution,[status(thm)],[clause43,c55]) ).
cnf(c249,plain,
~ male(skc12,skc14),
inference(resolution,[status(thm)],[c245,clause31]) ).
cnf(c244,plain,
~ male(skc12,skc11),
inference(resolution,[status(thm)],[c242,clause31]) ).
cnf(c179,plain,
( ~ accessible_world(skc12,X176)
| unisex(X176,skc9) ),
inference(resolution,[status(thm)],[clause43,c147]) ).
cnf(c177,plain,
( ~ accessible_world(skc12,X172)
| singleton(X172,skc15) ),
inference(resolution,[status(thm)],[c175,clause40]) ).
cnf(c176,plain,
( ~ accessible_world(skc12,X171)
| thing(X171,skc15) ),
inference(resolution,[status(thm)],[c174,clause39]) ).
cnf(c173,plain,
( ~ accessible_world(skc8,X170)
| nonexistent(X170,skc9) ),
inference(resolution,[status(thm)],[clause42,c53]) ).
cnf(c172,plain,
( ~ accessible_world(skc8,X166)
| nonexistent(X166,skc13) ),
inference(resolution,[status(thm)],[clause42,c42]) ).
cnf(c171,plain,
( ~ accessible_world(skc12,X165)
| nonexistent(X165,skc9) ),
inference(resolution,[status(thm)],[clause42,c148]) ).
cnf(c170,plain,
( ~ accessible_world(skc12,X164)
| nonexistent(X164,skc13) ),
inference(resolution,[status(thm)],[clause42,c123]) ).
cnf(c235,plain,
~ general(skc12,skc15),
inference(resolution,[status(thm)],[c231,clause32]) ).
cnf(c166,plain,
( ~ accessible_world(skc12,X159)
| specific(X159,skc13) ),
inference(resolution,[status(thm)],[clause41,c126]) ).
cnf(c165,plain,
( ~ accessible_world(skc12,X158)
| specific(X158,skc9) ),
inference(resolution,[status(thm)],[clause41,c144]) ).
cnf(c164,plain,
( ~ accessible_world(skc8,X157)
| specific(X157,skc13) ),
inference(resolution,[status(thm)],[clause41,c41]) ).
cnf(c228,plain,
~ general(skc12,skc10),
inference(resolution,[status(thm)],[c226,clause32]) ).
cnf(c162,plain,
( ~ accessible_world(skc8,X152)
| specific(X152,skc9) ),
inference(resolution,[status(thm)],[clause41,c56]) ).
cnf(c161,plain,
( ~ accessible_world(skc12,X148)
| singleton(X148,skc9) ),
inference(resolution,[status(thm)],[c150,clause40]) ).
cnf(c159,plain,
( ~ accessible_world(skc12,X147)
| singleton(X147,skc13) ),
inference(resolution,[status(thm)],[clause40,c127]) ).
cnf(c158,plain,
( ~ accessible_world(skc8,X146)
| singleton(X146,skc14) ),
inference(resolution,[status(thm)],[clause40,c100]) ).
cnf(c157,plain,
( ~ accessible_world(skc8,X142)
| singleton(X142,skc15) ),
inference(resolution,[status(thm)],[clause40,c67]) ).
cnf(c156,plain,
( ~ accessible_world(skc8,X141)
| singleton(X141,skc13) ),
inference(resolution,[status(thm)],[clause40,c40]) ).
cnf(c155,plain,
( ~ accessible_world(skc8,X140)
| singleton(X140,skc11) ),
inference(resolution,[status(thm)],[clause40,c99]) ).
cnf(c154,plain,
( ~ accessible_world(skc8,X136)
| singleton(X136,skc10) ),
inference(resolution,[status(thm)],[clause40,c68]) ).
cnf(c153,plain,
( ~ accessible_world(skc8,X135)
| singleton(X135,skc12) ),
inference(resolution,[status(thm)],[clause40,c47]) ).
cnf(c152,plain,
( ~ accessible_world(skc8,X131)
| singleton(X131,skc9) ),
inference(resolution,[status(thm)],[clause40,c58]) ).
cnf(c151,plain,
( ~ accessible_world(skc12,X130)
| thing(X130,skc9) ),
inference(resolution,[status(thm)],[c146,clause39]) ).
cnf(c145,plain,
( ~ accessible_world(skc12,X129)
| eventuality(X129,skc9) ),
inference(resolution,[status(thm)],[c142,clause38]) ).
cnf(c143,plain,
( ~ accessible_world(skc12,X128)
| event(X128,skc9) ),
inference(resolution,[status(thm)],[c141,clause37]) ).
cnf(c139,plain,
( ~ accessible_world(skc8,X123)
| thing(X123,skc13) ),
inference(resolution,[status(thm)],[clause39,c39]) ).
cnf(c138,plain,
( ~ accessible_world(skc12,X122)
| thing(X122,skc13) ),
inference(resolution,[status(thm)],[clause39,c124]) ).
cnf(c135,plain,
( ~ accessible_world(skc8,X113)
| thing(X113,skc9) ),
inference(resolution,[status(thm)],[clause39,c54]) ).
cnf(c130,plain,
( ~ accessible_world(skc8,X104)
| eventuality(X104,skc13) ),
inference(resolution,[status(thm)],[clause38,c38]) ).
cnf(c129,plain,
( ~ accessible_world(skc12,X103)
| eventuality(X103,skc13) ),
inference(resolution,[status(thm)],[clause38,c121]) ).
cnf(c128,plain,
( ~ accessible_world(skc8,X102)
| eventuality(X102,skc9) ),
inference(resolution,[status(thm)],[clause38,c51]) ).
cnf(c122,plain,
( ~ accessible_world(skc12,X101)
| event(X101,skc13) ),
inference(resolution,[status(thm)],[c120,clause37]) ).
cnf(c160,plain,
~ male(skc12,skc9),
inference(resolution,[status(thm)],[c147,clause31]) ).
cnf(c149,plain,
~ general(skc12,skc9),
inference(resolution,[status(thm)],[c144,clause32]) ).
cnf(c132,plain,
~ general(skc12,skc13),
inference(resolution,[status(thm)],[c126,clause32]) ).
cnf(c131,plain,
~ male(skc12,skc13),
inference(resolution,[status(thm)],[c125,clause31]) ).
cnf(c37,axiom,
( X81 != X82
| ~ actual_world(X81)
| actual_world(X82) ),
theory(equality) ).
cnf(symmetry,axiom,
( X75 != X76
| X76 = X75 ),
theory(equality) ).
cnf(clause35,axiom,
( ~ be(X71,X73,X74,X72)
| X74 = X72 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c114,plain,
~ nonexistent(skc8,skc10),
inference(resolution,[status(thm)],[clause34,c72]) ).
cnf(c113,plain,
~ nonexistent(skc8,skc15),
inference(resolution,[status(thm)],[clause34,c71]) ).
cnf(c112,plain,
~ human(skc8,skc12),
inference(resolution,[status(thm)],[clause33,c48]) ).
cnf(c111,plain,
~ human(skc8,skc11),
inference(resolution,[status(thm)],[clause33,c92]) ).
cnf(c110,plain,
~ human(skc8,skc14),
inference(resolution,[status(thm)],[clause33,c96]) ).
cnf(c109,plain,
~ general(skc8,skc10),
inference(resolution,[status(thm)],[clause32,c70]) ).
cnf(c108,plain,
~ general(skc8,skc15),
inference(resolution,[status(thm)],[clause32,c69]) ).
cnf(c107,plain,
~ general(skc8,skc9),
inference(resolution,[status(thm)],[clause32,c56]) ).
cnf(c106,plain,
~ general(skc8,skc13),
inference(resolution,[status(thm)],[clause32,c41]) ).
cnf(c105,plain,
~ male(skc8,skc14),
inference(resolution,[status(thm)],[c95,clause31]) ).
cnf(c104,plain,
~ male(skc8,skc11),
inference(resolution,[status(thm)],[clause31,c91]) ).
cnf(c103,plain,
~ male(skc8,skc13),
inference(resolution,[status(thm)],[clause31,c43]) ).
cnf(c102,plain,
~ male(skc8,skc12),
inference(resolution,[status(thm)],[clause31,c50]) ).
cnf(c101,plain,
~ male(skc8,skc9),
inference(resolution,[status(thm)],[clause31,c55]) ).
cnf(clause30,axiom,
( ~ jules_forename(X61,X62)
| forename(X61,X62) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,axiom,
( ~ vincent_forename(X59,X60)
| forename(X59,X60) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(clause72,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP255-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n010.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 13:26:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 4.68/4.85 % Version: 1.5
% 4.68/4.85 % SZS status Satisfiable
% 4.68/4.85 % SZS output start Saturation
% See solution above
% 4.72/4.87
% 4.72/4.87 % Initial clauses : 136
% 4.72/4.87 % Processed clauses : 946
% 4.72/4.87 % Factors computed : 90
% 4.72/4.87 % Resolvents computed: 1026
% 4.72/4.87 % Tautologies deleted: 3
% 4.72/4.87 % Forward subsumed : 303
% 4.72/4.87 % Backward subsumed : 49
% 4.72/4.87 % -------- CPU Time ---------
% 4.72/4.87 % User time : 4.504 s
% 4.72/4.87 % System time : 0.020 s
% 4.72/4.87 % Total time : 4.524 s
%------------------------------------------------------------------------------