%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP256-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:54 EDT 2024
% Result : Satisfiable 2.66s 2.85s
% Output : Saturation 2.66s
% 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(X163,X161)
| ~ man(X163,X162)
| man(X161,X162) ),
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(c388,plain,
agent(skc12,skf2(skc10),skc10),
inference(resolution,[status(thm)],[clause93,c331]) ).
cnf(clause88,negated_conjecture,
of(skc8,skc11,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
cnf(clause68,axiom,
( ~ accessible_world(X249,X247)
| ~ of(X249,X248,X246)
| of(X247,X248,X246) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
cnf(c324,plain,
( ~ accessible_world(skc8,X502)
| of(X502,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,
( ~ accessible_world(X300,X288)
| ~ proposition(X300,X288)
| ~ proposition(X300,X289)
| ~ accessible_world(X300,X289)
| ~ think_believe_consider(X300,X294)
| ~ present(X300,X294)
| ~ event(X300,X294)
| ~ theme(X300,X294,X289)
| ~ vincent_forename(X300,X290)
| ~ forename(X300,X290)
| ~ forename(X300,X296)
| ~ jules_forename(X300,X296)
| ~ of(X300,X296,X299)
| ~ smoke(X288,X292)
| ~ present(X288,X292)
| ~ agent(X288,X292,X299)
| ~ event(X288,X292)
| ~ agent(X300,X294,X299)
| ~ man(X300,X299)
| ~ of(X300,X290,X299)
| ~ theme(X300,X293,X288)
| ~ event(X300,X293)
| ~ present(X300,X293)
| ~ think_believe_consider(X300,X293)
| ~ state(X300,X295)
| ~ of(X300,X297,X291)
| ~ vincent_forename(X300,X297)
| ~ forename(X300,X297)
| ~ man(X300,X291)
| ~ be(X300,X295,X291,X291)
| ~ agent(X300,X293,X291)
| ~ forename(X300,X298)
| ~ jules_forename(X300,X298)
| ~ of(X300,X298,X291)
| ~ actual_world(X300)
| man(X289,skf4(X289)) ),
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,X252)
| ~ be(X256,X253,X255,X254)
| be(X252,X253,X255,X254) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
cnf(c330,plain,
( ~ accessible_world(skc8,X511)
| be(X511,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[clause69,clause89]) ).
cnf(c587,plain,
be(skc12,skc9,skc10,skc10),
inference(resolution,[status(thm)],[c330,clause83]) ).
cnf(c591,plain,
( ~ accessible_world(skc12,X1052)
| ~ proposition(skc12,X1052)
| ~ proposition(skc12,X1060)
| ~ accessible_world(skc12,X1060)
| ~ think_believe_consider(skc12,X1055)
| ~ present(skc12,X1055)
| ~ event(skc12,X1055)
| ~ theme(skc12,X1055,X1060)
| ~ vincent_forename(skc12,X1057)
| ~ forename(skc12,X1057)
| ~ forename(skc12,X1054)
| ~ jules_forename(skc12,X1054)
| ~ of(skc12,X1054,X1056)
| ~ smoke(X1052,X1059)
| ~ present(X1052,X1059)
| ~ agent(X1052,X1059,X1056)
| ~ event(X1052,X1059)
| ~ agent(skc12,X1055,X1056)
| ~ man(skc12,X1056)
| ~ of(skc12,X1057,X1056)
| ~ theme(skc12,X1061,X1052)
| ~ event(skc12,X1061)
| ~ present(skc12,X1061)
| ~ think_believe_consider(skc12,X1061)
| ~ state(skc12,skc9)
| ~ of(skc12,X1053,skc10)
| ~ vincent_forename(skc12,X1053)
| ~ forename(skc12,X1053)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1061,skc10)
| ~ forename(skc12,X1058)
| ~ jules_forename(skc12,X1058)
| ~ of(skc12,X1058,skc10)
| ~ actual_world(skc12)
| man(X1060,skf4(X1060)) ),
inference(resolution,[status(thm)],[c587,clause94]) ).
cnf(c928,plain,
( ~ accessible_world(skc12,X1532)
| ~ proposition(skc12,X1532)
| ~ proposition(skc12,X1529)
| ~ accessible_world(skc12,X1529)
| ~ think_believe_consider(skc12,X1535)
| ~ present(skc12,X1535)
| ~ event(skc12,X1535)
| ~ theme(skc12,X1535,X1529)
| ~ vincent_forename(skc12,X1530)
| ~ forename(skc12,X1530)
| ~ forename(skc12,X1533)
| ~ jules_forename(skc12,X1533)
| ~ of(skc12,X1533,X1534)
| ~ smoke(X1532,X1536)
| ~ present(X1532,X1536)
| ~ agent(X1532,X1536,X1534)
| ~ event(X1532,X1536)
| ~ agent(skc12,X1535,X1534)
| ~ man(skc12,X1534)
| ~ of(skc12,X1530,X1534)
| ~ theme(skc12,X1531,X1532)
| ~ event(skc12,X1531)
| ~ present(skc12,X1531)
| ~ think_believe_consider(skc12,X1531)
| ~ state(skc12,skc9)
| ~ of(skc12,X1537,skc10)
| ~ vincent_forename(skc12,X1537)
| ~ forename(skc12,X1537)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1531,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1529,skf4(X1529)) ),
inference(resolution,[status(thm)],[c591,c580]) ).
cnf(c1084,plain,
( ~ accessible_world(skc12,X1677)
| ~ proposition(skc12,X1677)
| ~ proposition(skc12,X1674)
| ~ accessible_world(skc12,X1674)
| ~ think_believe_consider(skc12,X1675)
| ~ present(skc12,X1675)
| ~ event(skc12,X1675)
| ~ theme(skc12,X1675,X1674)
| ~ vincent_forename(skc12,X1679)
| ~ forename(skc12,X1679)
| ~ forename(skc12,X1678)
| ~ jules_forename(skc12,X1678)
| ~ of(skc12,X1678,X1676)
| ~ smoke(X1677,X1680)
| ~ present(X1677,X1680)
| ~ agent(X1677,X1680,X1676)
| ~ event(X1677,X1680)
| ~ agent(skc12,X1675,X1676)
| ~ man(skc12,X1676)
| ~ of(skc12,X1679,X1676)
| ~ theme(skc12,skf2(skc10),X1677)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1681,skc10)
| ~ vincent_forename(skc12,X1681)
| ~ forename(skc12,X1681)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1674,skf4(X1674)) ),
inference(resolution,[status(thm)],[c928,c388]) ).
cnf(c1102,plain,
( ~ accessible_world(skc12,X1686)
| ~ proposition(skc12,X1686)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1686)
| ~ vincent_forename(skc12,X1685)
| ~ forename(skc12,X1685)
| ~ forename(skc12,X1682)
| ~ jules_forename(skc12,X1682)
| ~ of(skc12,X1682,X1684)
| ~ smoke(X1686,X1683)
| ~ present(X1686,X1683)
| ~ agent(X1686,X1683,X1684)
| ~ event(X1686,X1683)
| ~ agent(skc12,skf2(skc10),X1684)
| ~ man(skc12,X1684)
| ~ of(skc12,X1685,X1684)
| ~ state(skc12,skc9)
| ~ of(skc12,X1687,skc10)
| ~ vincent_forename(skc12,X1687)
| ~ forename(skc12,X1687)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1686,skf4(X1686)) ),
inference(factor,[status(thm)],[c1084]) ).
cnf(c1103,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1694)
| ~ forename(skc12,X1694)
| ~ forename(skc12,X1693)
| ~ jules_forename(skc12,X1693)
| ~ of(skc12,X1693,X1695)
| ~ smoke(skc12,skf2(skc10))
| ~ agent(skc12,skf2(skc10),X1695)
| ~ man(skc12,X1695)
| ~ of(skc12,X1694,X1695)
| ~ state(skc12,skc9)
| ~ of(skc12,X1696,skc10)
| ~ vincent_forename(skc12,X1696)
| ~ forename(skc12,X1696)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1102]) ).
cnf(c1105,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1697)
| ~ forename(skc12,X1697)
| ~ forename(skc12,X1699)
| ~ jules_forename(skc12,X1699)
| ~ of(skc12,X1699,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ man(skc12,skc10)
| ~ of(skc12,X1697,skc10)
| ~ state(skc12,skc9)
| ~ of(skc12,X1698,skc10)
| ~ vincent_forename(skc12,X1698)
| ~ forename(skc12,X1698)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1103,c388]) ).
cnf(c1104,plain,
( ~ accessible_world(skc12,X1692)
| ~ proposition(skc12,X1692)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1692)
| ~ vincent_forename(skc12,X1689)
| ~ forename(skc12,X1689)
| ~ forename(skc12,X1688)
| ~ jules_forename(skc12,X1688)
| ~ of(skc12,X1688,skc10)
| ~ smoke(X1692,X1690)
| ~ present(X1692,X1690)
| ~ agent(X1692,X1690,skc10)
| ~ event(X1692,X1690)
| ~ man(skc12,skc10)
| ~ of(skc12,X1689,skc10)
| ~ state(skc12,skc9)
| ~ of(skc12,X1691,skc10)
| ~ vincent_forename(skc12,X1691)
| ~ forename(skc12,X1691)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1692,skf4(X1692)) ),
inference(resolution,[status(thm)],[c1102,c388]) ).
cnf(c927,plain,
( ~ accessible_world(skc12,X1499)
| ~ proposition(skc12,X1499)
| ~ proposition(skc12,X1496)
| ~ accessible_world(skc12,X1496)
| ~ think_believe_consider(skc12,X1502)
| ~ present(skc12,X1502)
| ~ event(skc12,X1502)
| ~ theme(skc12,X1502,X1496)
| ~ vincent_forename(skc12,X1497)
| ~ forename(skc12,X1497)
| ~ forename(skc12,X1500)
| ~ jules_forename(skc12,X1500)
| ~ of(skc12,X1500,X1501)
| ~ smoke(X1499,X1503)
| ~ present(X1499,X1503)
| ~ agent(X1499,X1503,X1501)
| ~ event(X1499,X1503)
| ~ agent(skc12,X1502,X1501)
| ~ man(skc12,X1501)
| ~ of(skc12,X1497,X1501)
| ~ theme(skc12,X1498,X1499)
| ~ event(skc12,X1498)
| ~ present(skc12,X1498)
| ~ think_believe_consider(skc12,X1498)
| ~ state(skc12,skc9)
| ~ of(skc12,X1504,skc10)
| ~ vincent_forename(skc12,X1504)
| ~ forename(skc12,X1504)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1498,skc10)
| ~ jules_forename(skc12,X1504)
| ~ actual_world(skc12)
| man(X1496,skf4(X1496)) ),
inference(factor,[status(thm)],[c591]) ).
cnf(c1077,plain,
( ~ accessible_world(skc12,X1654)
| ~ proposition(skc12,X1654)
| ~ proposition(skc12,X1653)
| ~ accessible_world(skc12,X1653)
| ~ think_believe_consider(skc12,X1655)
| ~ present(skc12,X1655)
| ~ event(skc12,X1655)
| ~ theme(skc12,X1655,X1653)
| ~ vincent_forename(skc12,X1652)
| ~ forename(skc12,X1652)
| ~ forename(skc12,X1656)
| ~ jules_forename(skc12,X1656)
| ~ of(skc12,X1656,X1658)
| ~ smoke(X1654,X1651)
| ~ present(X1654,X1651)
| ~ agent(X1654,X1651,X1658)
| ~ event(X1654,X1651)
| ~ agent(skc12,X1655,X1658)
| ~ man(skc12,X1658)
| ~ of(skc12,X1652,X1658)
| ~ theme(skc12,skf2(skc10),X1654)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1657,skc10)
| ~ vincent_forename(skc12,X1657)
| ~ forename(skc12,X1657)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1657)
| ~ actual_world(skc12)
| man(X1653,skf4(X1653)) ),
inference(resolution,[status(thm)],[c927,c388]) ).
cnf(c1099,plain,
( ~ accessible_world(skc12,X1659)
| ~ proposition(skc12,X1659)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1659)
| ~ vincent_forename(skc12,X1661)
| ~ forename(skc12,X1661)
| ~ forename(skc12,X1662)
| ~ jules_forename(skc12,X1662)
| ~ of(skc12,X1662,X1660)
| ~ smoke(X1659,X1664)
| ~ present(X1659,X1664)
| ~ agent(X1659,X1664,X1660)
| ~ event(X1659,X1664)
| ~ agent(skc12,skf2(skc10),X1660)
| ~ man(skc12,X1660)
| ~ of(skc12,X1661,X1660)
| ~ state(skc12,skc9)
| ~ of(skc12,X1663,skc10)
| ~ vincent_forename(skc12,X1663)
| ~ forename(skc12,X1663)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1663)
| ~ actual_world(skc12)
| man(X1659,skf4(X1659)) ),
inference(factor,[status(thm)],[c1077]) ).
cnf(clause95,negated_conjecture,
( ~ accessible_world(X314,X301)
| ~ proposition(X314,X301)
| ~ proposition(X314,X302)
| ~ accessible_world(X314,X302)
| ~ smoke(X302,X308)
| ~ present(X302,X308)
| ~ agent(X302,X308,skf4(X302))
| ~ event(X302,X308)
| ~ think_believe_consider(X314,X303)
| ~ present(X314,X303)
| ~ event(X314,X303)
| ~ theme(X314,X303,X302)
| ~ vincent_forename(X314,X310)
| ~ forename(X314,X310)
| ~ forename(X314,X313)
| ~ jules_forename(X314,X313)
| ~ of(X314,X313,X305)
| ~ smoke(X301,X306)
| ~ present(X301,X306)
| ~ agent(X301,X306,X305)
| ~ event(X301,X306)
| ~ agent(X314,X303,X305)
| ~ man(X314,X305)
| ~ of(X314,X310,X305)
| ~ theme(X314,X309,X301)
| ~ event(X314,X309)
| ~ present(X314,X309)
| ~ think_believe_consider(X314,X309)
| ~ state(X314,X311)
| ~ of(X314,X304,X312)
| ~ vincent_forename(X314,X304)
| ~ forename(X314,X304)
| ~ man(X314,X312)
| ~ be(X314,X311,X312,X312)
| ~ agent(X314,X309,X312)
| ~ forename(X314,X307)
| ~ jules_forename(X314,X307)
| ~ of(X314,X307,X312)
| ~ actual_world(X314) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
cnf(c589,plain,
( ~ accessible_world(skc12,X1044)
| ~ proposition(skc12,X1044)
| ~ proposition(skc12,X1038)
| ~ accessible_world(skc12,X1038)
| ~ smoke(X1038,X1037)
| ~ present(X1038,X1037)
| ~ agent(X1038,X1037,skf4(X1038))
| ~ event(X1038,X1037)
| ~ think_believe_consider(skc12,X1035)
| ~ present(skc12,X1035)
| ~ event(skc12,X1035)
| ~ theme(skc12,X1035,X1038)
| ~ vincent_forename(skc12,X1043)
| ~ forename(skc12,X1043)
| ~ forename(skc12,X1039)
| ~ jules_forename(skc12,X1039)
| ~ of(skc12,X1039,X1036)
| ~ smoke(X1044,X1042)
| ~ present(X1044,X1042)
| ~ agent(X1044,X1042,X1036)
| ~ event(X1044,X1042)
| ~ agent(skc12,X1035,X1036)
| ~ man(skc12,X1036)
| ~ of(skc12,X1043,X1036)
| ~ theme(skc12,X1045,X1044)
| ~ event(skc12,X1045)
| ~ present(skc12,X1045)
| ~ think_believe_consider(skc12,X1045)
| ~ state(skc12,skc9)
| ~ of(skc12,X1041,skc10)
| ~ vincent_forename(skc12,X1041)
| ~ forename(skc12,X1041)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1045,skc10)
| ~ forename(skc12,X1040)
| ~ jules_forename(skc12,X1040)
| ~ of(skc12,X1040,skc10)
| ~ actual_world(skc12) ),
inference(resolution,[status(thm)],[c587,clause95]) ).
cnf(c920,plain,
( ~ accessible_world(skc12,X1452)
| ~ proposition(skc12,X1452)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ smoke(skc12,X1457)
| ~ present(skc12,X1457)
| ~ agent(skc12,X1457,skf4(skc12))
| ~ event(skc12,X1457)
| ~ think_believe_consider(skc12,X1457)
| ~ theme(skc12,X1457,skc12)
| ~ vincent_forename(skc12,X1454)
| ~ forename(skc12,X1454)
| ~ forename(skc12,X1458)
| ~ jules_forename(skc12,X1458)
| ~ of(skc12,X1458,skf4(skc12))
| ~ smoke(X1452,X1451)
| ~ present(X1452,X1451)
| ~ agent(X1452,X1451,skf4(skc12))
| ~ event(X1452,X1451)
| ~ man(skc12,skf4(skc12))
| ~ of(skc12,X1454,skf4(skc12))
| ~ theme(skc12,X1456,X1452)
| ~ event(skc12,X1456)
| ~ present(skc12,X1456)
| ~ think_believe_consider(skc12,X1456)
| ~ state(skc12,skc9)
| ~ of(skc12,X1455,skc10)
| ~ vincent_forename(skc12,X1455)
| ~ forename(skc12,X1455)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1456,skc10)
| ~ forename(skc12,X1453)
| ~ jules_forename(skc12,X1453)
| ~ of(skc12,X1453,skc10)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c589]) ).
cnf(c1068,plain,
( ~ accessible_world(skc12,X1640)
| ~ proposition(skc12,X1640)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ smoke(skc12,X1642)
| ~ present(skc12,X1642)
| ~ agent(skc12,X1642,skf4(skc12))
| ~ event(skc12,X1642)
| ~ think_believe_consider(skc12,X1642)
| ~ theme(skc12,X1642,skc12)
| ~ vincent_forename(skc12,X1644)
| ~ forename(skc12,X1644)
| ~ jules_forename(skc12,X1644)
| ~ of(skc12,X1644,skf4(skc12))
| ~ smoke(X1640,X1643)
| ~ present(X1640,X1643)
| ~ agent(X1640,X1643,skf4(skc12))
| ~ event(X1640,X1643)
| ~ man(skc12,skf4(skc12))
| ~ theme(skc12,X1645,X1640)
| ~ event(skc12,X1645)
| ~ present(skc12,X1645)
| ~ think_believe_consider(skc12,X1645)
| ~ state(skc12,skc9)
| ~ of(skc12,X1639,skc10)
| ~ vincent_forename(skc12,X1639)
| ~ forename(skc12,X1639)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1645,skc10)
| ~ forename(skc12,X1641)
| ~ jules_forename(skc12,X1641)
| ~ of(skc12,X1641,skc10)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c920]) ).
cnf(c919,plain,
( ~ accessible_world(skc12,X1425)
| ~ proposition(skc12,X1425)
| ~ smoke(X1425,X1419)
| ~ present(X1425,X1419)
| ~ agent(X1425,X1419,skf4(X1425))
| ~ event(X1425,X1419)
| ~ think_believe_consider(skc12,X1424)
| ~ present(skc12,X1424)
| ~ event(skc12,X1424)
| ~ theme(skc12,X1424,X1425)
| ~ vincent_forename(skc12,X1421)
| ~ forename(skc12,X1421)
| ~ forename(skc12,X1426)
| ~ jules_forename(skc12,X1426)
| ~ of(skc12,X1426,skf4(X1425))
| ~ agent(skc12,X1424,skf4(X1425))
| ~ man(skc12,skf4(X1425))
| ~ of(skc12,X1421,skf4(X1425))
| ~ theme(skc12,X1423,X1425)
| ~ event(skc12,X1423)
| ~ present(skc12,X1423)
| ~ think_believe_consider(skc12,X1423)
| ~ state(skc12,skc9)
| ~ of(skc12,X1422,skc10)
| ~ vincent_forename(skc12,X1422)
| ~ forename(skc12,X1422)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1423,skc10)
| ~ forename(skc12,X1420)
| ~ jules_forename(skc12,X1420)
| ~ of(skc12,X1420,skc10)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c589]) ).
cnf(c1057,plain,
( ~ accessible_world(skc12,X1625)
| ~ proposition(skc12,X1625)
| ~ smoke(X1625,X1627)
| ~ present(X1625,X1627)
| ~ agent(X1625,X1627,skf4(X1625))
| ~ event(X1625,X1627)
| ~ think_believe_consider(skc12,X1621)
| ~ present(skc12,X1621)
| ~ event(skc12,X1621)
| ~ theme(skc12,X1621,X1625)
| ~ vincent_forename(skc12,X1626)
| ~ forename(skc12,X1626)
| ~ jules_forename(skc12,X1626)
| ~ of(skc12,X1626,skf4(X1625))
| ~ agent(skc12,X1621,skf4(X1625))
| ~ man(skc12,skf4(X1625))
| ~ theme(skc12,X1624,X1625)
| ~ event(skc12,X1624)
| ~ present(skc12,X1624)
| ~ think_believe_consider(skc12,X1624)
| ~ state(skc12,skc9)
| ~ of(skc12,X1622,skc10)
| ~ vincent_forename(skc12,X1622)
| ~ forename(skc12,X1622)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1624,skc10)
| ~ forename(skc12,X1623)
| ~ jules_forename(skc12,X1623)
| ~ of(skc12,X1623,skc10)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c919]) ).
cnf(c1097,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ smoke(skc12,X1628)
| ~ present(skc12,X1628)
| ~ agent(skc12,X1628,skf4(skc12))
| ~ event(skc12,X1628)
| ~ think_believe_consider(skc12,X1628)
| ~ theme(skc12,X1628,skc12)
| ~ vincent_forename(skc12,X1631)
| ~ forename(skc12,X1631)
| ~ jules_forename(skc12,X1631)
| ~ of(skc12,X1631,skf4(skc12))
| ~ man(skc12,skf4(skc12))
| ~ theme(skc12,X1632,skc12)
| ~ event(skc12,X1632)
| ~ present(skc12,X1632)
| ~ think_believe_consider(skc12,X1632)
| ~ state(skc12,skc9)
| ~ of(skc12,X1629,skc10)
| ~ vincent_forename(skc12,X1629)
| ~ forename(skc12,X1629)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1632,skc10)
| ~ forename(skc12,X1630)
| ~ jules_forename(skc12,X1630)
| ~ of(skc12,X1630,skc10)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c1057]) ).
cnf(c925,plain,
( ~ accessible_world(skc12,X1414)
| ~ proposition(skc12,X1414)
| ~ proposition(skc12,X1411)
| ~ accessible_world(skc12,X1411)
| ~ think_believe_consider(skc12,X1415)
| ~ present(skc12,X1415)
| ~ event(skc12,X1415)
| ~ theme(skc12,X1415,X1411)
| ~ vincent_forename(skc12,X1412)
| ~ forename(skc12,X1412)
| ~ forename(skc12,X1417)
| ~ jules_forename(skc12,X1417)
| ~ of(skc12,X1417,skc10)
| ~ smoke(X1414,X1416)
| ~ present(X1414,X1416)
| ~ agent(X1414,X1416,skc10)
| ~ event(X1414,X1416)
| ~ agent(skc12,X1415,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1412,skc10)
| ~ theme(skc12,X1413,X1414)
| ~ event(skc12,X1413)
| ~ present(skc12,X1413)
| ~ think_believe_consider(skc12,X1413)
| ~ state(skc12,skc9)
| ~ of(skc12,X1418,skc10)
| ~ vincent_forename(skc12,X1418)
| ~ forename(skc12,X1418)
| ~ agent(skc12,X1413,skc10)
| ~ actual_world(skc12)
| man(X1411,skf4(X1411)) ),
inference(factor,[status(thm)],[c591]) ).
cnf(c1056,plain,
( ~ accessible_world(skc12,X1604)
| ~ proposition(skc12,X1604)
| ~ proposition(skc12,X1607)
| ~ accessible_world(skc12,X1607)
| ~ think_believe_consider(skc12,X1609)
| ~ present(skc12,X1609)
| ~ event(skc12,X1609)
| ~ theme(skc12,X1609,X1607)
| ~ vincent_forename(skc12,X1603)
| ~ forename(skc12,X1603)
| ~ forename(skc12,X1605)
| ~ jules_forename(skc12,X1605)
| ~ of(skc12,X1605,skc10)
| ~ smoke(X1604,X1606)
| ~ present(X1604,X1606)
| ~ agent(X1604,X1606,skc10)
| ~ event(X1604,X1606)
| ~ agent(skc12,X1609,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1603,skc10)
| ~ theme(skc12,skf2(skc10),X1604)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ of(skc12,X1608,skc10)
| ~ vincent_forename(skc12,X1608)
| ~ forename(skc12,X1608)
| ~ actual_world(skc12)
| man(X1607,skf4(X1607)) ),
inference(resolution,[status(thm)],[c925,c388]) ).
cnf(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
cnf(clause67,axiom,
( ~ accessible_world(X243,X241)
| ~ theme(X243,X242,X240)
| theme(X241,X242,X240) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
cnf(c320,plain,
( ~ accessible_world(skc8,X496)
| theme(X496,skc13,skc12) ),
inference(resolution,[status(thm)],[clause67,clause87]) ).
cnf(c571,plain,
theme(skc12,skc13,skc12),
inference(resolution,[status(thm)],[c320,clause83]) ).
cnf(c1054,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1525)
| ~ accessible_world(skc12,X1525)
| ~ think_believe_consider(skc12,X1528)
| ~ present(skc12,X1528)
| ~ event(skc12,X1528)
| ~ theme(skc12,X1528,X1525)
| ~ vincent_forename(skc12,X1523)
| ~ forename(skc12,X1523)
| ~ forename(skc12,X1524)
| ~ jules_forename(skc12,X1524)
| ~ of(skc12,X1524,skc10)
| ~ smoke(skc12,X1526)
| ~ present(skc12,X1526)
| ~ agent(skc12,X1526,skc10)
| ~ event(skc12,X1526)
| ~ agent(skc12,X1528,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1523,skc10)
| ~ theme(skc12,X1526,skc12)
| ~ think_believe_consider(skc12,X1526)
| ~ state(skc12,skc9)
| ~ of(skc12,X1527,skc10)
| ~ vincent_forename(skc12,X1527)
| ~ forename(skc12,X1527)
| ~ actual_world(skc12)
| man(X1525,skf4(X1525)) ),
inference(factor,[status(thm)],[c925]) ).
cnf(c1080,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1542)
| ~ accessible_world(skc12,X1542)
| ~ think_believe_consider(skc12,X1540)
| ~ present(skc12,X1540)
| ~ event(skc12,X1540)
| ~ theme(skc12,X1540,X1542)
| ~ vincent_forename(skc12,X1539)
| ~ forename(skc12,X1539)
| ~ forename(skc12,X1538)
| ~ jules_forename(skc12,X1538)
| ~ of(skc12,X1538,skc10)
| ~ smoke(skc12,X1541)
| ~ present(skc12,X1541)
| ~ agent(skc12,X1541,skc10)
| ~ event(skc12,X1541)
| ~ agent(skc12,X1540,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1539,skc10)
| ~ theme(skc12,X1541,skc12)
| ~ think_believe_consider(skc12,X1541)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1542,skf4(X1542)) ),
inference(factor,[status(thm)],[c1054]) ).
cnf(c1086,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1553)
| ~ accessible_world(skc12,X1553)
| ~ think_believe_consider(skc12,X1550)
| ~ present(skc12,X1550)
| ~ event(skc12,X1550)
| ~ theme(skc12,X1550,X1553)
| ~ vincent_forename(skc12,X1551)
| ~ forename(skc12,X1551)
| ~ forename(skc12,X1552)
| ~ jules_forename(skc12,X1552)
| ~ of(skc12,X1552,skc10)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ agent(skc12,X1550,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1551,skc10)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1553,skf4(X1553)) ),
inference(resolution,[status(thm)],[c1080,c571]) ).
cnf(c1090,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1569)
| ~ accessible_world(skc12,X1569)
| ~ think_believe_consider(skc12,X1568)
| ~ present(skc12,X1568)
| ~ event(skc12,X1568)
| ~ theme(skc12,X1568,X1569)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1567)
| ~ jules_forename(skc12,X1567)
| ~ of(skc12,X1567,skc10)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ agent(skc12,X1568,skc10)
| ~ man(skc12,skc10)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1569,skf4(X1569)) ),
inference(resolution,[status(thm)],[c1086,c580]) ).
cnf(c1094,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1580)
| ~ accessible_world(skc12,X1580)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1580)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1579)
| ~ jules_forename(skc12,X1579)
| ~ of(skc12,X1579,skc10)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ man(skc12,skc10)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1580,skf4(X1580)) ),
inference(resolution,[status(thm)],[c1090,c388]) ).
cnf(c405,plain,
( ~ accessible_world(skc8,X698)
| ~ proposition(skc8,X698)
| ~ proposition(skc8,X692)
| ~ accessible_world(skc8,X692)
| ~ smoke(X692,X691)
| ~ present(X692,X691)
| ~ agent(X692,X691,skf4(X692))
| ~ event(X692,X691)
| ~ think_believe_consider(skc8,X689)
| ~ present(skc8,X689)
| ~ event(skc8,X689)
| ~ theme(skc8,X689,X692)
| ~ vincent_forename(skc8,X697)
| ~ forename(skc8,X697)
| ~ forename(skc8,X693)
| ~ jules_forename(skc8,X693)
| ~ of(skc8,X693,X690)
| ~ smoke(X698,X696)
| ~ present(X698,X696)
| ~ agent(X698,X696,X690)
| ~ event(X698,X696)
| ~ agent(skc8,X689,X690)
| ~ man(skc8,X690)
| ~ of(skc8,X697,X690)
| ~ theme(skc8,X699,X698)
| ~ event(skc8,X699)
| ~ present(skc8,X699)
| ~ think_believe_consider(skc8,X699)
| ~ state(skc8,skc9)
| ~ of(skc8,X695,skc10)
| ~ vincent_forename(skc8,X695)
| ~ forename(skc8,X695)
| ~ man(skc8,skc10)
| ~ agent(skc8,X699,skc10)
| ~ forename(skc8,X694)
| ~ jules_forename(skc8,X694)
| ~ of(skc8,X694,skc10)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[clause95,clause89]) ).
cnf(c706,plain,
( ~ accessible_world(skc8,X1385)
| ~ proposition(skc8,X1385)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ smoke(skc8,X1378)
| ~ present(skc8,X1378)
| ~ agent(skc8,X1378,skf4(skc8))
| ~ event(skc8,X1378)
| ~ think_believe_consider(skc8,X1378)
| ~ theme(skc8,X1378,skc8)
| ~ vincent_forename(skc8,X1384)
| ~ forename(skc8,X1384)
| ~ forename(skc8,X1382)
| ~ jules_forename(skc8,X1382)
| ~ of(skc8,X1382,skf4(skc8))
| ~ smoke(X1385,X1379)
| ~ present(X1385,X1379)
| ~ agent(X1385,X1379,skf4(skc8))
| ~ event(X1385,X1379)
| ~ man(skc8,skf4(skc8))
| ~ of(skc8,X1384,skf4(skc8))
| ~ theme(skc8,X1381,X1385)
| ~ event(skc8,X1381)
| ~ present(skc8,X1381)
| ~ think_believe_consider(skc8,X1381)
| ~ state(skc8,skc9)
| ~ of(skc8,X1383,skc10)
| ~ vincent_forename(skc8,X1383)
| ~ forename(skc8,X1383)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1381,skc10)
| ~ forename(skc8,X1380)
| ~ jules_forename(skc8,X1380)
| ~ of(skc8,X1380,skc10)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1052,plain,
( ~ accessible_world(skc8,X1575)
| ~ proposition(skc8,X1575)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ smoke(skc8,X1577)
| ~ present(skc8,X1577)
| ~ agent(skc8,X1577,skf4(skc8))
| ~ event(skc8,X1577)
| ~ think_believe_consider(skc8,X1577)
| ~ theme(skc8,X1577,skc8)
| ~ vincent_forename(skc8,X1576)
| ~ forename(skc8,X1576)
| ~ jules_forename(skc8,X1576)
| ~ of(skc8,X1576,skf4(skc8))
| ~ smoke(X1575,X1572)
| ~ present(X1575,X1572)
| ~ agent(X1575,X1572,skf4(skc8))
| ~ event(X1575,X1572)
| ~ man(skc8,skf4(skc8))
| ~ theme(skc8,X1578,X1575)
| ~ event(skc8,X1578)
| ~ present(skc8,X1578)
| ~ think_believe_consider(skc8,X1578)
| ~ state(skc8,skc9)
| ~ of(skc8,X1573,skc10)
| ~ vincent_forename(skc8,X1573)
| ~ forename(skc8,X1573)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1578,skc10)
| ~ forename(skc8,X1574)
| ~ jules_forename(skc8,X1574)
| ~ of(skc8,X1574,skc10)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c706]) ).
cnf(c1089,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1561)
| ~ accessible_world(skc12,X1561)
| ~ think_believe_consider(skc12,X1560)
| ~ present(skc12,X1560)
| ~ event(skc12,X1560)
| ~ theme(skc12,X1560,X1561)
| ~ vincent_forename(skc12,X1562)
| ~ forename(skc12,X1562)
| ~ jules_forename(skc12,X1562)
| ~ of(skc12,X1562,skc10)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ agent(skc12,X1560,skc10)
| ~ man(skc12,skc10)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1561,skf4(X1561)) ),
inference(factor,[status(thm)],[c1086]) ).
cnf(c1092,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1566)
| ~ accessible_world(skc12,X1566)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1566)
| ~ vincent_forename(skc12,X1565)
| ~ forename(skc12,X1565)
| ~ jules_forename(skc12,X1565)
| ~ of(skc12,X1565,skc10)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ man(skc12,skc10)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1566,skf4(X1566)) ),
inference(resolution,[status(thm)],[c1089,c388]) ).
cnf(c1085,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1543)
| ~ present(skc12,X1543)
| ~ event(skc12,X1543)
| ~ theme(skc12,X1543,skc12)
| ~ vincent_forename(skc12,X1545)
| ~ forename(skc12,X1545)
| ~ forename(skc12,X1544)
| ~ jules_forename(skc12,X1544)
| ~ of(skc12,X1544,skc10)
| ~ smoke(skc12,X1543)
| ~ agent(skc12,X1543,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1545,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1080]) ).
cnf(c1055,plain,
( ~ accessible_world(skc12,X1428)
| ~ proposition(skc12,X1428)
| ~ proposition(skc12,X1429)
| ~ accessible_world(skc12,X1429)
| ~ think_believe_consider(skc12,X1431)
| ~ present(skc12,X1431)
| ~ event(skc12,X1431)
| ~ theme(skc12,X1431,X1429)
| ~ vincent_forename(skc12,X1427)
| ~ forename(skc12,X1427)
| ~ forename(skc12,X1433)
| ~ jules_forename(skc12,X1433)
| ~ of(skc12,X1433,skc10)
| ~ smoke(X1428,X1430)
| ~ present(X1428,X1430)
| ~ agent(X1428,X1430,skc10)
| ~ event(X1428,X1430)
| ~ agent(skc12,X1431,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1427,skc10)
| ~ theme(skc12,X1431,X1428)
| ~ state(skc12,skc9)
| ~ of(skc12,X1432,skc10)
| ~ vincent_forename(skc12,X1432)
| ~ forename(skc12,X1432)
| ~ actual_world(skc12)
| man(X1429,skf4(X1429)) ),
inference(factor,[status(thm)],[c925]) ).
cnf(c1059,plain,
( ~ accessible_world(skc12,X1435)
| ~ proposition(skc12,X1435)
| ~ proposition(skc12,X1439)
| ~ accessible_world(skc12,X1439)
| ~ think_believe_consider(skc12,X1434)
| ~ present(skc12,X1434)
| ~ event(skc12,X1434)
| ~ theme(skc12,X1434,X1439)
| ~ vincent_forename(skc12,X1437)
| ~ forename(skc12,X1437)
| ~ forename(skc12,X1436)
| ~ jules_forename(skc12,X1436)
| ~ of(skc12,X1436,skc10)
| ~ smoke(X1435,X1438)
| ~ present(X1435,X1438)
| ~ agent(X1435,X1438,skc10)
| ~ event(X1435,X1438)
| ~ agent(skc12,X1434,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1437,skc10)
| ~ theme(skc12,X1434,X1435)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1439,skf4(X1439)) ),
inference(factor,[status(thm)],[c1055]) ).
cnf(c1062,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1490)
| ~ accessible_world(skc12,X1490)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1490)
| ~ vincent_forename(skc12,X1488)
| ~ forename(skc12,X1488)
| ~ forename(skc12,X1487)
| ~ jules_forename(skc12,X1487)
| ~ of(skc12,X1487,skc10)
| ~ smoke(skc12,X1489)
| ~ present(skc12,X1489)
| ~ agent(skc12,X1489,skc10)
| ~ event(skc12,X1489)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1488,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1490,skf4(X1490)) ),
inference(resolution,[status(thm)],[c1059,c571]) ).
cnf(c1073,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1507)
| ~ accessible_world(skc12,X1507)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1507)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1506)
| ~ jules_forename(skc12,X1506)
| ~ of(skc12,X1506,skc10)
| ~ smoke(skc12,X1505)
| ~ present(skc12,X1505)
| ~ agent(skc12,X1505,skc10)
| ~ event(skc12,X1505)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1507,skf4(X1507)) ),
inference(resolution,[status(thm)],[c1062,c580]) ).
cnf(c1078,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1508)
| ~ accessible_world(skc12,X1508)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1508)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1509)
| ~ jules_forename(skc12,X1509)
| ~ of(skc12,X1509,skc10)
| ~ smoke(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1508,skf4(X1508)) ),
inference(factor,[status(thm)],[c1073]) ).
cnf(c1072,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1493)
| ~ accessible_world(skc12,X1493)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1493)
| ~ vincent_forename(skc12,X1491)
| ~ forename(skc12,X1491)
| ~ jules_forename(skc12,X1491)
| ~ of(skc12,X1491,skc10)
| ~ smoke(skc12,X1492)
| ~ present(skc12,X1492)
| ~ agent(skc12,X1492,skc10)
| ~ event(skc12,X1492)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1493,skf4(X1493)) ),
inference(factor,[status(thm)],[c1062]) ).
cnf(c1074,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1494)
| ~ accessible_world(skc12,X1494)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1494)
| ~ vincent_forename(skc12,X1495)
| ~ forename(skc12,X1495)
| ~ jules_forename(skc12,X1495)
| ~ of(skc12,X1495,skc10)
| ~ smoke(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1494,skf4(X1494)) ),
inference(factor,[status(thm)],[c1072]) ).
cnf(c1061,plain,
( ~ accessible_world(skc12,X1442)
| ~ proposition(skc12,X1442)
| ~ think_believe_consider(skc12,X1440)
| ~ present(skc12,X1440)
| ~ event(skc12,X1440)
| ~ theme(skc12,X1440,X1442)
| ~ vincent_forename(skc12,X1443)
| ~ forename(skc12,X1443)
| ~ forename(skc12,X1441)
| ~ jules_forename(skc12,X1441)
| ~ of(skc12,X1441,skc10)
| ~ smoke(X1442,X1444)
| ~ present(X1442,X1444)
| ~ agent(X1442,X1444,skc10)
| ~ event(X1442,X1444)
| ~ agent(skc12,X1440,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1443,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1442,skf4(X1442)) ),
inference(factor,[status(thm)],[c1059]) ).
cnf(c1064,plain,
( ~ accessible_world(skc12,X1466)
| ~ proposition(skc12,X1466)
| ~ think_believe_consider(skc12,X1464)
| ~ present(skc12,X1464)
| ~ event(skc12,X1464)
| ~ theme(skc12,X1464,X1466)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1463)
| ~ jules_forename(skc12,X1463)
| ~ of(skc12,X1463,skc10)
| ~ smoke(X1466,X1465)
| ~ present(X1466,X1465)
| ~ agent(X1466,X1465,skc10)
| ~ event(X1466,X1465)
| ~ agent(skc12,X1464,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1466,skf4(X1466)) ),
inference(resolution,[status(thm)],[c1061,c580]) ).
cnf(c1070,plain,
( ~ accessible_world(skc12,X1479)
| ~ proposition(skc12,X1479)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1479)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1478)
| ~ jules_forename(skc12,X1478)
| ~ of(skc12,X1478,skc10)
| ~ smoke(X1479,X1480)
| ~ present(X1479,X1480)
| ~ agent(X1479,X1480,skc10)
| ~ event(X1479,X1480)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1479,skf4(X1479)) ),
inference(resolution,[status(thm)],[c1064,c388]) ).
cnf(c1069,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1468)
| ~ present(skc12,X1468)
| ~ event(skc12,X1468)
| ~ theme(skc12,X1468,skc12)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ forename(skc12,X1467)
| ~ jules_forename(skc12,X1467)
| ~ of(skc12,X1467,skc10)
| ~ smoke(skc12,X1468)
| ~ agent(skc12,X1468,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1064]) ).
cnf(c1071,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(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)
| ~ forename(skc12,X1469)
| ~ jules_forename(skc12,X1469)
| ~ of(skc12,X1469,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1069,c388]) ).
cnf(c1063,plain,
( ~ accessible_world(skc12,X1448)
| ~ proposition(skc12,X1448)
| ~ think_believe_consider(skc12,X1447)
| ~ present(skc12,X1447)
| ~ event(skc12,X1447)
| ~ theme(skc12,X1447,X1448)
| ~ vincent_forename(skc12,X1445)
| ~ forename(skc12,X1445)
| ~ jules_forename(skc12,X1445)
| ~ of(skc12,X1445,skc10)
| ~ smoke(X1448,X1446)
| ~ present(X1448,X1446)
| ~ agent(X1448,X1446,skc10)
| ~ event(X1448,X1446)
| ~ agent(skc12,X1447,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1448,skf4(X1448)) ),
inference(factor,[status(thm)],[c1061]) ).
cnf(c1066,plain,
( ~ accessible_world(skc12,X1462)
| ~ proposition(skc12,X1462)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1462)
| ~ vincent_forename(skc12,X1460)
| ~ forename(skc12,X1460)
| ~ jules_forename(skc12,X1460)
| ~ of(skc12,X1460,skc10)
| ~ smoke(X1462,X1461)
| ~ present(X1462,X1461)
| ~ agent(X1462,X1461,skc10)
| ~ event(X1462,X1461)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1462,skf4(X1462)) ),
inference(resolution,[status(thm)],[c1063,c388]) ).
cnf(c1065,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1450)
| ~ present(skc12,X1450)
| ~ event(skc12,X1450)
| ~ theme(skc12,X1450,skc12)
| ~ vincent_forename(skc12,X1449)
| ~ forename(skc12,X1449)
| ~ jules_forename(skc12,X1449)
| ~ of(skc12,X1449,skc10)
| ~ smoke(skc12,X1450)
| ~ agent(skc12,X1450,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1063]) ).
cnf(c1067,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),skc12)
| ~ vincent_forename(skc12,X1459)
| ~ forename(skc12,X1459)
| ~ jules_forename(skc12,X1459)
| ~ of(skc12,X1459,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1065,c388]) ).
cnf(c705,plain,
( ~ accessible_world(skc8,X1360)
| ~ proposition(skc8,X1360)
| ~ smoke(X1360,X1353)
| ~ present(X1360,X1353)
| ~ agent(X1360,X1353,skf4(X1360))
| ~ event(X1360,X1353)
| ~ think_believe_consider(skc8,X1354)
| ~ present(skc8,X1354)
| ~ event(skc8,X1354)
| ~ theme(skc8,X1354,X1360)
| ~ vincent_forename(skc8,X1359)
| ~ forename(skc8,X1359)
| ~ forename(skc8,X1357)
| ~ jules_forename(skc8,X1357)
| ~ of(skc8,X1357,skf4(X1360))
| ~ agent(skc8,X1354,skf4(X1360))
| ~ man(skc8,skf4(X1360))
| ~ of(skc8,X1359,skf4(X1360))
| ~ theme(skc8,X1356,X1360)
| ~ event(skc8,X1356)
| ~ present(skc8,X1356)
| ~ think_believe_consider(skc8,X1356)
| ~ state(skc8,skc9)
| ~ of(skc8,X1358,skc10)
| ~ vincent_forename(skc8,X1358)
| ~ forename(skc8,X1358)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1356,skc10)
| ~ forename(skc8,X1355)
| ~ jules_forename(skc8,X1355)
| ~ of(skc8,X1355,skc10)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1049,plain,
( ~ accessible_world(skc8,X1404)
| ~ proposition(skc8,X1404)
| ~ smoke(X1404,X1402)
| ~ present(X1404,X1402)
| ~ agent(X1404,X1402,skf4(X1404))
| ~ event(X1404,X1402)
| ~ think_believe_consider(skc8,X1399)
| ~ present(skc8,X1399)
| ~ event(skc8,X1399)
| ~ theme(skc8,X1399,X1404)
| ~ vincent_forename(skc8,X1401)
| ~ forename(skc8,X1401)
| ~ jules_forename(skc8,X1401)
| ~ of(skc8,X1401,skf4(X1404))
| ~ agent(skc8,X1399,skf4(X1404))
| ~ man(skc8,skf4(X1404))
| ~ theme(skc8,X1405,X1404)
| ~ event(skc8,X1405)
| ~ present(skc8,X1405)
| ~ think_believe_consider(skc8,X1405)
| ~ state(skc8,skc9)
| ~ of(skc8,X1403,skc10)
| ~ vincent_forename(skc8,X1403)
| ~ forename(skc8,X1403)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1405,skc10)
| ~ forename(skc8,X1400)
| ~ jules_forename(skc8,X1400)
| ~ of(skc8,X1400,skc10)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c705]) ).
cnf(c1053,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ smoke(skc8,X1407)
| ~ present(skc8,X1407)
| ~ agent(skc8,X1407,skf4(skc8))
| ~ event(skc8,X1407)
| ~ think_believe_consider(skc8,X1407)
| ~ theme(skc8,X1407,skc8)
| ~ vincent_forename(skc8,X1408)
| ~ forename(skc8,X1408)
| ~ jules_forename(skc8,X1408)
| ~ of(skc8,X1408,skf4(skc8))
| ~ man(skc8,skf4(skc8))
| ~ theme(skc8,X1409,skc8)
| ~ event(skc8,X1409)
| ~ present(skc8,X1409)
| ~ think_believe_consider(skc8,X1409)
| ~ state(skc8,skc9)
| ~ of(skc8,X1410,skc10)
| ~ vincent_forename(skc8,X1410)
| ~ forename(skc8,X1410)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1409,skc10)
| ~ forename(skc8,X1406)
| ~ jules_forename(skc8,X1406)
| ~ of(skc8,X1406,skc10)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c1049]) ).
cnf(c397,plain,
( ~ accessible_world(skc8,X675)
| ~ proposition(skc8,X675)
| ~ proposition(skc8,X683)
| ~ accessible_world(skc8,X683)
| ~ think_believe_consider(skc8,X678)
| ~ present(skc8,X678)
| ~ event(skc8,X678)
| ~ theme(skc8,X678,X683)
| ~ vincent_forename(skc8,X680)
| ~ forename(skc8,X680)
| ~ forename(skc8,X677)
| ~ jules_forename(skc8,X677)
| ~ of(skc8,X677,X679)
| ~ smoke(X675,X682)
| ~ present(X675,X682)
| ~ agent(X675,X682,X679)
| ~ event(X675,X682)
| ~ agent(skc8,X678,X679)
| ~ man(skc8,X679)
| ~ of(skc8,X680,X679)
| ~ theme(skc8,X684,X675)
| ~ event(skc8,X684)
| ~ present(skc8,X684)
| ~ think_believe_consider(skc8,X684)
| ~ state(skc8,skc9)
| ~ of(skc8,X676,skc10)
| ~ vincent_forename(skc8,X676)
| ~ forename(skc8,X676)
| ~ man(skc8,skc10)
| ~ agent(skc8,X684,skc10)
| ~ forename(skc8,X681)
| ~ jules_forename(skc8,X681)
| ~ of(skc8,X681,skc10)
| ~ actual_world(skc8)
| man(X683,skf4(X683)) ),
inference(resolution,[status(thm)],[clause94,clause89]) ).
cnf(c698,plain,
( ~ accessible_world(skc8,X1256)
| ~ proposition(skc8,X1256)
| ~ proposition(skc8,X1255)
| ~ accessible_world(skc8,X1255)
| ~ think_believe_consider(skc8,X1251)
| ~ present(skc8,X1251)
| ~ event(skc8,X1251)
| ~ theme(skc8,X1251,X1255)
| ~ vincent_forename(skc8,X1254)
| ~ forename(skc8,X1254)
| ~ forename(skc8,X1250)
| ~ jules_forename(skc8,X1250)
| ~ of(skc8,X1250,skc10)
| ~ smoke(X1256,X1253)
| ~ present(X1256,X1253)
| ~ agent(X1256,X1253,skc10)
| ~ event(X1256,X1253)
| ~ agent(skc8,X1251,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1254,skc10)
| ~ theme(skc8,X1249,X1256)
| ~ event(skc8,X1249)
| ~ present(skc8,X1249)
| ~ think_believe_consider(skc8,X1249)
| ~ state(skc8,skc9)
| ~ of(skc8,X1252,skc10)
| ~ vincent_forename(skc8,X1252)
| ~ forename(skc8,X1252)
| ~ agent(skc8,X1249,skc10)
| ~ actual_world(skc8)
| man(X1255,skf4(X1255)) ),
inference(factor,[status(thm)],[c397]) ).
cnf(c1028,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ proposition(skc8,X1346)
| ~ accessible_world(skc8,X1346)
| ~ think_believe_consider(skc8,X1344)
| ~ present(skc8,X1344)
| ~ event(skc8,X1344)
| ~ theme(skc8,X1344,X1346)
| ~ vincent_forename(skc8,X1342)
| ~ forename(skc8,X1342)
| ~ forename(skc8,X1347)
| ~ jules_forename(skc8,X1347)
| ~ of(skc8,X1347,skc10)
| ~ smoke(skc8,X1343)
| ~ present(skc8,X1343)
| ~ agent(skc8,X1343,skc10)
| ~ event(skc8,X1343)
| ~ agent(skc8,X1344,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1342,skc10)
| ~ theme(skc8,X1343,skc8)
| ~ think_believe_consider(skc8,X1343)
| ~ state(skc8,skc9)
| ~ of(skc8,X1345,skc10)
| ~ vincent_forename(skc8,X1345)
| ~ forename(skc8,X1345)
| ~ actual_world(skc8)
| man(X1346,skf4(X1346)) ),
inference(factor,[status(thm)],[c698]) ).
cnf(c1046,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ proposition(skc8,X1348)
| ~ accessible_world(skc8,X1348)
| ~ think_believe_consider(skc8,X1349)
| ~ present(skc8,X1349)
| ~ event(skc8,X1349)
| ~ theme(skc8,X1349,X1348)
| ~ vincent_forename(skc8,X1350)
| ~ forename(skc8,X1350)
| ~ forename(skc8,X1352)
| ~ jules_forename(skc8,X1352)
| ~ of(skc8,X1352,skc10)
| ~ smoke(skc8,X1351)
| ~ present(skc8,X1351)
| ~ agent(skc8,X1351,skc10)
| ~ event(skc8,X1351)
| ~ agent(skc8,X1349,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1350,skc10)
| ~ theme(skc8,X1351,skc8)
| ~ think_believe_consider(skc8,X1351)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1348,skf4(X1348)) ),
inference(factor,[status(thm)],[c1028]) ).
cnf(c1048,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1361)
| ~ present(skc8,X1361)
| ~ event(skc8,X1361)
| ~ theme(skc8,X1361,skc8)
| ~ vincent_forename(skc8,X1363)
| ~ forename(skc8,X1363)
| ~ forename(skc8,X1362)
| ~ jules_forename(skc8,X1362)
| ~ of(skc8,X1362,skc10)
| ~ smoke(skc8,X1361)
| ~ agent(skc8,X1361,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1363,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1046]) ).
cnf(c1029,plain,
( ~ accessible_world(skc8,X1269)
| ~ proposition(skc8,X1269)
| ~ proposition(skc8,X1268)
| ~ accessible_world(skc8,X1268)
| ~ think_believe_consider(skc8,X1266)
| ~ present(skc8,X1266)
| ~ event(skc8,X1266)
| ~ theme(skc8,X1266,X1268)
| ~ vincent_forename(skc8,X1265)
| ~ forename(skc8,X1265)
| ~ forename(skc8,X1270)
| ~ jules_forename(skc8,X1270)
| ~ of(skc8,X1270,skc10)
| ~ smoke(X1269,X1271)
| ~ present(X1269,X1271)
| ~ agent(X1269,X1271,skc10)
| ~ event(X1269,X1271)
| ~ agent(skc8,X1266,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1265,skc10)
| ~ theme(skc8,X1266,X1269)
| ~ state(skc8,skc9)
| ~ of(skc8,X1267,skc10)
| ~ vincent_forename(skc8,X1267)
| ~ forename(skc8,X1267)
| ~ actual_world(skc8)
| man(X1268,skf4(X1268)) ),
inference(factor,[status(thm)],[c698]) ).
cnf(c1031,plain,
( ~ accessible_world(skc8,X1277)
| ~ proposition(skc8,X1277)
| ~ proposition(skc8,X1275)
| ~ accessible_world(skc8,X1275)
| ~ think_believe_consider(skc8,X1273)
| ~ present(skc8,X1273)
| ~ event(skc8,X1273)
| ~ theme(skc8,X1273,X1275)
| ~ vincent_forename(skc8,X1272)
| ~ forename(skc8,X1272)
| ~ forename(skc8,X1276)
| ~ jules_forename(skc8,X1276)
| ~ of(skc8,X1276,skc10)
| ~ smoke(X1277,X1274)
| ~ present(X1277,X1274)
| ~ agent(X1277,X1274,skc10)
| ~ event(X1277,X1274)
| ~ agent(skc8,X1273,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1272,skc10)
| ~ theme(skc8,X1273,X1277)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1275,skf4(X1275)) ),
inference(factor,[status(thm)],[c1029]) ).
cnf(c1034,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1312)
| ~ accessible_world(skc8,X1312)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1312)
| ~ vincent_forename(skc8,X1310)
| ~ forename(skc8,X1310)
| ~ forename(skc8,X1313)
| ~ jules_forename(skc8,X1313)
| ~ of(skc8,X1313,skc10)
| ~ smoke(skc12,X1311)
| ~ present(skc12,X1311)
| ~ agent(skc12,X1311,skc10)
| ~ event(skc12,X1311)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1310,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1312,skf4(X1312)) ),
inference(resolution,[status(thm)],[c1031,clause87]) ).
cnf(c1042,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1326)
| ~ accessible_world(skc8,X1326)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1326)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ forename(skc8,X1327)
| ~ jules_forename(skc8,X1327)
| ~ of(skc8,X1327,skc10)
| ~ smoke(skc12,X1328)
| ~ present(skc12,X1328)
| ~ agent(skc12,X1328,skc10)
| ~ event(skc12,X1328)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1326,skf4(X1326)) ),
inference(resolution,[status(thm)],[c1034,clause88]) ).
cnf(c701,plain,
( ~ accessible_world(skc8,X1325)
| ~ proposition(skc8,X1325)
| ~ proposition(skc8,X1324)
| ~ accessible_world(skc8,X1324)
| ~ think_believe_consider(skc8,X1319)
| ~ present(skc8,X1319)
| ~ event(skc8,X1319)
| ~ theme(skc8,X1319,X1324)
| ~ vincent_forename(skc8,X1323)
| ~ forename(skc8,X1323)
| ~ forename(skc8,X1317)
| ~ jules_forename(skc8,X1317)
| ~ of(skc8,X1317,X1320)
| ~ smoke(X1325,X1322)
| ~ present(X1325,X1322)
| ~ agent(X1325,X1322,X1320)
| ~ event(X1325,X1322)
| ~ agent(skc8,X1319,X1320)
| ~ man(skc8,X1320)
| ~ of(skc8,X1323,X1320)
| ~ theme(skc8,X1318,X1325)
| ~ event(skc8,X1318)
| ~ present(skc8,X1318)
| ~ think_believe_consider(skc8,X1318)
| ~ state(skc8,skc9)
| ~ of(skc8,X1321,skc10)
| ~ vincent_forename(skc8,X1321)
| ~ forename(skc8,X1321)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1318,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1324,skf4(X1324)) ),
inference(resolution,[status(thm)],[c397,clause88]) ).
cnf(c1041,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1315)
| ~ accessible_world(skc8,X1315)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1315)
| ~ vincent_forename(skc8,X1314)
| ~ forename(skc8,X1314)
| ~ jules_forename(skc8,X1314)
| ~ of(skc8,X1314,skc10)
| ~ smoke(skc12,X1316)
| ~ present(skc12,X1316)
| ~ agent(skc12,X1316,skc10)
| ~ event(skc12,X1316)
| ~ agent(skc8,skc13,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1315,skf4(X1315)) ),
inference(factor,[status(thm)],[c1034]) ).
cnf(c1033,plain,
( ~ accessible_world(skc8,X1282)
| ~ proposition(skc8,X1282)
| ~ think_believe_consider(skc8,X1278)
| ~ present(skc8,X1278)
| ~ event(skc8,X1278)
| ~ theme(skc8,X1278,X1282)
| ~ vincent_forename(skc8,X1279)
| ~ forename(skc8,X1279)
| ~ forename(skc8,X1280)
| ~ jules_forename(skc8,X1280)
| ~ of(skc8,X1280,skc10)
| ~ smoke(X1282,X1281)
| ~ present(X1282,X1281)
| ~ agent(X1282,X1281,skc10)
| ~ event(X1282,X1281)
| ~ agent(skc8,X1278,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1279,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1282,skf4(X1282)) ),
inference(factor,[status(thm)],[c1031]) ).
cnf(c1036,plain,
( ~ accessible_world(skc8,X1300)
| ~ proposition(skc8,X1300)
| ~ think_believe_consider(skc8,X1298)
| ~ present(skc8,X1298)
| ~ event(skc8,X1298)
| ~ theme(skc8,X1298,X1300)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ forename(skc8,X1301)
| ~ jules_forename(skc8,X1301)
| ~ of(skc8,X1301,skc10)
| ~ smoke(X1300,X1299)
| ~ present(X1300,X1299)
| ~ agent(X1300,X1299,skc10)
| ~ event(X1300,X1299)
| ~ agent(skc8,X1298,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1300,skf4(X1300)) ),
inference(resolution,[status(thm)],[c1033,clause88]) ).
cnf(c1040,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1303)
| ~ present(skc8,X1303)
| ~ event(skc8,X1303)
| ~ theme(skc8,X1303,skc8)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ forename(skc8,X1302)
| ~ jules_forename(skc8,X1302)
| ~ of(skc8,X1302,skc10)
| ~ smoke(skc8,X1303)
| ~ agent(skc8,X1303,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1036]) ).
cnf(c700,plain,
( ~ accessible_world(skc8,X1297)
| ~ proposition(skc8,X1297)
| ~ proposition(skc8,X1296)
| ~ accessible_world(skc8,X1296)
| ~ think_believe_consider(skc8,X1292)
| ~ present(skc8,X1292)
| ~ event(skc8,X1292)
| ~ theme(skc8,X1292,X1296)
| ~ vincent_forename(skc8,X1295)
| ~ forename(skc8,X1295)
| ~ forename(skc8,X1289)
| ~ jules_forename(skc8,X1289)
| ~ of(skc8,X1289,X1293)
| ~ smoke(X1297,X1294)
| ~ present(X1297,X1294)
| ~ agent(X1297,X1294,X1293)
| ~ event(X1297,X1294)
| ~ agent(skc8,X1292,X1293)
| ~ man(skc8,X1293)
| ~ of(skc8,X1295,X1293)
| ~ theme(skc8,X1290,X1297)
| ~ event(skc8,X1290)
| ~ present(skc8,X1290)
| ~ think_believe_consider(skc8,X1290)
| ~ state(skc8,skc9)
| ~ of(skc8,X1291,skc10)
| ~ vincent_forename(skc8,X1291)
| ~ forename(skc8,X1291)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1290,skc10)
| ~ jules_forename(skc8,X1291)
| ~ actual_world(skc8)
| man(X1296,skf4(X1296)) ),
inference(factor,[status(thm)],[c397]) ).
cnf(c1035,plain,
( ~ accessible_world(skc8,X1285)
| ~ proposition(skc8,X1285)
| ~ think_believe_consider(skc8,X1283)
| ~ present(skc8,X1283)
| ~ event(skc8,X1283)
| ~ theme(skc8,X1283,X1285)
| ~ vincent_forename(skc8,X1286)
| ~ forename(skc8,X1286)
| ~ jules_forename(skc8,X1286)
| ~ of(skc8,X1286,skc10)
| ~ smoke(X1285,X1284)
| ~ present(X1285,X1284)
| ~ agent(X1285,X1284,skc10)
| ~ event(X1285,X1284)
| ~ agent(skc8,X1283,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1285,skf4(X1285)) ),
inference(factor,[status(thm)],[c1033]) ).
cnf(c1037,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1288)
| ~ present(skc8,X1288)
| ~ event(skc8,X1288)
| ~ theme(skc8,X1288,skc8)
| ~ vincent_forename(skc8,X1287)
| ~ forename(skc8,X1287)
| ~ jules_forename(skc8,X1287)
| ~ of(skc8,X1287,skc10)
| ~ smoke(skc8,X1288)
| ~ agent(skc8,X1288,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1035]) ).
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(c387,plain,
agent(skc12,skf2(skc15),skc15),
inference(resolution,[status(thm)],[clause93,c379]) ).
cnf(clause71,axiom,
( ~ proposition(X268,X263)
| ~ proposition(X268,X264)
| ~ theme(X268,X266,X263)
| ~ think_believe_consider(X268,X266)
| ~ think_believe_consider(X268,X265)
| ~ theme(X268,X265,X264)
| ~ agent(X268,X265,X267)
| ~ agent(X268,X266,X267)
| X263 = X264 ),
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(X236,X234)
| ~ agent(X236,X235,X233)
| agent(X234,X235,X233) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
cnf(c316,plain,
( ~ accessible_world(skc8,X495)
| agent(X495,skc13,skc15) ),
inference(resolution,[status(thm)],[clause66,clause86]) ).
cnf(c568,plain,
agent(skc12,skc13,skc15),
inference(resolution,[status(thm)],[c316,clause83]) ).
cnf(c570,plain,
( ~ proposition(skc12,X1004)
| ~ proposition(skc12,X1006)
| ~ theme(skc12,skc13,X1004)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,X1005)
| ~ theme(skc12,X1005,X1006)
| ~ agent(skc12,X1005,skc15)
| X1004 = X1006 ),
inference(resolution,[status(thm)],[c568,clause71]) ).
cnf(c899,plain,
( ~ proposition(skc12,X1247)
| ~ proposition(skc12,X1248)
| ~ theme(skc12,skc13,X1247)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1248)
| X1247 = X1248 ),
inference(resolution,[status(thm)],[c570,c387]) ).
cnf(c350,plain,
( ~ proposition(X656,X657)
| ~ proposition(X656,X658)
| ~ theme(X656,X660,X657)
| ~ think_believe_consider(X656,X660)
| ~ theme(X656,X660,X658)
| ~ agent(X656,X660,X659)
| X657 = X658 ),
inference(factor,[status(thm)],[clause71]) ).
cnf(c687,plain,
( ~ proposition(skc12,X1216)
| ~ proposition(skc12,X1217)
| ~ theme(skc12,skc13,X1216)
| ~ think_believe_consider(skc12,skc13)
| ~ theme(skc12,skc13,X1217)
| X1216 = X1217 ),
inference(resolution,[status(thm)],[c350,c568]) ).
cnf(c1019,plain,
( ~ proposition(skc12,X1240)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skc13,X1240)
| ~ think_believe_consider(skc12,skc13)
| X1240 = skc12 ),
inference(resolution,[status(thm)],[c687,c571]) ).
cnf(c686,plain,
( ~ proposition(skc8,X1205)
| ~ proposition(skc8,X1206)
| ~ theme(skc8,skc13,X1205)
| ~ think_believe_consider(skc8,skc13)
| ~ theme(skc8,skc13,X1206)
| X1205 = X1206 ),
inference(resolution,[status(thm)],[c350,clause86]) ).
cnf(c1013,plain,
( ~ proposition(skc8,X1239)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,skc13,X1239)
| ~ think_believe_consider(skc8,skc13)
| X1239 = skc12 ),
inference(resolution,[status(thm)],[c686,clause87]) ).
cnf(c689,plain,
( ~ proposition(skc12,X1236)
| ~ proposition(skc12,X1237)
| ~ theme(skc12,skf2(skc10),X1236)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1237)
| X1236 = X1237 ),
inference(resolution,[status(thm)],[c350,c388]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c30,axiom,
( X573 != X569
| X566 != X571
| X567 != X572
| X570 != X568
| ~ be(X573,X566,X567,X570)
| be(X569,X571,X572,X568) ),
theory(equality) ).
cnf(c633,plain,
( skc8 != X1126
| skc9 != X1124
| skc10 != X1125
| skc10 != X1123
| be(X1126,X1124,X1125,X1123) ),
inference(resolution,[status(thm)],[c30,clause89]) ).
cnf(c970,plain,
( skc8 != X1228
| skc9 != X1229
| skc10 != X1230
| be(X1228,X1229,X1230,skc10) ),
inference(resolution,[status(thm)],[c633,reflexivity]) ).
cnf(c688,plain,
( ~ proposition(skc12,X1226)
| ~ proposition(skc12,X1227)
| ~ theme(skc12,skf2(skc15),X1226)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1227)
| X1226 = X1227 ),
inference(resolution,[status(thm)],[c350,c387]) ).
cnf(c632,plain,
( skc12 != X1118
| skc9 != X1116
| skc10 != X1117
| skc10 != X1115
| be(X1118,X1116,X1117,X1115) ),
inference(resolution,[status(thm)],[c30,c587]) ).
cnf(c965,plain,
( skc12 != X1223
| skc9 != X1222
| skc10 != X1221
| be(X1223,X1222,X1221,skc10) ),
inference(resolution,[status(thm)],[c632,reflexivity]) ).
cnf(c969,plain,
( skc8 != X1213
| skc9 != X1214
| skc10 != X1215
| be(X1213,X1214,X1215,X1215) ),
inference(factor,[status(thm)],[c633]) ).
cnf(c1017,plain,
( skc8 != X1219
| skc9 != X1218
| be(X1219,X1218,skc10,skc10) ),
inference(resolution,[status(thm)],[c969,reflexivity]) ).
cnf(c1020,plain,
( skc8 != X1220
| be(X1220,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1017,reflexivity]) ).
cnf(c964,plain,
( skc12 != X1209
| skc9 != X1208
| skc10 != X1207
| be(X1209,X1208,X1207,X1207) ),
inference(factor,[status(thm)],[c632]) ).
cnf(c1014,plain,
( skc12 != X1211
| skc9 != X1210
| be(X1211,X1210,skc10,skc10) ),
inference(resolution,[status(thm)],[c964,reflexivity]) ).
cnf(c1015,plain,
( skc12 != X1212
| be(X1212,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1014,reflexivity]) ).
cnf(clause85,negated_conjecture,
of(skc8,skc14,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
cnf(c323,plain,
( ~ accessible_world(skc8,X501)
| of(X501,skc14,skc15) ),
inference(resolution,[status(thm)],[clause68,clause85]) ).
cnf(c577,plain,
of(skc12,skc14,skc15),
inference(resolution,[status(thm)],[c323,clause83]) ).
cnf(c36,axiom,
( X631 != X628
| X626 != X629
| X627 != X630
| ~ of(X631,X626,X627)
| of(X628,X629,X630) ),
theory(equality) ).
cnf(c669,plain,
( skc12 != X1199
| skc14 != X1200
| skc15 != X1198
| of(X1199,X1200,X1198) ),
inference(resolution,[status(thm)],[c36,c577]) ).
cnf(c1008,plain,
( skc12 != X1202
| skc14 != X1203
| of(X1202,X1203,skc15) ),
inference(resolution,[status(thm)],[c669,reflexivity]) ).
cnf(c1010,plain,
( skc12 != X1204
| of(X1204,skc14,skc15) ),
inference(resolution,[status(thm)],[c1008,reflexivity]) ).
cnf(c668,plain,
( skc8 != X1194
| skc11 != X1195
| skc10 != X1193
| of(X1194,X1195,X1193) ),
inference(resolution,[status(thm)],[c36,clause88]) ).
cnf(c1006,plain,
( skc8 != X1196
| skc11 != X1197
| of(X1196,X1197,skc10) ),
inference(resolution,[status(thm)],[c668,reflexivity]) ).
cnf(c1007,plain,
( skc8 != X1201
| of(X1201,skc11,skc10) ),
inference(resolution,[status(thm)],[c1006,reflexivity]) ).
cnf(c667,plain,
( skc8 != X1188
| skc14 != X1189
| skc15 != X1187
| of(X1188,X1189,X1187) ),
inference(resolution,[status(thm)],[c36,clause85]) ).
cnf(c1003,plain,
( skc8 != X1190
| skc14 != X1191
| of(X1190,X1191,skc15) ),
inference(resolution,[status(thm)],[c667,reflexivity]) ).
cnf(c1004,plain,
( skc8 != X1192
| of(X1192,skc14,skc15) ),
inference(resolution,[status(thm)],[c1003,reflexivity]) ).
cnf(c666,plain,
( skc12 != X1181
| skc11 != X1182
| skc10 != X1180
| of(X1181,X1182,X1180) ),
inference(resolution,[status(thm)],[c36,c580]) ).
cnf(c999,plain,
( skc12 != X1184
| skc11 != X1185
| of(X1184,X1185,skc10) ),
inference(resolution,[status(thm)],[c666,reflexivity]) ).
cnf(c1001,plain,
( skc12 != X1186
| of(X1186,skc11,skc10) ),
inference(resolution,[status(thm)],[c999,reflexivity]) ).
cnf(c35,axiom,
( X621 != X618
| X616 != X619
| X617 != X620
| ~ theme(X621,X616,X617)
| theme(X618,X619,X620) ),
theory(equality) ).
cnf(c662,plain,
( skc12 != X1173
| skc13 != X1172
| skc12 != X1174
| theme(X1173,X1172,X1174) ),
inference(resolution,[status(thm)],[c35,c571]) ).
cnf(c995,plain,
( skc12 != X1178
| skc13 != X1179
| theme(X1178,X1179,skc12) ),
inference(resolution,[status(thm)],[c662,reflexivity]) ).
cnf(c998,plain,
( skc12 != X1183
| theme(X1183,skc13,skc12) ),
inference(resolution,[status(thm)],[c995,reflexivity]) ).
cnf(c994,plain,
( skc12 != X1176
| skc13 != X1175
| theme(X1176,X1175,X1176) ),
inference(factor,[status(thm)],[c662]) ).
cnf(c996,plain,
( skc12 != X1177
| theme(X1177,skc13,X1177) ),
inference(resolution,[status(thm)],[c994,reflexivity]) ).
cnf(c34,axiom,
( X610 != X607
| X605 != X608
| X606 != X609
| ~ agent(X610,X605,X606)
| agent(X607,X608,X609) ),
theory(equality) ).
cnf(c657,plain,
( skc12 != X1164
| skf2(skc10) != X1165
| skc10 != X1163
| agent(X1164,X1165,X1163) ),
inference(resolution,[status(thm)],[c34,c388]) ).
cnf(c989,plain,
( skc12 != X1170
| skc10 != X1169
| agent(X1170,skf2(skc10),X1169) ),
inference(resolution,[status(thm)],[c657,reflexivity]) ).
cnf(c992,plain,
( skc12 != X1171
| agent(X1171,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c989,reflexivity]) ).
cnf(c661,plain,
( skc8 != X1161
| skc13 != X1160
| skc12 != X1162
| theme(X1161,X1160,X1162) ),
inference(resolution,[status(thm)],[c35,clause87]) ).
cnf(c988,plain,
( skc8 != X1167
| skc13 != X1166
| theme(X1167,X1166,skc12) ),
inference(resolution,[status(thm)],[c661,reflexivity]) ).
cnf(c990,plain,
( skc8 != X1168
| theme(X1168,skc13,skc12) ),
inference(resolution,[status(thm)],[c988,reflexivity]) ).
cnf(c656,plain,
( skc12 != X1155
| skf2(skc15) != X1156
| skc15 != X1154
| agent(X1155,X1156,X1154) ),
inference(resolution,[status(thm)],[c34,c387]) ).
cnf(c985,plain,
( skc12 != X1157
| skc15 != X1158
| agent(X1157,skf2(skc15),X1158) ),
inference(resolution,[status(thm)],[c656,reflexivity]) ).
cnf(c986,plain,
( skc12 != X1159
| agent(X1159,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c985,reflexivity]) ).
cnf(c655,plain,
( skc12 != X1149
| skc13 != X1150
| skc15 != X1148
| agent(X1149,X1150,X1148) ),
inference(resolution,[status(thm)],[c34,c568]) ).
cnf(c982,plain,
( skc12 != X1151
| skc13 != X1152
| agent(X1151,X1152,skc15) ),
inference(resolution,[status(thm)],[c655,reflexivity]) ).
cnf(c983,plain,
( skc12 != X1153
| agent(X1153,skc13,skc15) ),
inference(resolution,[status(thm)],[c982,reflexivity]) ).
cnf(c654,plain,
( skc8 != X1143
| skc13 != X1144
| skc15 != X1142
| agent(X1143,X1144,X1142) ),
inference(resolution,[status(thm)],[c34,clause86]) ).
cnf(c979,plain,
( skc8 != X1146
| skc13 != X1145
| agent(X1146,X1145,skc15) ),
inference(resolution,[status(thm)],[c654,reflexivity]) ).
cnf(c980,plain,
( skc8 != X1147
| agent(X1147,skc13,skc15) ),
inference(resolution,[status(thm)],[c979,reflexivity]) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
cnf(c33,axiom,
( X599 != X600
| X597 != X598
| ~ think_believe_consider(X599,X597)
| think_believe_consider(X600,X598) ),
theory(equality) ).
cnf(c649,plain,
( skc8 != X1140
| skc13 != X1139
| think_believe_consider(X1140,X1139) ),
inference(resolution,[status(thm)],[c33,clause78]) ).
cnf(c977,plain,
( skc8 != X1141
| think_believe_consider(X1141,skc13) ),
inference(resolution,[status(thm)],[c649,reflexivity]) ).
cnf(clause91,negated_conjecture,
( ~ man(skc12,X276)
| present(skc12,skf2(X275)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
cnf(c371,plain,
present(skc12,skf2(X281)),
inference(resolution,[status(thm)],[clause91,c331]) ).
cnf(c32,axiom,
( X589 != X590
| X587 != X588
| ~ present(X589,X587)
| present(X590,X588) ),
theory(equality) ).
cnf(c641,plain,
( skc12 != X1133
| skf2(X1135) != X1134
| present(X1133,X1134) ),
inference(resolution,[status(thm)],[c32,c371]) ).
cnf(c975,plain,
( skc12 != X1137
| present(X1137,skf2(X1136)) ),
inference(resolution,[status(thm)],[c641,reflexivity]) ).
cnf(clause45,axiom,
( ~ accessible_world(X122,X120)
| ~ think_believe_consider(X122,X121)
| think_believe_consider(X120,X121) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(c198,plain,
( ~ accessible_world(skc8,X201)
| think_believe_consider(X201,skc13) ),
inference(resolution,[status(thm)],[clause45,clause78]) ).
cnf(c263,plain,
think_believe_consider(skc12,skc13),
inference(resolution,[status(thm)],[c198,clause83]) ).
cnf(c648,plain,
( skc12 != X1131
| skc13 != X1130
| think_believe_consider(X1131,X1130) ),
inference(resolution,[status(thm)],[c33,c263]) ).
cnf(c973,plain,
( skc12 != X1132
| think_believe_consider(X1132,skc13) ),
inference(resolution,[status(thm)],[c648,reflexivity]) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
cnf(c643,plain,
( skc8 != X1127
| skc13 != X1128
| present(X1127,X1128) ),
inference(resolution,[status(thm)],[c32,clause77]) ).
cnf(c971,plain,
( skc8 != X1129
| present(X1129,skc13) ),
inference(resolution,[status(thm)],[c643,reflexivity]) ).
cnf(clause44,axiom,
( ~ accessible_world(X117,X115)
| ~ present(X117,X116)
| present(X115,X116) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c190,plain,
( ~ accessible_world(skc8,X194)
| present(X194,skc13) ),
inference(resolution,[status(thm)],[clause44,clause77]) ).
cnf(c259,plain,
present(skc12,skc13),
inference(resolution,[status(thm)],[c190,clause83]) ).
cnf(c642,plain,
( skc12 != X1120
| skc13 != X1121
| present(X1120,X1121) ),
inference(resolution,[status(thm)],[c32,c259]) ).
cnf(c967,plain,
( skc12 != X1122
| present(X1122,skc13) ),
inference(resolution,[status(thm)],[c642,reflexivity]) ).
cnf(c31,axiom,
( X581 != X582
| X579 != X580
| ~ accessible_world(X581,X579)
| accessible_world(X582,X580) ),
theory(equality) ).
cnf(c637,plain,
( skc8 != X1113
| skc12 != X1114
| accessible_world(X1113,X1114) ),
inference(resolution,[status(thm)],[c31,clause83]) ).
cnf(c963,plain,
( skc8 != X1119
| accessible_world(X1119,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,
( X558 != X559
| X556 != X557
| ~ jules_forename(X558,X556)
| jules_forename(X559,X557) ),
theory(equality) ).
cnf(c627,plain,
( skc8 != X1110
| skc11 != X1109
| jules_forename(X1110,X1109) ),
inference(resolution,[status(thm)],[c29,clause79]) ).
cnf(c960,plain,
( skc8 != X1112
| jules_forename(X1112,skc11) ),
inference(resolution,[status(thm)],[c627,reflexivity]) ).
cnf(clause65,axiom,
( ~ accessible_world(X230,X228)
| ~ jules_forename(X230,X229)
| jules_forename(X228,X229) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
cnf(c313,plain,
( ~ accessible_world(skc8,X417)
| jules_forename(X417,skc11) ),
inference(resolution,[status(thm)],[clause65,clause79]) ).
cnf(c529,plain,
jules_forename(skc12,skc11),
inference(resolution,[status(thm)],[c313,clause83]) ).
cnf(c626,plain,
( skc12 != X1108
| skc11 != X1107
| jules_forename(X1108,X1107) ),
inference(resolution,[status(thm)],[c29,c529]) ).
cnf(c959,plain,
( skc12 != X1111
| jules_forename(X1111,skc11) ),
inference(resolution,[status(thm)],[c626,reflexivity]) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
cnf(c28,axiom,
( X550 != X551
| X548 != X549
| ~ vincent_forename(X550,X548)
| vincent_forename(X551,X549) ),
theory(equality) ).
cnf(c622,plain,
( skc8 != X1104
| skc14 != X1103
| vincent_forename(X1104,X1103) ),
inference(resolution,[status(thm)],[c28,clause75]) ).
cnf(c956,plain,
( skc8 != X1106
| vincent_forename(X1106,skc14) ),
inference(resolution,[status(thm)],[c622,reflexivity]) ).
cnf(clause64,axiom,
( ~ accessible_world(X226,X224)
| ~ vincent_forename(X226,X225)
| vincent_forename(X224,X225) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
cnf(c308,plain,
( ~ accessible_world(skc8,X410)
| vincent_forename(X410,skc14) ),
inference(resolution,[status(thm)],[clause64,clause75]) ).
cnf(c520,plain,
vincent_forename(skc12,skc14),
inference(resolution,[status(thm)],[c308,clause83]) ).
cnf(c621,plain,
( skc12 != X1102
| skc14 != X1101
| vincent_forename(X1102,X1101) ),
inference(resolution,[status(thm)],[c28,c520]) ).
cnf(c955,plain,
( skc12 != X1105
| vincent_forename(X1105,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(X56,X55)
| relname(X56,X55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c83,plain,
relname(skc8,skc14),
inference(resolution,[status(thm)],[clause27,clause74]) ).
cnf(c27,axiom,
( X541 != X542
| X539 != X540
| ~ relname(X541,X539)
| relname(X542,X540) ),
theory(equality) ).
cnf(c617,plain,
( skc8 != X1098
| skc14 != X1097
| relname(X1098,X1097) ),
inference(resolution,[status(thm)],[c27,c83]) ).
cnf(c952,plain,
( skc8 != X1100
| relname(X1100,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(X219,X217)
| ~ forename(X219,X218)
| forename(X217,X218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
cnf(c289,plain,
( ~ accessible_world(skc8,X390)
| forename(X390,skc11) ),
inference(resolution,[status(thm)],[clause62,clause80]) ).
cnf(c499,plain,
forename(skc12,skc11),
inference(resolution,[status(thm)],[c289,clause83]) ).
cnf(c501,plain,
relname(skc12,skc11),
inference(resolution,[status(thm)],[c499,clause27]) ).
cnf(c616,plain,
( skc12 != X1096
| skc11 != X1095
| relname(X1096,X1095) ),
inference(resolution,[status(thm)],[c27,c501]) ).
cnf(c951,plain,
( skc12 != X1099
| relname(X1099,skc11) ),
inference(resolution,[status(thm)],[c616,reflexivity]) ).
cnf(c84,plain,
relname(skc8,skc11),
inference(resolution,[status(thm)],[clause27,clause80]) ).
cnf(c615,plain,
( skc8 != X1092
| skc11 != X1091
| relname(X1092,X1091) ),
inference(resolution,[status(thm)],[c27,c84]) ).
cnf(c948,plain,
( skc8 != X1094
| relname(X1094,skc11) ),
inference(resolution,[status(thm)],[c615,reflexivity]) ).
cnf(c288,plain,
( ~ accessible_world(skc8,X385)
| forename(X385,skc14) ),
inference(resolution,[status(thm)],[clause62,clause74]) ).
cnf(c483,plain,
forename(skc12,skc14),
inference(resolution,[status(thm)],[c288,clause83]) ).
cnf(c485,plain,
relname(skc12,skc14),
inference(resolution,[status(thm)],[c483,clause27]) ).
cnf(c614,plain,
( skc12 != X1090
| skc14 != X1089
| relname(X1090,X1089) ),
inference(resolution,[status(thm)],[c27,c485]) ).
cnf(c947,plain,
( skc12 != X1093
| relname(X1093,skc14) ),
inference(resolution,[status(thm)],[c614,reflexivity]) ).
cnf(c26,axiom,
( X531 != X532
| X529 != X530
| ~ forename(X531,X529)
| forename(X532,X530) ),
theory(equality) ).
cnf(c609,plain,
( skc8 != X1085
| skc11 != X1086
| forename(X1085,X1086) ),
inference(resolution,[status(thm)],[c26,clause80]) ).
cnf(c944,plain,
( skc8 != X1088
| forename(X1088,skc11) ),
inference(resolution,[status(thm)],[c609,reflexivity]) ).
cnf(c608,plain,
( skc12 != X1083
| skc14 != X1084
| forename(X1083,X1084) ),
inference(resolution,[status(thm)],[c26,c483]) ).
cnf(c943,plain,
( skc12 != X1087
| forename(X1087,skc14) ),
inference(resolution,[status(thm)],[c608,reflexivity]) ).
cnf(c607,plain,
( skc8 != X1079
| skc14 != X1080
| forename(X1079,X1080) ),
inference(resolution,[status(thm)],[c26,clause74]) ).
cnf(c940,plain,
( skc8 != X1082
| forename(X1082,skc14) ),
inference(resolution,[status(thm)],[c607,reflexivity]) ).
cnf(c606,plain,
( skc12 != X1077
| skc11 != X1078
| forename(X1077,X1078) ),
inference(resolution,[status(thm)],[c26,c499]) ).
cnf(c939,plain,
( skc12 != X1081
| forename(X1081,skc11) ),
inference(resolution,[status(thm)],[c606,reflexivity]) ).
cnf(clause26,axiom,
( ~ man(X54,X53)
| male(X54,X53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c81,plain,
male(skc8,skc10),
inference(resolution,[status(thm)],[clause26,clause81]) ).
cnf(c25,axiom,
( X523 != X524
| X521 != X522
| ~ male(X523,X521)
| male(X524,X522) ),
theory(equality) ).
cnf(c602,plain,
( skc8 != X1073
| skc10 != X1074
| male(X1073,X1074) ),
inference(resolution,[status(thm)],[c25,c81]) ).
cnf(c936,plain,
( skc8 != X1076
| male(X1076,skc10) ),
inference(resolution,[status(thm)],[c602,reflexivity]) ).
cnf(c82,plain,
male(skc8,skc15),
inference(resolution,[status(thm)],[clause26,clause73]) ).
cnf(c601,plain,
( skc8 != X1071
| skc15 != X1072
| male(X1071,X1072) ),
inference(resolution,[status(thm)],[c25,c82]) ).
cnf(c935,plain,
( skc8 != X1075
| male(X1075,skc15) ),
inference(resolution,[status(thm)],[c601,reflexivity]) ).
cnf(c381,plain,
male(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause26]) ).
cnf(c600,plain,
( skc12 != X1067
| skc15 != X1068
| male(X1067,X1068) ),
inference(resolution,[status(thm)],[c25,c381]) ).
cnf(c932,plain,
( skc12 != X1070
| male(X1070,skc15) ),
inference(resolution,[status(thm)],[c600,reflexivity]) ).
cnf(c332,plain,
male(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause26]) ).
cnf(c599,plain,
( skc12 != X1065
| skc10 != X1066
| male(X1065,X1066) ),
inference(resolution,[status(thm)],[c25,c332]) ).
cnf(c931,plain,
( skc12 != X1069
| male(X1069,skc10) ),
inference(resolution,[status(thm)],[c599,reflexivity]) ).
cnf(clause25,axiom,
( ~ human_person(X52,X51)
| animate(X52,X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(clause16,axiom,
( ~ man(X34,X33)
| human_person(X34,X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c333,plain,
human_person(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause16]) ).
cnf(c342,plain,
animate(skc12,skc10),
inference(resolution,[status(thm)],[c333,clause25]) ).
cnf(c24,axiom,
( X514 != X515
| X512 != X513
| ~ animate(X514,X512)
| animate(X515,X513) ),
theory(equality) ).
cnf(c595,plain,
( skc12 != X1062
| skc10 != X1063
| animate(X1062,X1063) ),
inference(resolution,[status(thm)],[c24,c342]) ).
cnf(c929,plain,
( skc12 != X1064
| animate(X1064,skc10) ),
inference(resolution,[status(thm)],[c595,reflexivity]) ).
cnf(c380,plain,
human_person(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause16]) ).
cnf(c386,plain,
animate(skc12,skc15),
inference(resolution,[status(thm)],[c380,clause25]) ).
cnf(c594,plain,
( skc12 != X1049
| skc15 != X1050
| animate(X1049,X1050) ),
inference(resolution,[status(thm)],[c24,c386]) ).
cnf(c923,plain,
( skc12 != X1051
| animate(X1051,skc15) ),
inference(resolution,[status(thm)],[c594,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(c593,plain,
( skc8 != X1046
| skc15 != X1047
| animate(X1046,X1047) ),
inference(resolution,[status(thm)],[c24,c80]) ).
cnf(c921,plain,
( skc8 != X1048
| animate(X1048,skc15) ),
inference(resolution,[status(thm)],[c593,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(c592,plain,
( skc8 != X1032
| skc10 != X1033
| animate(X1032,X1033) ),
inference(resolution,[status(thm)],[c24,c79]) ).
cnf(c917,plain,
( skc8 != X1034
| animate(X1034,skc10) ),
inference(resolution,[status(thm)],[c592,reflexivity]) ).
cnf(clause24,axiom,
( ~ human_person(X50,X49)
| human(X50,X49) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c77,plain,
human(skc8,skc10),
inference(resolution,[status(thm)],[clause24,c59]) ).
cnf(c23,axiom,
( X506 != X507
| X504 != X505
| ~ human(X506,X504)
| human(X507,X505) ),
theory(equality) ).
cnf(c586,plain,
( skc8 != X1028
| skc10 != X1029
| human(X1028,X1029) ),
inference(resolution,[status(thm)],[c23,c77]) ).
cnf(c915,plain,
( skc8 != X1031
| human(X1031,skc10) ),
inference(resolution,[status(thm)],[c586,reflexivity]) ).
cnf(c588,plain,
( ~ accessible_world(skc12,X1030)
| be(X1030,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c587,clause69]) ).
cnf(c341,plain,
human(skc12,skc10),
inference(resolution,[status(thm)],[c333,clause24]) ).
cnf(c585,plain,
( skc12 != X1025
| skc10 != X1026
| human(X1025,X1026) ),
inference(resolution,[status(thm)],[c23,c341]) ).
cnf(c913,plain,
( skc12 != X1027
| human(X1027,skc10) ),
inference(resolution,[status(thm)],[c585,reflexivity]) ).
cnf(clause70,axiom,
( ~ forename(X262,X260)
| ~ of(X262,X261,X259)
| ~ forename(X262,X261)
| ~ of(X262,X260,X259)
| ~ entity(X262,X259)
| X261 = X260 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
cnf(c582,plain,
( ~ forename(skc12,skc11)
| ~ of(skc12,X1024,skc10)
| ~ forename(skc12,X1024)
| ~ entity(skc12,skc10)
| X1024 = skc11 ),
inference(resolution,[status(thm)],[c580,clause70]) ).
cnf(c78,plain,
human(skc8,skc15),
inference(resolution,[status(thm)],[clause24,c60]) ).
cnf(c584,plain,
( skc8 != X1021
| skc15 != X1022
| human(X1021,X1022) ),
inference(resolution,[status(thm)],[c23,c78]) ).
cnf(c910,plain,
( skc8 != X1023
| human(X1023,skc15) ),
inference(resolution,[status(thm)],[c584,reflexivity]) ).
cnf(c385,plain,
human(skc12,skc15),
inference(resolution,[status(thm)],[c380,clause24]) ).
cnf(c583,plain,
( skc12 != X1018
| skc15 != X1019
| human(X1018,X1019) ),
inference(resolution,[status(thm)],[c23,c385]) ).
cnf(c908,plain,
( skc12 != X1020
| human(X1020,skc15) ),
inference(resolution,[status(thm)],[c583,reflexivity]) ).
cnf(c579,plain,
( ~ forename(skc12,skc14)
| ~ of(skc12,X1017,skc15)
| ~ forename(skc12,X1017)
| ~ entity(skc12,skc15)
| X1017 = skc14 ),
inference(resolution,[status(thm)],[c577,clause70]) ).
cnf(clause17,axiom,
( ~ human_person(X36,X35)
| organism(X36,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c61,plain,
organism(skc8,skc10),
inference(resolution,[status(thm)],[clause17,c59]) ).
cnf(clause23,axiom,
( ~ organism(X48,X47)
| living(X48,X47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(c75,plain,
living(skc8,skc10),
inference(resolution,[status(thm)],[clause23,c61]) ).
cnf(c22,axiom,
( X499 != X500
| X497 != X498
| ~ living(X499,X497)
| living(X500,X498) ),
theory(equality) ).
cnf(c576,plain,
( skc8 != X1014
| skc10 != X1015
| living(X1014,X1015) ),
inference(resolution,[status(thm)],[c22,c75]) ).
cnf(c905,plain,
( skc8 != X1016
| living(X1016,skc10) ),
inference(resolution,[status(thm)],[c576,reflexivity]) ).
cnf(c384,plain,
organism(skc12,skc15),
inference(resolution,[status(thm)],[c380,clause17]) ).
cnf(c393,plain,
living(skc12,skc15),
inference(resolution,[status(thm)],[c384,clause23]) ).
cnf(c575,plain,
( skc12 != X1011
| skc15 != X1012
| living(X1011,X1012) ),
inference(resolution,[status(thm)],[c22,c393]) ).
cnf(c903,plain,
( skc12 != X1013
| living(X1013,skc15) ),
inference(resolution,[status(thm)],[c575,reflexivity]) ).
cnf(c340,plain,
organism(skc12,skc10),
inference(resolution,[status(thm)],[c333,clause17]) ).
cnf(c346,plain,
living(skc12,skc10),
inference(resolution,[status(thm)],[c340,clause23]) ).
cnf(c574,plain,
( skc12 != X1008
| skc10 != X1009
| living(X1008,X1009) ),
inference(resolution,[status(thm)],[c22,c346]) ).
cnf(c901,plain,
( skc12 != X1010
| living(X1010,skc10) ),
inference(resolution,[status(thm)],[c574,reflexivity]) ).
cnf(c62,plain,
organism(skc8,skc15),
inference(resolution,[status(thm)],[clause17,c60]) ).
cnf(c76,plain,
living(skc8,skc15),
inference(resolution,[status(thm)],[clause23,c62]) ).
cnf(c573,plain,
( skc8 != X1002
| skc15 != X1003
| living(X1002,X1003) ),
inference(resolution,[status(thm)],[c22,c76]) ).
cnf(c897,plain,
( skc8 != X1007
| living(X1007,skc15) ),
inference(resolution,[status(thm)],[c573,reflexivity]) ).
cnf(clause22,axiom,
( ~ organism(X46,X45)
| impartial(X46,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c73,plain,
impartial(skc8,skc10),
inference(resolution,[status(thm)],[clause22,c61]) ).
cnf(c21,axiom,
( X491 != X492
| X489 != X490
| ~ impartial(X491,X489)
| impartial(X492,X490) ),
theory(equality) ).
cnf(c567,plain,
( skc8 != X999
| skc10 != X998
| impartial(X999,X998) ),
inference(resolution,[status(thm)],[c21,c73]) ).
cnf(c894,plain,
( skc8 != X1001
| impartial(X1001,skc10) ),
inference(resolution,[status(thm)],[c567,reflexivity]) ).
cnf(c74,plain,
impartial(skc8,skc15),
inference(resolution,[status(thm)],[clause22,c62]) ).
cnf(c566,plain,
( skc8 != X997
| skc15 != X996
| impartial(X997,X996) ),
inference(resolution,[status(thm)],[c21,c74]) ).
cnf(c893,plain,
( skc8 != X1000
| impartial(X1000,skc15) ),
inference(resolution,[status(thm)],[c566,reflexivity]) ).
cnf(c343,plain,
impartial(skc12,skc10),
inference(resolution,[status(thm)],[c340,clause22]) ).
cnf(c565,plain,
( skc12 != X993
| skc10 != X992
| impartial(X993,X992) ),
inference(resolution,[status(thm)],[c21,c343]) ).
cnf(c890,plain,
( skc12 != X995
| impartial(X995,skc10) ),
inference(resolution,[status(thm)],[c565,reflexivity]) ).
cnf(c390,plain,
impartial(skc12,skc15),
inference(resolution,[status(thm)],[c384,clause22]) ).
cnf(c564,plain,
( skc12 != X991
| skc15 != X990
| impartial(X991,X990) ),
inference(resolution,[status(thm)],[c21,c390]) ).
cnf(c889,plain,
( skc12 != X994
| impartial(X994,skc15) ),
inference(resolution,[status(thm)],[c564,reflexivity]) ).
cnf(clause21,axiom,
( ~ entity(X44,X43)
| existent(X44,X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(clause18,axiom,
( ~ organism(X38,X37)
| entity(X38,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c345,plain,
entity(skc12,skc10),
inference(resolution,[status(thm)],[c340,clause18]) ).
cnf(c354,plain,
existent(skc12,skc10),
inference(resolution,[status(thm)],[c345,clause21]) ).
cnf(c20,axiom,
( X477 != X478
| X475 != X476
| ~ existent(X477,X475)
| existent(X478,X476) ),
theory(equality) ).
cnf(c563,plain,
( skc12 != X987
| skc10 != X986
| existent(X987,X986) ),
inference(resolution,[status(thm)],[c20,c354]) ).
cnf(c886,plain,
( skc12 != X989
| existent(X989,skc10) ),
inference(resolution,[status(thm)],[c563,reflexivity]) ).
cnf(c63,plain,
entity(skc8,skc10),
inference(resolution,[status(thm)],[clause18,c61]) ).
cnf(c71,plain,
existent(skc8,skc10),
inference(resolution,[status(thm)],[clause21,c63]) ).
cnf(c562,plain,
( skc8 != X985
| skc10 != X984
| existent(X985,X984) ),
inference(resolution,[status(thm)],[c20,c71]) ).
cnf(c885,plain,
( skc8 != X988
| existent(X988,skc10) ),
inference(resolution,[status(thm)],[c562,reflexivity]) ).
cnf(c392,plain,
entity(skc12,skc15),
inference(resolution,[status(thm)],[c384,clause18]) ).
cnf(c400,plain,
existent(skc12,skc15),
inference(resolution,[status(thm)],[c392,clause21]) ).
cnf(c561,plain,
( skc12 != X981
| skc15 != X980
| existent(X981,X980) ),
inference(resolution,[status(thm)],[c20,c400]) ).
cnf(c882,plain,
( skc12 != X983
| existent(X983,skc15) ),
inference(resolution,[status(thm)],[c561,reflexivity]) ).
cnf(c64,plain,
entity(skc8,skc15),
inference(resolution,[status(thm)],[clause18,c62]) ).
cnf(c72,plain,
existent(skc8,skc15),
inference(resolution,[status(thm)],[clause21,c64]) ).
cnf(c560,plain,
( skc8 != X979
| skc15 != X978
| existent(X979,X978) ),
inference(resolution,[status(thm)],[c20,c72]) ).
cnf(c881,plain,
( skc8 != X982
| existent(X982,skc15) ),
inference(resolution,[status(thm)],[c560,reflexivity]) ).
cnf(c19,axiom,
( X465 != X466
| X463 != X464
| ~ entity(X465,X463)
| entity(X466,X464) ),
theory(equality) ).
cnf(c559,plain,
( skc8 != X974
| skc15 != X975
| entity(X974,X975) ),
inference(resolution,[status(thm)],[c19,c64]) ).
cnf(c878,plain,
( skc8 != X977
| entity(X977,skc15) ),
inference(resolution,[status(thm)],[c559,reflexivity]) ).
cnf(c558,plain,
( skc8 != X972
| skc10 != X973
| entity(X972,X973) ),
inference(resolution,[status(thm)],[c19,c63]) ).
cnf(c877,plain,
( skc8 != X976
| entity(X976,skc10) ),
inference(resolution,[status(thm)],[c558,reflexivity]) ).
cnf(c557,plain,
( skc12 != X968
| skc15 != X969
| entity(X968,X969) ),
inference(resolution,[status(thm)],[c19,c392]) ).
cnf(c874,plain,
( skc12 != X971
| entity(X971,skc15) ),
inference(resolution,[status(thm)],[c557,reflexivity]) ).
cnf(c556,plain,
( skc12 != X966
| skc10 != X967
| entity(X966,X967) ),
inference(resolution,[status(thm)],[c19,c345]) ).
cnf(c873,plain,
( skc12 != X970
| entity(X970,skc10) ),
inference(resolution,[status(thm)],[c556,reflexivity]) ).
cnf(c18,axiom,
( X456 != X457
| X454 != X455
| ~ organism(X456,X454)
| organism(X457,X455) ),
theory(equality) ).
cnf(c555,plain,
( skc8 != X963
| skc15 != X962
| organism(X963,X962) ),
inference(resolution,[status(thm)],[c18,c62]) ).
cnf(c870,plain,
( skc8 != X965
| organism(X965,skc15) ),
inference(resolution,[status(thm)],[c555,reflexivity]) ).
cnf(c554,plain,
( skc12 != X961
| skc15 != X960
| organism(X961,X960) ),
inference(resolution,[status(thm)],[c18,c384]) ).
cnf(c869,plain,
( skc12 != X964
| organism(X964,skc15) ),
inference(resolution,[status(thm)],[c554,reflexivity]) ).
cnf(c553,plain,
( skc8 != X957
| skc10 != X956
| organism(X957,X956) ),
inference(resolution,[status(thm)],[c18,c61]) ).
cnf(c866,plain,
( skc8 != X959
| organism(X959,skc10) ),
inference(resolution,[status(thm)],[c553,reflexivity]) ).
cnf(c552,plain,
( skc12 != X955
| skc10 != X954
| organism(X955,X954) ),
inference(resolution,[status(thm)],[c18,c340]) ).
cnf(c865,plain,
( skc12 != X958
| organism(X958,skc10) ),
inference(resolution,[status(thm)],[c552,reflexivity]) ).
cnf(c17,axiom,
( X447 != X448
| X445 != X446
| ~ human_person(X447,X445)
| human_person(X448,X446) ),
theory(equality) ).
cnf(c551,plain,
( skc12 != X951
| skc15 != X952
| human_person(X951,X952) ),
inference(resolution,[status(thm)],[c17,c380]) ).
cnf(c863,plain,
( skc12 != X953
| human_person(X953,skc15) ),
inference(resolution,[status(thm)],[c551,reflexivity]) ).
cnf(c547,plain,
( ~ proposition(skc12,X948)
| ~ proposition(skc12,X950)
| ~ theme(skc12,skf2(skc10),X948)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,X949)
| ~ theme(skc12,X949,X950)
| ~ agent(skc12,X949,skc10)
| X948 = X950 ),
inference(resolution,[status(thm)],[c388,clause71]) ).
cnf(c550,plain,
( skc8 != X945
| skc15 != X946
| human_person(X945,X946) ),
inference(resolution,[status(thm)],[c17,c60]) ).
cnf(c860,plain,
( skc8 != X947
| human_person(X947,skc15) ),
inference(resolution,[status(thm)],[c550,reflexivity]) ).
cnf(c549,plain,
( skc12 != X942
| skc10 != X943
| human_person(X942,X943) ),
inference(resolution,[status(thm)],[c17,c333]) ).
cnf(c858,plain,
( skc12 != X944
| human_person(X944,skc10) ),
inference(resolution,[status(thm)],[c549,reflexivity]) ).
cnf(c545,plain,
( ~ proposition(skc12,X939)
| ~ proposition(skc12,X941)
| ~ theme(skc12,skf2(skc15),X939)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ think_believe_consider(skc12,X940)
| ~ theme(skc12,X940,X941)
| ~ agent(skc12,X940,skc15)
| X939 = X941 ),
inference(resolution,[status(thm)],[c387,clause71]) ).
cnf(c548,plain,
( skc8 != X936
| skc10 != X937
| human_person(X936,X937) ),
inference(resolution,[status(thm)],[c17,c59]) ).
cnf(c855,plain,
( skc8 != X938
| human_person(X938,skc10) ),
inference(resolution,[status(thm)],[c548,reflexivity]) ).
cnf(c546,plain,
( ~ accessible_world(skc12,X935)
| agent(X935,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c388,clause66]) ).
cnf(c544,plain,
( ~ accessible_world(skc12,X934)
| agent(X934,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c387,clause66]) ).
cnf(c16,axiom,
( X440 != X441
| X438 != X439
| ~ man(X440,X438)
| man(X441,X439) ),
theory(equality) ).
cnf(c543,plain,
( skc12 != X931
| skc10 != X932
| man(X931,X932) ),
inference(resolution,[status(thm)],[c16,c331]) ).
cnf(c853,plain,
( skc12 != X933
| man(X933,skc10) ),
inference(resolution,[status(thm)],[c543,reflexivity]) ).
cnf(c542,plain,
( skc8 != X928
| skc15 != X929
| man(X928,X929) ),
inference(resolution,[status(thm)],[c16,clause73]) ).
cnf(c851,plain,
( skc8 != X930
| man(X930,skc15) ),
inference(resolution,[status(thm)],[c542,reflexivity]) ).
cnf(c541,plain,
( skc8 != X925
| skc10 != X926
| man(X925,X926) ),
inference(resolution,[status(thm)],[c16,clause81]) ).
cnf(c849,plain,
( skc8 != X927
| man(X927,skc10) ),
inference(resolution,[status(thm)],[c541,reflexivity]) ).
cnf(c540,plain,
( skc12 != X922
| skc15 != X923
| man(X922,X923) ),
inference(resolution,[status(thm)],[c16,c379]) ).
cnf(c847,plain,
( skc12 != X924
| man(X924,skc15) ),
inference(resolution,[status(thm)],[c540,reflexivity]) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
cnf(c15,axiom,
( X431 != X432
| X429 != X430
| ~ state(X431,X429)
| state(X432,X430) ),
theory(equality) ).
cnf(c539,plain,
( skc8 != X920
| skc9 != X919
| state(X920,X919) ),
inference(resolution,[status(thm)],[c15,clause82]) ).
cnf(c845,plain,
( skc8 != X921
| state(X921,skc9) ),
inference(resolution,[status(thm)],[c539,reflexivity]) ).
cnf(clause51,axiom,
( ~ accessible_world(X157,X155)
| ~ state(X157,X156)
| state(X155,X156) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c227,plain,
( ~ accessible_world(skc8,X251)
| state(X251,skc9) ),
inference(resolution,[status(thm)],[clause51,clause82]) ).
cnf(c326,plain,
state(skc12,skc9),
inference(resolution,[status(thm)],[c227,clause83]) ).
cnf(c538,plain,
( skc12 != X917
| skc9 != X916
| state(X917,X916) ),
inference(resolution,[status(thm)],[c15,c326]) ).
cnf(c843,plain,
( skc12 != X918
| state(X918,skc9) ),
inference(resolution,[status(thm)],[c538,reflexivity]) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
cnf(clause8,axiom,
( ~ proposition(X18,X17)
| relation(X18,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c44,plain,
relation(skc8,skc12),
inference(resolution,[status(thm)],[clause8,clause84]) ).
cnf(clause9,axiom,
( ~ relation(X20,X19)
| abstraction(X20,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(c45,plain,
abstraction(skc8,skc12),
inference(resolution,[status(thm)],[clause9,c44]) ).
cnf(clause12,axiom,
( ~ abstraction(X26,X25)
| general(X26,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c49,plain,
general(skc8,skc12),
inference(resolution,[status(thm)],[clause12,c45]) ).
cnf(c14,axiom,
( X422 != X423
| X420 != X421
| ~ general(X422,X420)
| general(X423,X421) ),
theory(equality) ).
cnf(c537,plain,
( skc8 != X914
| skc12 != X913
| general(X914,X913) ),
inference(resolution,[status(thm)],[c14,c49]) ).
cnf(c841,plain,
( skc8 != X915
| general(X915,skc12) ),
inference(resolution,[status(thm)],[c537,reflexivity]) ).
cnf(clause28,axiom,
( ~ relname(X58,X57)
| relation(X58,X57) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c85,plain,
relation(skc8,skc11),
inference(resolution,[status(thm)],[clause28,c84]) ).
cnf(clause47,axiom,
( ~ accessible_world(X134,X132)
| ~ relation(X134,X133)
| relation(X132,X133) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c209,plain,
( ~ accessible_world(skc8,X223)
| relation(X223,skc11) ),
inference(resolution,[status(thm)],[clause47,c85]) ).
cnf(c300,plain,
relation(skc12,skc11),
inference(resolution,[status(thm)],[c209,clause83]) ).
cnf(c301,plain,
abstraction(skc12,skc11),
inference(resolution,[status(thm)],[c300,clause9]) ).
cnf(c304,plain,
general(skc12,skc11),
inference(resolution,[status(thm)],[c301,clause12]) ).
cnf(c536,plain,
( skc12 != X911
| skc11 != X910
| general(X911,X910) ),
inference(resolution,[status(thm)],[c14,c304]) ).
cnf(c839,plain,
( skc12 != X912
| general(X912,skc11) ),
inference(resolution,[status(thm)],[c536,reflexivity]) ).
cnf(c88,plain,
abstraction(skc8,skc11),
inference(resolution,[status(thm)],[c85,clause9]) ).
cnf(c92,plain,
general(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause12]) ).
cnf(c535,plain,
( skc8 != X908
| skc11 != X907
| general(X908,X907) ),
inference(resolution,[status(thm)],[c14,c92]) ).
cnf(c837,plain,
( skc8 != X909
| general(X909,skc11) ),
inference(resolution,[status(thm)],[c535,reflexivity]) ).
cnf(c86,plain,
relation(skc8,skc14),
inference(resolution,[status(thm)],[clause28,c83]) ).
cnf(c208,plain,
( ~ accessible_world(skc8,X216)
| relation(X216,skc14) ),
inference(resolution,[status(thm)],[clause47,c86]) ).
cnf(c285,plain,
relation(skc12,skc14),
inference(resolution,[status(thm)],[c208,clause83]) ).
cnf(c286,plain,
abstraction(skc12,skc14),
inference(resolution,[status(thm)],[c285,clause9]) ).
cnf(c291,plain,
general(skc12,skc14),
inference(resolution,[status(thm)],[c286,clause12]) ).
cnf(c534,plain,
( skc12 != X905
| skc14 != X904
| general(X905,X904) ),
inference(resolution,[status(thm)],[c14,c291]) ).
cnf(c835,plain,
( skc12 != X906
| general(X906,skc14) ),
inference(resolution,[status(thm)],[c534,reflexivity]) ).
cnf(clause46,axiom,
( ~ accessible_world(X127,X125)
| ~ proposition(X127,X126)
| proposition(X125,X126) ),
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(c268,plain,
relation(skc12,skc12),
inference(resolution,[status(thm)],[c267,clause8]) ).
cnf(c270,plain,
abstraction(skc12,skc12),
inference(resolution,[status(thm)],[c268,clause9]) ).
cnf(c273,plain,
general(skc12,skc12),
inference(resolution,[status(thm)],[c270,clause12]) ).
cnf(c533,plain,
( skc12 != X900
| skc12 != X899
| general(X900,X899) ),
inference(resolution,[status(thm)],[c14,c273]) ).
cnf(c831,plain,
( skc12 != X903
| general(X903,skc12) ),
inference(resolution,[status(thm)],[c533,reflexivity]) ).
cnf(c89,plain,
abstraction(skc8,skc14),
inference(resolution,[status(thm)],[c86,clause9]) ).
cnf(c96,plain,
general(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause12]) ).
cnf(c532,plain,
( skc8 != X898
| skc14 != X897
| general(X898,X897) ),
inference(resolution,[status(thm)],[c14,c96]) ).
cnf(c829,plain,
( skc8 != X902
| general(X902,skc14) ),
inference(resolution,[status(thm)],[c532,reflexivity]) ).
cnf(c830,plain,
( skc12 != X901
| general(X901,X901) ),
inference(factor,[status(thm)],[c533]) ).
cnf(clause11,axiom,
( ~ abstraction(X24,X23)
| nonhuman(X24,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c294,plain,
nonhuman(skc12,skc14),
inference(resolution,[status(thm)],[c286,clause11]) ).
cnf(c13,axiom,
( X415 != X416
| X413 != X414
| ~ nonhuman(X415,X413)
| nonhuman(X416,X414) ),
theory(equality) ).
cnf(c528,plain,
( skc12 != X894
| skc14 != X893
| nonhuman(X894,X893) ),
inference(resolution,[status(thm)],[c13,c294]) ).
cnf(c826,plain,
( skc12 != X896
| nonhuman(X896,skc14) ),
inference(resolution,[status(thm)],[c528,reflexivity]) ).
cnf(c48,plain,
nonhuman(skc8,skc12),
inference(resolution,[status(thm)],[clause11,c45]) ).
cnf(c527,plain,
( skc8 != X892
| skc12 != X891
| nonhuman(X892,X891) ),
inference(resolution,[status(thm)],[c13,c48]) ).
cnf(c825,plain,
( skc8 != X895
| nonhuman(X895,skc12) ),
inference(resolution,[status(thm)],[c527,reflexivity]) ).
cnf(c95,plain,
nonhuman(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause11]) ).
cnf(c526,plain,
( skc8 != X888
| skc14 != X887
| nonhuman(X888,X887) ),
inference(resolution,[status(thm)],[c13,c95]) ).
cnf(c822,plain,
( skc8 != X890
| nonhuman(X890,skc14) ),
inference(resolution,[status(thm)],[c526,reflexivity]) ).
cnf(c276,plain,
nonhuman(skc12,skc12),
inference(resolution,[status(thm)],[c270,clause11]) ).
cnf(c525,plain,
( skc12 != X885
| skc12 != X884
| nonhuman(X885,X884) ),
inference(resolution,[status(thm)],[c13,c276]) ).
cnf(c820,plain,
( skc12 != X889
| nonhuman(X889,skc12) ),
inference(resolution,[status(thm)],[c525,reflexivity]) ).
cnf(c819,plain,
( skc12 != X886
| nonhuman(X886,X886) ),
inference(factor,[status(thm)],[c525]) ).
cnf(c307,plain,
nonhuman(skc12,skc11),
inference(resolution,[status(thm)],[c301,clause11]) ).
cnf(c524,plain,
( skc12 != X882
| skc11 != X881
| nonhuman(X882,X881) ),
inference(resolution,[status(thm)],[c13,c307]) ).
cnf(c817,plain,
( skc12 != X883
| nonhuman(X883,skc11) ),
inference(resolution,[status(thm)],[c524,reflexivity]) ).
cnf(c91,plain,
nonhuman(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause11]) ).
cnf(c523,plain,
( skc8 != X879
| skc11 != X878
| nonhuman(X879,X878) ),
inference(resolution,[status(thm)],[c13,c91]) ).
cnf(c815,plain,
( skc8 != X880
| nonhuman(X880,skc11) ),
inference(resolution,[status(thm)],[c523,reflexivity]) ).
cnf(c12,axiom,
( X408 != X409
| X406 != X407
| ~ abstraction(X408,X406)
| abstraction(X409,X407) ),
theory(equality) ).
cnf(c519,plain,
( skc12 != X876
| skc14 != X875
| abstraction(X876,X875) ),
inference(resolution,[status(thm)],[c12,c286]) ).
cnf(c813,plain,
( skc12 != X877
| abstraction(X877,skc14) ),
inference(resolution,[status(thm)],[c519,reflexivity]) ).
cnf(c518,plain,
( skc12 != X873
| skc11 != X872
| abstraction(X873,X872) ),
inference(resolution,[status(thm)],[c12,c301]) ).
cnf(c811,plain,
( skc12 != X874
| abstraction(X874,skc11) ),
inference(resolution,[status(thm)],[c518,reflexivity]) ).
cnf(c517,plain,
( skc8 != X870
| skc12 != X869
| abstraction(X870,X869) ),
inference(resolution,[status(thm)],[c12,c45]) ).
cnf(c809,plain,
( skc8 != X871
| abstraction(X871,skc12) ),
inference(resolution,[status(thm)],[c517,reflexivity]) ).
cnf(c516,plain,
( skc8 != X867
| skc11 != X866
| abstraction(X867,X866) ),
inference(resolution,[status(thm)],[c12,c88]) ).
cnf(c807,plain,
( skc8 != X868
| abstraction(X868,skc11) ),
inference(resolution,[status(thm)],[c516,reflexivity]) ).
cnf(c515,plain,
( skc8 != X864
| skc14 != X863
| abstraction(X864,X863) ),
inference(resolution,[status(thm)],[c12,c89]) ).
cnf(c805,plain,
( skc8 != X865
| abstraction(X865,skc14) ),
inference(resolution,[status(thm)],[c515,reflexivity]) ).
cnf(c514,plain,
( skc12 != X860
| skc12 != X859
| abstraction(X860,X859) ),
inference(resolution,[status(thm)],[c12,c270]) ).
cnf(c802,plain,
( skc12 != X862
| abstraction(X862,skc12) ),
inference(resolution,[status(thm)],[c514,reflexivity]) ).
cnf(c801,plain,
( skc12 != X861
| abstraction(X861,X861) ),
inference(factor,[status(thm)],[c514]) ).
cnf(c11,axiom,
( X401 != X402
| X399 != X400
| ~ relation(X401,X399)
| relation(X402,X400) ),
theory(equality) ).
cnf(c512,plain,
( skc12 != X856
| skc11 != X857
| relation(X856,X857) ),
inference(resolution,[status(thm)],[c11,c300]) ).
cnf(c799,plain,
( skc12 != X858
| relation(X858,skc11) ),
inference(resolution,[status(thm)],[c512,reflexivity]) ).
cnf(c511,plain,
( skc12 != X853
| skc14 != X854
| relation(X853,X854) ),
inference(resolution,[status(thm)],[c11,c285]) ).
cnf(c797,plain,
( skc12 != X855
| relation(X855,skc14) ),
inference(resolution,[status(thm)],[c511,reflexivity]) ).
cnf(c510,plain,
( skc8 != X850
| skc12 != X851
| relation(X850,X851) ),
inference(resolution,[status(thm)],[c11,c44]) ).
cnf(c795,plain,
( skc8 != X852
| relation(X852,skc12) ),
inference(resolution,[status(thm)],[c510,reflexivity]) ).
cnf(c509,plain,
( skc8 != X847
| skc14 != X848
| relation(X847,X848) ),
inference(resolution,[status(thm)],[c11,c86]) ).
cnf(c793,plain,
( skc8 != X849
| relation(X849,skc14) ),
inference(resolution,[status(thm)],[c509,reflexivity]) ).
cnf(c508,plain,
( skc8 != X842
| skc11 != X843
| relation(X842,X843) ),
inference(resolution,[status(thm)],[c11,c85]) ).
cnf(c789,plain,
( skc8 != X846
| relation(X846,skc11) ),
inference(resolution,[status(thm)],[c508,reflexivity]) ).
cnf(c507,plain,
( skc12 != X840
| skc12 != X841
| relation(X840,X841) ),
inference(resolution,[status(thm)],[c11,c268]) ).
cnf(c788,plain,
( skc12 != X845
| relation(X845,skc12) ),
inference(resolution,[status(thm)],[c507,reflexivity]) ).
cnf(c787,plain,
( skc12 != X844
| relation(X844,X844) ),
inference(factor,[status(thm)],[c507]) ).
cnf(c10,axiom,
( X393 != X394
| X391 != X392
| ~ proposition(X393,X391)
| proposition(X394,X392) ),
theory(equality) ).
cnf(c505,plain,
( skc8 != X836
| skc12 != X837
| proposition(X836,X837) ),
inference(resolution,[status(thm)],[c10,clause84]) ).
cnf(c784,plain,
( skc8 != X839
| proposition(X839,skc12) ),
inference(resolution,[status(thm)],[c505,reflexivity]) ).
cnf(c504,plain,
( skc12 != X832
| skc12 != X833
| proposition(X832,X833) ),
inference(resolution,[status(thm)],[c10,c267]) ).
cnf(c781,plain,
( skc12 != X838
| proposition(X838,skc12) ),
inference(resolution,[status(thm)],[c504,reflexivity]) ).
cnf(clause13,axiom,
( ~ abstraction(X28,X27)
| unisex(X28,X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c50,plain,
unisex(skc8,skc12),
inference(resolution,[status(thm)],[clause13,c45]) ).
cnf(clause43,axiom,
( ~ accessible_world(X112,X110)
| ~ unisex(X112,X111)
| unisex(X110,X111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c179,plain,
( ~ accessible_world(skc8,X177)
| unisex(X177,skc12) ),
inference(resolution,[status(thm)],[clause43,c50]) ).
cnf(c243,plain,
unisex(skc12,skc12),
inference(resolution,[status(thm)],[c179,clause83]) ).
cnf(c9,axiom,
( X388 != X389
| X386 != X387
| ~ unisex(X388,X386)
| unisex(X389,X387) ),
theory(equality) ).
cnf(c496,plain,
( skc12 != X830
| skc12 != X829
| unisex(X830,X829) ),
inference(resolution,[status(thm)],[c9,c243]) ).
cnf(c778,plain,
( skc12 != X835
| unisex(X835,skc12) ),
inference(resolution,[status(thm)],[c496,reflexivity]) ).
cnf(c780,plain,
( skc12 != X834
| proposition(X834,X834) ),
inference(factor,[status(thm)],[c504]) ).
cnf(c777,plain,
( skc12 != X831
| unisex(X831,X831) ),
inference(factor,[status(thm)],[c496]) ).
cnf(clause7,axiom,
( ~ eventuality(X16,X15)
| unisex(X16,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause2,axiom,
( ~ event(X6,X5)
| eventuality(X6,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause15,axiom,
( ~ state(X32,X31)
| event(X32,X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c52,plain,
event(skc8,skc9),
inference(resolution,[status(thm)],[clause15,clause82]) ).
cnf(clause37,axiom,
( ~ accessible_world(X86,X84)
| ~ event(X86,X85)
| event(X84,X85) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c118,plain,
( ~ accessible_world(skc8,X87)
| event(X87,skc9) ),
inference(resolution,[status(thm)],[clause37,c52]) ).
cnf(c120,plain,
event(skc12,skc9),
inference(resolution,[status(thm)],[c118,clause83]) ).
cnf(c122,plain,
eventuality(skc12,skc9),
inference(resolution,[status(thm)],[c120,clause2]) ).
cnf(c124,plain,
unisex(skc12,skc9),
inference(resolution,[status(thm)],[c122,clause7]) ).
cnf(c495,plain,
( skc12 != X827
| skc9 != X826
| unisex(X827,X826) ),
inference(resolution,[status(thm)],[c9,c124]) ).
cnf(c775,plain,
( skc12 != X828
| unisex(X828,skc9) ),
inference(resolution,[status(thm)],[c495,reflexivity]) ).
cnf(c93,plain,
unisex(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause13]) ).
cnf(c494,plain,
( skc8 != X824
| skc11 != X823
| unisex(X824,X823) ),
inference(resolution,[status(thm)],[c9,c93]) ).
cnf(c773,plain,
( skc8 != X825
| unisex(X825,skc11) ),
inference(resolution,[status(thm)],[c494,reflexivity]) ).
cnf(clause14,axiom,
( ~ state(X30,X29)
| eventuality(X30,X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c51,plain,
eventuality(skc8,skc9),
inference(resolution,[status(thm)],[clause14,clause82]) ).
cnf(c54,plain,
unisex(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause7]) ).
cnf(c493,plain,
( skc8 != X821
| skc9 != X820
| unisex(X821,X820) ),
inference(resolution,[status(thm)],[c9,c54]) ).
cnf(c771,plain,
( skc8 != X822
| unisex(X822,skc9) ),
inference(resolution,[status(thm)],[c493,reflexivity]) ).
cnf(c97,plain,
unisex(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause13]) ).
cnf(c492,plain,
( skc8 != X818
| skc14 != X817
| unisex(X818,X817) ),
inference(resolution,[status(thm)],[c9,c97]) ).
cnf(c769,plain,
( skc8 != X819
| unisex(X819,skc14) ),
inference(resolution,[status(thm)],[c492,reflexivity]) ).
cnf(clause1,axiom,
( ~ smoke(X4,X3)
| event(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause90,negated_conjecture,
( ~ man(skc12,X270)
| smoke(skc12,skf2(X269)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
cnf(c359,plain,
smoke(skc12,skf2(X271)),
inference(resolution,[status(thm)],[clause90,c331]) ).
cnf(c360,plain,
event(skc12,skf2(X272)),
inference(resolution,[status(thm)],[c359,clause1]) ).
cnf(c363,plain,
eventuality(skc12,skf2(X273)),
inference(resolution,[status(thm)],[c360,clause2]) ).
cnf(c365,plain,
unisex(skc12,skf2(X277)),
inference(resolution,[status(thm)],[c363,clause7]) ).
cnf(c491,plain,
( skc12 != X813
| skf2(X811) != X812
| unisex(X813,X812) ),
inference(resolution,[status(thm)],[c9,c365]) ).
cnf(c767,plain,
( skc12 != X815
| unisex(X815,skf2(X814)) ),
inference(resolution,[status(thm)],[c491,reflexivity]) ).
cnf(c183,plain,
( ~ accessible_world(skc8,X187)
| unisex(X187,skc11) ),
inference(resolution,[status(thm)],[clause43,c93]) ).
cnf(c254,plain,
unisex(skc12,skc11),
inference(resolution,[status(thm)],[c183,clause83]) ).
cnf(c490,plain,
( skc12 != X809
| skc11 != X808
| unisex(X809,X808) ),
inference(resolution,[status(thm)],[c9,c254]) ).
cnf(c765,plain,
( skc12 != X810
| unisex(X810,skc11) ),
inference(resolution,[status(thm)],[c490,reflexivity]) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
cnf(c119,plain,
( ~ accessible_world(skc8,X94)
| event(X94,skc13) ),
inference(resolution,[status(thm)],[clause37,clause76]) ).
cnf(c141,plain,
event(skc12,skc13),
inference(resolution,[status(thm)],[c119,clause83]) ).
cnf(c143,plain,
eventuality(skc12,skc13),
inference(resolution,[status(thm)],[c141,clause2]) ).
cnf(c145,plain,
unisex(skc12,skc13),
inference(resolution,[status(thm)],[c143,clause7]) ).
cnf(c489,plain,
( skc12 != X806
| skc13 != X805
| unisex(X806,X805) ),
inference(resolution,[status(thm)],[c9,c145]) ).
cnf(c763,plain,
( skc12 != X807
| unisex(X807,skc13) ),
inference(resolution,[status(thm)],[c489,reflexivity]) ).
cnf(c488,plain,
( skc8 != X803
| skc12 != X802
| unisex(X803,X802) ),
inference(resolution,[status(thm)],[c9,c50]) ).
cnf(c761,plain,
( skc8 != X804
| unisex(X804,skc12) ),
inference(resolution,[status(thm)],[c488,reflexivity]) ).
cnf(c181,plain,
( ~ accessible_world(skc8,X182)
| unisex(X182,skc14) ),
inference(resolution,[status(thm)],[clause43,c97]) ).
cnf(c248,plain,
unisex(skc12,skc14),
inference(resolution,[status(thm)],[c181,clause83]) ).
cnf(c487,plain,
( skc12 != X800
| skc14 != X799
| unisex(X800,X799) ),
inference(resolution,[status(thm)],[c9,c248]) ).
cnf(c759,plain,
( skc12 != X801
| unisex(X801,skc14) ),
inference(resolution,[status(thm)],[c487,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(c486,plain,
( skc8 != X797
| skc13 != X796
| unisex(X797,X796) ),
inference(resolution,[status(thm)],[c9,c43]) ).
cnf(c757,plain,
( skc8 != X798
| unisex(X798,skc13) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(clause6,axiom,
( ~ eventuality(X14,X13)
| nonexistent(X14,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c42,plain,
nonexistent(skc8,skc13),
inference(resolution,[status(thm)],[clause6,c38]) ).
cnf(c8,axiom,
( X381 != X382
| X379 != X380
| ~ nonexistent(X381,X379)
| nonexistent(X382,X380) ),
theory(equality) ).
cnf(c481,plain,
( skc8 != X794
| skc13 != X793
| nonexistent(X794,X793) ),
inference(resolution,[status(thm)],[c8,c42]) ).
cnf(c755,plain,
( skc8 != X795
| nonexistent(X795,skc13) ),
inference(resolution,[status(thm)],[c481,reflexivity]) ).
cnf(c56,plain,
nonexistent(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause6]) ).
cnf(c480,plain,
( skc8 != X791
| skc9 != X790
| nonexistent(X791,X790) ),
inference(resolution,[status(thm)],[c8,c56]) ).
cnf(c753,plain,
( skc8 != X792
| nonexistent(X792,skc9) ),
inference(resolution,[status(thm)],[c480,reflexivity]) ).
cnf(c367,plain,
nonexistent(skc12,skf2(X278)),
inference(resolution,[status(thm)],[c363,clause6]) ).
cnf(c478,plain,
( skc12 != X786
| skf2(X784) != X785
| nonexistent(X786,X785) ),
inference(resolution,[status(thm)],[c8,c367]) ).
cnf(c751,plain,
( skc12 != X787
| nonexistent(X787,skf2(X788)) ),
inference(resolution,[status(thm)],[c478,reflexivity]) ).
cnf(c147,plain,
nonexistent(skc12,skc13),
inference(resolution,[status(thm)],[c143,clause6]) ).
cnf(c479,plain,
( skc12 != X782
| skc13 != X781
| nonexistent(X782,X781) ),
inference(resolution,[status(thm)],[c8,c147]) ).
cnf(c749,plain,
( skc12 != X783
| nonexistent(X783,skc13) ),
inference(resolution,[status(thm)],[c479,reflexivity]) ).
cnf(c126,plain,
nonexistent(skc12,skc9),
inference(resolution,[status(thm)],[c122,clause6]) ).
cnf(c477,plain,
( skc12 != X779
| skc9 != X778
| nonexistent(X779,X778) ),
inference(resolution,[status(thm)],[c8,c126]) ).
cnf(c747,plain,
( skc12 != X780
| nonexistent(X780,skc9) ),
inference(resolution,[status(thm)],[c477,reflexivity]) ).
cnf(clause20,axiom,
( ~ entity(X42,X41)
| specific(X42,X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c69,plain,
specific(skc8,skc10),
inference(resolution,[status(thm)],[clause20,c63]) ).
cnf(c7,axiom,
( X374 != X375
| X372 != X373
| ~ specific(X374,X372)
| specific(X375,X373) ),
theory(equality) ).
cnf(c475,plain,
( skc8 != X775
| skc10 != X776
| specific(X775,X776) ),
inference(resolution,[status(thm)],[c7,c69]) ).
cnf(c745,plain,
( skc8 != X777
| specific(X777,skc10) ),
inference(resolution,[status(thm)],[c475,reflexivity]) ).
cnf(clause41,axiom,
( ~ accessible_world(X100,X98)
| ~ specific(X100,X99)
| specific(X98,X99) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c167,plain,
( ~ accessible_world(skc8,X160)
| specific(X160,skc10) ),
inference(resolution,[status(thm)],[clause41,c69]) ).
cnf(c231,plain,
specific(skc12,skc10),
inference(resolution,[status(thm)],[c167,clause83]) ).
cnf(c474,plain,
( skc12 != X772
| skc10 != X773
| specific(X772,X773) ),
inference(resolution,[status(thm)],[c7,c231]) ).
cnf(c743,plain,
( skc12 != X774
| specific(X774,skc10) ),
inference(resolution,[status(thm)],[c474,reflexivity]) ).
cnf(clause5,axiom,
( ~ eventuality(X12,X11)
| specific(X12,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c148,plain,
specific(skc12,skc13),
inference(resolution,[status(thm)],[c143,clause5]) ).
cnf(c473,plain,
( skc12 != X769
| skc13 != X770
| specific(X769,X770) ),
inference(resolution,[status(thm)],[c7,c148]) ).
cnf(c741,plain,
( skc12 != X771
| specific(X771,skc13) ),
inference(resolution,[status(thm)],[c473,reflexivity]) ).
cnf(c70,plain,
specific(skc8,skc15),
inference(resolution,[status(thm)],[clause20,c64]) ).
cnf(c165,plain,
( ~ accessible_world(skc8,X158)
| specific(X158,skc15) ),
inference(resolution,[status(thm)],[clause41,c70]) ).
cnf(c228,plain,
specific(skc12,skc15),
inference(resolution,[status(thm)],[c165,clause83]) ).
cnf(c472,plain,
( skc12 != X766
| skc15 != X767
| specific(X766,X767) ),
inference(resolution,[status(thm)],[c7,c228]) ).
cnf(c739,plain,
( skc12 != X768
| specific(X768,skc15) ),
inference(resolution,[status(thm)],[c472,reflexivity]) ).
cnf(c471,plain,
( skc8 != X763
| skc15 != X764
| specific(X763,X764) ),
inference(resolution,[status(thm)],[c7,c70]) ).
cnf(c737,plain,
( skc8 != X765
| specific(X765,skc15) ),
inference(resolution,[status(thm)],[c471,reflexivity]) ).
cnf(c55,plain,
specific(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause5]) ).
cnf(c470,plain,
( skc8 != X760
| skc9 != X761
| specific(X760,X761) ),
inference(resolution,[status(thm)],[c7,c55]) ).
cnf(c735,plain,
( skc8 != X762
| specific(X762,skc9) ),
inference(resolution,[status(thm)],[c470,reflexivity]) ).
cnf(c41,plain,
specific(skc8,skc13),
inference(resolution,[status(thm)],[clause5,c38]) ).
cnf(c469,plain,
( skc8 != X757
| skc13 != X758
| specific(X757,X758) ),
inference(resolution,[status(thm)],[c7,c41]) ).
cnf(c733,plain,
( skc8 != X759
| specific(X759,skc13) ),
inference(resolution,[status(thm)],[c469,reflexivity]) ).
cnf(c368,plain,
specific(skc12,skf2(X279)),
inference(resolution,[status(thm)],[c363,clause5]) ).
cnf(c467,plain,
( skc12 != X752
| skf2(X753) != X751
| specific(X752,X751) ),
inference(resolution,[status(thm)],[c7,c368]) ).
cnf(c731,plain,
( skc12 != X755
| specific(X755,skf2(X754)) ),
inference(resolution,[status(thm)],[c467,reflexivity]) ).
cnf(c125,plain,
specific(skc12,skc9),
inference(resolution,[status(thm)],[c122,clause5]) ).
cnf(c468,plain,
( skc12 != X748
| skc9 != X749
| specific(X748,X749) ),
inference(resolution,[status(thm)],[c7,c125]) ).
cnf(c729,plain,
( skc12 != X750
| specific(X750,skc9) ),
inference(resolution,[status(thm)],[c468,reflexivity]) ).
cnf(clause4,axiom,
( ~ thing(X10,X9)
| singleton(X10,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause3,axiom,
( ~ eventuality(X8,X7)
| thing(X8,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c364,plain,
thing(skc12,skf2(X274)),
inference(resolution,[status(thm)],[c363,clause3]) ).
cnf(c370,plain,
singleton(skc12,skf2(X280)),
inference(resolution,[status(thm)],[c364,clause4]) ).
cnf(c6,axiom,
( X366 != X367
| X364 != X365
| ~ singleton(X366,X364)
| singleton(X367,X365) ),
theory(equality) ).
cnf(c464,plain,
( skc12 != X744
| skf2(X743) != X742
| singleton(X744,X742) ),
inference(resolution,[status(thm)],[c6,c370]) ).
cnf(c727,plain,
( skc12 != X745
| singleton(X745,skf2(X746)) ),
inference(resolution,[status(thm)],[c464,reflexivity]) ).
cnf(clause19,axiom,
( ~ entity(X40,X39)
| thing(X40,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c65,plain,
thing(skc8,skc10),
inference(resolution,[status(thm)],[clause19,c63]) ).
cnf(c67,plain,
singleton(skc8,skc10),
inference(resolution,[status(thm)],[c65,clause4]) ).
cnf(c463,plain,
( skc8 != X740
| skc10 != X739
| singleton(X740,X739) ),
inference(resolution,[status(thm)],[c6,c67]) ).
cnf(c725,plain,
( skc8 != X741
| singleton(X741,skc10) ),
inference(resolution,[status(thm)],[c463,reflexivity]) ).
cnf(c5,axiom,
( X359 != X360
| X357 != X358
| ~ thing(X359,X357)
| thing(X360,X358) ),
theory(equality) ).
cnf(c436,plain,
( skc12 != X735
| skf2(X734) != X733
| thing(X735,X733) ),
inference(resolution,[status(thm)],[c5,c364]) ).
cnf(c723,plain,
( skc12 != X736
| thing(X736,skf2(X737)) ),
inference(resolution,[status(thm)],[c436,reflexivity]) ).
cnf(clause10,axiom,
( ~ abstraction(X22,X21)
| thing(X22,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c46,plain,
thing(skc8,skc12),
inference(resolution,[status(thm)],[clause10,c45]) ).
cnf(c47,plain,
singleton(skc8,skc12),
inference(resolution,[status(thm)],[c46,clause4]) ).
cnf(c462,plain,
( skc8 != X731
| skc12 != X730
| singleton(X731,X730) ),
inference(resolution,[status(thm)],[c6,c47]) ).
cnf(c721,plain,
( skc8 != X732
| singleton(X732,skc12) ),
inference(resolution,[status(thm)],[c462,reflexivity]) ).
cnf(c4,axiom,
( X352 != X353
| X350 != X351
| ~ eventuality(X352,X350)
| eventuality(X353,X351) ),
theory(equality) ).
cnf(c430,plain,
( skc12 != X724
| skf2(X725) != X726
| eventuality(X724,X726) ),
inference(resolution,[status(thm)],[c4,c363]) ).
cnf(c719,plain,
( skc12 != X728
| eventuality(X728,skf2(X727)) ),
inference(resolution,[status(thm)],[c430,reflexivity]) ).
cnf(c144,plain,
thing(skc12,skc13),
inference(resolution,[status(thm)],[c143,clause3]) ).
cnf(c150,plain,
singleton(skc12,skc13),
inference(resolution,[status(thm)],[c144,clause4]) ).
cnf(c461,plain,
( skc12 != X722
| skc13 != X721
| singleton(X722,X721) ),
inference(resolution,[status(thm)],[c6,c150]) ).
cnf(c717,plain,
( skc12 != X723
| singleton(X723,skc13) ),
inference(resolution,[status(thm)],[c461,reflexivity]) ).
cnf(c3,axiom,
( X345 != X346
| X343 != X344
| ~ event(X345,X343)
| event(X346,X344) ),
theory(equality) ).
cnf(c420,plain,
( skc12 != X717
| skf2(X716) != X715
| event(X717,X715) ),
inference(resolution,[status(thm)],[c3,c360]) ).
cnf(c715,plain,
( skc12 != X719
| event(X719,skf2(X718)) ),
inference(resolution,[status(thm)],[c420,reflexivity]) ).
cnf(c66,plain,
thing(skc8,skc15),
inference(resolution,[status(thm)],[clause19,c64]) ).
cnf(c68,plain,
singleton(skc8,skc15),
inference(resolution,[status(thm)],[c66,clause4]) ).
cnf(c460,plain,
( skc8 != X713
| skc15 != X712
| singleton(X713,X712) ),
inference(resolution,[status(thm)],[c6,c68]) ).
cnf(c713,plain,
( skc8 != X714
| singleton(X714,skc15) ),
inference(resolution,[status(thm)],[c460,reflexivity]) ).
cnf(c2,axiom,
( X338 != X339
| X336 != X337
| ~ smoke(X338,X336)
| smoke(X339,X337) ),
theory(equality) ).
cnf(c416,plain,
( skc12 != X707
| skf2(X708) != X706
| smoke(X707,X706) ),
inference(resolution,[status(thm)],[c2,c359]) ).
cnf(c711,plain,
( skc12 != X709
| smoke(X709,skf2(X710)) ),
inference(resolution,[status(thm)],[c416,reflexivity]) ).
cnf(c94,plain,
thing(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause10]) ).
cnf(clause39,axiom,
( ~ accessible_world(X93,X91)
| ~ thing(X93,X92)
| thing(X91,X92) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c135,plain,
( ~ accessible_world(skc8,X113)
| thing(X113,skc14) ),
inference(resolution,[status(thm)],[clause39,c94]) ).
cnf(c185,plain,
thing(skc12,skc14),
inference(resolution,[status(thm)],[c135,clause83]) ).
cnf(c187,plain,
singleton(skc12,skc14),
inference(resolution,[status(thm)],[c185,clause4]) ).
cnf(c459,plain,
( skc12 != X704
| skc14 != X703
| singleton(X704,X703) ),
inference(resolution,[status(thm)],[c6,c187]) ).
cnf(c709,plain,
( skc12 != X705
| singleton(X705,skc14) ),
inference(resolution,[status(thm)],[c459,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 != X701
| skc13 != X700
| singleton(X701,X700) ),
inference(resolution,[status(thm)],[c6,c40]) ).
cnf(c707,plain,
( skc8 != X702
| singleton(X702,skc13) ),
inference(resolution,[status(thm)],[c458,reflexivity]) ).
cnf(c90,plain,
thing(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause10]) ).
cnf(c140,plain,
( ~ accessible_world(skc8,X124)
| thing(X124,skc11) ),
inference(resolution,[status(thm)],[clause39,c90]) ).
cnf(c201,plain,
thing(skc12,skc11),
inference(resolution,[status(thm)],[c140,clause83]) ).
cnf(c203,plain,
singleton(skc12,skc11),
inference(resolution,[status(thm)],[c201,clause4]) ).
cnf(c457,plain,
( skc12 != X687
| skc11 != X686
| singleton(X687,X686) ),
inference(resolution,[status(thm)],[c6,c203]) ).
cnf(c703,plain,
( skc12 != X688
| singleton(X688,skc11) ),
inference(resolution,[status(thm)],[c457,reflexivity]) ).
cnf(c134,plain,
( ~ accessible_world(skc8,X109)
| thing(X109,skc15) ),
inference(resolution,[status(thm)],[clause39,c66]) ).
cnf(c174,plain,
thing(skc12,skc15),
inference(resolution,[status(thm)],[c134,clause83]) ).
cnf(c176,plain,
singleton(skc12,skc15),
inference(resolution,[status(thm)],[c174,clause4]) ).
cnf(c456,plain,
( skc12 != X674
| skc15 != X673
| singleton(X674,X673) ),
inference(resolution,[status(thm)],[c6,c176]) ).
cnf(c697,plain,
( skc12 != X685
| singleton(X685,skc15) ),
inference(resolution,[status(thm)],[c456,reflexivity]) ).
cnf(c53,plain,
thing(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause3]) ).
cnf(c58,plain,
singleton(skc8,skc9),
inference(resolution,[status(thm)],[c53,clause4]) ).
cnf(c455,plain,
( skc8 != X671
| skc9 != X670
| singleton(X671,X670) ),
inference(resolution,[status(thm)],[c6,c58]) ).
cnf(c695,plain,
( skc8 != X672
| singleton(X672,skc9) ),
inference(resolution,[status(thm)],[c455,reflexivity]) ).
cnf(c351,plain,
( ~ proposition(skc8,X667)
| ~ proposition(skc8,X669)
| ~ theme(skc8,skc13,X667)
| ~ think_believe_consider(skc8,skc13)
| ~ think_believe_consider(skc8,X668)
| ~ theme(skc8,X668,X669)
| ~ agent(skc8,X668,skc15)
| X667 = X669 ),
inference(resolution,[status(thm)],[clause71,clause86]) ).
cnf(c123,plain,
thing(skc12,skc9),
inference(resolution,[status(thm)],[c122,clause3]) ).
cnf(c127,plain,
singleton(skc12,skc9),
inference(resolution,[status(thm)],[c123,clause4]) ).
cnf(c454,plain,
( skc12 != X665
| skc9 != X664
| singleton(X665,X664) ),
inference(resolution,[status(thm)],[c6,c127]) ).
cnf(c692,plain,
( skc12 != X666
| singleton(X666,skc9) ),
inference(resolution,[status(thm)],[c454,reflexivity]) ).
cnf(c100,plain,
singleton(skc8,skc14),
inference(resolution,[status(thm)],[c94,clause4]) ).
cnf(c453,plain,
( skc8 != X662
| skc14 != X661
| singleton(X662,X661) ),
inference(resolution,[status(thm)],[c6,c100]) ).
cnf(c690,plain,
( skc8 != X663
| singleton(X663,skc14) ),
inference(resolution,[status(thm)],[c453,reflexivity]) ).
cnf(c138,plain,
( ~ accessible_world(skc8,X119)
| thing(X119,skc10) ),
inference(resolution,[status(thm)],[clause39,c65]) ).
cnf(c195,plain,
thing(skc12,skc10),
inference(resolution,[status(thm)],[c138,clause83]) ).
cnf(c197,plain,
singleton(skc12,skc10),
inference(resolution,[status(thm)],[c195,clause4]) ).
cnf(c452,plain,
( skc12 != X654
| skc10 != X653
| singleton(X654,X653) ),
inference(resolution,[status(thm)],[c6,c197]) ).
cnf(c684,plain,
( skc12 != X655
| singleton(X655,skc10) ),
inference(resolution,[status(thm)],[c452,reflexivity]) ).
cnf(c137,plain,
( ~ accessible_world(skc8,X118)
| thing(X118,skc12) ),
inference(resolution,[status(thm)],[clause39,c46]) ).
cnf(c191,plain,
thing(skc12,skc12),
inference(resolution,[status(thm)],[c137,clause83]) ).
cnf(c193,plain,
singleton(skc12,skc12),
inference(resolution,[status(thm)],[c191,clause4]) ).
cnf(c451,plain,
( skc12 != X649
| skc12 != X648
| singleton(X649,X648) ),
inference(resolution,[status(thm)],[c6,c193]) ).
cnf(c680,plain,
( skc12 != X652
| singleton(X652,skc12) ),
inference(resolution,[status(thm)],[c451,reflexivity]) ).
cnf(c338,plain,
( ~ forename(skc8,skc11)
| ~ of(skc8,X651,skc10)
| ~ forename(skc8,X651)
| ~ entity(skc8,skc10)
| X651 = skc11 ),
inference(resolution,[status(thm)],[clause70,clause88]) ).
cnf(c679,plain,
( skc12 != X650
| singleton(X650,X650) ),
inference(factor,[status(thm)],[c451]) ).
cnf(c99,plain,
singleton(skc8,skc11),
inference(resolution,[status(thm)],[c90,clause4]) ).
cnf(c450,plain,
( skc8 != X645
| skc11 != X644
| singleton(X645,X644) ),
inference(resolution,[status(thm)],[c6,c99]) ).
cnf(c676,plain,
( skc8 != X647
| singleton(X647,skc11) ),
inference(resolution,[status(thm)],[c450,reflexivity]) ).
cnf(c337,plain,
( ~ forename(skc8,skc14)
| ~ of(skc8,X646,skc15)
| ~ forename(skc8,X646)
| ~ entity(skc8,skc15)
| X646 = skc14 ),
inference(resolution,[status(thm)],[clause70,clause85]) ).
cnf(c447,plain,
( skc8 != X642
| skc11 != X641
| thing(X642,X641) ),
inference(resolution,[status(thm)],[c5,c90]) ).
cnf(c674,plain,
( skc8 != X643
| thing(X643,skc11) ),
inference(resolution,[status(thm)],[c447,reflexivity]) ).
cnf(c446,plain,
( skc8 != X636
| skc9 != X635
| thing(X636,X635) ),
inference(resolution,[status(thm)],[c5,c53]) ).
cnf(c672,plain,
( skc8 != X637
| thing(X637,skc9) ),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c445,plain,
( skc8 != X633
| skc10 != X632
| thing(X633,X632) ),
inference(resolution,[status(thm)],[c5,c65]) ).
cnf(c670,plain,
( skc8 != X634
| thing(X634,skc10) ),
inference(resolution,[status(thm)],[c445,reflexivity]) ).
cnf(c444,plain,
( skc12 != X624
| skc11 != X623
| thing(X624,X623) ),
inference(resolution,[status(thm)],[c5,c201]) ).
cnf(c664,plain,
( skc12 != X625
| thing(X625,skc11) ),
inference(resolution,[status(thm)],[c444,reflexivity]) ).
cnf(c443,plain,
( skc12 != X615
| skc10 != X614
| thing(X615,X614) ),
inference(resolution,[status(thm)],[c5,c195]) ).
cnf(c660,plain,
( skc12 != X622
| thing(X622,skc10) ),
inference(resolution,[status(thm)],[c443,reflexivity]) ).
cnf(c442,plain,
( skc12 != X612
| skc14 != X611
| thing(X612,X611) ),
inference(resolution,[status(thm)],[c5,c185]) ).
cnf(c658,plain,
( skc12 != X613
| thing(X613,skc14) ),
inference(resolution,[status(thm)],[c442,reflexivity]) ).
cnf(c441,plain,
( skc12 != X602
| skc12 != X601
| thing(X602,X601) ),
inference(resolution,[status(thm)],[c5,c191]) ).
cnf(c651,plain,
( skc12 != X604
| thing(X604,skc12) ),
inference(resolution,[status(thm)],[c441,reflexivity]) ).
cnf(c650,plain,
( skc12 != X603
| thing(X603,X603) ),
inference(factor,[status(thm)],[c441]) ).
cnf(c440,plain,
( skc8 != X595
| skc12 != X594
| thing(X595,X594) ),
inference(resolution,[status(thm)],[c5,c46]) ).
cnf(c646,plain,
( skc8 != X596
| thing(X596,skc12) ),
inference(resolution,[status(thm)],[c440,reflexivity]) ).
cnf(c439,plain,
( skc8 != X592
| skc13 != X591
| thing(X592,X591) ),
inference(resolution,[status(thm)],[c5,c39]) ).
cnf(c644,plain,
( skc8 != X593
| thing(X593,skc13) ),
inference(resolution,[status(thm)],[c439,reflexivity]) ).
cnf(c438,plain,
( skc12 != X585
| skc15 != X584
| thing(X585,X584) ),
inference(resolution,[status(thm)],[c5,c174]) ).
cnf(c639,plain,
( skc12 != X586
| thing(X586,skc15) ),
inference(resolution,[status(thm)],[c438,reflexivity]) ).
cnf(c437,plain,
( skc8 != X578
| skc14 != X577
| thing(X578,X577) ),
inference(resolution,[status(thm)],[c5,c94]) ).
cnf(c636,plain,
( skc8 != X583
| thing(X583,skc14) ),
inference(resolution,[status(thm)],[c437,reflexivity]) ).
cnf(c435,plain,
( skc8 != X575
| skc15 != X574
| thing(X575,X574) ),
inference(resolution,[status(thm)],[c5,c66]) ).
cnf(c634,plain,
( skc8 != X576
| thing(X576,skc15) ),
inference(resolution,[status(thm)],[c435,reflexivity]) ).
cnf(c434,plain,
( skc12 != X564
| skc13 != X563
| thing(X564,X563) ),
inference(resolution,[status(thm)],[c5,c144]) ).
cnf(c630,plain,
( skc12 != X565
| thing(X565,skc13) ),
inference(resolution,[status(thm)],[c434,reflexivity]) ).
cnf(c433,plain,
( skc12 != X561
| skc9 != X560
| thing(X561,X560) ),
inference(resolution,[status(thm)],[c5,c123]) ).
cnf(c628,plain,
( skc12 != X562
| thing(X562,skc9) ),
inference(resolution,[status(thm)],[c433,reflexivity]) ).
cnf(c429,plain,
( skc12 != X553
| skc13 != X554
| eventuality(X553,X554) ),
inference(resolution,[status(thm)],[c4,c143]) ).
cnf(c624,plain,
( skc12 != X555
| eventuality(X555,skc13) ),
inference(resolution,[status(thm)],[c429,reflexivity]) ).
cnf(c428,plain,
( skc8 != X546
| skc9 != X547
| eventuality(X546,X547) ),
inference(resolution,[status(thm)],[c4,c51]) ).
cnf(c620,plain,
( skc8 != X552
| eventuality(X552,skc9) ),
inference(resolution,[status(thm)],[c428,reflexivity]) ).
cnf(c427,plain,
( skc8 != X543
| skc13 != X544
| eventuality(X543,X544) ),
inference(resolution,[status(thm)],[c4,c38]) ).
cnf(c618,plain,
( skc8 != X545
| eventuality(X545,skc13) ),
inference(resolution,[status(thm)],[c427,reflexivity]) ).
cnf(c426,plain,
( skc12 != X536
| skc9 != X537
| eventuality(X536,X537) ),
inference(resolution,[status(thm)],[c4,c122]) ).
cnf(c612,plain,
( skc12 != X538
| eventuality(X538,skc9) ),
inference(resolution,[status(thm)],[c426,reflexivity]) ).
cnf(c423,plain,
( skc12 != X534
| skc9 != X533
| event(X534,X533) ),
inference(resolution,[status(thm)],[c3,c120]) ).
cnf(c610,plain,
( skc12 != X535
| event(X535,skc9) ),
inference(resolution,[status(thm)],[c423,reflexivity]) ).
cnf(c422,plain,
( skc8 != X527
| skc13 != X526
| event(X527,X526) ),
inference(resolution,[status(thm)],[c3,clause76]) ).
cnf(c604,plain,
( skc8 != X528
| event(X528,skc13) ),
inference(resolution,[status(thm)],[c422,reflexivity]) ).
cnf(c421,plain,
( skc12 != X520
| skc13 != X519
| event(X520,X519) ),
inference(resolution,[status(thm)],[c3,c141]) ).
cnf(c598,plain,
( skc12 != X525
| event(X525,skc13) ),
inference(resolution,[status(thm)],[c421,reflexivity]) ).
cnf(c419,plain,
( skc8 != X517
| skc9 != X516
| event(X517,X516) ),
inference(resolution,[status(thm)],[c3,c52]) ).
cnf(c596,plain,
( skc8 != X518
| event(X518,skc9) ),
inference(resolution,[status(thm)],[c419,reflexivity]) ).
cnf(c581,plain,
( ~ accessible_world(skc12,X510)
| of(X510,skc11,skc10) ),
inference(resolution,[status(thm)],[c580,clause68]) ).
cnf(c578,plain,
( ~ accessible_world(skc12,X509)
| of(X509,skc14,skc15) ),
inference(resolution,[status(thm)],[c577,clause68]) ).
cnf(c572,plain,
( ~ accessible_world(skc12,X508)
| theme(X508,skc13,skc12) ),
inference(resolution,[status(thm)],[c571,clause67]) ).
cnf(c569,plain,
( ~ accessible_world(skc12,X503)
| agent(X503,skc13,skc15) ),
inference(resolution,[status(thm)],[c568,clause66]) ).
cnf(c378,plain,
( ~ accessible_world(skc12,X493)
| present(X493,skf2(X494)) ),
inference(resolution,[status(thm)],[c371,clause44]) ).
cnf(clause40,axiom,
( ~ accessible_world(X97,X95)
| ~ singleton(X97,X96)
| singleton(X95,X96) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c377,plain,
( ~ accessible_world(skc12,X487)
| singleton(X487,skf2(X488)) ),
inference(resolution,[status(thm)],[c370,clause40]) ).
cnf(c375,plain,
( ~ accessible_world(skc12,X485)
| specific(X485,skf2(X486)) ),
inference(resolution,[status(thm)],[c368,clause41]) ).
cnf(clause42,axiom,
( ~ accessible_world(X107,X105)
| ~ nonexistent(X107,X106)
| nonexistent(X105,X106) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c374,plain,
( ~ accessible_world(skc12,X483)
| nonexistent(X483,skf2(X484)) ),
inference(resolution,[status(thm)],[c367,clause42]) ).
cnf(c373,plain,
( ~ accessible_world(skc12,X482)
| unisex(X482,skf2(X481)) ),
inference(resolution,[status(thm)],[c365,clause43]) ).
cnf(c369,plain,
( ~ accessible_world(skc12,X479)
| thing(X479,skf2(X480)) ),
inference(resolution,[status(thm)],[c364,clause39]) ).
cnf(clause38,axiom,
( ~ accessible_world(X90,X88)
| ~ eventuality(X90,X89)
| eventuality(X88,X89) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c366,plain,
( ~ accessible_world(skc12,X474)
| eventuality(X474,skf2(X473)) ),
inference(resolution,[status(thm)],[c363,clause38]) ).
cnf(c362,plain,
( ~ accessible_world(skc12,X471)
| event(X471,skf2(X472)) ),
inference(resolution,[status(thm)],[c360,clause37]) ).
cnf(clause36,axiom,
( ~ accessible_world(X79,X77)
| ~ smoke(X79,X78)
| smoke(X77,X78) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c361,plain,
( ~ accessible_world(skc12,X470)
| smoke(X470,skf2(X469)) ),
inference(resolution,[status(thm)],[c359,clause36]) ).
cnf(c531,plain,
( ~ accessible_world(skc12,X468)
| jules_forename(X468,skc11) ),
inference(resolution,[status(thm)],[c529,clause65]) ).
cnf(c522,plain,
( ~ accessible_world(skc12,X467)
| vincent_forename(X467,skc14) ),
inference(resolution,[status(thm)],[c520,clause64]) ).
cnf(clause63,axiom,
( ~ accessible_world(X222,X220)
| ~ relname(X222,X221)
| relname(X220,X221) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
cnf(c503,plain,
( ~ accessible_world(skc12,X462)
| relname(X462,skc11) ),
inference(resolution,[status(thm)],[c501,clause63]) ).
cnf(c500,plain,
( ~ accessible_world(skc12,X461)
| forename(X461,skc11) ),
inference(resolution,[status(thm)],[c499,clause62]) ).
cnf(c498,plain,
( ~ accessible_world(skc12,X460)
| relname(X460,skc14) ),
inference(resolution,[status(thm)],[c485,clause63]) ).
cnf(c484,plain,
( ~ accessible_world(skc12,X459)
| forename(X459,skc14) ),
inference(resolution,[status(thm)],[c483,clause62]) ).
cnf(clause56,axiom,
( ~ accessible_world(X186,X184)
| ~ existent(X186,X185)
| existent(X184,X185) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
cnf(c404,plain,
( ~ accessible_world(skc12,X458)
| existent(X458,skc15) ),
inference(resolution,[status(thm)],[c400,clause56]) ).
cnf(clause58,axiom,
( ~ accessible_world(X198,X196)
| ~ living(X198,X197)
| living(X196,X197) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
cnf(c402,plain,
( ~ accessible_world(skc12,X453)
| living(X453,skc15) ),
inference(resolution,[status(thm)],[c393,clause58]) ).
cnf(clause55,axiom,
( ~ accessible_world(X180,X178)
| ~ entity(X180,X179)
| entity(X178,X179) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
cnf(c399,plain,
( ~ accessible_world(skc12,X452)
| entity(X452,skc15) ),
inference(resolution,[status(thm)],[c392,clause55]) ).
cnf(clause57,axiom,
( ~ accessible_world(X191,X189)
| ~ impartial(X191,X190)
| impartial(X189,X190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
cnf(c396,plain,
( ~ accessible_world(skc12,X451)
| impartial(X451,skc15) ),
inference(resolution,[status(thm)],[c390,clause57]) ).
cnf(clause60,axiom,
( ~ accessible_world(X210,X208)
| ~ animate(X210,X209)
| animate(X208,X209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
cnf(c395,plain,
( ~ accessible_world(skc12,X450)
| animate(X450,skc15) ),
inference(resolution,[status(thm)],[c386,clause60]) ).
cnf(clause59,axiom,
( ~ accessible_world(X205,X203)
| ~ human(X205,X204)
| human(X203,X204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
cnf(c394,plain,
( ~ accessible_world(skc12,X449)
| human(X449,skc15) ),
inference(resolution,[status(thm)],[c385,clause59]) ).
cnf(clause54,axiom,
( ~ accessible_world(X175,X173)
| ~ organism(X175,X174)
| organism(X173,X174) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
cnf(c391,plain,
( ~ accessible_world(skc12,X444)
| organism(X444,skc15) ),
inference(resolution,[status(thm)],[c384,clause54]) ).
cnf(clause61,axiom,
( ~ accessible_world(X213,X211)
| ~ male(X213,X212)
| male(X211,X212) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
cnf(c389,plain,
( ~ accessible_world(skc12,X443)
| male(X443,skc15) ),
inference(resolution,[status(thm)],[c381,clause61]) ).
cnf(clause53,axiom,
( ~ accessible_world(X168,X166)
| ~ human_person(X168,X167)
| human_person(X166,X167) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(c383,plain,
( ~ accessible_world(skc12,X442)
| human_person(X442,skc15) ),
inference(resolution,[status(thm)],[c380,clause53]) ).
cnf(c382,plain,
( ~ accessible_world(skc12,X437)
| man(X437,skc15) ),
inference(resolution,[status(thm)],[c379,clause52]) ).
cnf(c358,plain,
( ~ accessible_world(skc12,X436)
| existent(X436,skc10) ),
inference(resolution,[status(thm)],[c354,clause56]) ).
cnf(c356,plain,
( ~ accessible_world(skc12,X435)
| living(X435,skc10) ),
inference(resolution,[status(thm)],[c346,clause58]) ).
cnf(c353,plain,
( ~ accessible_world(skc12,X434)
| entity(X434,skc10) ),
inference(resolution,[status(thm)],[c345,clause55]) ).
cnf(c349,plain,
( ~ accessible_world(skc12,X433)
| impartial(X433,skc10) ),
inference(resolution,[status(thm)],[c343,clause57]) ).
cnf(c348,plain,
( ~ accessible_world(skc12,X428)
| animate(X428,skc10) ),
inference(resolution,[status(thm)],[c342,clause60]) ).
cnf(c347,plain,
( ~ accessible_world(skc12,X427)
| human(X427,skc10) ),
inference(resolution,[status(thm)],[c341,clause59]) ).
cnf(c344,plain,
( ~ accessible_world(skc12,X426)
| organism(X426,skc10) ),
inference(resolution,[status(thm)],[c340,clause54]) ).
cnf(c339,plain,
( ~ accessible_world(skc12,X425)
| human_person(X425,skc10) ),
inference(resolution,[status(thm)],[c333,clause53]) ).
cnf(c335,plain,
( ~ accessible_world(skc12,X424)
| male(X424,skc10) ),
inference(resolution,[status(thm)],[c332,clause61]) ).
cnf(c334,plain,
( ~ accessible_world(skc12,X419)
| man(X419,skc10) ),
inference(resolution,[status(thm)],[c331,clause52]) ).
cnf(c328,plain,
( ~ accessible_world(skc12,X418)
| state(X418,skc9) ),
inference(resolution,[status(thm)],[c326,clause51]) ).
cnf(clause49,axiom,
( ~ accessible_world(X145,X143)
| ~ nonhuman(X145,X144)
| nonhuman(X143,X144) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c311,plain,
( ~ accessible_world(skc12,X412)
| nonhuman(X412,skc11) ),
inference(resolution,[status(thm)],[c307,clause49]) ).
cnf(clause50,axiom,
( ~ accessible_world(X151,X149)
| ~ general(X151,X150)
| general(X149,X150) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c309,plain,
( ~ accessible_world(skc12,X411)
| general(X411,skc11) ),
inference(resolution,[status(thm)],[c304,clause50]) ).
cnf(clause48,axiom,
( ~ accessible_world(X140,X138)
| ~ abstraction(X140,X139)
| abstraction(X138,X139) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(c306,plain,
( ~ accessible_world(skc12,X405)
| abstraction(X405,skc11) ),
inference(resolution,[status(thm)],[c301,clause48]) ).
cnf(c302,plain,
( ~ accessible_world(skc12,X404)
| relation(X404,skc11) ),
inference(resolution,[status(thm)],[c300,clause47]) ).
cnf(c299,plain,
( ~ accessible_world(skc8,X403)
| relname(X403,skc14) ),
inference(resolution,[status(thm)],[clause63,c83]) ).
cnf(c298,plain,
( ~ accessible_world(skc8,X398)
| relname(X398,skc11) ),
inference(resolution,[status(thm)],[clause63,c84]) ).
cnf(c297,plain,
( ~ accessible_world(skc12,X397)
| nonhuman(X397,skc14) ),
inference(resolution,[status(thm)],[c294,clause49]) ).
cnf(c295,plain,
( ~ accessible_world(skc12,X396)
| general(X396,skc14) ),
inference(resolution,[status(thm)],[c291,clause50]) ).
cnf(c293,plain,
( ~ accessible_world(skc12,X395)
| abstraction(X395,skc14) ),
inference(resolution,[status(thm)],[c286,clause48]) ).
cnf(c287,plain,
( ~ accessible_world(skc12,X384)
| relation(X384,skc14) ),
inference(resolution,[status(thm)],[c285,clause47]) ).
cnf(c283,plain,
( ~ accessible_world(skc8,X383)
| male(X383,skc10) ),
inference(resolution,[status(thm)],[clause61,c81]) ).
cnf(c282,plain,
( ~ accessible_world(skc8,X378)
| male(X378,skc15) ),
inference(resolution,[status(thm)],[clause61,c82]) ).
cnf(c281,plain,
( ~ accessible_world(skc12,X377)
| nonhuman(X377,skc12) ),
inference(resolution,[status(thm)],[c276,clause49]) ).
cnf(c279,plain,
( ~ accessible_world(skc12,X376)
| general(X376,skc12) ),
inference(resolution,[status(thm)],[c273,clause50]) ).
cnf(c278,plain,
( ~ accessible_world(skc8,X371)
| animate(X371,skc15) ),
inference(resolution,[status(thm)],[clause60,c80]) ).
cnf(c277,plain,
( ~ accessible_world(skc8,X370)
| animate(X370,skc10) ),
inference(resolution,[status(thm)],[clause60,c79]) ).
cnf(c275,plain,
( ~ accessible_world(skc12,X369)
| abstraction(X369,skc12) ),
inference(resolution,[status(thm)],[c270,clause48]) ).
cnf(c271,plain,
( ~ accessible_world(skc12,X368)
| relation(X368,skc12) ),
inference(resolution,[status(thm)],[c268,clause47]) ).
cnf(c269,plain,
( ~ accessible_world(skc12,X363)
| proposition(X363,skc12) ),
inference(resolution,[status(thm)],[c267,clause46]) ).
cnf(c266,plain,
( ~ accessible_world(skc8,X362)
| human(X362,skc10) ),
inference(resolution,[status(thm)],[clause59,c77]) ).
cnf(c265,plain,
( ~ accessible_world(skc8,X361)
| human(X361,skc15) ),
inference(resolution,[status(thm)],[clause59,c78]) ).
cnf(c264,plain,
( ~ accessible_world(skc12,X356)
| think_believe_consider(X356,skc13) ),
inference(resolution,[status(thm)],[c263,clause45]) ).
cnf(c262,plain,
( ~ accessible_world(skc8,X355)
| living(X355,skc10) ),
inference(resolution,[status(thm)],[clause58,c75]) ).
cnf(c261,plain,
( ~ accessible_world(skc8,X354)
| living(X354,skc15) ),
inference(resolution,[status(thm)],[clause58,c76]) ).
cnf(c260,plain,
( ~ accessible_world(skc12,X349)
| present(X349,skc13) ),
inference(resolution,[status(thm)],[c259,clause44]) ).
cnf(c258,plain,
( ~ accessible_world(skc8,X348)
| impartial(X348,skc10) ),
inference(resolution,[status(thm)],[clause57,c73]) ).
cnf(c257,plain,
( ~ accessible_world(skc8,X347)
| impartial(X347,skc15) ),
inference(resolution,[status(thm)],[clause57,c74]) ).
cnf(c256,plain,
( ~ accessible_world(skc12,X342)
| unisex(X342,skc11) ),
inference(resolution,[status(thm)],[c254,clause43]) ).
cnf(c253,plain,
( ~ accessible_world(skc8,X341)
| existent(X341,skc10) ),
inference(resolution,[status(thm)],[clause56,c71]) ).
cnf(c252,plain,
( ~ accessible_world(skc8,X340)
| existent(X340,skc15) ),
inference(resolution,[status(thm)],[clause56,c72]) ).
cnf(c250,plain,
( ~ accessible_world(skc12,X335)
| unisex(X335,skc14) ),
inference(resolution,[status(thm)],[c248,clause43]) ).
cnf(c247,plain,
( ~ accessible_world(skc8,X334)
| entity(X334,skc15) ),
inference(resolution,[status(thm)],[clause55,c64]) ).
cnf(c1,axiom,
( X331 != X332
| skf4(X331) = skf4(X332) ),
theory(equality) ).
cnf(c246,plain,
( ~ accessible_world(skc8,X330)
| entity(X330,skc10) ),
inference(resolution,[status(thm)],[clause55,c63]) ).
cnf(c245,plain,
( ~ accessible_world(skc12,X329)
| unisex(X329,skc12) ),
inference(resolution,[status(thm)],[c243,clause43]) ).
cnf(c241,plain,
( ~ accessible_world(skc8,X328)
| organism(X328,skc15) ),
inference(resolution,[status(thm)],[clause54,c62]) ).
cnf(c0,axiom,
( X325 != X326
| skf2(X325) = skf2(X326) ),
theory(equality) ).
cnf(c240,plain,
( ~ accessible_world(skc8,X324)
| organism(X324,skc10) ),
inference(resolution,[status(thm)],[clause54,c61]) ).
cnf(transitivity,axiom,
( X318 != X320
| X320 != X319
| X318 = X319 ),
theory(equality) ).
cnf(c238,plain,
( ~ accessible_world(skc8,X317)
| human_person(X317,skc15) ),
inference(resolution,[status(thm)],[clause53,c60]) ).
cnf(c237,plain,
( ~ accessible_world(skc8,X316)
| human_person(X316,skc10) ),
inference(resolution,[status(thm)],[clause53,c59]) ).
cnf(c234,plain,
( ~ accessible_world(skc12,X315)
| specific(X315,skc10) ),
inference(resolution,[status(thm)],[c231,clause41]) ).
cnf(clause34,axiom,
( ~ nonexistent(X70,X69)
| ~ existent(X70,X69) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c403,plain,
~ nonexistent(skc12,skc15),
inference(resolution,[status(thm)],[c400,clause34]) ).
cnf(clause32,axiom,
( ~ general(X66,X65)
| ~ specific(X66,X65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c376,plain,
~ general(skc12,skf2(X285)),
inference(resolution,[status(thm)],[c368,clause32]) ).
cnf(clause31,axiom,
( ~ male(X64,X63)
| ~ unisex(X64,X63) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c372,plain,
~ male(skc12,skf2(X284)),
inference(resolution,[status(thm)],[c365,clause31]) ).
cnf(c357,plain,
~ nonexistent(skc12,skc10),
inference(resolution,[status(thm)],[c354,clause34]) ).
cnf(c229,plain,
( ~ accessible_world(skc12,X257)
| specific(X257,skc15) ),
inference(resolution,[status(thm)],[c228,clause41]) ).
cnf(c224,plain,
( ~ accessible_world(skc8,X250)
| general(X250,skc12) ),
inference(resolution,[status(thm)],[clause50,c49]) ).
cnf(c223,plain,
( ~ accessible_world(skc8,X245)
| general(X245,skc11) ),
inference(resolution,[status(thm)],[clause50,c92]) ).
cnf(c222,plain,
( ~ accessible_world(skc8,X244)
| general(X244,skc14) ),
inference(resolution,[status(thm)],[clause50,c96]) ).
cnf(c219,plain,
( ~ accessible_world(skc8,X239)
| nonhuman(X239,skc12) ),
inference(resolution,[status(thm)],[clause49,c48]) ).
cnf(c218,plain,
( ~ accessible_world(skc8,X238)
| nonhuman(X238,skc14) ),
inference(resolution,[status(thm)],[clause49,c95]) ).
cnf(c217,plain,
( ~ accessible_world(skc8,X237)
| nonhuman(X237,skc11) ),
inference(resolution,[status(thm)],[clause49,c91]) ).
cnf(c214,plain,
( ~ accessible_world(skc8,X232)
| abstraction(X232,skc12) ),
inference(resolution,[status(thm)],[clause48,c45]) ).
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,skc14) ),
inference(resolution,[status(thm)],[clause48,c89]) ).
cnf(clause33,axiom,
( ~ human(X68,X67)
| ~ nonhuman(X68,X67) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c310,plain,
~ human(skc12,skc11),
inference(resolution,[status(thm)],[c307,clause33]) ).
cnf(c296,plain,
~ human(skc12,skc14),
inference(resolution,[status(thm)],[c294,clause33]) ).
cnf(c207,plain,
( ~ accessible_world(skc8,X215)
| relation(X215,skc12) ),
inference(resolution,[status(thm)],[clause47,c44]) ).
cnf(c205,plain,
( ~ accessible_world(skc12,X214)
| singleton(X214,skc11) ),
inference(resolution,[status(thm)],[c203,clause40]) ).
cnf(c280,plain,
~ human(skc12,skc12),
inference(resolution,[status(thm)],[c276,clause33]) ).
cnf(c202,plain,
( ~ accessible_world(skc12,X206)
| thing(X206,skc11) ),
inference(resolution,[status(thm)],[c201,clause39]) ).
cnf(c199,plain,
( ~ accessible_world(skc12,X202)
| singleton(X202,skc10) ),
inference(resolution,[status(thm)],[c197,clause40]) ).
cnf(c196,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)],[c193,clause40]) ).
cnf(c192,plain,
( ~ accessible_world(skc12,X195)
| thing(X195,skc12) ),
inference(resolution,[status(thm)],[c191,clause39]) ).
cnf(c188,plain,
( ~ accessible_world(skc12,X193)
| singleton(X193,skc14) ),
inference(resolution,[status(thm)],[c187,clause40]) ).
cnf(c186,plain,
( ~ accessible_world(skc12,X192)
| thing(X192,skc14) ),
inference(resolution,[status(thm)],[c185,clause39]) ).
cnf(c184,plain,
( ~ accessible_world(skc12,X188)
| unisex(X188,skc9) ),
inference(resolution,[status(thm)],[clause43,c124]) ).
cnf(c255,plain,
~ male(skc12,skc11),
inference(resolution,[status(thm)],[c254,clause31]) ).
cnf(c182,plain,
( ~ accessible_world(skc8,X183)
| unisex(X183,skc9) ),
inference(resolution,[status(thm)],[clause43,c54]) ).
cnf(c249,plain,
~ male(skc12,skc14),
inference(resolution,[status(thm)],[c248,clause31]) ).
cnf(c180,plain,
( ~ accessible_world(skc12,X181)
| unisex(X181,skc13) ),
inference(resolution,[status(thm)],[clause43,c145]) ).
cnf(c244,plain,
~ male(skc12,skc12),
inference(resolution,[status(thm)],[c243,clause31]) ).
cnf(c178,plain,
( ~ accessible_world(skc8,X176)
| unisex(X176,skc13) ),
inference(resolution,[status(thm)],[clause43,c43]) ).
cnf(c177,plain,
( ~ accessible_world(skc12,X172)
| singleton(X172,skc15) ),
inference(resolution,[status(thm)],[c176,clause40]) ).
cnf(c175,plain,
( ~ accessible_world(skc12,X171)
| thing(X171,skc15) ),
inference(resolution,[status(thm)],[c174,clause39]) ).
cnf(c173,plain,
( ~ accessible_world(skc12,X170)
| nonexistent(X170,skc13) ),
inference(resolution,[status(thm)],[clause42,c147]) ).
cnf(c172,plain,
( ~ accessible_world(skc8,X169)
| nonexistent(X169,skc13) ),
inference(resolution,[status(thm)],[clause42,c42]) ).
cnf(c171,plain,
( ~ accessible_world(skc12,X165)
| nonexistent(X165,skc9) ),
inference(resolution,[status(thm)],[clause42,c126]) ).
cnf(c170,plain,
( ~ accessible_world(skc8,X164)
| nonexistent(X164,skc9) ),
inference(resolution,[status(thm)],[clause42,c56]) ).
cnf(c235,plain,
~ general(skc12,skc10),
inference(resolution,[status(thm)],[c231,clause32]) ).
cnf(c166,plain,
( ~ accessible_world(skc12,X159)
| specific(X159,skc13) ),
inference(resolution,[status(thm)],[clause41,c148]) ).
cnf(c230,plain,
~ general(skc12,skc15),
inference(resolution,[status(thm)],[c228,clause32]) ).
cnf(c164,plain,
( ~ accessible_world(skc8,X154)
| specific(X154,skc9) ),
inference(resolution,[status(thm)],[clause41,c55]) ).
cnf(c163,plain,
( ~ accessible_world(skc8,X153)
| specific(X153,skc13) ),
inference(resolution,[status(thm)],[clause41,c41]) ).
cnf(c162,plain,
( ~ accessible_world(skc12,X152)
| specific(X152,skc9) ),
inference(resolution,[status(thm)],[clause41,c125]) ).
cnf(c161,plain,
( ~ accessible_world(skc12,X148)
| singleton(X148,skc13) ),
inference(resolution,[status(thm)],[c150,clause40]) ).
cnf(c159,plain,
( ~ accessible_world(skc8,X147)
| singleton(X147,skc10) ),
inference(resolution,[status(thm)],[clause40,c67]) ).
cnf(c158,plain,
( ~ accessible_world(skc8,X146)
| singleton(X146,skc12) ),
inference(resolution,[status(thm)],[clause40,c47]) ).
cnf(c157,plain,
( ~ accessible_world(skc8,X142)
| singleton(X142,skc15) ),
inference(resolution,[status(thm)],[clause40,c68]) ).
cnf(c156,plain,
( ~ accessible_world(skc8,X141)
| singleton(X141,skc13) ),
inference(resolution,[status(thm)],[clause40,c40]) ).
cnf(c155,plain,
( ~ accessible_world(skc8,X137)
| singleton(X137,skc9) ),
inference(resolution,[status(thm)],[clause40,c58]) ).
cnf(c154,plain,
( ~ accessible_world(skc12,X136)
| singleton(X136,skc9) ),
inference(resolution,[status(thm)],[clause40,c127]) ).
cnf(c153,plain,
( ~ accessible_world(skc8,X135)
| singleton(X135,skc14) ),
inference(resolution,[status(thm)],[clause40,c100]) ).
cnf(c152,plain,
( ~ accessible_world(skc8,X131)
| singleton(X131,skc11) ),
inference(resolution,[status(thm)],[clause40,c99]) ).
cnf(c149,plain,
( ~ accessible_world(skc12,X130)
| thing(X130,skc13) ),
inference(resolution,[status(thm)],[c144,clause39]) ).
cnf(c146,plain,
( ~ accessible_world(skc12,X129)
| eventuality(X129,skc13) ),
inference(resolution,[status(thm)],[c143,clause38]) ).
cnf(c142,plain,
( ~ accessible_world(skc12,X128)
| event(X128,skc13) ),
inference(resolution,[status(thm)],[c141,clause37]) ).
cnf(c139,plain,
( ~ accessible_world(skc8,X123)
| thing(X123,skc9) ),
inference(resolution,[status(thm)],[clause39,c53]) ).
cnf(c136,plain,
( ~ accessible_world(skc8,X114)
| thing(X114,skc13) ),
inference(resolution,[status(thm)],[clause39,c39]) ).
cnf(c133,plain,
( ~ accessible_world(skc12,X108)
| thing(X108,skc9) ),
inference(resolution,[status(thm)],[clause39,c123]) ).
cnf(c131,plain,
( ~ accessible_world(skc8,X104)
| eventuality(X104,skc9) ),
inference(resolution,[status(thm)],[clause38,c51]) ).
cnf(c130,plain,
( ~ accessible_world(skc8,X103)
| eventuality(X103,skc13) ),
inference(resolution,[status(thm)],[clause38,c38]) ).
cnf(c129,plain,
( ~ accessible_world(skc12,X102)
| eventuality(X102,skc9) ),
inference(resolution,[status(thm)],[clause38,c122]) ).
cnf(c121,plain,
( ~ accessible_world(skc12,X101)
| event(X101,skc9) ),
inference(resolution,[status(thm)],[c120,clause37]) ).
cnf(c160,plain,
~ general(skc12,skc13),
inference(resolution,[status(thm)],[c148,clause32]) ).
cnf(c151,plain,
~ male(skc12,skc13),
inference(resolution,[status(thm)],[c145,clause31]) ).
cnf(c132,plain,
~ general(skc12,skc9),
inference(resolution,[status(thm)],[c125,clause32]) ).
cnf(c128,plain,
~ male(skc12,skc9),
inference(resolution,[status(thm)],[c124,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(X74,X72,X73,X71)
| X73 = X71 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c114,plain,
~ nonexistent(skc8,skc10),
inference(resolution,[status(thm)],[clause34,c71]) ).
cnf(c113,plain,
~ nonexistent(skc8,skc15),
inference(resolution,[status(thm)],[clause34,c72]) ).
cnf(c112,plain,
~ human(skc8,skc12),
inference(resolution,[status(thm)],[clause33,c48]) ).
cnf(c111,plain,
~ human(skc8,skc14),
inference(resolution,[status(thm)],[clause33,c95]) ).
cnf(c110,plain,
~ human(skc8,skc11),
inference(resolution,[status(thm)],[clause33,c91]) ).
cnf(c109,plain,
~ general(skc8,skc10),
inference(resolution,[status(thm)],[clause32,c69]) ).
cnf(c108,plain,
~ general(skc8,skc13),
inference(resolution,[status(thm)],[clause32,c41]) ).
cnf(c107,plain,
~ general(skc8,skc15),
inference(resolution,[status(thm)],[clause32,c70]) ).
cnf(c106,plain,
~ general(skc8,skc9),
inference(resolution,[status(thm)],[clause32,c55]) ).
cnf(c105,plain,
~ male(skc8,skc14),
inference(resolution,[status(thm)],[c97,clause31]) ).
cnf(c104,plain,
~ male(skc8,skc11),
inference(resolution,[status(thm)],[clause31,c93]) ).
cnf(c103,plain,
~ male(skc8,skc9),
inference(resolution,[status(thm)],[clause31,c54]) ).
cnf(c102,plain,
~ male(skc8,skc13),
inference(resolution,[status(thm)],[clause31,c43]) ).
cnf(c101,plain,
~ male(skc8,skc12),
inference(resolution,[status(thm)],[clause31,c50]) ).
cnf(clause30,axiom,
( ~ jules_forename(X62,X61)
| forename(X62,X61) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,axiom,
( ~ vincent_forename(X60,X59)
| forename(X60,X59) ),
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.11/0.12 % Problem : NLP256-1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:36:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 2.66/2.85 % Version: 1.5
% 2.66/2.85 % SZS status Satisfiable
% 2.66/2.85 % SZS output start Saturation
% See solution above
% 2.66/2.88
% 2.66/2.88 % Initial clauses : 136
% 2.66/2.88 % Processed clauses : 910
% 2.66/2.88 % Factors computed : 82
% 2.66/2.88 % Resolvents computed: 986
% 2.66/2.88 % Tautologies deleted: 3
% 2.66/2.88 % Forward subsumed : 291
% 2.66/2.88 % Backward subsumed : 6
% 2.66/2.88 % -------- CPU Time ---------
% 2.66/2.88 % User time : 2.516 s
% 2.66/2.88 % System time : 0.014 s
% 2.66/2.88 % Total time : 2.530 s
%------------------------------------------------------------------------------