%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP259-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:56 EDT 2024
% Result : Satisfiable 4.73s 4.89s
% Output : Saturation 4.73s
% 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(clause73,negated_conjecture,
man(skc8,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
cnf(clause52,axiom,
( ~ accessible_world(X160,X162)
| ~ man(X160,X161)
| man(X162,X161) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c234,plain,
( ~ accessible_world(skc8,X287)
| man(X287,skc15) ),
inference(resolution,[status(thm)],[clause52,clause73]) ).
cnf(c379,plain,
man(skc12,skc15),
inference(resolution,[status(thm)],[c234,clause83]) ).
cnf(clause93,negated_conjecture,
( ~ man(skc12,X288)
| agent(skc12,skf2(X288),X288) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
cnf(c383,plain,
agent(skc12,skf2(skc15),skc15),
inference(resolution,[status(thm)],[clause93,c379]) ).
cnf(clause85,negated_conjecture,
of(skc8,skc14,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
cnf(clause68,axiom,
( ~ accessible_world(X246,X249)
| ~ of(X246,X248,X247)
| of(X249,X248,X247) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
cnf(c323,plain,
( ~ accessible_world(skc8,X499)
| of(X499,skc14,skc15) ),
inference(resolution,[status(thm)],[clause68,clause85]) ).
cnf(c579,plain,
of(skc12,skc14,skc15),
inference(resolution,[status(thm)],[c323,clause83]) ).
cnf(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
cnf(clause67,axiom,
( ~ accessible_world(X240,X243)
| ~ theme(X240,X242,X241)
| theme(X243,X242,X241) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
cnf(c320,plain,
( ~ accessible_world(skc8,X494)
| theme(X494,skc13,skc12) ),
inference(resolution,[status(thm)],[clause67,clause87]) ).
cnf(c573,plain,
theme(skc12,skc13,skc12),
inference(resolution,[status(thm)],[c320,clause83]) ).
cnf(clause94,negated_conjecture,
( ~ state(X299,X294)
| ~ man(X299,X290)
| ~ be(X299,X294,X290,X290)
| ~ forename(X299,X289)
| ~ jules_forename(X299,X289)
| ~ of(X299,X289,X290)
| ~ accessible_world(X299,X297)
| ~ proposition(X299,X297)
| ~ proposition(X299,X293)
| ~ accessible_world(X299,X293)
| ~ think_believe_consider(X299,X291)
| ~ present(X299,X291)
| ~ event(X299,X291)
| ~ theme(X299,X291,X293)
| ~ forename(X299,X292)
| ~ jules_forename(X299,X292)
| ~ of(X299,X292,X296)
| ~ smoke(X297,X295)
| ~ present(X297,X295)
| ~ agent(X297,X295,X296)
| ~ event(X297,X295)
| ~ agent(X299,X298,X296)
| ~ agent(X299,X291,X296)
| ~ man(X299,X296)
| ~ of(X299,X300,X296)
| ~ vincent_forename(X299,X300)
| ~ forename(X299,X300)
| ~ theme(X299,X298,X297)
| ~ event(X299,X298)
| ~ present(X299,X298)
| ~ think_believe_consider(X299,X298)
| ~ actual_world(X299)
| man(X293,skf4(X293)) ),
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(X257,X255)
| ~ be(X257,X254,X253,X256)
| be(X255,X254,X253,X256) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
cnf(c330,plain,
( ~ accessible_world(skc8,X509)
| be(X509,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[clause69,clause89]) ).
cnf(c589,plain,
be(skc12,skc9,skc10,skc10),
inference(resolution,[status(thm)],[c330,clause83]) ).
cnf(c590,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1058)
| ~ jules_forename(skc12,X1058)
| ~ of(skc12,X1058,skc10)
| ~ accessible_world(skc12,X1051)
| ~ proposition(skc12,X1051)
| ~ proposition(skc12,X1055)
| ~ accessible_world(skc12,X1055)
| ~ think_believe_consider(skc12,X1052)
| ~ present(skc12,X1052)
| ~ event(skc12,X1052)
| ~ theme(skc12,X1052,X1055)
| ~ forename(skc12,X1056)
| ~ jules_forename(skc12,X1056)
| ~ of(skc12,X1056,X1057)
| ~ smoke(X1051,X1050)
| ~ present(X1051,X1050)
| ~ agent(X1051,X1050,X1057)
| ~ event(X1051,X1050)
| ~ agent(skc12,X1053,X1057)
| ~ agent(skc12,X1052,X1057)
| ~ man(skc12,X1057)
| ~ of(skc12,X1054,X1057)
| ~ vincent_forename(skc12,X1054)
| ~ forename(skc12,X1054)
| ~ theme(skc12,X1053,X1051)
| ~ event(skc12,X1053)
| ~ present(skc12,X1053)
| ~ think_believe_consider(skc12,X1053)
| ~ actual_world(skc12)
| man(X1055,skf4(X1055)) ),
inference(resolution,[status(thm)],[c589,clause94]) ).
cnf(c922,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1435)
| ~ jules_forename(skc12,X1435)
| ~ of(skc12,X1435,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1432)
| ~ accessible_world(skc12,X1432)
| ~ think_believe_consider(skc12,X1433)
| ~ present(skc12,X1433)
| ~ event(skc12,X1433)
| ~ theme(skc12,X1433,X1432)
| ~ forename(skc12,X1437)
| ~ jules_forename(skc12,X1437)
| ~ of(skc12,X1437,X1436)
| ~ smoke(skc12,X1434)
| ~ present(skc12,X1434)
| ~ agent(skc12,X1434,X1436)
| ~ event(skc12,X1434)
| ~ agent(skc12,skc13,X1436)
| ~ agent(skc12,X1433,X1436)
| ~ man(skc12,X1436)
| ~ of(skc12,X1431,X1436)
| ~ vincent_forename(skc12,X1431)
| ~ forename(skc12,X1431)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1432,skf4(X1432)) ),
inference(resolution,[status(thm)],[c590,c573]) ).
cnf(c1080,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1569)
| ~ jules_forename(skc12,X1569)
| ~ of(skc12,X1569,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1568)
| ~ accessible_world(skc12,X1568)
| ~ think_believe_consider(skc12,X1570)
| ~ present(skc12,X1570)
| ~ event(skc12,X1570)
| ~ theme(skc12,X1570,X1568)
| ~ forename(skc12,X1572)
| ~ jules_forename(skc12,X1572)
| ~ of(skc12,X1572,skc15)
| ~ smoke(skc12,X1571)
| ~ present(skc12,X1571)
| ~ agent(skc12,X1571,skc15)
| ~ event(skc12,X1571)
| ~ agent(skc12,skc13,skc15)
| ~ agent(skc12,X1570,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1568,skf4(X1568)) ),
inference(resolution,[status(thm)],[c922,c579]) ).
cnf(c1142,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1817)
| ~ jules_forename(skc12,X1817)
| ~ of(skc12,X1817,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1819)
| ~ accessible_world(skc12,X1819)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1819)
| ~ forename(skc12,X1816)
| ~ jules_forename(skc12,X1816)
| ~ of(skc12,X1816,skc15)
| ~ smoke(skc12,X1818)
| ~ present(skc12,X1818)
| ~ agent(skc12,X1818,skc15)
| ~ event(skc12,X1818)
| ~ agent(skc12,skc13,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1819,skf4(X1819)) ),
inference(resolution,[status(thm)],[c1080,c383]) ).
cnf(clause86,negated_conjecture,
agent(skc8,skc13,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
cnf(clause66,axiom,
( ~ accessible_world(X233,X236)
| ~ agent(X233,X235,X234)
| agent(X236,X235,X234) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
cnf(c316,plain,
( ~ accessible_world(skc8,X493)
| agent(X493,skc13,skc15) ),
inference(resolution,[status(thm)],[clause66,clause86]) ).
cnf(c570,plain,
agent(skc12,skc13,skc15),
inference(resolution,[status(thm)],[c316,clause83]) ).
cnf(c1139,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1791)
| ~ jules_forename(skc12,X1791)
| ~ of(skc12,X1791,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1793)
| ~ accessible_world(skc12,X1793)
| ~ think_believe_consider(skc12,X1792)
| ~ present(skc12,X1792)
| ~ event(skc12,X1792)
| ~ theme(skc12,X1792,X1793)
| ~ forename(skc12,X1790)
| ~ jules_forename(skc12,X1790)
| ~ of(skc12,X1790,skc15)
| ~ smoke(skc12,X1792)
| ~ agent(skc12,X1792,skc15)
| ~ agent(skc12,skc13,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1793,skf4(X1793)) ),
inference(factor,[status(thm)],[c1080]) ).
cnf(c1196,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1803)
| ~ jules_forename(skc12,X1803)
| ~ of(skc12,X1803,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1804)
| ~ accessible_world(skc12,X1804)
| ~ think_believe_consider(skc12,X1802)
| ~ present(skc12,X1802)
| ~ event(skc12,X1802)
| ~ theme(skc12,X1802,X1804)
| ~ forename(skc12,X1805)
| ~ jules_forename(skc12,X1805)
| ~ of(skc12,X1805,skc15)
| ~ smoke(skc12,X1802)
| ~ agent(skc12,X1802,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1804,skf4(X1804)) ),
inference(resolution,[status(thm)],[c1139,c570]) ).
cnf(c1199,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1814)
| ~ jules_forename(skc12,X1814)
| ~ of(skc12,X1814,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1813)
| ~ accessible_world(skc12,X1813)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1813)
| ~ forename(skc12,X1815)
| ~ jules_forename(skc12,X1815)
| ~ of(skc12,X1815,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1813,skf4(X1813)) ),
inference(resolution,[status(thm)],[c1196,c383]) ).
cnf(clause81,negated_conjecture,
man(skc8,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
cnf(c233,plain,
( ~ accessible_world(skc8,X259)
| man(X259,skc10) ),
inference(resolution,[status(thm)],[clause52,clause81]) ).
cnf(c331,plain,
man(skc12,skc10),
inference(resolution,[status(thm)],[c233,clause83]) ).
cnf(clause90,negated_conjecture,
( ~ man(skc12,X270)
| smoke(skc12,skf2(X271)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
cnf(c359,plain,
smoke(skc12,skf2(X272)),
inference(resolution,[status(thm)],[clause90,c331]) ).
cnf(clause91,negated_conjecture,
( ~ man(skc12,X275)
| present(skc12,skf2(X276)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
cnf(c369,plain,
present(skc12,skf2(X281)),
inference(resolution,[status(thm)],[clause91,c331]) ).
cnf(clause1,axiom,
( ~ smoke(X3,X4)
| event(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(c361,plain,
event(skc12,skf2(X273)),
inference(resolution,[status(thm)],[c359,clause1]) ).
cnf(c1140,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1759)
| ~ jules_forename(skc12,X1759)
| ~ of(skc12,X1759,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1761)
| ~ accessible_world(skc12,X1761)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1761)
| ~ forename(skc12,X1758)
| ~ jules_forename(skc12,X1758)
| ~ of(skc12,X1758,skc15)
| ~ smoke(skc12,X1760)
| ~ present(skc12,X1760)
| ~ agent(skc12,X1760,skc15)
| ~ event(skc12,X1760)
| ~ agent(skc12,skc13,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1761,skf4(X1761)) ),
inference(factor,[status(thm)],[c1080]) ).
cnf(c1187,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1774)
| ~ jules_forename(skc12,X1774)
| ~ of(skc12,X1774,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1777)
| ~ accessible_world(skc12,X1777)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1777)
| ~ forename(skc12,X1776)
| ~ jules_forename(skc12,X1776)
| ~ of(skc12,X1776,skc15)
| ~ smoke(skc12,X1775)
| ~ present(skc12,X1775)
| ~ agent(skc12,X1775,skc15)
| ~ event(skc12,X1775)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1777,skf4(X1777)) ),
inference(resolution,[status(thm)],[c1140,c570]) ).
cnf(c1191,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1783)
| ~ jules_forename(skc12,X1783)
| ~ of(skc12,X1783,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1782)
| ~ accessible_world(skc12,X1782)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1782)
| ~ forename(skc12,X1781)
| ~ jules_forename(skc12,X1781)
| ~ of(skc12,X1781,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1782,skf4(X1782)) ),
inference(resolution,[status(thm)],[c1187,c383]) ).
cnf(c1192,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1785)
| ~ jules_forename(skc12,X1785)
| ~ of(skc12,X1785,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1786)
| ~ accessible_world(skc12,X1786)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1786)
| ~ forename(skc12,X1784)
| ~ jules_forename(skc12,X1784)
| ~ of(skc12,X1784,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1786,skf4(X1786)) ),
inference(resolution,[status(thm)],[c1191,c361]) ).
cnf(c1193,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1789)
| ~ jules_forename(skc12,X1789)
| ~ of(skc12,X1789,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1787)
| ~ accessible_world(skc12,X1787)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1787)
| ~ forename(skc12,X1788)
| ~ jules_forename(skc12,X1788)
| ~ of(skc12,X1788,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1787,skf4(X1787)) ),
inference(resolution,[status(thm)],[c1192,c369]) ).
cnf(c1194,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1796)
| ~ jules_forename(skc12,X1796)
| ~ of(skc12,X1796,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1794)
| ~ accessible_world(skc12,X1794)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1794)
| ~ forename(skc12,X1795)
| ~ jules_forename(skc12,X1795)
| ~ of(skc12,X1795,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1794,skf4(X1794)) ),
inference(resolution,[status(thm)],[c1193,c359]) ).
cnf(c384,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(c324,plain,
( ~ accessible_world(skc8,X500)
| of(X500,skc11,skc10) ),
inference(resolution,[status(thm)],[clause68,clause88]) ).
cnf(c582,plain,
of(skc12,skc11,skc10),
inference(resolution,[status(thm)],[c324,clause83]) ).
cnf(c1079,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1553)
| ~ jules_forename(skc12,X1553)
| ~ of(skc12,X1553,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1552)
| ~ accessible_world(skc12,X1552)
| ~ think_believe_consider(skc12,X1554)
| ~ present(skc12,X1554)
| ~ event(skc12,X1554)
| ~ theme(skc12,X1554,X1552)
| ~ forename(skc12,X1556)
| ~ jules_forename(skc12,X1556)
| ~ of(skc12,X1556,skc10)
| ~ smoke(skc12,X1555)
| ~ present(skc12,X1555)
| ~ agent(skc12,X1555,skc10)
| ~ event(skc12,X1555)
| ~ agent(skc12,skc13,skc10)
| ~ agent(skc12,X1554,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1552,skf4(X1552)) ),
inference(resolution,[status(thm)],[c922,c582]) ).
cnf(c1135,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1771)
| ~ jules_forename(skc12,X1771)
| ~ of(skc12,X1771,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1770)
| ~ accessible_world(skc12,X1770)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1770)
| ~ forename(skc12,X1773)
| ~ jules_forename(skc12,X1773)
| ~ of(skc12,X1773,skc10)
| ~ smoke(skc12,X1772)
| ~ present(skc12,X1772)
| ~ agent(skc12,X1772,skc10)
| ~ event(skc12,X1772)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1770,skf4(X1770)) ),
inference(resolution,[status(thm)],[c1079,c384]) ).
cnf(c1133,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1748)
| ~ jules_forename(skc12,X1748)
| ~ of(skc12,X1748,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1747)
| ~ accessible_world(skc12,X1747)
| ~ think_believe_consider(skc12,X1749)
| ~ present(skc12,X1749)
| ~ event(skc12,X1749)
| ~ theme(skc12,X1749,X1747)
| ~ forename(skc12,X1750)
| ~ jules_forename(skc12,X1750)
| ~ of(skc12,X1750,skc10)
| ~ smoke(skc12,X1749)
| ~ agent(skc12,X1749,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1747,skf4(X1747)) ),
inference(factor,[status(thm)],[c1079]) ).
cnf(c1078,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1543)
| ~ jules_forename(skc12,X1543)
| ~ of(skc12,X1543,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1541)
| ~ accessible_world(skc12,X1541)
| ~ think_believe_consider(skc12,X1544)
| ~ present(skc12,X1544)
| ~ event(skc12,X1544)
| ~ theme(skc12,X1544,X1541)
| ~ forename(skc12,X1542)
| ~ jules_forename(skc12,X1542)
| ~ of(skc12,X1542,X1546)
| ~ smoke(skc12,X1545)
| ~ present(skc12,X1545)
| ~ agent(skc12,X1545,X1546)
| ~ event(skc12,X1545)
| ~ agent(skc12,skc13,X1546)
| ~ agent(skc12,X1544,X1546)
| ~ man(skc12,X1546)
| ~ vincent_forename(skc12,X1542)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1541,skf4(X1541)) ),
inference(factor,[status(thm)],[c922]) ).
cnf(c1125,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1699)
| ~ jules_forename(skc12,X1699)
| ~ of(skc12,X1699,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1702)
| ~ accessible_world(skc12,X1702)
| ~ think_believe_consider(skc12,X1700)
| ~ present(skc12,X1700)
| ~ event(skc12,X1700)
| ~ theme(skc12,X1700,X1702)
| ~ forename(skc12,X1701)
| ~ jules_forename(skc12,X1701)
| ~ of(skc12,X1701,X1703)
| ~ smoke(skc12,X1700)
| ~ agent(skc12,X1700,X1703)
| ~ agent(skc12,skc13,X1703)
| ~ man(skc12,X1703)
| ~ vincent_forename(skc12,X1701)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1702,skf4(X1702)) ),
inference(factor,[status(thm)],[c1078]) ).
cnf(c1177,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1710)
| ~ jules_forename(skc12,X1710)
| ~ of(skc12,X1710,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1709)
| ~ accessible_world(skc12,X1709)
| ~ think_believe_consider(skc12,X1708)
| ~ present(skc12,X1708)
| ~ event(skc12,X1708)
| ~ theme(skc12,X1708,X1709)
| ~ forename(skc12,X1711)
| ~ jules_forename(skc12,X1711)
| ~ of(skc12,X1711,skc15)
| ~ smoke(skc12,X1708)
| ~ agent(skc12,X1708,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1711)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1709,skf4(X1709)) ),
inference(resolution,[status(thm)],[c1125,c570]) ).
cnf(c1179,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1746)
| ~ jules_forename(skc12,X1746)
| ~ of(skc12,X1746,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1745)
| ~ accessible_world(skc12,X1745)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1745)
| ~ forename(skc12,X1744)
| ~ jules_forename(skc12,X1744)
| ~ of(skc12,X1744,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1744)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1745,skf4(X1745)) ),
inference(resolution,[status(thm)],[c1177,c383]) ).
cnf(c396,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X681)
| ~ jules_forename(skc8,X681)
| ~ of(skc8,X681,skc10)
| ~ accessible_world(skc8,X674)
| ~ proposition(skc8,X674)
| ~ proposition(skc8,X678)
| ~ accessible_world(skc8,X678)
| ~ think_believe_consider(skc8,X675)
| ~ present(skc8,X675)
| ~ event(skc8,X675)
| ~ theme(skc8,X675,X678)
| ~ forename(skc8,X679)
| ~ jules_forename(skc8,X679)
| ~ of(skc8,X679,X680)
| ~ smoke(X674,X673)
| ~ present(X674,X673)
| ~ agent(X674,X673,X680)
| ~ event(X674,X673)
| ~ agent(skc8,X676,X680)
| ~ agent(skc8,X675,X680)
| ~ man(skc8,X680)
| ~ of(skc8,X677,X680)
| ~ vincent_forename(skc8,X677)
| ~ forename(skc8,X677)
| ~ theme(skc8,X676,X674)
| ~ event(skc8,X676)
| ~ present(skc8,X676)
| ~ think_believe_consider(skc8,X676)
| ~ actual_world(skc8)
| man(X678,skf4(X678)) ),
inference(resolution,[status(thm)],[clause94,clause89]) ).
cnf(c699,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1280)
| ~ jules_forename(skc8,X1280)
| ~ of(skc8,X1280,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1281)
| ~ accessible_world(skc8,X1281)
| ~ think_believe_consider(skc8,X1284)
| ~ present(skc8,X1284)
| ~ event(skc8,X1284)
| ~ theme(skc8,X1284,X1281)
| ~ forename(skc8,X1286)
| ~ jules_forename(skc8,X1286)
| ~ of(skc8,X1286,X1285)
| ~ smoke(skc12,X1282)
| ~ present(skc12,X1282)
| ~ agent(skc12,X1282,X1285)
| ~ event(skc12,X1282)
| ~ agent(skc8,skc13,X1285)
| ~ agent(skc8,X1284,X1285)
| ~ man(skc8,X1285)
| ~ of(skc8,X1283,X1285)
| ~ vincent_forename(skc8,X1283)
| ~ forename(skc8,X1283)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(X1281,skf4(X1281)) ),
inference(resolution,[status(thm)],[c396,clause87]) ).
cnf(c1038,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1511)
| ~ jules_forename(skc8,X1511)
| ~ of(skc8,X1511,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1508)
| ~ accessible_world(skc8,X1508)
| ~ think_believe_consider(skc8,X1509)
| ~ present(skc8,X1509)
| ~ event(skc8,X1509)
| ~ theme(skc8,X1509,X1508)
| ~ forename(skc8,X1510)
| ~ jules_forename(skc8,X1510)
| ~ of(skc8,X1510,skc15)
| ~ smoke(skc12,X1512)
| ~ present(skc12,X1512)
| ~ agent(skc12,X1512,skc15)
| ~ event(skc12,X1512)
| ~ agent(skc8,skc13,skc15)
| ~ agent(skc8,X1509,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(X1508,skf4(X1508)) ),
inference(resolution,[status(thm)],[c699,clause85]) ).
cnf(c1105,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1621)
| ~ jules_forename(skc8,X1621)
| ~ of(skc8,X1621,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1620)
| ~ accessible_world(skc8,X1620)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1620)
| ~ forename(skc8,X1618)
| ~ jules_forename(skc8,X1618)
| ~ of(skc8,X1618,skc15)
| ~ smoke(skc12,X1619)
| ~ present(skc12,X1619)
| ~ agent(skc12,X1619,skc15)
| ~ event(skc12,X1619)
| ~ agent(skc8,skc13,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1620,skf4(X1620)) ),
inference(factor,[status(thm)],[c1038]) ).
cnf(c1155,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1689)
| ~ jules_forename(skc8,X1689)
| ~ of(skc8,X1689,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1686)
| ~ accessible_world(skc8,X1686)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1686)
| ~ forename(skc8,X1687)
| ~ jules_forename(skc8,X1687)
| ~ of(skc8,X1687,skc15)
| ~ smoke(skc12,X1688)
| ~ present(skc12,X1688)
| ~ agent(skc12,X1688,skc15)
| ~ event(skc12,X1688)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1686,skf4(X1686)) ),
inference(resolution,[status(thm)],[c1105,clause86]) ).
cnf(c1174,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1726)
| ~ jules_forename(skc8,X1726)
| ~ of(skc8,X1726,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1727)
| ~ accessible_world(skc8,X1727)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1727)
| ~ forename(skc8,X1728)
| ~ jules_forename(skc8,X1728)
| ~ of(skc8,X1728,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1727,skf4(X1727)) ),
inference(resolution,[status(thm)],[c1155,c383]) ).
cnf(c1181,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1729)
| ~ jules_forename(skc8,X1729)
| ~ of(skc8,X1729,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1730)
| ~ accessible_world(skc8,X1730)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1730)
| ~ forename(skc8,X1731)
| ~ jules_forename(skc8,X1731)
| ~ of(skc8,X1731,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1730,skf4(X1730)) ),
inference(resolution,[status(thm)],[c1174,c361]) ).
cnf(c1182,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1737)
| ~ jules_forename(skc8,X1737)
| ~ of(skc8,X1737,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1738)
| ~ accessible_world(skc8,X1738)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1738)
| ~ forename(skc8,X1736)
| ~ jules_forename(skc8,X1736)
| ~ of(skc8,X1736,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1738,skf4(X1738)) ),
inference(resolution,[status(thm)],[c1181,c369]) ).
cnf(c1183,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1739)
| ~ jules_forename(skc8,X1739)
| ~ of(skc8,X1739,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1740)
| ~ accessible_world(skc8,X1740)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1740)
| ~ forename(skc8,X1741)
| ~ jules_forename(skc8,X1741)
| ~ of(skc8,X1741,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1740,skf4(X1740)) ),
inference(resolution,[status(thm)],[c1182,c359]) ).
cnf(c1128,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1732)
| ~ jules_forename(skc12,X1732)
| ~ of(skc12,X1732,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1735)
| ~ accessible_world(skc12,X1735)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1735)
| ~ forename(skc12,X1734)
| ~ jules_forename(skc12,X1734)
| ~ of(skc12,X1734,skc15)
| ~ smoke(skc12,X1733)
| ~ present(skc12,X1733)
| ~ agent(skc12,X1733,skc15)
| ~ event(skc12,X1733)
| ~ agent(skc12,skc13,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1734)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1735,skf4(X1735)) ),
inference(resolution,[status(thm)],[c1078,c383]) ).
cnf(c1134,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1720)
| ~ jules_forename(skc12,X1720)
| ~ of(skc12,X1720,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1719)
| ~ accessible_world(skc12,X1719)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1719)
| ~ forename(skc12,X1722)
| ~ jules_forename(skc12,X1722)
| ~ of(skc12,X1722,skc10)
| ~ smoke(skc12,X1721)
| ~ present(skc12,X1721)
| ~ agent(skc12,X1721,skc10)
| ~ event(skc12,X1721)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1719,skf4(X1719)) ),
inference(factor,[status(thm)],[c1079]) ).
cnf(c1180,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1724)
| ~ jules_forename(skc12,X1724)
| ~ of(skc12,X1724,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1723)
| ~ accessible_world(skc12,X1723)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1723)
| ~ forename(skc12,X1725)
| ~ jules_forename(skc12,X1725)
| ~ of(skc12,X1725,skc10)
| ~ smoke(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1723,skf4(X1723)) ),
inference(factor,[status(thm)],[c1134]) ).
cnf(c1077,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1531)
| ~ jules_forename(skc12,X1531)
| ~ of(skc12,X1531,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1530)
| ~ accessible_world(skc12,X1530)
| ~ think_believe_consider(skc12,X1532)
| ~ present(skc12,X1532)
| ~ event(skc12,X1532)
| ~ theme(skc12,X1532,X1530)
| ~ forename(skc12,X1534)
| ~ jules_forename(skc12,X1534)
| ~ of(skc12,X1534,skc10)
| ~ smoke(skc12,X1533)
| ~ present(skc12,X1533)
| ~ agent(skc12,X1533,skc10)
| ~ event(skc12,X1533)
| ~ agent(skc12,skc13,skc10)
| ~ agent(skc12,X1532,skc10)
| ~ vincent_forename(skc12,X1531)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1530,skf4(X1530)) ),
inference(factor,[status(thm)],[c922]) ).
cnf(c1119,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1690)
| ~ jules_forename(skc12,X1690)
| ~ of(skc12,X1690,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1692)
| ~ accessible_world(skc12,X1692)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1692)
| ~ forename(skc12,X1693)
| ~ jules_forename(skc12,X1693)
| ~ of(skc12,X1693,skc10)
| ~ smoke(skc12,X1691)
| ~ present(skc12,X1691)
| ~ agent(skc12,X1691,skc10)
| ~ event(skc12,X1691)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,X1690)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1692,skf4(X1692)) ),
inference(resolution,[status(thm)],[c1077,c384]) ).
cnf(c1126,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1638)
| ~ jules_forename(skc12,X1638)
| ~ of(skc12,X1638,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1640)
| ~ accessible_world(skc12,X1640)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1640)
| ~ forename(skc12,X1639)
| ~ jules_forename(skc12,X1639)
| ~ of(skc12,X1639,X1642)
| ~ smoke(skc12,X1641)
| ~ present(skc12,X1641)
| ~ agent(skc12,X1641,X1642)
| ~ event(skc12,X1641)
| ~ agent(skc12,skc13,X1642)
| ~ man(skc12,X1642)
| ~ vincent_forename(skc12,X1639)
| ~ actual_world(skc12)
| man(X1640,skf4(X1640)) ),
inference(factor,[status(thm)],[c1078]) ).
cnf(c1161,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1659)
| ~ jules_forename(skc12,X1659)
| ~ of(skc12,X1659,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1660)
| ~ accessible_world(skc12,X1660)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1660)
| ~ forename(skc12,X1657)
| ~ jules_forename(skc12,X1657)
| ~ of(skc12,X1657,skc15)
| ~ smoke(skc12,X1658)
| ~ present(skc12,X1658)
| ~ agent(skc12,X1658,skc15)
| ~ event(skc12,X1658)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1657)
| ~ actual_world(skc12)
| man(X1660,skf4(X1660)) ),
inference(resolution,[status(thm)],[c1126,c570]) ).
cnf(c1166,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1664)
| ~ jules_forename(skc12,X1664)
| ~ of(skc12,X1664,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1666)
| ~ accessible_world(skc12,X1666)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1666)
| ~ forename(skc12,X1665)
| ~ jules_forename(skc12,X1665)
| ~ of(skc12,X1665,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1665)
| ~ actual_world(skc12)
| man(X1666,skf4(X1666)) ),
inference(resolution,[status(thm)],[c1161,c383]) ).
cnf(c1167,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1668)
| ~ jules_forename(skc12,X1668)
| ~ of(skc12,X1668,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1669)
| ~ accessible_world(skc12,X1669)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1669)
| ~ forename(skc12,X1667)
| ~ jules_forename(skc12,X1667)
| ~ of(skc12,X1667,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1667)
| ~ actual_world(skc12)
| man(X1669,skf4(X1669)) ),
inference(resolution,[status(thm)],[c1166,c361]) ).
cnf(c1168,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1672)
| ~ jules_forename(skc12,X1672)
| ~ of(skc12,X1672,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1671)
| ~ accessible_world(skc12,X1671)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1671)
| ~ forename(skc12,X1670)
| ~ jules_forename(skc12,X1670)
| ~ of(skc12,X1670,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1670)
| ~ actual_world(skc12)
| man(X1671,skf4(X1671)) ),
inference(resolution,[status(thm)],[c1167,c369]) ).
cnf(c1169,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1678)
| ~ jules_forename(skc12,X1678)
| ~ of(skc12,X1678,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1679)
| ~ accessible_world(skc12,X1679)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1679)
| ~ forename(skc12,X1677)
| ~ jules_forename(skc12,X1677)
| ~ of(skc12,X1677,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1677)
| ~ actual_world(skc12)
| man(X1679,skf4(X1679)) ),
inference(resolution,[status(thm)],[c1168,c359]) ).
cnf(c1171,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1680)
| ~ jules_forename(skc12,X1680)
| ~ of(skc12,X1680,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1681)
| ~ accessible_world(skc12,X1681)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1681)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1681,skf4(X1681)) ),
inference(resolution,[status(thm)],[c1169,c579]) ).
cnf(c1117,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1673)
| ~ jules_forename(skc12,X1673)
| ~ of(skc12,X1673,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1675)
| ~ accessible_world(skc12,X1675)
| ~ think_believe_consider(skc12,X1676)
| ~ present(skc12,X1676)
| ~ event(skc12,X1676)
| ~ theme(skc12,X1676,X1675)
| ~ forename(skc12,X1674)
| ~ jules_forename(skc12,X1674)
| ~ of(skc12,X1674,skc10)
| ~ smoke(skc12,X1676)
| ~ agent(skc12,X1676,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,X1673)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ actual_world(skc12)
| man(X1675,skf4(X1675)) ),
inference(factor,[status(thm)],[c1077]) ).
cnf(c1039,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1524)
| ~ jules_forename(skc8,X1524)
| ~ of(skc8,X1524,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1521)
| ~ accessible_world(skc8,X1521)
| ~ think_believe_consider(skc8,X1522)
| ~ present(skc8,X1522)
| ~ event(skc8,X1522)
| ~ theme(skc8,X1522,X1521)
| ~ forename(skc8,X1523)
| ~ jules_forename(skc8,X1523)
| ~ of(skc8,X1523,skc10)
| ~ smoke(skc12,X1525)
| ~ present(skc12,X1525)
| ~ agent(skc12,X1525,skc10)
| ~ event(skc12,X1525)
| ~ agent(skc8,skc13,skc10)
| ~ agent(skc8,X1522,skc10)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(X1521,skf4(X1521)) ),
inference(resolution,[status(thm)],[c699,clause88]) ).
cnf(c1112,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1653)
| ~ jules_forename(skc8,X1653)
| ~ of(skc8,X1653,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1656)
| ~ accessible_world(skc8,X1656)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1656)
| ~ forename(skc8,X1654)
| ~ jules_forename(skc8,X1654)
| ~ of(skc8,X1654,skc10)
| ~ smoke(skc12,X1655)
| ~ present(skc12,X1655)
| ~ agent(skc12,X1655,skc10)
| ~ event(skc12,X1655)
| ~ agent(skc8,skc13,skc10)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1656,skf4(X1656)) ),
inference(factor,[status(thm)],[c1039]) ).
cnf(c1160,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1645)
| ~ jules_forename(skc12,X1645)
| ~ of(skc12,X1645,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1646)
| ~ accessible_world(skc12,X1646)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1646)
| ~ forename(skc12,X1643)
| ~ jules_forename(skc12,X1643)
| ~ of(skc12,X1643,X1644)
| ~ smoke(skc12,skc13)
| ~ agent(skc12,skc13,X1644)
| ~ man(skc12,X1644)
| ~ vincent_forename(skc12,X1643)
| ~ actual_world(skc12)
| man(X1646,skf4(X1646)) ),
inference(factor,[status(thm)],[c1126]) ).
cnf(c1037,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1494)
| ~ jules_forename(skc8,X1494)
| ~ of(skc8,X1494,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1492)
| ~ accessible_world(skc8,X1492)
| ~ think_believe_consider(skc8,X1493)
| ~ present(skc8,X1493)
| ~ event(skc8,X1493)
| ~ theme(skc8,X1493,X1492)
| ~ forename(skc8,X1495)
| ~ jules_forename(skc8,X1495)
| ~ of(skc8,X1495,X1491)
| ~ smoke(skc12,X1496)
| ~ present(skc12,X1496)
| ~ agent(skc12,X1496,X1491)
| ~ event(skc12,X1496)
| ~ agent(skc8,skc13,X1491)
| ~ agent(skc8,X1493,X1491)
| ~ man(skc8,X1491)
| ~ vincent_forename(skc8,X1495)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(X1492,skf4(X1492)) ),
inference(factor,[status(thm)],[c699]) ).
cnf(c1099,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1588)
| ~ jules_forename(skc8,X1588)
| ~ of(skc8,X1588,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1586)
| ~ accessible_world(skc8,X1586)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1586)
| ~ forename(skc8,X1584)
| ~ jules_forename(skc8,X1584)
| ~ of(skc8,X1584,X1585)
| ~ smoke(skc12,X1587)
| ~ present(skc12,X1587)
| ~ agent(skc12,X1587,X1585)
| ~ event(skc12,X1587)
| ~ agent(skc8,skc13,X1585)
| ~ man(skc8,X1585)
| ~ vincent_forename(skc8,X1584)
| ~ actual_world(skc8)
| man(X1586,skf4(X1586)) ),
inference(factor,[status(thm)],[c1037]) ).
cnf(c1146,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1597)
| ~ jules_forename(skc8,X1597)
| ~ of(skc8,X1597,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1594)
| ~ accessible_world(skc8,X1594)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1594)
| ~ forename(skc8,X1596)
| ~ jules_forename(skc8,X1596)
| ~ of(skc8,X1596,skc15)
| ~ smoke(skc12,X1595)
| ~ present(skc12,X1595)
| ~ agent(skc12,X1595,skc15)
| ~ event(skc12,X1595)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1596)
| ~ actual_world(skc8)
| man(X1594,skf4(X1594)) ),
inference(resolution,[status(thm)],[c1099,clause86]) ).
cnf(c1150,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1617)
| ~ jules_forename(skc8,X1617)
| ~ of(skc8,X1617,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1616)
| ~ accessible_world(skc8,X1616)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1616)
| ~ forename(skc8,X1615)
| ~ jules_forename(skc8,X1615)
| ~ of(skc8,X1615,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1615)
| ~ actual_world(skc8)
| man(X1616,skf4(X1616)) ),
inference(resolution,[status(thm)],[c1146,c383]) ).
cnf(c1154,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1623)
| ~ jules_forename(skc8,X1623)
| ~ of(skc8,X1623,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1624)
| ~ accessible_world(skc8,X1624)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1624)
| ~ forename(skc8,X1622)
| ~ jules_forename(skc8,X1622)
| ~ of(skc8,X1622,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1622)
| ~ actual_world(skc8)
| man(X1624,skf4(X1624)) ),
inference(resolution,[status(thm)],[c1150,c361]) ).
cnf(c1156,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1625)
| ~ jules_forename(skc8,X1625)
| ~ of(skc8,X1625,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1626)
| ~ accessible_world(skc8,X1626)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1626)
| ~ forename(skc8,X1627)
| ~ jules_forename(skc8,X1627)
| ~ of(skc8,X1627,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1627)
| ~ actual_world(skc8)
| man(X1626,skf4(X1626)) ),
inference(resolution,[status(thm)],[c1154,c369]) ).
cnf(c1157,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1630)
| ~ jules_forename(skc8,X1630)
| ~ of(skc8,X1630,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1628)
| ~ accessible_world(skc8,X1628)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1628)
| ~ forename(skc8,X1629)
| ~ jules_forename(skc8,X1629)
| ~ of(skc8,X1629,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1629)
| ~ actual_world(skc8)
| man(X1628,skf4(X1628)) ),
inference(resolution,[status(thm)],[c1156,c359]) ).
cnf(c1158,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1632)
| ~ jules_forename(skc8,X1632)
| ~ of(skc8,X1632,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1631)
| ~ accessible_world(skc8,X1631)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1631)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1631,skf4(X1631)) ),
inference(resolution,[status(thm)],[c1157,clause85]) ).
cnf(c1118,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1608)
| ~ jules_forename(skc12,X1608)
| ~ of(skc12,X1608,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1610)
| ~ accessible_world(skc12,X1610)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1610)
| ~ forename(skc12,X1611)
| ~ jules_forename(skc12,X1611)
| ~ of(skc12,X1611,skc10)
| ~ smoke(skc12,X1609)
| ~ present(skc12,X1609)
| ~ agent(skc12,X1609,skc10)
| ~ event(skc12,X1609)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,X1608)
| ~ actual_world(skc12)
| man(X1610,skf4(X1610)) ),
inference(factor,[status(thm)],[c1077]) ).
cnf(c1153,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1614)
| ~ jules_forename(skc12,X1614)
| ~ of(skc12,X1614,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ proposition(skc12,X1612)
| ~ accessible_world(skc12,X1612)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1612)
| ~ forename(skc12,X1613)
| ~ jules_forename(skc12,X1613)
| ~ of(skc12,X1613,skc10)
| ~ smoke(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ vincent_forename(skc12,X1614)
| ~ actual_world(skc12)
| man(X1612,skf4(X1612)) ),
inference(factor,[status(thm)],[c1118]) ).
cnf(c921,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1359)
| ~ jules_forename(skc12,X1359)
| ~ of(skc12,X1359,skc10)
| ~ accessible_world(skc12,X1358)
| ~ proposition(skc12,X1358)
| ~ think_believe_consider(skc12,X1361)
| ~ present(skc12,X1361)
| ~ event(skc12,X1361)
| ~ theme(skc12,X1361,X1358)
| ~ forename(skc12,X1362)
| ~ jules_forename(skc12,X1362)
| ~ of(skc12,X1362,X1360)
| ~ smoke(X1358,X1357)
| ~ present(X1358,X1357)
| ~ agent(X1358,X1357,X1360)
| ~ event(X1358,X1357)
| ~ agent(skc12,X1361,X1360)
| ~ man(skc12,X1360)
| ~ of(skc12,X1356,X1360)
| ~ vincent_forename(skc12,X1356)
| ~ forename(skc12,X1356)
| ~ actual_world(skc12)
| man(X1358,skf4(X1358)) ),
inference(factor,[status(thm)],[c590]) ).
cnf(c1058,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1481)
| ~ jules_forename(skc12,X1481)
| ~ of(skc12,X1481,skc10)
| ~ accessible_world(skc12,X1484)
| ~ proposition(skc12,X1484)
| ~ think_believe_consider(skc12,X1485)
| ~ present(skc12,X1485)
| ~ event(skc12,X1485)
| ~ theme(skc12,X1485,X1484)
| ~ forename(skc12,X1483)
| ~ jules_forename(skc12,X1483)
| ~ of(skc12,X1483,skc15)
| ~ smoke(X1484,X1482)
| ~ present(X1484,X1482)
| ~ agent(X1484,X1482,skc15)
| ~ event(X1484,X1482)
| ~ agent(skc12,X1485,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1484,skf4(X1484)) ),
inference(resolution,[status(thm)],[c921,c579]) ).
cnf(c1094,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1500)
| ~ jules_forename(skc12,X1500)
| ~ of(skc12,X1500,skc10)
| ~ accessible_world(skc12,X1501)
| ~ proposition(skc12,X1501)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1501)
| ~ forename(skc12,X1499)
| ~ jules_forename(skc12,X1499)
| ~ of(skc12,X1499,skc15)
| ~ smoke(X1501,X1498)
| ~ present(X1501,X1498)
| ~ agent(X1501,X1498,skc15)
| ~ event(X1501,X1498)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1501,skf4(X1501)) ),
inference(resolution,[status(thm)],[c1058,c570]) ).
cnf(c1102,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1581)
| ~ jules_forename(skc12,X1581)
| ~ of(skc12,X1581,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1580)
| ~ jules_forename(skc12,X1580)
| ~ of(skc12,X1580,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1094,c383]) ).
cnf(c1144,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1583)
| ~ jules_forename(skc12,X1583)
| ~ of(skc12,X1583,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1582)
| ~ jules_forename(skc12,X1582)
| ~ of(skc12,X1582,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1102,c361]) ).
cnf(c1145,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1590)
| ~ jules_forename(skc12,X1590)
| ~ of(skc12,X1590,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1589)
| ~ jules_forename(skc12,X1589)
| ~ of(skc12,X1589,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1144,c369]) ).
cnf(c1147,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1591)
| ~ jules_forename(skc12,X1591)
| ~ of(skc12,X1591,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1592)
| ~ jules_forename(skc12,X1592)
| ~ of(skc12,X1592,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1145,c359]) ).
cnf(c1036,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1471)
| ~ jules_forename(skc8,X1471)
| ~ of(skc8,X1471,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1468)
| ~ accessible_world(skc8,X1468)
| ~ think_believe_consider(skc8,X1469)
| ~ present(skc8,X1469)
| ~ event(skc8,X1469)
| ~ theme(skc8,X1469,X1468)
| ~ forename(skc8,X1470)
| ~ jules_forename(skc8,X1470)
| ~ of(skc8,X1470,skc10)
| ~ smoke(skc12,X1472)
| ~ present(skc12,X1472)
| ~ agent(skc12,X1472,skc10)
| ~ event(skc12,X1472)
| ~ agent(skc8,skc13,skc10)
| ~ agent(skc8,X1469,skc10)
| ~ vincent_forename(skc8,X1471)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(X1468,skf4(X1468)) ),
inference(factor,[status(thm)],[c699]) ).
cnf(c1092,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1579)
| ~ jules_forename(skc8,X1579)
| ~ of(skc8,X1579,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ proposition(skc8,X1577)
| ~ accessible_world(skc8,X1577)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1577)
| ~ forename(skc8,X1578)
| ~ jules_forename(skc8,X1578)
| ~ of(skc8,X1578,skc10)
| ~ smoke(skc12,X1576)
| ~ present(skc12,X1576)
| ~ agent(skc12,X1576,skc10)
| ~ event(skc12,X1576)
| ~ agent(skc8,skc13,skc10)
| ~ vincent_forename(skc8,X1579)
| ~ actual_world(skc8)
| man(X1577,skf4(X1577)) ),
inference(factor,[status(thm)],[c1036]) ).
cnf(c698,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1253)
| ~ jules_forename(skc8,X1253)
| ~ of(skc8,X1253,skc10)
| ~ accessible_world(skc8,X1259)
| ~ proposition(skc8,X1259)
| ~ think_believe_consider(skc8,X1256)
| ~ present(skc8,X1256)
| ~ event(skc8,X1256)
| ~ theme(skc8,X1256,X1259)
| ~ forename(skc8,X1258)
| ~ jules_forename(skc8,X1258)
| ~ of(skc8,X1258,X1257)
| ~ smoke(X1259,X1254)
| ~ present(X1259,X1254)
| ~ agent(X1259,X1254,X1257)
| ~ event(X1259,X1254)
| ~ agent(skc8,X1256,X1257)
| ~ man(skc8,X1257)
| ~ of(skc8,X1255,X1257)
| ~ vincent_forename(skc8,X1255)
| ~ forename(skc8,X1255)
| ~ actual_world(skc8)
| man(X1259,skf4(X1259)) ),
inference(factor,[status(thm)],[c396]) ).
cnf(c1029,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1455)
| ~ jules_forename(skc8,X1455)
| ~ of(skc8,X1455,skc10)
| ~ accessible_world(skc8,X1452)
| ~ proposition(skc8,X1452)
| ~ think_believe_consider(skc8,X1454)
| ~ present(skc8,X1454)
| ~ event(skc8,X1454)
| ~ theme(skc8,X1454,X1452)
| ~ forename(skc8,X1451)
| ~ jules_forename(skc8,X1451)
| ~ of(skc8,X1451,skc15)
| ~ smoke(X1452,X1453)
| ~ present(X1452,X1453)
| ~ agent(X1452,X1453,skc15)
| ~ event(X1452,X1453)
| ~ agent(skc8,X1454,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1452,skf4(X1452)) ),
inference(resolution,[status(thm)],[c698,clause85]) ).
cnf(c1086,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1462)
| ~ jules_forename(skc8,X1462)
| ~ of(skc8,X1462,skc10)
| ~ accessible_world(skc8,X1464)
| ~ proposition(skc8,X1464)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1464)
| ~ forename(skc8,X1463)
| ~ jules_forename(skc8,X1463)
| ~ of(skc8,X1463,skc15)
| ~ smoke(X1464,X1465)
| ~ present(X1464,X1465)
| ~ agent(X1464,X1465,skc15)
| ~ event(X1464,X1465)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1464,skf4(X1464)) ),
inference(resolution,[status(thm)],[c1029,clause86]) ).
cnf(c1090,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1562)
| ~ jules_forename(skc8,X1562)
| ~ of(skc8,X1562,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1563)
| ~ jules_forename(skc8,X1563)
| ~ of(skc8,X1563,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1086,c383]) ).
cnf(c1136,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1564)
| ~ jules_forename(skc8,X1564)
| ~ of(skc8,X1564,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1565)
| ~ jules_forename(skc8,X1565)
| ~ of(skc8,X1565,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1090,c361]) ).
cnf(c1137,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1566)
| ~ jules_forename(skc8,X1566)
| ~ of(skc8,X1566,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1567)
| ~ jules_forename(skc8,X1567)
| ~ of(skc8,X1567,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1136,c369]) ).
cnf(c1138,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1573)
| ~ jules_forename(skc8,X1573)
| ~ of(skc8,X1573,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1574)
| ~ jules_forename(skc8,X1574)
| ~ of(skc8,X1574,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1137,c359]) ).
cnf(c1095,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1560)
| ~ jules_forename(skc12,X1560)
| ~ of(skc12,X1560,skc10)
| ~ accessible_world(skc12,X1561)
| ~ proposition(skc12,X1561)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1561)
| ~ forename(skc12,X1559)
| ~ jules_forename(skc12,X1559)
| ~ of(skc12,X1559,skc15)
| ~ smoke(X1561,X1558)
| ~ present(X1561,X1558)
| ~ agent(X1561,X1558,skc15)
| ~ event(X1561,X1558)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(X1561,skf4(X1561)) ),
inference(resolution,[status(thm)],[c1058,c383]) ).
cnf(c1103,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1551)
| ~ jules_forename(skc12,X1551)
| ~ of(skc12,X1551,skc10)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc8)
| ~ forename(skc12,X1550)
| ~ jules_forename(skc12,X1550)
| ~ of(skc12,X1550,skc15)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1094,clause86]) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
cnf(clause64,axiom,
( ~ accessible_world(X223,X225)
| ~ vincent_forename(X223,X224)
| vincent_forename(X225,X224) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
cnf(c310,plain,
( ~ accessible_world(skc8,X410)
| vincent_forename(X410,skc14) ),
inference(resolution,[status(thm)],[clause64,clause75]) ).
cnf(c522,plain,
vincent_forename(skc12,skc14),
inference(resolution,[status(thm)],[c310,clause83]) ).
cnf(c1056,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1385)
| ~ jules_forename(skc12,X1385)
| ~ of(skc12,X1385,skc10)
| ~ accessible_world(skc12,X1386)
| ~ proposition(skc12,X1386)
| ~ think_believe_consider(skc12,X1387)
| ~ present(skc12,X1387)
| ~ event(skc12,X1387)
| ~ theme(skc12,X1387,X1386)
| ~ forename(skc12,X1382)
| ~ jules_forename(skc12,X1382)
| ~ of(skc12,X1382,X1383)
| ~ smoke(X1386,X1384)
| ~ present(X1386,X1384)
| ~ agent(X1386,X1384,X1383)
| ~ event(X1386,X1384)
| ~ agent(skc12,X1387,X1383)
| ~ man(skc12,X1383)
| ~ vincent_forename(skc12,X1382)
| ~ actual_world(skc12)
| man(X1386,skf4(X1386)) ),
inference(factor,[status(thm)],[c921]) ).
cnf(c1063,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1418)
| ~ jules_forename(skc12,X1418)
| ~ of(skc12,X1418,skc10)
| ~ accessible_world(skc12,X1416)
| ~ proposition(skc12,X1416)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,X1416)
| ~ forename(skc12,X1415)
| ~ jules_forename(skc12,X1415)
| ~ of(skc12,X1415,skc15)
| ~ smoke(X1416,X1417)
| ~ present(X1416,X1417)
| ~ agent(X1416,X1417,skc15)
| ~ event(X1416,X1417)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1415)
| ~ actual_world(skc12)
| man(X1416,skf4(X1416)) ),
inference(resolution,[status(thm)],[c1056,c570]) ).
cnf(c1075,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1526)
| ~ jules_forename(skc12,X1526)
| ~ of(skc12,X1526,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1527)
| ~ jules_forename(skc12,X1527)
| ~ of(skc12,X1527,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1527)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1063,c383]) ).
cnf(c1115,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1528)
| ~ jules_forename(skc12,X1528)
| ~ of(skc12,X1528,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1529)
| ~ jules_forename(skc12,X1529)
| ~ of(skc12,X1529,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1529)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1075,c361]) ).
cnf(c1116,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1536)
| ~ jules_forename(skc12,X1536)
| ~ of(skc12,X1536,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1535)
| ~ jules_forename(skc12,X1535)
| ~ of(skc12,X1535,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1535)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1115,c369]) ).
cnf(c1120,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1538)
| ~ jules_forename(skc12,X1538)
| ~ of(skc12,X1538,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,X1537)
| ~ jules_forename(skc12,X1537)
| ~ of(skc12,X1537,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1537)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1116,c359]) ).
cnf(c1121,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1539)
| ~ jules_forename(skc12,X1539)
| ~ of(skc12,X1539,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc12)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1120,c579]) ).
cnf(c1122,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1540)
| ~ jules_forename(skc12,X1540)
| ~ of(skc12,X1540,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1121,c573]) ).
cnf(c1123,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1122,c582]) ).
cnf(c1124,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ man(skc12,skc15)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1123,c522]) ).
cnf(c1130,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,skc11)
| ~ jules_forename(skc12,skc11)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1124,c379]) ).
cnf(c1028,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1273)
| ~ jules_forename(skc8,X1273)
| ~ of(skc8,X1273,skc10)
| ~ accessible_world(skc8,X1268)
| ~ proposition(skc8,X1268)
| ~ think_believe_consider(skc8,X1272)
| ~ present(skc8,X1272)
| ~ event(skc8,X1272)
| ~ theme(skc8,X1272,X1268)
| ~ forename(skc8,X1270)
| ~ jules_forename(skc8,X1270)
| ~ of(skc8,X1270,X1269)
| ~ smoke(X1268,X1271)
| ~ present(X1268,X1271)
| ~ agent(X1268,X1271,X1269)
| ~ event(X1268,X1271)
| ~ agent(skc8,X1272,X1269)
| ~ man(skc8,X1269)
| ~ vincent_forename(skc8,X1270)
| ~ actual_world(skc8)
| man(X1268,skf4(X1268)) ),
inference(factor,[status(thm)],[c698]) ).
cnf(c1033,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1289)
| ~ jules_forename(skc8,X1289)
| ~ of(skc8,X1289,skc10)
| ~ accessible_world(skc8,X1290)
| ~ proposition(skc8,X1290)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1290)
| ~ forename(skc8,X1291)
| ~ jules_forename(skc8,X1291)
| ~ of(skc8,X1291,skc15)
| ~ smoke(X1290,X1288)
| ~ present(X1290,X1288)
| ~ agent(X1290,X1288,skc15)
| ~ event(X1290,X1288)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1291)
| ~ actual_world(skc8)
| man(X1290,skf4(X1290)) ),
inference(resolution,[status(thm)],[c1028,clause86]) ).
cnf(c1041,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1507)
| ~ jules_forename(skc8,X1507)
| ~ of(skc8,X1507,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1506)
| ~ jules_forename(skc8,X1506)
| ~ of(skc8,X1506,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1506)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1033,c383]) ).
cnf(c1104,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1514)
| ~ jules_forename(skc8,X1514)
| ~ of(skc8,X1514,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1513)
| ~ jules_forename(skc8,X1513)
| ~ of(skc8,X1513,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1513)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1041,c361]) ).
cnf(c1107,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1515)
| ~ jules_forename(skc8,X1515)
| ~ of(skc8,X1515,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1516)
| ~ jules_forename(skc8,X1516)
| ~ of(skc8,X1516,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1516)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1104,c369]) ).
cnf(c1108,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1518)
| ~ jules_forename(skc8,X1518)
| ~ of(skc8,X1518,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,X1517)
| ~ jules_forename(skc8,X1517)
| ~ of(skc8,X1517,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1517)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1107,c359]) ).
cnf(c1109,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1519)
| ~ jules_forename(skc8,X1519)
| ~ of(skc8,X1519,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1108,clause85]) ).
cnf(c1110,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1520)
| ~ jules_forename(skc8,X1520)
| ~ of(skc8,X1520,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1109,clause87]) ).
cnf(c1111,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1110,clause88]) ).
cnf(c1113,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ man(skc8,skc15)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1111,clause75]) ).
cnf(c1114,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1113,clause73]) ).
cnf(c1093,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1487)
| ~ jules_forename(skc12,X1487)
| ~ of(skc12,X1487,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1488)
| ~ present(skc12,X1488)
| ~ event(skc12,X1488)
| ~ theme(skc12,X1488,skc12)
| ~ forename(skc12,X1486)
| ~ jules_forename(skc12,X1486)
| ~ of(skc12,X1486,skc15)
| ~ smoke(skc12,X1488)
| ~ agent(skc12,X1488,skc15)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1058]) ).
cnf(c1097,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1505)
| ~ jules_forename(skc12,X1505)
| ~ of(skc12,X1505,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),skc12)
| ~ forename(skc12,X1504)
| ~ jules_forename(skc12,X1504)
| ~ of(skc12,X1504,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1093,c383]) ).
cnf(c1057,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1438)
| ~ jules_forename(skc12,X1438)
| ~ of(skc12,X1438,skc10)
| ~ accessible_world(skc12,X1441)
| ~ proposition(skc12,X1441)
| ~ think_believe_consider(skc12,X1442)
| ~ present(skc12,X1442)
| ~ event(skc12,X1442)
| ~ theme(skc12,X1442,X1441)
| ~ forename(skc12,X1440)
| ~ jules_forename(skc12,X1440)
| ~ of(skc12,X1440,skc10)
| ~ smoke(X1441,X1439)
| ~ present(X1441,X1439)
| ~ agent(X1441,X1439,skc10)
| ~ event(X1441,X1439)
| ~ agent(skc12,X1442,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1441,skf4(X1441)) ),
inference(resolution,[status(thm)],[c921,c582]) ).
cnf(c1082,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1480)
| ~ jules_forename(skc12,X1480)
| ~ of(skc12,X1480,skc10)
| ~ accessible_world(skc12,X1477)
| ~ proposition(skc12,X1477)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1477)
| ~ forename(skc12,X1479)
| ~ jules_forename(skc12,X1479)
| ~ of(skc12,X1479,skc10)
| ~ smoke(X1477,X1478)
| ~ present(X1477,X1478)
| ~ agent(X1477,X1478,skc10)
| ~ event(X1477,X1478)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1477,skf4(X1477)) ),
inference(resolution,[status(thm)],[c1057,c384]) ).
cnf(c1064,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1476)
| ~ jules_forename(skc12,X1476)
| ~ of(skc12,X1476,skc10)
| ~ accessible_world(skc12,X1474)
| ~ proposition(skc12,X1474)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1474)
| ~ forename(skc12,X1473)
| ~ jules_forename(skc12,X1473)
| ~ of(skc12,X1473,skc15)
| ~ smoke(X1474,X1475)
| ~ present(X1474,X1475)
| ~ agent(X1474,X1475,skc15)
| ~ event(X1474,X1475)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1473)
| ~ actual_world(skc12)
| man(X1474,skf4(X1474)) ),
inference(resolution,[status(thm)],[c1056,c383]) ).
cnf(c1085,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1456)
| ~ jules_forename(skc8,X1456)
| ~ of(skc8,X1456,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1457)
| ~ present(skc8,X1457)
| ~ event(skc8,X1457)
| ~ theme(skc8,X1457,skc8)
| ~ forename(skc8,X1458)
| ~ jules_forename(skc8,X1458)
| ~ of(skc8,X1458,skc15)
| ~ smoke(skc8,X1457)
| ~ agent(skc8,X1457,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1029]) ).
cnf(c1087,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1460)
| ~ jules_forename(skc8,X1460)
| ~ of(skc8,X1460,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc8)
| ~ forename(skc8,X1459)
| ~ jules_forename(skc8,X1459)
| ~ of(skc8,X1459,skc15)
| ~ smoke(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1085,clause86]) ).
cnf(c1076,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1448)
| ~ jules_forename(skc12,X1448)
| ~ of(skc12,X1448,skc10)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc8)
| ~ forename(skc12,X1449)
| ~ jules_forename(skc12,X1449)
| ~ of(skc12,X1449,skc15)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1449)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1063,clause86]) ).
cnf(c1084,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1450)
| ~ jules_forename(skc12,X1450)
| ~ of(skc12,X1450,skc10)
| ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ think_believe_consider(skc12,skc13)
| ~ present(skc12,skc13)
| ~ event(skc12,skc13)
| ~ theme(skc12,skc13,skc8)
| ~ forename(skc12,skc14)
| ~ jules_forename(skc12,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,skc14)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1076,c579]) ).
cnf(c1081,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1445)
| ~ jules_forename(skc12,X1445)
| ~ of(skc12,X1445,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1443)
| ~ present(skc12,X1443)
| ~ event(skc12,X1443)
| ~ theme(skc12,X1443,skc12)
| ~ forename(skc12,X1444)
| ~ jules_forename(skc12,X1444)
| ~ of(skc12,X1444,skc10)
| ~ smoke(skc12,X1443)
| ~ agent(skc12,X1443,skc10)
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1057]) ).
cnf(c1083,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1446)
| ~ jules_forename(skc12,X1446)
| ~ of(skc12,X1446,skc10)
| ~ 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)
| ~ forename(skc12,X1447)
| ~ jules_forename(skc12,X1447)
| ~ of(skc12,X1447,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ vincent_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1081,c384]) ).
cnf(c1062,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1391)
| ~ jules_forename(skc12,X1391)
| ~ of(skc12,X1391,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1390)
| ~ present(skc12,X1390)
| ~ event(skc12,X1390)
| ~ theme(skc12,X1390,skc12)
| ~ forename(skc12,X1388)
| ~ jules_forename(skc12,X1388)
| ~ of(skc12,X1388,X1389)
| ~ smoke(skc12,X1390)
| ~ agent(skc12,X1390,X1389)
| ~ man(skc12,X1389)
| ~ vincent_forename(skc12,X1388)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1056]) ).
cnf(c1067,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1430)
| ~ jules_forename(skc12,X1430)
| ~ of(skc12,X1430,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ present(skc12,skf2(skc15))
| ~ event(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),skc12)
| ~ forename(skc12,X1429)
| ~ jules_forename(skc12,X1429)
| ~ of(skc12,X1429,skc15)
| ~ smoke(skc12,skf2(skc15))
| ~ man(skc12,skc15)
| ~ vincent_forename(skc12,X1429)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1062,c383]) ).
cnf(c1055,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1363)
| ~ jules_forename(skc12,X1363)
| ~ of(skc12,X1363,skc10)
| ~ accessible_world(skc12,X1366)
| ~ proposition(skc12,X1366)
| ~ think_believe_consider(skc12,X1367)
| ~ present(skc12,X1367)
| ~ event(skc12,X1367)
| ~ theme(skc12,X1367,X1366)
| ~ forename(skc12,X1365)
| ~ jules_forename(skc12,X1365)
| ~ of(skc12,X1365,skc10)
| ~ smoke(X1366,X1364)
| ~ present(X1366,X1364)
| ~ agent(X1366,X1364,skc10)
| ~ event(X1366,X1364)
| ~ agent(skc12,X1367,skc10)
| ~ vincent_forename(skc12,X1363)
| ~ actual_world(skc12)
| man(X1366,skf4(X1366)) ),
inference(factor,[status(thm)],[c921]) ).
cnf(c1060,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1422)
| ~ jules_forename(skc12,X1422)
| ~ of(skc12,X1422,skc10)
| ~ accessible_world(skc12,X1423)
| ~ proposition(skc12,X1423)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1423)
| ~ forename(skc12,X1424)
| ~ jules_forename(skc12,X1424)
| ~ of(skc12,X1424,skc10)
| ~ smoke(X1423,X1421)
| ~ present(X1423,X1421)
| ~ agent(X1423,X1421,skc10)
| ~ event(X1423,X1421)
| ~ vincent_forename(skc12,X1422)
| ~ actual_world(skc12)
| man(X1423,skf4(X1423)) ),
inference(resolution,[status(thm)],[c1055,c384]) ).
cnf(c1059,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1369)
| ~ jules_forename(skc12,X1369)
| ~ of(skc12,X1369,skc10)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ think_believe_consider(skc12,X1368)
| ~ present(skc12,X1368)
| ~ event(skc12,X1368)
| ~ theme(skc12,X1368,skc12)
| ~ forename(skc12,X1370)
| ~ jules_forename(skc12,X1370)
| ~ of(skc12,X1370,skc10)
| ~ smoke(skc12,X1368)
| ~ agent(skc12,X1368,skc10)
| ~ vincent_forename(skc12,X1369)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1055]) ).
cnf(c1061,plain,
( ~ state(skc12,skc9)
| ~ man(skc12,skc10)
| ~ forename(skc12,X1380)
| ~ jules_forename(skc12,X1380)
| ~ of(skc12,X1380,skc10)
| ~ 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)
| ~ forename(skc12,X1381)
| ~ jules_forename(skc12,X1381)
| ~ of(skc12,X1381,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ vincent_forename(skc12,X1380)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1059,c384]) ).
cnf(clause95,negated_conjecture,
( ~ state(X312,X307)
| ~ man(X312,X302)
| ~ be(X312,X307,X302,X302)
| ~ forename(X312,X301)
| ~ jules_forename(X312,X301)
| ~ of(X312,X301,X302)
| ~ accessible_world(X312,X310)
| ~ proposition(X312,X310)
| ~ proposition(X312,X306)
| ~ accessible_world(X312,X306)
| ~ smoke(X306,X303)
| ~ present(X306,X303)
| ~ agent(X306,X303,skf4(X306))
| ~ event(X306,X303)
| ~ think_believe_consider(X312,X304)
| ~ present(X312,X304)
| ~ event(X312,X304)
| ~ theme(X312,X304,X306)
| ~ forename(X312,X309)
| ~ jules_forename(X312,X309)
| ~ of(X312,X309,X308)
| ~ smoke(X310,X311)
| ~ present(X310,X311)
| ~ agent(X310,X311,X308)
| ~ event(X310,X311)
| ~ agent(X312,X313,X308)
| ~ agent(X312,X304,X308)
| ~ man(X312,X308)
| ~ of(X312,X305,X308)
| ~ vincent_forename(X312,X305)
| ~ forename(X312,X305)
| ~ theme(X312,X313,X310)
| ~ event(X312,X313)
| ~ present(X312,X313)
| ~ think_believe_consider(X312,X313)
| ~ actual_world(X312) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
cnf(c405,plain,
( ~ state(X689,X696)
| ~ man(X689,X692)
| ~ be(X689,X696,X692,X692)
| ~ forename(X689,X695)
| ~ jules_forename(X689,X695)
| ~ of(X689,X695,X692)
| ~ accessible_world(X689,X697)
| ~ proposition(X689,X697)
| ~ smoke(X697,X690)
| ~ present(X697,X690)
| ~ agent(X697,X690,skf4(X697))
| ~ event(X697,X690)
| ~ think_believe_consider(X689,X691)
| ~ present(X689,X691)
| ~ event(X689,X691)
| ~ theme(X689,X691,X697)
| ~ forename(X689,X693)
| ~ jules_forename(X689,X693)
| ~ of(X689,X693,skf4(X697))
| ~ agent(X689,X688,skf4(X697))
| ~ agent(X689,X691,skf4(X697))
| ~ man(X689,skf4(X697))
| ~ of(X689,X694,skf4(X697))
| ~ vincent_forename(X689,X694)
| ~ forename(X689,X694)
| ~ theme(X689,X688,X697)
| ~ event(X689,X688)
| ~ present(X689,X688)
| ~ think_believe_consider(X689,X688)
| ~ actual_world(X689) ),
inference(factor,[status(thm)],[clause95]) ).
cnf(c705,plain,
( ~ state(X1320,X1321)
| ~ man(X1320,X1315)
| ~ be(X1320,X1321,X1315,X1315)
| ~ forename(X1320,X1322)
| ~ jules_forename(X1320,X1322)
| ~ of(X1320,X1322,X1315)
| ~ accessible_world(X1320,X1319)
| ~ proposition(X1320,X1319)
| ~ smoke(X1319,X1316)
| ~ present(X1319,X1316)
| ~ agent(X1319,X1316,skf4(X1319))
| ~ event(X1319,X1316)
| ~ think_believe_consider(X1320,X1317)
| ~ present(X1320,X1317)
| ~ event(X1320,X1317)
| ~ theme(X1320,X1317,X1319)
| ~ forename(X1320,X1318)
| ~ jules_forename(X1320,X1318)
| ~ of(X1320,X1318,skf4(X1319))
| ~ agent(X1320,X1314,skf4(X1319))
| ~ agent(X1320,X1317,skf4(X1319))
| ~ man(X1320,skf4(X1319))
| ~ vincent_forename(X1320,X1318)
| ~ theme(X1320,X1314,X1319)
| ~ event(X1320,X1314)
| ~ present(X1320,X1314)
| ~ think_believe_consider(X1320,X1314)
| ~ actual_world(X1320) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1050,plain,
( ~ state(X1328,X1327)
| ~ man(X1328,X1323)
| ~ be(X1328,X1327,X1323,X1323)
| ~ forename(X1328,X1330)
| ~ jules_forename(X1328,X1330)
| ~ of(X1328,X1330,X1323)
| ~ accessible_world(X1328,X1324)
| ~ proposition(X1328,X1324)
| ~ smoke(X1324,X1326)
| ~ present(X1324,X1326)
| ~ agent(X1324,X1326,skf4(X1324))
| ~ event(X1324,X1326)
| ~ think_believe_consider(X1328,X1329)
| ~ present(X1328,X1329)
| ~ event(X1328,X1329)
| ~ theme(X1328,X1329,X1324)
| ~ forename(X1328,X1325)
| ~ jules_forename(X1328,X1325)
| ~ of(X1328,X1325,skf4(X1324))
| ~ agent(X1328,X1329,skf4(X1324))
| ~ man(X1328,skf4(X1324))
| ~ vincent_forename(X1328,X1325)
| ~ actual_world(X1328) ),
inference(factor,[status(thm)],[c705]) ).
cnf(c1053,plain,
( ~ state(X1335,X1334)
| ~ man(X1335,X1336)
| ~ be(X1335,X1334,X1336,X1336)
| ~ forename(X1335,X1332)
| ~ jules_forename(X1335,X1332)
| ~ of(X1335,X1332,X1336)
| ~ accessible_world(X1335,X1335)
| ~ proposition(X1335,X1335)
| ~ smoke(X1335,X1333)
| ~ present(X1335,X1333)
| ~ agent(X1335,X1333,skf4(X1335))
| ~ event(X1335,X1333)
| ~ think_believe_consider(X1335,X1333)
| ~ theme(X1335,X1333,X1335)
| ~ forename(X1335,X1331)
| ~ jules_forename(X1335,X1331)
| ~ of(X1335,X1331,skf4(X1335))
| ~ man(X1335,skf4(X1335))
| ~ vincent_forename(X1335,X1331)
| ~ actual_world(X1335) ),
inference(factor,[status(thm)],[c1050]) ).
cnf(c1054,plain,
( ~ state(X1348,X1347)
| ~ man(X1348,skf4(X1348))
| ~ be(X1348,X1347,skf4(X1348),skf4(X1348))
| ~ forename(X1348,X1345)
| ~ jules_forename(X1348,X1345)
| ~ of(X1348,X1345,skf4(X1348))
| ~ accessible_world(X1348,X1348)
| ~ proposition(X1348,X1348)
| ~ smoke(X1348,X1346)
| ~ present(X1348,X1346)
| ~ agent(X1348,X1346,skf4(X1348))
| ~ event(X1348,X1346)
| ~ think_believe_consider(X1348,X1346)
| ~ theme(X1348,X1346,X1348)
| ~ vincent_forename(X1348,X1345)
| ~ actual_world(X1348) ),
inference(factor,[status(thm)],[c1053]) ).
cnf(c406,plain,
( ~ state(X703,X710)
| ~ man(X703,X706)
| ~ be(X703,X710,X706,X706)
| ~ forename(X703,X709)
| ~ jules_forename(X703,X709)
| ~ of(X703,X709,X706)
| ~ accessible_world(X703,X711)
| ~ proposition(X703,X711)
| ~ proposition(X703,X703)
| ~ accessible_world(X703,X703)
| ~ smoke(X703,X702)
| ~ present(X703,X702)
| ~ agent(X703,X702,skf4(X703))
| ~ event(X703,X702)
| ~ think_believe_consider(X703,X705)
| ~ present(X703,X705)
| ~ event(X703,X705)
| ~ theme(X703,X705,X703)
| ~ forename(X703,X707)
| ~ jules_forename(X703,X707)
| ~ of(X703,X707,skf4(X703))
| ~ smoke(X711,X704)
| ~ present(X711,X704)
| ~ agent(X711,X704,skf4(X703))
| ~ event(X711,X704)
| ~ agent(X703,X705,skf4(X703))
| ~ man(X703,skf4(X703))
| ~ of(X703,X708,skf4(X703))
| ~ vincent_forename(X703,X708)
| ~ forename(X703,X708)
| ~ theme(X703,X702,X711)
| ~ think_believe_consider(X703,X702)
| ~ actual_world(X703) ),
inference(factor,[status(thm)],[clause95]) ).
cnf(c710,plain,
( ~ state(X1343,X1344)
| ~ man(X1343,skf4(X1343))
| ~ be(X1343,X1344,skf4(X1343),skf4(X1343))
| ~ forename(X1343,X1341)
| ~ jules_forename(X1343,X1341)
| ~ of(X1343,X1341,skf4(X1343))
| ~ accessible_world(X1343,X1337)
| ~ proposition(X1343,X1337)
| ~ proposition(X1343,X1343)
| ~ accessible_world(X1343,X1343)
| ~ smoke(X1343,X1342)
| ~ present(X1343,X1342)
| ~ agent(X1343,X1342,skf4(X1343))
| ~ event(X1343,X1342)
| ~ think_believe_consider(X1343,X1338)
| ~ present(X1343,X1338)
| ~ event(X1343,X1338)
| ~ theme(X1343,X1338,X1343)
| ~ forename(X1343,X1339)
| ~ jules_forename(X1343,X1339)
| ~ of(X1343,X1339,skf4(X1343))
| ~ smoke(X1337,X1340)
| ~ present(X1337,X1340)
| ~ agent(X1337,X1340,skf4(X1343))
| ~ event(X1337,X1340)
| ~ agent(X1343,X1338,skf4(X1343))
| ~ vincent_forename(X1343,X1341)
| ~ theme(X1343,X1342,X1337)
| ~ think_believe_consider(X1343,X1342)
| ~ actual_world(X1343) ),
inference(factor,[status(thm)],[c406]) ).
cnf(c704,plain,
( ~ state(X1308,X1309)
| ~ man(X1308,skf4(X1307))
| ~ be(X1308,X1309,skf4(X1307),skf4(X1307))
| ~ forename(X1308,X1306)
| ~ jules_forename(X1308,X1306)
| ~ of(X1308,X1306,skf4(X1307))
| ~ accessible_world(X1308,X1307)
| ~ proposition(X1308,X1307)
| ~ smoke(X1307,X1304)
| ~ present(X1307,X1304)
| ~ agent(X1307,X1304,skf4(X1307))
| ~ event(X1307,X1304)
| ~ think_believe_consider(X1308,X1305)
| ~ present(X1308,X1305)
| ~ event(X1308,X1305)
| ~ theme(X1308,X1305,X1307)
| ~ forename(X1308,X1302)
| ~ jules_forename(X1308,X1302)
| ~ of(X1308,X1302,skf4(X1307))
| ~ agent(X1308,X1303,skf4(X1307))
| ~ agent(X1308,X1305,skf4(X1307))
| ~ vincent_forename(X1308,X1306)
| ~ theme(X1308,X1303,X1307)
| ~ event(X1308,X1303)
| ~ present(X1308,X1303)
| ~ think_believe_consider(X1308,X1303)
| ~ actual_world(X1308) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1030,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1298)
| ~ jules_forename(skc8,X1298)
| ~ of(skc8,X1298,skc10)
| ~ accessible_world(skc8,X1295)
| ~ proposition(skc8,X1295)
| ~ think_believe_consider(skc8,X1297)
| ~ present(skc8,X1297)
| ~ event(skc8,X1297)
| ~ theme(skc8,X1297,X1295)
| ~ forename(skc8,X1294)
| ~ jules_forename(skc8,X1294)
| ~ of(skc8,X1294,skc10)
| ~ smoke(X1295,X1296)
| ~ present(X1295,X1296)
| ~ agent(X1295,X1296,skc10)
| ~ event(X1295,X1296)
| ~ agent(skc8,X1297,skc10)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1295,skf4(X1295)) ),
inference(resolution,[status(thm)],[c698,clause88]) ).
cnf(c1043,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1300)
| ~ jules_forename(skc8,X1300)
| ~ of(skc8,X1300,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1301)
| ~ present(skc8,X1301)
| ~ event(skc8,X1301)
| ~ theme(skc8,X1301,skc8)
| ~ forename(skc8,X1299)
| ~ jules_forename(skc8,X1299)
| ~ of(skc8,X1299,skc10)
| ~ smoke(skc8,X1301)
| ~ agent(skc8,X1301,skc10)
| ~ vincent_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1030]) ).
cnf(c1032,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1275)
| ~ jules_forename(skc8,X1275)
| ~ of(skc8,X1275,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1274)
| ~ present(skc8,X1274)
| ~ event(skc8,X1274)
| ~ theme(skc8,X1274,skc8)
| ~ forename(skc8,X1276)
| ~ jules_forename(skc8,X1276)
| ~ of(skc8,X1276,X1277)
| ~ smoke(skc8,X1274)
| ~ agent(skc8,X1274,X1277)
| ~ man(skc8,X1277)
| ~ vincent_forename(skc8,X1276)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1028]) ).
cnf(c1034,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1279)
| ~ jules_forename(skc8,X1279)
| ~ of(skc8,X1279,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc8)
| ~ forename(skc8,X1278)
| ~ jules_forename(skc8,X1278)
| ~ of(skc8,X1278,skc15)
| ~ smoke(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,X1278)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1032,clause86]) ).
cnf(c1035,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1287)
| ~ jules_forename(skc8,X1287)
| ~ of(skc8,X1287,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc8)
| ~ forename(skc8,skc14)
| ~ jules_forename(skc8,skc14)
| ~ smoke(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1034,clause85]) ).
cnf(c1027,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1262)
| ~ jules_forename(skc8,X1262)
| ~ of(skc8,X1262,skc10)
| ~ accessible_world(skc8,X1261)
| ~ proposition(skc8,X1261)
| ~ think_believe_consider(skc8,X1264)
| ~ present(skc8,X1264)
| ~ event(skc8,X1264)
| ~ theme(skc8,X1264,X1261)
| ~ forename(skc8,X1260)
| ~ jules_forename(skc8,X1260)
| ~ of(skc8,X1260,skc10)
| ~ smoke(X1261,X1263)
| ~ present(X1261,X1263)
| ~ agent(X1261,X1263,skc10)
| ~ event(X1261,X1263)
| ~ agent(skc8,X1264,skc10)
| ~ vincent_forename(skc8,X1262)
| ~ actual_world(skc8)
| man(X1261,skf4(X1261)) ),
inference(factor,[status(thm)],[c698]) ).
cnf(c1031,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,X1266)
| ~ jules_forename(skc8,X1266)
| ~ of(skc8,X1266,skc10)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ think_believe_consider(skc8,X1267)
| ~ present(skc8,X1267)
| ~ event(skc8,X1267)
| ~ theme(skc8,X1267,skc8)
| ~ forename(skc8,X1265)
| ~ jules_forename(skc8,X1265)
| ~ of(skc8,X1265,skc10)
| ~ smoke(skc8,X1267)
| ~ agent(skc8,X1267,skc10)
| ~ vincent_forename(skc8,X1266)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1027]) ).
cnf(clause71,axiom,
( ~ proposition(X269,X267)
| ~ proposition(X269,X265)
| ~ theme(X269,X264,X267)
| ~ think_believe_consider(X269,X264)
| ~ think_believe_consider(X269,X268)
| ~ theme(X269,X268,X265)
| ~ agent(X269,X268,X266)
| ~ agent(X269,X264,X266)
| X267 = X265 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
cnf(c572,plain,
( ~ proposition(skc12,X1020)
| ~ proposition(skc12,X1019)
| ~ theme(skc12,skc13,X1020)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,X1018)
| ~ theme(skc12,X1018,X1019)
| ~ agent(skc12,X1018,skc15)
| X1020 = X1019 ),
inference(resolution,[status(thm)],[c570,clause71]) ).
cnf(c901,plain,
( ~ proposition(skc12,X1251)
| ~ proposition(skc12,X1252)
| ~ theme(skc12,skc13,X1251)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1252)
| X1251 = X1252 ),
inference(resolution,[status(thm)],[c572,c383]) ).
cnf(c349,plain,
( ~ proposition(X658,X657)
| ~ proposition(X658,X660)
| ~ theme(X658,X656,X657)
| ~ think_believe_consider(X658,X656)
| ~ theme(X658,X656,X660)
| ~ agent(X658,X656,X659)
| X657 = X660 ),
inference(factor,[status(thm)],[clause71]) ).
cnf(c690,plain,
( ~ proposition(skc8,X1240)
| ~ proposition(skc8,X1239)
| ~ theme(skc8,skc13,X1240)
| ~ think_believe_consider(skc8,skc13)
| ~ theme(skc8,skc13,X1239)
| X1240 = X1239 ),
inference(resolution,[status(thm)],[c349,clause86]) ).
cnf(c1024,plain,
( ~ proposition(skc8,X1244)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,skc13,X1244)
| ~ think_believe_consider(skc8,skc13)
| X1244 = skc12 ),
inference(resolution,[status(thm)],[c690,clause87]) ).
cnf(c687,plain,
( ~ proposition(skc12,X1210)
| ~ proposition(skc12,X1209)
| ~ theme(skc12,skc13,X1210)
| ~ think_believe_consider(skc12,skc13)
| ~ theme(skc12,skc13,X1209)
| X1210 = X1209 ),
inference(resolution,[status(thm)],[c349,c570]) ).
cnf(c1012,plain,
( ~ proposition(skc12,X1243)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skc13,X1243)
| ~ think_believe_consider(skc12,skc13)
| X1243 = skc12 ),
inference(resolution,[status(thm)],[c687,c573]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c30,axiom,
( X565 != X567
| X564 != X566
| X571 != X569
| X570 != X568
| ~ be(X565,X564,X571,X570)
| be(X567,X566,X569,X568) ),
theory(equality) ).
cnf(c634,plain,
( skc12 != X1130
| skc9 != X1127
| skc10 != X1128
| skc10 != X1129
| be(X1130,X1127,X1128,X1129) ),
inference(resolution,[status(thm)],[c30,c589]) ).
cnf(c969,plain,
( skc12 != X1232
| skc9 != X1233
| skc10 != X1234
| be(X1232,X1233,X1234,skc10) ),
inference(resolution,[status(thm)],[c634,reflexivity]) ).
cnf(c689,plain,
( ~ proposition(skc12,X1229)
| ~ proposition(skc12,X1228)
| ~ theme(skc12,skf2(skc10),X1229)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1228)
| X1229 = X1228 ),
inference(resolution,[status(thm)],[c349,c384]) ).
cnf(c633,plain,
( skc8 != X1120
| skc9 != X1117
| skc10 != X1118
| skc10 != X1119
| be(X1120,X1117,X1118,X1119) ),
inference(resolution,[status(thm)],[c30,clause89]) ).
cnf(c963,plain,
( skc8 != X1225
| skc9 != X1226
| skc10 != X1227
| be(X1225,X1226,X1227,skc10) ),
inference(resolution,[status(thm)],[c633,reflexivity]) ).
cnf(c968,plain,
( skc12 != X1219
| skc9 != X1221
| skc10 != X1220
| be(X1219,X1221,X1220,X1220) ),
inference(factor,[status(thm)],[c634]) ).
cnf(c1017,plain,
( skc12 != X1222
| skc9 != X1223
| be(X1222,X1223,skc10,skc10) ),
inference(resolution,[status(thm)],[c968,reflexivity]) ).
cnf(c1018,plain,
( skc12 != X1224
| be(X1224,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1017,reflexivity]) ).
cnf(c688,plain,
( ~ proposition(skc12,X1218)
| ~ proposition(skc12,X1217)
| ~ theme(skc12,skf2(skc15),X1218)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1217)
| X1218 = X1217 ),
inference(resolution,[status(thm)],[c349,c383]) ).
cnf(c962,plain,
( skc8 != X1211
| skc9 != X1212
| skc10 != X1213
| be(X1211,X1212,X1213,X1213) ),
inference(factor,[status(thm)],[c633]) ).
cnf(c1013,plain,
( skc8 != X1215
| skc9 != X1214
| be(X1215,X1214,skc10,skc10) ),
inference(resolution,[status(thm)],[c962,reflexivity]) ).
cnf(c1014,plain,
( skc8 != X1216
| be(X1216,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1013,reflexivity]) ).
cnf(c36,axiom,
( X625 != X627
| X624 != X626
| X629 != X628
| ~ of(X625,X624,X629)
| of(X627,X626,X628) ),
theory(equality) ).
cnf(c670,plain,
( skc12 != X1201
| skc14 != X1202
| skc15 != X1200
| of(X1201,X1202,X1200) ),
inference(resolution,[status(thm)],[c36,c579]) ).
cnf(c1006,plain,
( skc12 != X1207
| skc14 != X1206
| of(X1207,X1206,skc15) ),
inference(resolution,[status(thm)],[c670,reflexivity]) ).
cnf(c1009,plain,
( skc12 != X1208
| of(X1208,skc14,skc15) ),
inference(resolution,[status(thm)],[c1006,reflexivity]) ).
cnf(c669,plain,
( skc8 != X1198
| skc11 != X1199
| skc10 != X1197
| of(X1198,X1199,X1197) ),
inference(resolution,[status(thm)],[c36,clause88]) ).
cnf(c1005,plain,
( skc8 != X1204
| skc11 != X1203
| of(X1204,X1203,skc10) ),
inference(resolution,[status(thm)],[c669,reflexivity]) ).
cnf(c1007,plain,
( skc8 != X1205
| of(X1205,skc11,skc10) ),
inference(resolution,[status(thm)],[c1005,reflexivity]) ).
cnf(c668,plain,
( skc8 != X1192
| skc14 != X1193
| skc15 != X1191
| of(X1192,X1193,X1191) ),
inference(resolution,[status(thm)],[c36,clause85]) ).
cnf(c1002,plain,
( skc8 != X1194
| skc14 != X1195
| of(X1194,X1195,skc15) ),
inference(resolution,[status(thm)],[c668,reflexivity]) ).
cnf(c1003,plain,
( skc8 != X1196
| of(X1196,skc14,skc15) ),
inference(resolution,[status(thm)],[c1002,reflexivity]) ).
cnf(c667,plain,
( skc12 != X1183
| skc11 != X1184
| skc10 != X1182
| of(X1183,X1184,X1182) ),
inference(resolution,[status(thm)],[c36,c582]) ).
cnf(c997,plain,
( skc12 != X1188
| skc11 != X1189
| of(X1188,X1189,skc10) ),
inference(resolution,[status(thm)],[c667,reflexivity]) ).
cnf(c1000,plain,
( skc12 != X1190
| of(X1190,skc11,skc10) ),
inference(resolution,[status(thm)],[c997,reflexivity]) ).
cnf(c35,axiom,
( X615 != X617
| X614 != X616
| X619 != X618
| ~ theme(X615,X614,X619)
| theme(X617,X616,X618) ),
theory(equality) ).
cnf(c663,plain,
( skc12 != X1177
| skc13 != X1176
| skc12 != X1175
| theme(X1177,X1176,X1175) ),
inference(resolution,[status(thm)],[c35,c573]) ).
cnf(c993,plain,
( skc12 != X1185
| skc13 != X1186
| theme(X1185,X1186,skc12) ),
inference(resolution,[status(thm)],[c663,reflexivity]) ).
cnf(c998,plain,
( skc12 != X1187
| theme(X1187,skc13,skc12) ),
inference(resolution,[status(thm)],[c993,reflexivity]) ).
cnf(c992,plain,
( skc12 != X1179
| skc13 != X1180
| theme(X1179,X1180,X1179) ),
inference(factor,[status(thm)],[c663]) ).
cnf(c995,plain,
( skc12 != X1181
| theme(X1181,skc13,X1181) ),
inference(resolution,[status(thm)],[c992,reflexivity]) ).
cnf(c662,plain,
( skc8 != X1172
| skc13 != X1171
| skc12 != X1170
| theme(X1172,X1171,X1170) ),
inference(resolution,[status(thm)],[c35,clause87]) ).
cnf(c990,plain,
( skc8 != X1174
| skc13 != X1173
| theme(X1174,X1173,skc12) ),
inference(resolution,[status(thm)],[c662,reflexivity]) ).
cnf(c991,plain,
( skc8 != X1178
| theme(X1178,skc13,skc12) ),
inference(resolution,[status(thm)],[c990,reflexivity]) ).
cnf(c34,axiom,
( X604 != X606
| X603 != X605
| X608 != X607
| ~ agent(X604,X603,X608)
| agent(X606,X605,X607) ),
theory(equality) ).
cnf(c658,plain,
( skc8 != X1164
| skc13 != X1165
| skc15 != X1166
| agent(X1164,X1165,X1166) ),
inference(resolution,[status(thm)],[c34,clause86]) ).
cnf(c987,plain,
( skc8 != X1168
| skc13 != X1167
| agent(X1168,X1167,skc15) ),
inference(resolution,[status(thm)],[c658,reflexivity]) ).
cnf(c988,plain,
( skc8 != X1169
| agent(X1169,skc13,skc15) ),
inference(resolution,[status(thm)],[c987,reflexivity]) ).
cnf(c657,plain,
( skc12 != X1157
| skf2(skc10) != X1158
| skc10 != X1159
| agent(X1157,X1158,X1159) ),
inference(resolution,[status(thm)],[c34,c384]) ).
cnf(c983,plain,
( skc12 != X1161
| skc10 != X1162
| agent(X1161,skf2(skc10),X1162) ),
inference(resolution,[status(thm)],[c657,reflexivity]) ).
cnf(c985,plain,
( skc12 != X1163
| agent(X1163,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c983,reflexivity]) ).
cnf(c656,plain,
( skc12 != X1152
| skf2(skc15) != X1153
| skc15 != X1154
| agent(X1152,X1153,X1154) ),
inference(resolution,[status(thm)],[c34,c383]) ).
cnf(c981,plain,
( skc12 != X1155
| skc15 != X1156
| agent(X1155,skf2(skc15),X1156) ),
inference(resolution,[status(thm)],[c656,reflexivity]) ).
cnf(c982,plain,
( skc12 != X1160
| agent(X1160,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c981,reflexivity]) ).
cnf(c655,plain,
( skc12 != X1145
| skc13 != X1146
| skc15 != X1147
| agent(X1145,X1146,X1147) ),
inference(resolution,[status(thm)],[c34,c570]) ).
cnf(c977,plain,
( skc12 != X1149
| skc13 != X1150
| agent(X1149,X1150,skc15) ),
inference(resolution,[status(thm)],[c655,reflexivity]) ).
cnf(c979,plain,
( skc12 != X1151
| agent(X1151,skc13,skc15) ),
inference(resolution,[status(thm)],[c977,reflexivity]) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
cnf(clause45,axiom,
( ~ accessible_world(X120,X122)
| ~ think_believe_consider(X120,X121)
| think_believe_consider(X122,X121) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(c199,plain,
( ~ accessible_world(skc8,X202)
| think_believe_consider(X202,skc13) ),
inference(resolution,[status(thm)],[clause45,clause78]) ).
cnf(c263,plain,
think_believe_consider(skc12,skc13),
inference(resolution,[status(thm)],[c199,clause83]) ).
cnf(c33,axiom,
( X594 != X596
| X593 != X595
| ~ think_believe_consider(X594,X593)
| think_believe_consider(X596,X595) ),
theory(equality) ).
cnf(c650,plain,
( skc12 != X1144
| skc13 != X1143
| think_believe_consider(X1144,X1143) ),
inference(resolution,[status(thm)],[c33,c263]) ).
cnf(c976,plain,
( skc12 != X1148
| think_believe_consider(X1148,skc13) ),
inference(resolution,[status(thm)],[c650,reflexivity]) ).
cnf(c32,axiom,
( X586 != X588
| X585 != X587
| ~ present(X586,X585)
| present(X588,X587) ),
theory(equality) ).
cnf(c644,plain,
( skc12 != X1138
| skf2(X1137) != X1136
| present(X1138,X1136) ),
inference(resolution,[status(thm)],[c32,c369]) ).
cnf(c973,plain,
( skc12 != X1141
| present(X1141,skf2(X1140)) ),
inference(resolution,[status(thm)],[c644,reflexivity]) ).
cnf(c649,plain,
( skc8 != X1135
| skc13 != X1134
| think_believe_consider(X1135,X1134) ),
inference(resolution,[status(thm)],[c33,clause78]) ).
cnf(c972,plain,
( skc8 != X1139
| think_believe_consider(X1139,skc13) ),
inference(resolution,[status(thm)],[c649,reflexivity]) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
cnf(clause44,axiom,
( ~ accessible_world(X114,X116)
| ~ present(X114,X115)
| present(X116,X115) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c193,plain,
( ~ accessible_world(skc8,X196)
| present(X196,skc13) ),
inference(resolution,[status(thm)],[clause44,clause77]) ).
cnf(c259,plain,
present(skc12,skc13),
inference(resolution,[status(thm)],[c193,clause83]) ).
cnf(c645,plain,
( skc12 != X1132
| skc13 != X1131
| present(X1132,X1131) ),
inference(resolution,[status(thm)],[c32,c259]) ).
cnf(c970,plain,
( skc12 != X1133
| present(X1133,skc13) ),
inference(resolution,[status(thm)],[c645,reflexivity]) ).
cnf(c643,plain,
( skc8 != X1125
| skc13 != X1124
| present(X1125,X1124) ),
inference(resolution,[status(thm)],[c32,clause77]) ).
cnf(c966,plain,
( skc8 != X1126
| present(X1126,skc13) ),
inference(resolution,[status(thm)],[c643,reflexivity]) ).
cnf(c31,axiom,
( X578 != X580
| X577 != X579
| ~ accessible_world(X578,X577)
| accessible_world(X580,X579) ),
theory(equality) ).
cnf(c638,plain,
( skc8 != X1121
| skc12 != X1122
| accessible_world(X1121,X1122) ),
inference(resolution,[status(thm)],[c31,clause83]) ).
cnf(c964,plain,
( skc8 != X1123
| accessible_world(X1123,skc12) ),
inference(resolution,[status(thm)],[c638,reflexivity]) ).
cnf(clause79,negated_conjecture,
jules_forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
cnf(clause65,axiom,
( ~ accessible_world(X228,X230)
| ~ jules_forename(X228,X229)
| jules_forename(X230,X229) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
cnf(c313,plain,
( ~ accessible_world(skc8,X415)
| jules_forename(X415,skc11) ),
inference(resolution,[status(thm)],[clause65,clause79]) ).
cnf(c531,plain,
jules_forename(skc12,skc11),
inference(resolution,[status(thm)],[c313,clause83]) ).
cnf(c29,axiom,
( X555 != X557
| X554 != X556
| ~ jules_forename(X555,X554)
| jules_forename(X557,X556) ),
theory(equality) ).
cnf(c628,plain,
( skc12 != X1114
| skc11 != X1115
| jules_forename(X1114,X1115) ),
inference(resolution,[status(thm)],[c29,c531]) ).
cnf(c960,plain,
( skc12 != X1116
| jules_forename(X1116,skc11) ),
inference(resolution,[status(thm)],[c628,reflexivity]) ).
cnf(c627,plain,
( skc8 != X1111
| skc11 != X1112
| jules_forename(X1111,X1112) ),
inference(resolution,[status(thm)],[c29,clause79]) ).
cnf(c958,plain,
( skc8 != X1113
| jules_forename(X1113,skc11) ),
inference(resolution,[status(thm)],[c627,reflexivity]) ).
cnf(c28,axiom,
( X547 != X549
| X546 != X548
| ~ vincent_forename(X547,X546)
| vincent_forename(X549,X548) ),
theory(equality) ).
cnf(c623,plain,
( skc8 != X1109
| skc14 != X1108
| vincent_forename(X1109,X1108) ),
inference(resolution,[status(thm)],[c28,clause75]) ).
cnf(c956,plain,
( skc8 != X1110
| vincent_forename(X1110,skc14) ),
inference(resolution,[status(thm)],[c623,reflexivity]) ).
cnf(c622,plain,
( skc12 != X1106
| skc14 != X1105
| vincent_forename(X1106,X1105) ),
inference(resolution,[status(thm)],[c28,c522]) ).
cnf(c954,plain,
( skc12 != X1107
| vincent_forename(X1107,skc14) ),
inference(resolution,[status(thm)],[c622,reflexivity]) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
cnf(clause27,axiom,
( ~ forename(X55,X56)
| relname(X55,X56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c84,plain,
relname(skc8,skc11),
inference(resolution,[status(thm)],[clause27,clause80]) ).
cnf(c27,axiom,
( X538 != X540
| X537 != X539
| ~ relname(X538,X537)
| relname(X540,X539) ),
theory(equality) ).
cnf(c618,plain,
( skc8 != X1102
| skc11 != X1103
| relname(X1102,X1103) ),
inference(resolution,[status(thm)],[c27,c84]) ).
cnf(c952,plain,
( skc8 != X1104
| relname(X1104,skc11) ),
inference(resolution,[status(thm)],[c618,reflexivity]) ).
cnf(clause74,negated_conjecture,
forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
cnf(c83,plain,
relname(skc8,skc14),
inference(resolution,[status(thm)],[clause27,clause74]) ).
cnf(c617,plain,
( skc8 != X1099
| skc14 != X1100
| relname(X1099,X1100) ),
inference(resolution,[status(thm)],[c27,c83]) ).
cnf(c950,plain,
( skc8 != X1101
| relname(X1101,skc14) ),
inference(resolution,[status(thm)],[c617,reflexivity]) ).
cnf(clause62,axiom,
( ~ accessible_world(X216,X218)
| ~ forename(X216,X217)
| forename(X218,X217) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
cnf(c292,plain,
( ~ accessible_world(skc8,X384)
| forename(X384,skc14) ),
inference(resolution,[status(thm)],[clause62,clause74]) ).
cnf(c485,plain,
forename(skc12,skc14),
inference(resolution,[status(thm)],[c292,clause83]) ).
cnf(c498,plain,
relname(skc12,skc14),
inference(resolution,[status(thm)],[c485,clause27]) ).
cnf(c616,plain,
( skc12 != X1096
| skc14 != X1097
| relname(X1096,X1097) ),
inference(resolution,[status(thm)],[c27,c498]) ).
cnf(c948,plain,
( skc12 != X1098
| relname(X1098,skc14) ),
inference(resolution,[status(thm)],[c616,reflexivity]) ).
cnf(c293,plain,
( ~ accessible_world(skc8,X389)
| forename(X389,skc11) ),
inference(resolution,[status(thm)],[clause62,clause80]) ).
cnf(c501,plain,
forename(skc12,skc11),
inference(resolution,[status(thm)],[c293,clause83]) ).
cnf(c503,plain,
relname(skc12,skc11),
inference(resolution,[status(thm)],[c501,clause27]) ).
cnf(c615,plain,
( skc12 != X1093
| skc11 != X1094
| relname(X1093,X1094) ),
inference(resolution,[status(thm)],[c27,c503]) ).
cnf(c946,plain,
( skc12 != X1095
| relname(X1095,skc11) ),
inference(resolution,[status(thm)],[c615,reflexivity]) ).
cnf(c26,axiom,
( X528 != X530
| X527 != X529
| ~ forename(X528,X527)
| forename(X530,X529) ),
theory(equality) ).
cnf(c610,plain,
( skc8 != X1091
| skc11 != X1090
| forename(X1091,X1090) ),
inference(resolution,[status(thm)],[c26,clause80]) ).
cnf(c944,plain,
( skc8 != X1092
| forename(X1092,skc11) ),
inference(resolution,[status(thm)],[c610,reflexivity]) ).
cnf(c609,plain,
( skc8 != X1088
| skc14 != X1087
| forename(X1088,X1087) ),
inference(resolution,[status(thm)],[c26,clause74]) ).
cnf(c942,plain,
( skc8 != X1089
| forename(X1089,skc14) ),
inference(resolution,[status(thm)],[c609,reflexivity]) ).
cnf(c608,plain,
( skc12 != X1085
| skc14 != X1084
| forename(X1085,X1084) ),
inference(resolution,[status(thm)],[c26,c485]) ).
cnf(c940,plain,
( skc12 != X1086
| forename(X1086,skc14) ),
inference(resolution,[status(thm)],[c608,reflexivity]) ).
cnf(c607,plain,
( skc12 != X1082
| skc11 != X1081
| forename(X1082,X1081) ),
inference(resolution,[status(thm)],[c26,c501]) ).
cnf(c938,plain,
( skc12 != X1083
| forename(X1083,skc11) ),
inference(resolution,[status(thm)],[c607,reflexivity]) ).
cnf(clause26,axiom,
( ~ man(X53,X54)
| male(X53,X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c82,plain,
male(skc8,skc15),
inference(resolution,[status(thm)],[clause26,clause73]) ).
cnf(c25,axiom,
( X520 != X522
| X519 != X521
| ~ male(X520,X519)
| male(X522,X521) ),
theory(equality) ).
cnf(c603,plain,
( skc8 != X1078
| skc15 != X1079
| male(X1078,X1079) ),
inference(resolution,[status(thm)],[c25,c82]) ).
cnf(c936,plain,
( skc8 != X1080
| male(X1080,skc15) ),
inference(resolution,[status(thm)],[c603,reflexivity]) ).
cnf(c332,plain,
male(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause26]) ).
cnf(c602,plain,
( skc12 != X1075
| skc10 != X1076
| male(X1075,X1076) ),
inference(resolution,[status(thm)],[c25,c332]) ).
cnf(c934,plain,
( skc12 != X1077
| male(X1077,skc10) ),
inference(resolution,[status(thm)],[c602,reflexivity]) ).
cnf(c81,plain,
male(skc8,skc10),
inference(resolution,[status(thm)],[clause26,clause81]) ).
cnf(c601,plain,
( skc8 != X1072
| skc10 != X1073
| male(X1072,X1073) ),
inference(resolution,[status(thm)],[c25,c81]) ).
cnf(c932,plain,
( skc8 != X1074
| male(X1074,skc10) ),
inference(resolution,[status(thm)],[c601,reflexivity]) ).
cnf(c380,plain,
male(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause26]) ).
cnf(c600,plain,
( skc12 != X1069
| skc15 != X1070
| male(X1069,X1070) ),
inference(resolution,[status(thm)],[c25,c380]) ).
cnf(c930,plain,
( skc12 != X1071
| male(X1071,skc15) ),
inference(resolution,[status(thm)],[c600,reflexivity]) ).
cnf(clause25,axiom,
( ~ human_person(X51,X52)
| animate(X51,X52) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(clause16,axiom,
( ~ man(X33,X34)
| human_person(X33,X34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c382,plain,
human_person(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause16]) ).
cnf(c389,plain,
animate(skc12,skc15),
inference(resolution,[status(thm)],[c382,clause25]) ).
cnf(c24,axiom,
( X511 != X513
| X510 != X512
| ~ animate(X511,X510)
| animate(X513,X512) ),
theory(equality) ).
cnf(c596,plain,
( skc12 != X1066
| skc15 != X1067
| animate(X1066,X1067) ),
inference(resolution,[status(thm)],[c24,c389]) ).
cnf(c928,plain,
( skc12 != X1068
| animate(X1068,skc15) ),
inference(resolution,[status(thm)],[c596,reflexivity]) ).
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(c595,plain,
( skc12 != X1063
| skc10 != X1064
| animate(X1063,X1064) ),
inference(resolution,[status(thm)],[c24,c342]) ).
cnf(c926,plain,
( skc12 != X1065
| animate(X1065,skc10) ),
inference(resolution,[status(thm)],[c595,reflexivity]) ).
cnf(c59,plain,
human_person(skc8,skc15),
inference(resolution,[status(thm)],[clause16,clause73]) ).
cnf(c80,plain,
animate(skc8,skc15),
inference(resolution,[status(thm)],[clause25,c59]) ).
cnf(c594,plain,
( skc8 != X1060
| skc15 != X1061
| animate(X1060,X1061) ),
inference(resolution,[status(thm)],[c24,c80]) ).
cnf(c924,plain,
( skc8 != X1062
| animate(X1062,skc15) ),
inference(resolution,[status(thm)],[c594,reflexivity]) ).
cnf(c58,plain,
human_person(skc8,skc10),
inference(resolution,[status(thm)],[clause16,clause81]) ).
cnf(c79,plain,
animate(skc8,skc10),
inference(resolution,[status(thm)],[clause25,c58]) ).
cnf(c593,plain,
( skc8 != X1048
| skc10 != X1049
| animate(X1048,X1049) ),
inference(resolution,[status(thm)],[c24,c79]) ).
cnf(c920,plain,
( skc8 != X1059
| animate(X1059,skc10) ),
inference(resolution,[status(thm)],[c593,reflexivity]) ).
cnf(c592,plain,
( ~ accessible_world(skc12,X1047)
| be(X1047,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c589,clause69]) ).
cnf(clause24,axiom,
( ~ human_person(X49,X50)
| human(X49,X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c78,plain,
human(skc8,skc15),
inference(resolution,[status(thm)],[clause24,c59]) ).
cnf(c23,axiom,
( X503 != X505
| X502 != X504
| ~ human(X503,X502)
| human(X505,X504) ),
theory(equality) ).
cnf(c588,plain,
( skc8 != X1045
| skc15 != X1044
| human(X1045,X1044) ),
inference(resolution,[status(thm)],[c23,c78]) ).
cnf(c918,plain,
( skc8 != X1046
| human(X1046,skc15) ),
inference(resolution,[status(thm)],[c588,reflexivity]) ).
cnf(c77,plain,
human(skc8,skc10),
inference(resolution,[status(thm)],[clause24,c58]) ).
cnf(c587,plain,
( skc8 != X1042
| skc10 != X1041
| human(X1042,X1041) ),
inference(resolution,[status(thm)],[c23,c77]) ).
cnf(c916,plain,
( skc8 != X1043
| human(X1043,skc10) ),
inference(resolution,[status(thm)],[c587,reflexivity]) ).
cnf(c340,plain,
human(skc12,skc10),
inference(resolution,[status(thm)],[c333,clause24]) ).
cnf(c586,plain,
( skc12 != X1039
| skc10 != X1038
| human(X1039,X1038) ),
inference(resolution,[status(thm)],[c23,c340]) ).
cnf(c914,plain,
( skc12 != X1040
| human(X1040,skc10) ),
inference(resolution,[status(thm)],[c586,reflexivity]) ).
cnf(clause70,axiom,
( ~ forename(X260,X263)
| ~ of(X260,X262,X261)
| ~ forename(X260,X262)
| ~ of(X260,X263,X261)
| ~ entity(X260,X261)
| X262 = X263 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
cnf(c583,plain,
( ~ forename(skc12,skc11)
| ~ of(skc12,X1037,skc10)
| ~ forename(skc12,X1037)
| ~ entity(skc12,skc10)
| X1037 = skc11 ),
inference(resolution,[status(thm)],[c582,clause70]) ).
cnf(c387,plain,
human(skc12,skc15),
inference(resolution,[status(thm)],[c382,clause24]) ).
cnf(c585,plain,
( skc12 != X1035
| skc15 != X1034
| human(X1035,X1034) ),
inference(resolution,[status(thm)],[c23,c387]) ).
cnf(c911,plain,
( skc12 != X1036
| human(X1036,skc15) ),
inference(resolution,[status(thm)],[c585,reflexivity]) ).
cnf(clause17,axiom,
( ~ human_person(X35,X36)
| organism(X35,X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c62,plain,
organism(skc8,skc15),
inference(resolution,[status(thm)],[clause17,c59]) ).
cnf(clause23,axiom,
( ~ organism(X47,X48)
| living(X47,X48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(c76,plain,
living(skc8,skc15),
inference(resolution,[status(thm)],[clause23,c62]) ).
cnf(c22,axiom,
( X496 != X498
| X495 != X497
| ~ living(X496,X495)
| living(X498,X497) ),
theory(equality) ).
cnf(c578,plain,
( skc8 != X1030
| skc15 != X1031
| living(X1030,X1031) ),
inference(resolution,[status(thm)],[c22,c76]) ).
cnf(c908,plain,
( skc8 != X1033
| living(X1033,skc15) ),
inference(resolution,[status(thm)],[c578,reflexivity]) ).
cnf(c580,plain,
( ~ forename(skc12,skc14)
| ~ of(skc12,X1032,skc15)
| ~ forename(skc12,X1032)
| ~ entity(skc12,skc15)
| X1032 = skc14 ),
inference(resolution,[status(thm)],[c579,clause70]) ).
cnf(c61,plain,
organism(skc8,skc10),
inference(resolution,[status(thm)],[clause17,c58]) ).
cnf(c75,plain,
living(skc8,skc10),
inference(resolution,[status(thm)],[clause23,c61]) ).
cnf(c577,plain,
( skc8 != X1026
| skc10 != X1027
| living(X1026,X1027) ),
inference(resolution,[status(thm)],[c22,c75]) ).
cnf(c905,plain,
( skc8 != X1029
| living(X1029,skc10) ),
inference(resolution,[status(thm)],[c577,reflexivity]) ).
cnf(c388,plain,
organism(skc12,skc15),
inference(resolution,[status(thm)],[c382,clause17]) ).
cnf(c394,plain,
living(skc12,skc15),
inference(resolution,[status(thm)],[c388,clause23]) ).
cnf(c576,plain,
( skc12 != X1024
| skc15 != X1025
| living(X1024,X1025) ),
inference(resolution,[status(thm)],[c22,c394]) ).
cnf(c904,plain,
( skc12 != X1028
| living(X1028,skc15) ),
inference(resolution,[status(thm)],[c576,reflexivity]) ).
cnf(c341,plain,
organism(skc12,skc10),
inference(resolution,[status(thm)],[c333,clause17]) ).
cnf(c347,plain,
living(skc12,skc10),
inference(resolution,[status(thm)],[c341,clause23]) ).
cnf(c575,plain,
( skc12 != X1021
| skc10 != X1022
| living(X1021,X1022) ),
inference(resolution,[status(thm)],[c22,c347]) ).
cnf(c902,plain,
( skc12 != X1023
| living(X1023,skc10) ),
inference(resolution,[status(thm)],[c575,reflexivity]) ).
cnf(clause22,axiom,
( ~ organism(X45,X46)
| impartial(X45,X46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c74,plain,
impartial(skc8,skc15),
inference(resolution,[status(thm)],[clause22,c62]) ).
cnf(c21,axiom,
( X488 != X490
| X487 != X489
| ~ impartial(X488,X487)
| impartial(X490,X489) ),
theory(equality) ).
cnf(c569,plain,
( skc8 != X1015
| skc15 != X1016
| impartial(X1015,X1016) ),
inference(resolution,[status(thm)],[c21,c74]) ).
cnf(c898,plain,
( skc8 != X1017
| impartial(X1017,skc15) ),
inference(resolution,[status(thm)],[c569,reflexivity]) ).
cnf(c392,plain,
impartial(skc12,skc15),
inference(resolution,[status(thm)],[c388,clause22]) ).
cnf(c568,plain,
( skc12 != X1012
| skc15 != X1013
| impartial(X1012,X1013) ),
inference(resolution,[status(thm)],[c21,c392]) ).
cnf(c896,plain,
( skc12 != X1014
| impartial(X1014,skc15) ),
inference(resolution,[status(thm)],[c568,reflexivity]) ).
cnf(c73,plain,
impartial(skc8,skc10),
inference(resolution,[status(thm)],[clause22,c61]) ).
cnf(c567,plain,
( skc8 != X1009
| skc10 != X1010
| impartial(X1009,X1010) ),
inference(resolution,[status(thm)],[c21,c73]) ).
cnf(c894,plain,
( skc8 != X1011
| impartial(X1011,skc10) ),
inference(resolution,[status(thm)],[c567,reflexivity]) ).
cnf(c345,plain,
impartial(skc12,skc10),
inference(resolution,[status(thm)],[c341,clause22]) ).
cnf(c566,plain,
( skc12 != X1006
| skc10 != X1007
| impartial(X1006,X1007) ),
inference(resolution,[status(thm)],[c21,c345]) ).
cnf(c892,plain,
( skc12 != X1008
| impartial(X1008,skc10) ),
inference(resolution,[status(thm)],[c566,reflexivity]) ).
cnf(clause18,axiom,
( ~ organism(X37,X38)
| entity(X37,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c63,plain,
entity(skc8,skc10),
inference(resolution,[status(thm)],[clause18,c61]) ).
cnf(clause21,axiom,
( ~ entity(X43,X44)
| existent(X43,X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c72,plain,
existent(skc8,skc10),
inference(resolution,[status(thm)],[clause21,c63]) ).
cnf(c20,axiom,
( X474 != X476
| X473 != X475
| ~ existent(X474,X473)
| existent(X476,X475) ),
theory(equality) ).
cnf(c565,plain,
( skc8 != X1004
| skc10 != X1003
| existent(X1004,X1003) ),
inference(resolution,[status(thm)],[c20,c72]) ).
cnf(c890,plain,
( skc8 != X1005
| existent(X1005,skc10) ),
inference(resolution,[status(thm)],[c565,reflexivity]) ).
cnf(c64,plain,
entity(skc8,skc15),
inference(resolution,[status(thm)],[clause18,c62]) ).
cnf(c71,plain,
existent(skc8,skc15),
inference(resolution,[status(thm)],[clause21,c64]) ).
cnf(c564,plain,
( skc8 != X1001
| skc15 != X1000
| existent(X1001,X1000) ),
inference(resolution,[status(thm)],[c20,c71]) ).
cnf(c888,plain,
( skc8 != X1002
| existent(X1002,skc15) ),
inference(resolution,[status(thm)],[c564,reflexivity]) ).
cnf(c391,plain,
entity(skc12,skc15),
inference(resolution,[status(thm)],[c388,clause18]) ).
cnf(c398,plain,
existent(skc12,skc15),
inference(resolution,[status(thm)],[c391,clause21]) ).
cnf(c563,plain,
( skc12 != X998
| skc15 != X997
| existent(X998,X997) ),
inference(resolution,[status(thm)],[c20,c398]) ).
cnf(c886,plain,
( skc12 != X999
| existent(X999,skc15) ),
inference(resolution,[status(thm)],[c563,reflexivity]) ).
cnf(c344,plain,
entity(skc12,skc10),
inference(resolution,[status(thm)],[c341,clause18]) ).
cnf(c352,plain,
existent(skc12,skc10),
inference(resolution,[status(thm)],[c344,clause21]) ).
cnf(c562,plain,
( skc12 != X995
| skc10 != X994
| existent(X995,X994) ),
inference(resolution,[status(thm)],[c20,c352]) ).
cnf(c884,plain,
( skc12 != X996
| existent(X996,skc10) ),
inference(resolution,[status(thm)],[c562,reflexivity]) ).
cnf(c19,axiom,
( X462 != X464
| X461 != X463
| ~ entity(X462,X461)
| entity(X464,X463) ),
theory(equality) ).
cnf(c561,plain,
( skc8 != X992
| skc10 != X991
| entity(X992,X991) ),
inference(resolution,[status(thm)],[c19,c63]) ).
cnf(c882,plain,
( skc8 != X993
| entity(X993,skc10) ),
inference(resolution,[status(thm)],[c561,reflexivity]) ).
cnf(c560,plain,
( skc12 != X989
| skc15 != X988
| entity(X989,X988) ),
inference(resolution,[status(thm)],[c19,c391]) ).
cnf(c880,plain,
( skc12 != X990
| entity(X990,skc15) ),
inference(resolution,[status(thm)],[c560,reflexivity]) ).
cnf(c559,plain,
( skc12 != X986
| skc10 != X985
| entity(X986,X985) ),
inference(resolution,[status(thm)],[c19,c344]) ).
cnf(c878,plain,
( skc12 != X987
| entity(X987,skc10) ),
inference(resolution,[status(thm)],[c559,reflexivity]) ).
cnf(c558,plain,
( skc8 != X983
| skc15 != X982
| entity(X983,X982) ),
inference(resolution,[status(thm)],[c19,c64]) ).
cnf(c876,plain,
( skc8 != X984
| entity(X984,skc15) ),
inference(resolution,[status(thm)],[c558,reflexivity]) ).
cnf(c18,axiom,
( X453 != X455
| X452 != X454
| ~ organism(X453,X452)
| organism(X455,X454) ),
theory(equality) ).
cnf(c557,plain,
( skc12 != X980
| skc10 != X979
| organism(X980,X979) ),
inference(resolution,[status(thm)],[c18,c341]) ).
cnf(c874,plain,
( skc12 != X981
| organism(X981,skc10) ),
inference(resolution,[status(thm)],[c557,reflexivity]) ).
cnf(c556,plain,
( skc8 != X977
| skc15 != X976
| organism(X977,X976) ),
inference(resolution,[status(thm)],[c18,c62]) ).
cnf(c872,plain,
( skc8 != X978
| organism(X978,skc15) ),
inference(resolution,[status(thm)],[c556,reflexivity]) ).
cnf(c555,plain,
( skc8 != X974
| skc10 != X973
| organism(X974,X973) ),
inference(resolution,[status(thm)],[c18,c61]) ).
cnf(c870,plain,
( skc8 != X975
| organism(X975,skc10) ),
inference(resolution,[status(thm)],[c555,reflexivity]) ).
cnf(c554,plain,
( skc12 != X971
| skc15 != X970
| organism(X971,X970) ),
inference(resolution,[status(thm)],[c18,c388]) ).
cnf(c868,plain,
( skc12 != X972
| organism(X972,skc15) ),
inference(resolution,[status(thm)],[c554,reflexivity]) ).
cnf(c17,axiom,
( X444 != X446
| X443 != X445
| ~ human_person(X444,X443)
| human_person(X446,X445) ),
theory(equality) ).
cnf(c553,plain,
( skc8 != X967
| skc15 != X968
| human_person(X967,X968) ),
inference(resolution,[status(thm)],[c17,c59]) ).
cnf(c866,plain,
( skc8 != X969
| human_person(X969,skc15) ),
inference(resolution,[status(thm)],[c553,reflexivity]) ).
cnf(c552,plain,
( skc12 != X964
| skc15 != X965
| human_person(X964,X965) ),
inference(resolution,[status(thm)],[c17,c382]) ).
cnf(c864,plain,
( skc12 != X966
| human_person(X966,skc15) ),
inference(resolution,[status(thm)],[c552,reflexivity]) ).
cnf(c549,plain,
( ~ proposition(skc12,X963)
| ~ proposition(skc12,X962)
| ~ theme(skc12,skf2(skc10),X963)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,X961)
| ~ theme(skc12,X961,X962)
| ~ agent(skc12,X961,skc10)
| X963 = X962 ),
inference(resolution,[status(thm)],[c384,clause71]) ).
cnf(c551,plain,
( skc12 != X958
| skc10 != X959
| human_person(X958,X959) ),
inference(resolution,[status(thm)],[c17,c333]) ).
cnf(c861,plain,
( skc12 != X960
| human_person(X960,skc10) ),
inference(resolution,[status(thm)],[c551,reflexivity]) ).
cnf(c550,plain,
( skc8 != X952
| skc10 != X953
| human_person(X952,X953) ),
inference(resolution,[status(thm)],[c17,c58]) ).
cnf(c858,plain,
( skc8 != X957
| human_person(X957,skc10) ),
inference(resolution,[status(thm)],[c550,reflexivity]) ).
cnf(c547,plain,
( ~ proposition(skc12,X956)
| ~ proposition(skc12,X955)
| ~ theme(skc12,skf2(skc15),X956)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ think_believe_consider(skc12,X954)
| ~ theme(skc12,X954,X955)
| ~ agent(skc12,X954,skc15)
| X956 = X955 ),
inference(resolution,[status(thm)],[c383,clause71]) ).
cnf(c548,plain,
( ~ accessible_world(skc12,X951)
| agent(X951,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c384,clause66]) ).
cnf(c546,plain,
( ~ accessible_world(skc12,X950)
| agent(X950,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c383,clause66]) ).
cnf(c16,axiom,
( X437 != X439
| X436 != X438
| ~ man(X437,X436)
| man(X439,X438) ),
theory(equality) ).
cnf(c545,plain,
( skc12 != X947
| skc10 != X948
| man(X947,X948) ),
inference(resolution,[status(thm)],[c16,c331]) ).
cnf(c856,plain,
( skc12 != X949
| man(X949,skc10) ),
inference(resolution,[status(thm)],[c545,reflexivity]) ).
cnf(c544,plain,
( skc12 != X944
| skc15 != X945
| man(X944,X945) ),
inference(resolution,[status(thm)],[c16,c379]) ).
cnf(c854,plain,
( skc12 != X946
| man(X946,skc15) ),
inference(resolution,[status(thm)],[c544,reflexivity]) ).
cnf(c543,plain,
( skc8 != X941
| skc15 != X942
| man(X941,X942) ),
inference(resolution,[status(thm)],[c16,clause73]) ).
cnf(c852,plain,
( skc8 != X943
| man(X943,skc15) ),
inference(resolution,[status(thm)],[c543,reflexivity]) ).
cnf(c542,plain,
( skc8 != X938
| skc10 != X939
| man(X938,X939) ),
inference(resolution,[status(thm)],[c16,clause81]) ).
cnf(c850,plain,
( skc8 != X940
| man(X940,skc10) ),
inference(resolution,[status(thm)],[c542,reflexivity]) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
cnf(c15,axiom,
( X428 != X430
| X427 != X429
| ~ state(X428,X427)
| state(X430,X429) ),
theory(equality) ).
cnf(c541,plain,
( skc8 != X935
| skc9 != X936
| state(X935,X936) ),
inference(resolution,[status(thm)],[c15,clause82]) ).
cnf(c848,plain,
( skc8 != X937
| state(X937,skc9) ),
inference(resolution,[status(thm)],[c541,reflexivity]) ).
cnf(clause51,axiom,
( ~ accessible_world(X154,X156)
| ~ state(X154,X155)
| state(X156,X155) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c229,plain,
( ~ accessible_world(skc8,X252)
| state(X252,skc9) ),
inference(resolution,[status(thm)],[clause51,clause82]) ).
cnf(c326,plain,
state(skc12,skc9),
inference(resolution,[status(thm)],[c229,clause83]) ).
cnf(c540,plain,
( skc12 != X932
| skc9 != X933
| state(X932,X933) ),
inference(resolution,[status(thm)],[c15,c326]) ).
cnf(c846,plain,
( skc12 != X934
| state(X934,skc9) ),
inference(resolution,[status(thm)],[c540,reflexivity]) ).
cnf(clause12,axiom,
( ~ abstraction(X25,X26)
| general(X25,X26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(clause9,axiom,
( ~ relation(X19,X20)
| abstraction(X19,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause28,axiom,
( ~ relname(X57,X58)
| relation(X57,X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c85,plain,
relation(skc8,skc14),
inference(resolution,[status(thm)],[clause28,c83]) ).
cnf(c88,plain,
abstraction(skc8,skc14),
inference(resolution,[status(thm)],[c85,clause9]) ).
cnf(c92,plain,
general(skc8,skc14),
inference(resolution,[status(thm)],[c88,clause12]) ).
cnf(c14,axiom,
( X419 != X421
| X418 != X420
| ~ general(X419,X418)
| general(X421,X420) ),
theory(equality) ).
cnf(c539,plain,
( skc8 != X930
| skc14 != X929
| general(X930,X929) ),
inference(resolution,[status(thm)],[c14,c92]) ).
cnf(c844,plain,
( skc8 != X931
| general(X931,skc14) ),
inference(resolution,[status(thm)],[c539,reflexivity]) ).
cnf(c86,plain,
relation(skc8,skc11),
inference(resolution,[status(thm)],[clause28,c84]) ).
cnf(clause47,axiom,
( ~ accessible_world(X132,X134)
| ~ relation(X132,X133)
| relation(X134,X133) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c207,plain,
( ~ accessible_world(skc8,X215)
| relation(X215,skc11) ),
inference(resolution,[status(thm)],[clause47,c86]) ).
cnf(c284,plain,
relation(skc12,skc11),
inference(resolution,[status(thm)],[c207,clause83]) ).
cnf(c286,plain,
abstraction(skc12,skc11),
inference(resolution,[status(thm)],[c284,clause9]) ).
cnf(c290,plain,
general(skc12,skc11),
inference(resolution,[status(thm)],[c286,clause12]) ).
cnf(c538,plain,
( skc12 != X926
| skc11 != X925
| general(X926,X925) ),
inference(resolution,[status(thm)],[c14,c290]) ).
cnf(c841,plain,
( skc12 != X928
| general(X928,skc11) ),
inference(resolution,[status(thm)],[c538,reflexivity]) ).
cnf(clause8,axiom,
( ~ proposition(X17,X18)
| relation(X17,X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
cnf(clause46,axiom,
( ~ accessible_world(X125,X127)
| ~ proposition(X125,X126)
| proposition(X127,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(c271,plain,
abstraction(skc12,skc12),
inference(resolution,[status(thm)],[c268,clause9]) ).
cnf(c275,plain,
general(skc12,skc12),
inference(resolution,[status(thm)],[c271,clause12]) ).
cnf(c537,plain,
( skc12 != X923
| skc12 != X922
| general(X923,X922) ),
inference(resolution,[status(thm)],[c14,c275]) ).
cnf(c839,plain,
( skc12 != X927
| general(X927,skc12) ),
inference(resolution,[status(thm)],[c537,reflexivity]) ).
cnf(c838,plain,
( skc12 != X924
| general(X924,X924) ),
inference(factor,[status(thm)],[c537]) ).
cnf(c89,plain,
abstraction(skc8,skc11),
inference(resolution,[status(thm)],[c86,clause9]) ).
cnf(c96,plain,
general(skc8,skc11),
inference(resolution,[status(thm)],[c89,clause12]) ).
cnf(c536,plain,
( skc8 != X920
| skc11 != X919
| general(X920,X919) ),
inference(resolution,[status(thm)],[c14,c96]) ).
cnf(c836,plain,
( skc8 != X921
| general(X921,skc11) ),
inference(resolution,[status(thm)],[c536,reflexivity]) ).
cnf(c208,plain,
( ~ accessible_world(skc8,X219)
| relation(X219,skc14) ),
inference(resolution,[status(thm)],[clause47,c85]) ).
cnf(c297,plain,
relation(skc12,skc14),
inference(resolution,[status(thm)],[c208,clause83]) ).
cnf(c301,plain,
abstraction(skc12,skc14),
inference(resolution,[status(thm)],[c297,clause9]) ).
cnf(c305,plain,
general(skc12,skc14),
inference(resolution,[status(thm)],[c301,clause12]) ).
cnf(c535,plain,
( skc12 != X917
| skc14 != X916
| general(X917,X916) ),
inference(resolution,[status(thm)],[c14,c305]) ).
cnf(c834,plain,
( skc12 != X918
| general(X918,skc14) ),
inference(resolution,[status(thm)],[c535,reflexivity]) ).
cnf(c44,plain,
relation(skc8,skc12),
inference(resolution,[status(thm)],[clause8,clause84]) ).
cnf(c45,plain,
abstraction(skc8,skc12),
inference(resolution,[status(thm)],[clause9,c44]) ).
cnf(c49,plain,
general(skc8,skc12),
inference(resolution,[status(thm)],[clause12,c45]) ).
cnf(c534,plain,
( skc8 != X914
| skc12 != X913
| general(X914,X913) ),
inference(resolution,[status(thm)],[c14,c49]) ).
cnf(c832,plain,
( skc8 != X915
| general(X915,skc12) ),
inference(resolution,[status(thm)],[c534,reflexivity]) ).
cnf(clause11,axiom,
( ~ abstraction(X23,X24)
| nonhuman(X23,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c274,plain,
nonhuman(skc12,skc12),
inference(resolution,[status(thm)],[c271,clause11]) ).
cnf(c13,axiom,
( X412 != X414
| X411 != X413
| ~ nonhuman(X412,X411)
| nonhuman(X414,X413) ),
theory(equality) ).
cnf(c530,plain,
( skc12 != X909
| skc12 != X908
| nonhuman(X909,X908) ),
inference(resolution,[status(thm)],[c13,c274]) ).
cnf(c828,plain,
( skc12 != X912
| nonhuman(X912,skc12) ),
inference(resolution,[status(thm)],[c530,reflexivity]) ).
cnf(c48,plain,
nonhuman(skc8,skc12),
inference(resolution,[status(thm)],[clause11,c45]) ).
cnf(c529,plain,
( skc8 != X907
| skc12 != X906
| nonhuman(X907,X906) ),
inference(resolution,[status(thm)],[c13,c48]) ).
cnf(c826,plain,
( skc8 != X911
| nonhuman(X911,skc12) ),
inference(resolution,[status(thm)],[c529,reflexivity]) ).
cnf(c827,plain,
( skc12 != X910
| nonhuman(X910,X910) ),
inference(factor,[status(thm)],[c530]) ).
cnf(c304,plain,
nonhuman(skc12,skc14),
inference(resolution,[status(thm)],[c301,clause11]) ).
cnf(c528,plain,
( skc12 != X903
| skc14 != X902
| nonhuman(X903,X902) ),
inference(resolution,[status(thm)],[c13,c304]) ).
cnf(c823,plain,
( skc12 != X905
| nonhuman(X905,skc14) ),
inference(resolution,[status(thm)],[c528,reflexivity]) ).
cnf(c95,plain,
nonhuman(skc8,skc11),
inference(resolution,[status(thm)],[c89,clause11]) ).
cnf(c527,plain,
( skc8 != X901
| skc11 != X900
| nonhuman(X901,X900) ),
inference(resolution,[status(thm)],[c13,c95]) ).
cnf(c822,plain,
( skc8 != X904
| nonhuman(X904,skc11) ),
inference(resolution,[status(thm)],[c527,reflexivity]) ).
cnf(c91,plain,
nonhuman(skc8,skc14),
inference(resolution,[status(thm)],[c88,clause11]) ).
cnf(c526,plain,
( skc8 != X897
| skc14 != X896
| nonhuman(X897,X896) ),
inference(resolution,[status(thm)],[c13,c91]) ).
cnf(c819,plain,
( skc8 != X899
| nonhuman(X899,skc14) ),
inference(resolution,[status(thm)],[c526,reflexivity]) ).
cnf(c289,plain,
nonhuman(skc12,skc11),
inference(resolution,[status(thm)],[c286,clause11]) ).
cnf(c525,plain,
( skc12 != X895
| skc11 != X894
| nonhuman(X895,X894) ),
inference(resolution,[status(thm)],[c13,c289]) ).
cnf(c818,plain,
( skc12 != X898
| nonhuman(X898,skc11) ),
inference(resolution,[status(thm)],[c525,reflexivity]) ).
cnf(c12,axiom,
( X405 != X407
| X404 != X406
| ~ abstraction(X405,X404)
| abstraction(X407,X406) ),
theory(equality) ).
cnf(c521,plain,
( skc8 != X890
| skc14 != X891
| abstraction(X890,X891) ),
inference(resolution,[status(thm)],[c12,c88]) ).
cnf(c815,plain,
( skc8 != X893
| abstraction(X893,skc14) ),
inference(resolution,[status(thm)],[c521,reflexivity]) ).
cnf(c520,plain,
( skc8 != X888
| skc12 != X889
| abstraction(X888,X889) ),
inference(resolution,[status(thm)],[c12,c45]) ).
cnf(c814,plain,
( skc8 != X892
| abstraction(X892,skc12) ),
inference(resolution,[status(thm)],[c520,reflexivity]) ).
cnf(c519,plain,
( skc12 != X884
| skc11 != X885
| abstraction(X884,X885) ),
inference(resolution,[status(thm)],[c12,c286]) ).
cnf(c811,plain,
( skc12 != X887
| abstraction(X887,skc11) ),
inference(resolution,[status(thm)],[c519,reflexivity]) ).
cnf(c518,plain,
( skc8 != X882
| skc11 != X883
| abstraction(X882,X883) ),
inference(resolution,[status(thm)],[c12,c89]) ).
cnf(c810,plain,
( skc8 != X886
| abstraction(X886,skc11) ),
inference(resolution,[status(thm)],[c518,reflexivity]) ).
cnf(c517,plain,
( skc12 != X878
| skc14 != X879
| abstraction(X878,X879) ),
inference(resolution,[status(thm)],[c12,c301]) ).
cnf(c807,plain,
( skc12 != X881
| abstraction(X881,skc14) ),
inference(resolution,[status(thm)],[c517,reflexivity]) ).
cnf(c516,plain,
( skc12 != X875
| skc12 != X876
| abstraction(X875,X876) ),
inference(resolution,[status(thm)],[c12,c271]) ).
cnf(c805,plain,
( skc12 != X880
| abstraction(X880,skc12) ),
inference(resolution,[status(thm)],[c516,reflexivity]) ).
cnf(c804,plain,
( skc12 != X877
| abstraction(X877,X877) ),
inference(factor,[status(thm)],[c516]) ).
cnf(c11,axiom,
( X398 != X400
| X397 != X399
| ~ relation(X398,X397)
| relation(X400,X399) ),
theory(equality) ).
cnf(c514,plain,
( skc8 != X872
| skc14 != X873
| relation(X872,X873) ),
inference(resolution,[status(thm)],[c11,c85]) ).
cnf(c802,plain,
( skc8 != X874
| relation(X874,skc14) ),
inference(resolution,[status(thm)],[c514,reflexivity]) ).
cnf(c513,plain,
( skc12 != X869
| skc14 != X870
| relation(X869,X870) ),
inference(resolution,[status(thm)],[c11,c297]) ).
cnf(c800,plain,
( skc12 != X871
| relation(X871,skc14) ),
inference(resolution,[status(thm)],[c513,reflexivity]) ).
cnf(c512,plain,
( skc12 != X866
| skc11 != X867
| relation(X866,X867) ),
inference(resolution,[status(thm)],[c11,c284]) ).
cnf(c798,plain,
( skc12 != X868
| relation(X868,skc11) ),
inference(resolution,[status(thm)],[c512,reflexivity]) ).
cnf(c511,plain,
( skc12 != X862
| skc12 != X863
| relation(X862,X863) ),
inference(resolution,[status(thm)],[c11,c268]) ).
cnf(c795,plain,
( skc12 != X865
| relation(X865,skc12) ),
inference(resolution,[status(thm)],[c511,reflexivity]) ).
cnf(c794,plain,
( skc12 != X864
| relation(X864,X864) ),
inference(factor,[status(thm)],[c511]) ).
cnf(c510,plain,
( skc8 != X859
| skc12 != X860
| relation(X859,X860) ),
inference(resolution,[status(thm)],[c11,c44]) ).
cnf(c792,plain,
( skc8 != X861
| relation(X861,skc12) ),
inference(resolution,[status(thm)],[c510,reflexivity]) ).
cnf(c509,plain,
( skc8 != X856
| skc11 != X857
| relation(X856,X857) ),
inference(resolution,[status(thm)],[c11,c86]) ).
cnf(c790,plain,
( skc8 != X858
| relation(X858,skc11) ),
inference(resolution,[status(thm)],[c509,reflexivity]) ).
cnf(c10,axiom,
( X391 != X393
| X390 != X392
| ~ proposition(X391,X390)
| proposition(X393,X392) ),
theory(equality) ).
cnf(c505,plain,
( skc12 != X851
| skc12 != X852
| proposition(X851,X852) ),
inference(resolution,[status(thm)],[c10,c267]) ).
cnf(c786,plain,
( skc12 != X855
| proposition(X855,skc12) ),
inference(resolution,[status(thm)],[c505,reflexivity]) ).
cnf(c504,plain,
( skc8 != X849
| skc12 != X850
| proposition(X849,X850) ),
inference(resolution,[status(thm)],[c10,clause84]) ).
cnf(c784,plain,
( skc8 != X854
| proposition(X854,skc12) ),
inference(resolution,[status(thm)],[c504,reflexivity]) ).
cnf(c785,plain,
( skc12 != X853
| proposition(X853,X853) ),
inference(factor,[status(thm)],[c505]) ).
cnf(clause13,axiom,
( ~ abstraction(X27,X28)
| unisex(X27,X28) ),
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(X110,X112)
| ~ unisex(X110,X111)
| unisex(X112,X111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c182,plain,
( ~ accessible_world(skc8,X182)
| unisex(X182,skc12) ),
inference(resolution,[status(thm)],[clause43,c50]) ).
cnf(c248,plain,
unisex(skc12,skc12),
inference(resolution,[status(thm)],[c182,clause83]) ).
cnf(c9,axiom,
( X386 != X388
| X385 != X387
| ~ unisex(X386,X385)
| unisex(X388,X387) ),
theory(equality) ).
cnf(c496,plain,
( skc12 != X846
| skc12 != X845
| unisex(X846,X845) ),
inference(resolution,[status(thm)],[c9,c248]) ).
cnf(c781,plain,
( skc12 != X848
| unisex(X848,skc12) ),
inference(resolution,[status(thm)],[c496,reflexivity]) ).
cnf(c780,plain,
( skc12 != X847
| unisex(X847,X847) ),
inference(factor,[status(thm)],[c496]) ).
cnf(clause7,axiom,
( ~ eventuality(X15,X16)
| unisex(X15,X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause2,axiom,
( ~ event(X5,X6)
| eventuality(X5,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
cnf(clause37,axiom,
( ~ accessible_world(X84,X86)
| ~ event(X84,X85)
| event(X86,X85) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
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(c142,plain,
eventuality(skc12,skc13),
inference(resolution,[status(thm)],[c141,clause2]) ).
cnf(c147,plain,
unisex(skc12,skc13),
inference(resolution,[status(thm)],[c142,clause7]) ).
cnf(c495,plain,
( skc12 != X843
| skc13 != X842
| unisex(X843,X842) ),
inference(resolution,[status(thm)],[c9,c147]) ).
cnf(c778,plain,
( skc12 != X844
| unisex(X844,skc13) ),
inference(resolution,[status(thm)],[c495,reflexivity]) ).
cnf(c90,plain,
unisex(skc8,skc14),
inference(resolution,[status(thm)],[c88,clause13]) ).
cnf(c180,plain,
( ~ accessible_world(skc8,X177)
| unisex(X177,skc14) ),
inference(resolution,[status(thm)],[clause43,c90]) ).
cnf(c242,plain,
unisex(skc12,skc14),
inference(resolution,[status(thm)],[c180,clause83]) ).
cnf(c494,plain,
( skc12 != X840
| skc14 != X839
| unisex(X840,X839) ),
inference(resolution,[status(thm)],[c9,c242]) ).
cnf(c776,plain,
( skc12 != X841
| unisex(X841,skc14) ),
inference(resolution,[status(thm)],[c494,reflexivity]) ).
cnf(c94,plain,
unisex(skc8,skc11),
inference(resolution,[status(thm)],[c89,clause13]) ).
cnf(c493,plain,
( skc8 != X837
| skc11 != X836
| unisex(X837,X836) ),
inference(resolution,[status(thm)],[c9,c94]) ).
cnf(c774,plain,
( skc8 != X838
| unisex(X838,skc11) ),
inference(resolution,[status(thm)],[c493,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(c492,plain,
( skc8 != X834
| skc13 != X833
| unisex(X834,X833) ),
inference(resolution,[status(thm)],[c9,c43]) ).
cnf(c772,plain,
( skc8 != X835
| unisex(X835,skc13) ),
inference(resolution,[status(thm)],[c492,reflexivity]) ).
cnf(c491,plain,
( skc8 != X831
| skc12 != X830
| unisex(X831,X830) ),
inference(resolution,[status(thm)],[c9,c50]) ).
cnf(c770,plain,
( skc8 != X832
| unisex(X832,skc12) ),
inference(resolution,[status(thm)],[c491,reflexivity]) ).
cnf(c362,plain,
eventuality(skc12,skf2(X274)),
inference(resolution,[status(thm)],[c361,clause2]) ).
cnf(c367,plain,
unisex(skc12,skf2(X279)),
inference(resolution,[status(thm)],[c362,clause7]) ).
cnf(c490,plain,
( skc12 != X825
| skf2(X826) != X824
| unisex(X825,X824) ),
inference(resolution,[status(thm)],[c9,c367]) ).
cnf(c768,plain,
( skc12 != X828
| unisex(X828,skf2(X827)) ),
inference(resolution,[status(thm)],[c490,reflexivity]) ).
cnf(clause14,axiom,
( ~ state(X29,X30)
| eventuality(X29,X30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c51,plain,
eventuality(skc8,skc9),
inference(resolution,[status(thm)],[clause14,clause82]) ).
cnf(c54,plain,
unisex(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause7]) ).
cnf(c489,plain,
( skc8 != X822
| skc9 != X821
| unisex(X822,X821) ),
inference(resolution,[status(thm)],[c9,c54]) ).
cnf(c766,plain,
( skc8 != X823
| unisex(X823,skc9) ),
inference(resolution,[status(thm)],[c489,reflexivity]) ).
cnf(c184,plain,
( ~ accessible_world(skc8,X187)
| unisex(X187,skc11) ),
inference(resolution,[status(thm)],[clause43,c94]) ).
cnf(c254,plain,
unisex(skc12,skc11),
inference(resolution,[status(thm)],[c184,clause83]) ).
cnf(c488,plain,
( skc12 != X819
| skc11 != X818
| unisex(X819,X818) ),
inference(resolution,[status(thm)],[c9,c254]) ).
cnf(c764,plain,
( skc12 != X820
| unisex(X820,skc11) ),
inference(resolution,[status(thm)],[c488,reflexivity]) ).
cnf(c487,plain,
( skc8 != X816
| skc14 != X815
| unisex(X816,X815) ),
inference(resolution,[status(thm)],[c9,c90]) ).
cnf(c762,plain,
( skc8 != X817
| unisex(X817,skc14) ),
inference(resolution,[status(thm)],[c487,reflexivity]) ).
cnf(clause15,axiom,
( ~ state(X31,X32)
| event(X31,X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c52,plain,
event(skc8,skc9),
inference(resolution,[status(thm)],[clause15,clause82]) ).
cnf(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(c121,plain,
eventuality(skc12,skc9),
inference(resolution,[status(thm)],[c120,clause2]) ).
cnf(c124,plain,
unisex(skc12,skc9),
inference(resolution,[status(thm)],[c121,clause7]) ).
cnf(c486,plain,
( skc12 != X813
| skc9 != X812
| unisex(X813,X812) ),
inference(resolution,[status(thm)],[c9,c124]) ).
cnf(c760,plain,
( skc12 != X814
| unisex(X814,skc9) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(clause6,axiom,
( ~ eventuality(X13,X14)
| nonexistent(X13,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c123,plain,
nonexistent(skc12,skc9),
inference(resolution,[status(thm)],[c121,clause6]) ).
cnf(c8,axiom,
( X378 != X380
| X377 != X379
| ~ nonexistent(X378,X377)
| nonexistent(X380,X379) ),
theory(equality) ).
cnf(c483,plain,
( skc12 != X810
| skc9 != X809
| nonexistent(X810,X809) ),
inference(resolution,[status(thm)],[c8,c123]) ).
cnf(c758,plain,
( skc12 != X811
| nonexistent(X811,skc9) ),
inference(resolution,[status(thm)],[c483,reflexivity]) ).
cnf(c366,plain,
nonexistent(skc12,skf2(X278)),
inference(resolution,[status(thm)],[c362,clause6]) ).
cnf(c481,plain,
( skc12 != X805
| skf2(X803) != X804
| nonexistent(X805,X804) ),
inference(resolution,[status(thm)],[c8,c366]) ).
cnf(c756,plain,
( skc12 != X806
| nonexistent(X806,skf2(X807)) ),
inference(resolution,[status(thm)],[c481,reflexivity]) ).
cnf(c146,plain,
nonexistent(skc12,skc13),
inference(resolution,[status(thm)],[c142,clause6]) ).
cnf(c482,plain,
( skc12 != X801
| skc13 != X800
| nonexistent(X801,X800) ),
inference(resolution,[status(thm)],[c8,c146]) ).
cnf(c754,plain,
( skc12 != X802
| nonexistent(X802,skc13) ),
inference(resolution,[status(thm)],[c482,reflexivity]) ).
cnf(c42,plain,
nonexistent(skc8,skc13),
inference(resolution,[status(thm)],[clause6,c38]) ).
cnf(c480,plain,
( skc8 != X798
| skc13 != X797
| nonexistent(X798,X797) ),
inference(resolution,[status(thm)],[c8,c42]) ).
cnf(c752,plain,
( skc8 != X799
| nonexistent(X799,skc13) ),
inference(resolution,[status(thm)],[c480,reflexivity]) ).
cnf(c53,plain,
nonexistent(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause6]) ).
cnf(c479,plain,
( skc8 != X795
| skc9 != X794
| nonexistent(X795,X794) ),
inference(resolution,[status(thm)],[c8,c53]) ).
cnf(c750,plain,
( skc8 != X796
| nonexistent(X796,skc9) ),
inference(resolution,[status(thm)],[c479,reflexivity]) ).
cnf(clause20,axiom,
( ~ entity(X41,X42)
| specific(X41,X42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c70,plain,
specific(skc8,skc10),
inference(resolution,[status(thm)],[clause20,c63]) ).
cnf(clause41,axiom,
( ~ accessible_world(X98,X100)
| ~ specific(X98,X99)
| specific(X100,X99) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c164,plain,
( ~ accessible_world(skc8,X157)
| specific(X157,skc10) ),
inference(resolution,[status(thm)],[clause41,c70]) ).
cnf(c230,plain,
specific(skc12,skc10),
inference(resolution,[status(thm)],[c164,clause83]) ).
cnf(c7,axiom,
( X371 != X373
| X370 != X372
| ~ specific(X371,X370)
| specific(X373,X372) ),
theory(equality) ).
cnf(c477,plain,
( skc12 != X792
| skc10 != X791
| specific(X792,X791) ),
inference(resolution,[status(thm)],[c7,c230]) ).
cnf(c748,plain,
( skc12 != X793
| specific(X793,skc10) ),
inference(resolution,[status(thm)],[c477,reflexivity]) ).
cnf(clause5,axiom,
( ~ eventuality(X11,X12)
| specific(X11,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c41,plain,
specific(skc8,skc13),
inference(resolution,[status(thm)],[clause5,c38]) ).
cnf(c476,plain,
( skc8 != X789
| skc13 != X788
| specific(X789,X788) ),
inference(resolution,[status(thm)],[c7,c41]) ).
cnf(c746,plain,
( skc8 != X790
| specific(X790,skc13) ),
inference(resolution,[status(thm)],[c476,reflexivity]) ).
cnf(c69,plain,
specific(skc8,skc15),
inference(resolution,[status(thm)],[clause20,c64]) ).
cnf(c162,plain,
( ~ accessible_world(skc8,X152)
| specific(X152,skc15) ),
inference(resolution,[status(thm)],[clause41,c69]) ).
cnf(c225,plain,
specific(skc12,skc15),
inference(resolution,[status(thm)],[c162,clause83]) ).
cnf(c475,plain,
( skc12 != X786
| skc15 != X785
| specific(X786,X785) ),
inference(resolution,[status(thm)],[c7,c225]) ).
cnf(c744,plain,
( skc12 != X787
| specific(X787,skc15) ),
inference(resolution,[status(thm)],[c475,reflexivity]) ).
cnf(c148,plain,
specific(skc12,skc13),
inference(resolution,[status(thm)],[c142,clause5]) ).
cnf(c474,plain,
( skc12 != X783
| skc13 != X782
| specific(X783,X782) ),
inference(resolution,[status(thm)],[c7,c148]) ).
cnf(c742,plain,
( skc12 != X784
| specific(X784,skc13) ),
inference(resolution,[status(thm)],[c474,reflexivity]) ).
cnf(c368,plain,
specific(skc12,skf2(X280)),
inference(resolution,[status(thm)],[c362,clause5]) ).
cnf(c469,plain,
( skc12 != X778
| skf2(X776) != X777
| specific(X778,X777) ),
inference(resolution,[status(thm)],[c7,c368]) ).
cnf(c740,plain,
( skc12 != X780
| specific(X780,skf2(X779)) ),
inference(resolution,[status(thm)],[c469,reflexivity]) ).
cnf(c125,plain,
specific(skc12,skc9),
inference(resolution,[status(thm)],[c121,clause5]) ).
cnf(c473,plain,
( skc12 != X774
| skc9 != X773
| specific(X774,X773) ),
inference(resolution,[status(thm)],[c7,c125]) ).
cnf(c738,plain,
( skc12 != X775
| specific(X775,skc9) ),
inference(resolution,[status(thm)],[c473,reflexivity]) ).
cnf(clause4,axiom,
( ~ thing(X9,X10)
| singleton(X9,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause3,axiom,
( ~ eventuality(X7,X8)
| thing(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c364,plain,
thing(skc12,skf2(X277)),
inference(resolution,[status(thm)],[c362,clause3]) ).
cnf(c370,plain,
singleton(skc12,skf2(X284)),
inference(resolution,[status(thm)],[c364,clause4]) ).
cnf(c6,axiom,
( X363 != X365
| X362 != X364
| ~ singleton(X363,X362)
| singleton(X365,X364) ),
theory(equality) ).
cnf(c455,plain,
( skc12 != X769
| skf2(X768) != X767
| singleton(X769,X767) ),
inference(resolution,[status(thm)],[c6,c370]) ).
cnf(c736,plain,
( skc12 != X770
| singleton(X770,skf2(X771)) ),
inference(resolution,[status(thm)],[c455,reflexivity]) ).
cnf(c472,plain,
( skc8 != X765
| skc10 != X764
| specific(X765,X764) ),
inference(resolution,[status(thm)],[c7,c70]) ).
cnf(c734,plain,
( skc8 != X766
| specific(X766,skc10) ),
inference(resolution,[status(thm)],[c472,reflexivity]) ).
cnf(c5,axiom,
( X356 != X358
| X355 != X357
| ~ thing(X356,X355)
| thing(X358,X357) ),
theory(equality) ).
cnf(c443,plain,
( skc12 != X760
| skf2(X759) != X758
| thing(X760,X758) ),
inference(resolution,[status(thm)],[c5,c364]) ).
cnf(c732,plain,
( skc12 != X762
| thing(X762,skf2(X761)) ),
inference(resolution,[status(thm)],[c443,reflexivity]) ).
cnf(c55,plain,
specific(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause5]) ).
cnf(c471,plain,
( skc8 != X756
| skc9 != X755
| specific(X756,X755) ),
inference(resolution,[status(thm)],[c7,c55]) ).
cnf(c730,plain,
( skc8 != X757
| specific(X757,skc9) ),
inference(resolution,[status(thm)],[c471,reflexivity]) ).
cnf(c4,axiom,
( X349 != X351
| X348 != X350
| ~ eventuality(X349,X348)
| eventuality(X351,X350) ),
theory(equality) ).
cnf(c431,plain,
( skc12 != X750
| skf2(X751) != X749
| eventuality(X750,X749) ),
inference(resolution,[status(thm)],[c4,c362]) ).
cnf(c728,plain,
( skc12 != X753
| eventuality(X753,skf2(X752)) ),
inference(resolution,[status(thm)],[c431,reflexivity]) ).
cnf(c470,plain,
( skc8 != X747
| skc15 != X746
| specific(X747,X746) ),
inference(resolution,[status(thm)],[c7,c69]) ).
cnf(c726,plain,
( skc8 != X748
| specific(X748,skc15) ),
inference(resolution,[status(thm)],[c470,reflexivity]) ).
cnf(c3,axiom,
( X342 != X344
| X341 != X343
| ~ event(X342,X341)
| event(X344,X343) ),
theory(equality) ).
cnf(c425,plain,
( skc12 != X742
| skf2(X740) != X741
| event(X742,X741) ),
inference(resolution,[status(thm)],[c3,c361]) ).
cnf(c724,plain,
( skc12 != X743
| event(X743,skf2(X744)) ),
inference(resolution,[status(thm)],[c425,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(c466,plain,
( skc8 != X738
| skc13 != X737
| singleton(X738,X737) ),
inference(resolution,[status(thm)],[c6,c40]) ).
cnf(c722,plain,
( skc8 != X739
| singleton(X739,skc13) ),
inference(resolution,[status(thm)],[c466,reflexivity]) ).
cnf(c2,axiom,
( X335 != X337
| X334 != X336
| ~ smoke(X335,X334)
| smoke(X337,X336) ),
theory(equality) ).
cnf(c418,plain,
( skc12 != X733
| skf2(X732) != X731
| smoke(X733,X731) ),
inference(resolution,[status(thm)],[c2,c359]) ).
cnf(c720,plain,
( skc12 != X734
| smoke(X734,skf2(X735)) ),
inference(resolution,[status(thm)],[c418,reflexivity]) ).
cnf(clause19,axiom,
( ~ entity(X39,X40)
| thing(X39,X40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c66,plain,
thing(skc8,skc10),
inference(resolution,[status(thm)],[clause19,c63]) ).
cnf(clause39,axiom,
( ~ accessible_world(X91,X93)
| ~ thing(X91,X92)
| thing(X93,X92) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c137,plain,
( ~ accessible_world(skc8,X118)
| thing(X118,skc10) ),
inference(resolution,[status(thm)],[clause39,c66]) ).
cnf(c194,plain,
thing(skc12,skc10),
inference(resolution,[status(thm)],[c137,clause83]) ).
cnf(c195,plain,
singleton(skc12,skc10),
inference(resolution,[status(thm)],[c194,clause4]) ).
cnf(c465,plain,
( skc12 != X729
| skc10 != X728
| singleton(X729,X728) ),
inference(resolution,[status(thm)],[c6,c195]) ).
cnf(c718,plain,
( skc12 != X730
| singleton(X730,skc10) ),
inference(resolution,[status(thm)],[c465,reflexivity]) ).
cnf(clause10,axiom,
( ~ abstraction(X21,X22)
| thing(X21,X22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c97,plain,
thing(skc8,skc11),
inference(resolution,[status(thm)],[c89,clause10]) ).
cnf(c105,plain,
singleton(skc8,skc11),
inference(resolution,[status(thm)],[c97,clause4]) ).
cnf(c464,plain,
( skc8 != X716
| skc11 != X715
| singleton(X716,X715) ),
inference(resolution,[status(thm)],[c6,c105]) ).
cnf(c714,plain,
( skc8 != X727
| singleton(X727,skc11) ),
inference(resolution,[status(thm)],[c464,reflexivity]) ).
cnf(c407,plain,
( ~ state(X718,X725)
| ~ man(X718,X721)
| ~ be(X718,X725,X721,X721)
| ~ forename(X718,X724)
| ~ jules_forename(X718,X724)
| ~ of(X718,X724,X721)
| ~ accessible_world(X718,X726)
| ~ proposition(X718,X726)
| ~ proposition(X718,X718)
| ~ accessible_world(X718,X718)
| ~ smoke(X718,X720)
| ~ present(X718,X720)
| ~ agent(X718,X720,skf4(X718))
| ~ event(X718,X720)
| ~ think_believe_consider(X718,X720)
| ~ theme(X718,X720,X718)
| ~ forename(X718,X722)
| ~ jules_forename(X718,X722)
| ~ of(X718,X722,skf4(X718))
| ~ smoke(X726,X719)
| ~ present(X726,X719)
| ~ agent(X726,X719,skf4(X718))
| ~ event(X726,X719)
| ~ agent(X718,X717,skf4(X718))
| ~ man(X718,skf4(X718))
| ~ of(X718,X723,skf4(X718))
| ~ vincent_forename(X718,X723)
| ~ forename(X718,X723)
| ~ theme(X718,X717,X726)
| ~ event(X718,X717)
| ~ present(X718,X717)
| ~ think_believe_consider(X718,X717)
| ~ actual_world(X718) ),
inference(factor,[status(thm)],[clause95]) ).
cnf(c126,plain,
thing(skc12,skc9),
inference(resolution,[status(thm)],[c121,clause3]) ).
cnf(c132,plain,
singleton(skc12,skc9),
inference(resolution,[status(thm)],[c126,clause4]) ).
cnf(c463,plain,
( skc12 != X713
| skc9 != X712
| singleton(X713,X712) ),
inference(resolution,[status(thm)],[c6,c132]) ).
cnf(c712,plain,
( skc12 != X714
| singleton(X714,skc9) ),
inference(resolution,[status(thm)],[c463,reflexivity]) ).
cnf(c46,plain,
thing(skc8,skc12),
inference(resolution,[status(thm)],[clause10,c45]) ).
cnf(c140,plain,
( ~ accessible_world(skc8,X124)
| thing(X124,skc12) ),
inference(resolution,[status(thm)],[clause39,c46]) ).
cnf(c201,plain,
thing(skc12,skc12),
inference(resolution,[status(thm)],[c140,clause83]) ).
cnf(c202,plain,
singleton(skc12,skc12),
inference(resolution,[status(thm)],[c201,clause4]) ).
cnf(c462,plain,
( skc12 != X699
| skc12 != X698
| singleton(X699,X698) ),
inference(resolution,[status(thm)],[c6,c202]) ).
cnf(c707,plain,
( skc12 != X701
| singleton(X701,skc12) ),
inference(resolution,[status(thm)],[c462,reflexivity]) ).
cnf(c706,plain,
( skc12 != X700
| singleton(X700,X700) ),
inference(factor,[status(thm)],[c462]) ).
cnf(c65,plain,
thing(skc8,skc15),
inference(resolution,[status(thm)],[clause19,c64]) ).
cnf(c134,plain,
( ~ accessible_world(skc8,X109)
| thing(X109,skc15) ),
inference(resolution,[status(thm)],[clause39,c65]) ).
cnf(c178,plain,
thing(skc12,skc15),
inference(resolution,[status(thm)],[c134,clause83]) ).
cnf(c186,plain,
singleton(skc12,skc15),
inference(resolution,[status(thm)],[c178,clause4]) ).
cnf(c461,plain,
( skc12 != X686
| skc15 != X685
| singleton(X686,X685) ),
inference(resolution,[status(thm)],[c6,c186]) ).
cnf(c702,plain,
( skc12 != X687
| singleton(X687,skc15) ),
inference(resolution,[status(thm)],[c461,reflexivity]) ).
cnf(c47,plain,
singleton(skc8,skc12),
inference(resolution,[status(thm)],[c46,clause4]) ).
cnf(c460,plain,
( skc8 != X683
| skc12 != X682
| singleton(X683,X682) ),
inference(resolution,[status(thm)],[c6,c47]) ).
cnf(c700,plain,
( skc8 != X684
| singleton(X684,skc12) ),
inference(resolution,[status(thm)],[c460,reflexivity]) ).
cnf(c56,plain,
thing(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause3]) ).
cnf(c60,plain,
singleton(skc8,skc9),
inference(resolution,[status(thm)],[c56,clause4]) ).
cnf(c459,plain,
( skc8 != X671
| skc9 != X670
| singleton(X671,X670) ),
inference(resolution,[status(thm)],[c6,c60]) ).
cnf(c696,plain,
( skc8 != X672
| singleton(X672,skc9) ),
inference(resolution,[status(thm)],[c459,reflexivity]) ).
cnf(c67,plain,
singleton(skc8,skc15),
inference(resolution,[status(thm)],[c65,clause4]) ).
cnf(c458,plain,
( skc8 != X665
| skc15 != X664
| singleton(X665,X664) ),
inference(resolution,[status(thm)],[c6,c67]) ).
cnf(c693,plain,
( skc8 != X669
| singleton(X669,skc15) ),
inference(resolution,[status(thm)],[c458,reflexivity]) ).
cnf(c350,plain,
( ~ proposition(skc8,X668)
| ~ proposition(skc8,X667)
| ~ theme(skc8,skc13,X668)
| ~ think_believe_consider(skc8,skc13)
| ~ think_believe_consider(skc8,X666)
| ~ theme(skc8,X666,X667)
| ~ agent(skc8,X666,skc15)
| X668 = X667 ),
inference(resolution,[status(thm)],[clause71,clause86]) ).
cnf(c93,plain,
thing(skc8,skc14),
inference(resolution,[status(thm)],[c88,clause10]) ).
cnf(c99,plain,
singleton(skc8,skc14),
inference(resolution,[status(thm)],[c93,clause4]) ).
cnf(c457,plain,
( skc8 != X662
| skc14 != X661
| singleton(X662,X661) ),
inference(resolution,[status(thm)],[c6,c99]) ).
cnf(c691,plain,
( skc8 != X663
| singleton(X663,skc14) ),
inference(resolution,[status(thm)],[c457,reflexivity]) ).
cnf(c133,plain,
( ~ accessible_world(skc8,X108)
| thing(X108,skc11) ),
inference(resolution,[status(thm)],[clause39,c97]) ).
cnf(c174,plain,
thing(skc12,skc11),
inference(resolution,[status(thm)],[c133,clause83]) ).
cnf(c175,plain,
singleton(skc12,skc11),
inference(resolution,[status(thm)],[c174,clause4]) ).
cnf(c456,plain,
( skc12 != X654
| skc11 != X653
| singleton(X654,X653) ),
inference(resolution,[status(thm)],[c6,c175]) ).
cnf(c685,plain,
( skc12 != X655
| singleton(X655,skc11) ),
inference(resolution,[status(thm)],[c456,reflexivity]) ).
cnf(c144,plain,
thing(skc12,skc13),
inference(resolution,[status(thm)],[c142,clause3]) ).
cnf(c149,plain,
singleton(skc12,skc13),
inference(resolution,[status(thm)],[c144,clause4]) ).
cnf(c454,plain,
( skc12 != X651
| skc13 != X650
| singleton(X651,X650) ),
inference(resolution,[status(thm)],[c6,c149]) ).
cnf(c683,plain,
( skc12 != X652
| singleton(X652,skc13) ),
inference(resolution,[status(thm)],[c454,reflexivity]) ).
cnf(c337,plain,
( ~ forename(skc8,skc11)
| ~ of(skc8,X649,skc10)
| ~ forename(skc8,X649)
| ~ entity(skc8,skc10)
| X649 = skc11 ),
inference(resolution,[status(thm)],[clause70,clause88]) ).
cnf(c68,plain,
singleton(skc8,skc10),
inference(resolution,[status(thm)],[c66,clause4]) ).
cnf(c453,plain,
( skc8 != X647
| skc10 != X646
| singleton(X647,X646) ),
inference(resolution,[status(thm)],[c6,c68]) ).
cnf(c680,plain,
( skc8 != X648
| singleton(X648,skc10) ),
inference(resolution,[status(thm)],[c453,reflexivity]) ).
cnf(c135,plain,
( ~ accessible_world(skc8,X113)
| thing(X113,skc14) ),
inference(resolution,[status(thm)],[clause39,c93]) ).
cnf(c189,plain,
thing(skc12,skc14),
inference(resolution,[status(thm)],[c135,clause83]) ).
cnf(c190,plain,
singleton(skc12,skc14),
inference(resolution,[status(thm)],[c189,clause4]) ).
cnf(c452,plain,
( skc12 != X643
| skc14 != X642
| singleton(X643,X642) ),
inference(resolution,[status(thm)],[c6,c190]) ).
cnf(c677,plain,
( skc12 != X645
| singleton(X645,skc14) ),
inference(resolution,[status(thm)],[c452,reflexivity]) ).
cnf(c336,plain,
( ~ forename(skc8,skc14)
| ~ of(skc8,X644,skc15)
| ~ forename(skc8,X644)
| ~ entity(skc8,skc15)
| X644 = skc14 ),
inference(resolution,[status(thm)],[clause70,clause85]) ).
cnf(c449,plain,
( skc8 != X640
| skc12 != X639
| thing(X640,X639) ),
inference(resolution,[status(thm)],[c5,c46]) ).
cnf(c675,plain,
( skc8 != X641
| thing(X641,skc12) ),
inference(resolution,[status(thm)],[c449,reflexivity]) ).
cnf(c448,plain,
( skc8 != X634
| skc13 != X633
| thing(X634,X633) ),
inference(resolution,[status(thm)],[c5,c39]) ).
cnf(c673,plain,
( skc8 != X635
| thing(X635,skc13) ),
inference(resolution,[status(thm)],[c448,reflexivity]) ).
cnf(c447,plain,
( skc8 != X631
| skc9 != X630
| thing(X631,X630) ),
inference(resolution,[status(thm)],[c5,c56]) ).
cnf(c671,plain,
( skc8 != X632
| thing(X632,skc9) ),
inference(resolution,[status(thm)],[c447,reflexivity]) ).
cnf(c446,plain,
( skc12 != X622
| skc13 != X621
| thing(X622,X621) ),
inference(resolution,[status(thm)],[c5,c144]) ).
cnf(c665,plain,
( skc12 != X623
| thing(X623,skc13) ),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c445,plain,
( skc8 != X613
| skc10 != X612
| thing(X613,X612) ),
inference(resolution,[status(thm)],[c5,c66]) ).
cnf(c661,plain,
( skc8 != X620
| thing(X620,skc10) ),
inference(resolution,[status(thm)],[c445,reflexivity]) ).
cnf(c444,plain,
( skc12 != X610
| skc9 != X609
| thing(X610,X609) ),
inference(resolution,[status(thm)],[c5,c126]) ).
cnf(c659,plain,
( skc12 != X611
| thing(X611,skc9) ),
inference(resolution,[status(thm)],[c444,reflexivity]) ).
cnf(c442,plain,
( skc8 != X601
| skc14 != X600
| thing(X601,X600) ),
inference(resolution,[status(thm)],[c5,c93]) ).
cnf(c653,plain,
( skc8 != X602
| thing(X602,skc14) ),
inference(resolution,[status(thm)],[c442,reflexivity]) ).
cnf(c441,plain,
( skc8 != X598
| skc15 != X597
| thing(X598,X597) ),
inference(resolution,[status(thm)],[c5,c65]) ).
cnf(c651,plain,
( skc8 != X599
| thing(X599,skc15) ),
inference(resolution,[status(thm)],[c441,reflexivity]) ).
cnf(c440,plain,
( skc12 != X591
| skc14 != X590
| thing(X591,X590) ),
inference(resolution,[status(thm)],[c5,c189]) ).
cnf(c647,plain,
( skc12 != X592
| thing(X592,skc14) ),
inference(resolution,[status(thm)],[c440,reflexivity]) ).
cnf(c439,plain,
( skc12 != X583
| skc12 != X582
| thing(X583,X582) ),
inference(resolution,[status(thm)],[c5,c201]) ).
cnf(c641,plain,
( skc12 != X589
| thing(X589,skc12) ),
inference(resolution,[status(thm)],[c439,reflexivity]) ).
cnf(c640,plain,
( skc12 != X584
| thing(X584,X584) ),
inference(factor,[status(thm)],[c439]) ).
cnf(c438,plain,
( skc12 != X576
| skc15 != X575
| thing(X576,X575) ),
inference(resolution,[status(thm)],[c5,c178]) ).
cnf(c637,plain,
( skc12 != X581
| thing(X581,skc15) ),
inference(resolution,[status(thm)],[c438,reflexivity]) ).
cnf(c437,plain,
( skc12 != X573
| skc11 != X572
| thing(X573,X572) ),
inference(resolution,[status(thm)],[c5,c174]) ).
cnf(c635,plain,
( skc12 != X574
| thing(X574,skc11) ),
inference(resolution,[status(thm)],[c437,reflexivity]) ).
cnf(c436,plain,
( skc8 != X562
| skc11 != X561
| thing(X562,X561) ),
inference(resolution,[status(thm)],[c5,c97]) ).
cnf(c631,plain,
( skc8 != X563
| thing(X563,skc11) ),
inference(resolution,[status(thm)],[c436,reflexivity]) ).
cnf(c435,plain,
( skc12 != X559
| skc10 != X558
| thing(X559,X558) ),
inference(resolution,[status(thm)],[c5,c194]) ).
cnf(c629,plain,
( skc12 != X560
| thing(X560,skc10) ),
inference(resolution,[status(thm)],[c435,reflexivity]) ).
cnf(c433,plain,
( skc8 != X552
| skc9 != X551
| eventuality(X552,X551) ),
inference(resolution,[status(thm)],[c4,c51]) ).
cnf(c625,plain,
( skc8 != X553
| eventuality(X553,skc9) ),
inference(resolution,[status(thm)],[c433,reflexivity]) ).
cnf(c432,plain,
( skc8 != X545
| skc13 != X544
| eventuality(X545,X544) ),
inference(resolution,[status(thm)],[c4,c38]) ).
cnf(c621,plain,
( skc8 != X550
| eventuality(X550,skc13) ),
inference(resolution,[status(thm)],[c432,reflexivity]) ).
cnf(c430,plain,
( skc12 != X542
| skc9 != X541
| eventuality(X542,X541) ),
inference(resolution,[status(thm)],[c4,c121]) ).
cnf(c619,plain,
( skc12 != X543
| eventuality(X543,skc9) ),
inference(resolution,[status(thm)],[c430,reflexivity]) ).
cnf(c429,plain,
( skc12 != X535
| skc13 != X534
| eventuality(X535,X534) ),
inference(resolution,[status(thm)],[c4,c142]) ).
cnf(c613,plain,
( skc12 != X536
| eventuality(X536,skc13) ),
inference(resolution,[status(thm)],[c429,reflexivity]) ).
cnf(c424,plain,
( skc8 != X532
| skc9 != X531
| event(X532,X531) ),
inference(resolution,[status(thm)],[c3,c52]) ).
cnf(c611,plain,
( skc8 != X533
| event(X533,skc9) ),
inference(resolution,[status(thm)],[c424,reflexivity]) ).
cnf(c423,plain,
( skc12 != X525
| skc13 != X524
| event(X525,X524) ),
inference(resolution,[status(thm)],[c3,c141]) ).
cnf(c605,plain,
( skc12 != X526
| event(X526,skc13) ),
inference(resolution,[status(thm)],[c423,reflexivity]) ).
cnf(c422,plain,
( skc12 != X518
| skc9 != X517
| event(X518,X517) ),
inference(resolution,[status(thm)],[c3,c120]) ).
cnf(c599,plain,
( skc12 != X523
| event(X523,skc9) ),
inference(resolution,[status(thm)],[c422,reflexivity]) ).
cnf(c421,plain,
( skc8 != X515
| skc13 != X514
| event(X515,X514) ),
inference(resolution,[status(thm)],[c3,clause76]) ).
cnf(c597,plain,
( skc8 != X516
| event(X516,skc13) ),
inference(resolution,[status(thm)],[c421,reflexivity]) ).
cnf(c584,plain,
( ~ accessible_world(skc12,X508)
| of(X508,skc11,skc10) ),
inference(resolution,[status(thm)],[c582,clause68]) ).
cnf(c581,plain,
( ~ accessible_world(skc12,X507)
| of(X507,skc14,skc15) ),
inference(resolution,[status(thm)],[c579,clause68]) ).
cnf(c574,plain,
( ~ accessible_world(skc12,X506)
| theme(X506,skc13,skc12) ),
inference(resolution,[status(thm)],[c573,clause67]) ).
cnf(c571,plain,
( ~ accessible_world(skc12,X501)
| agent(X501,skc13,skc15) ),
inference(resolution,[status(thm)],[c570,clause66]) ).
cnf(clause40,axiom,
( ~ accessible_world(X95,X97)
| ~ singleton(X95,X96)
| singleton(X97,X96) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c378,plain,
( ~ accessible_world(skc12,X492)
| singleton(X492,skf2(X491)) ),
inference(resolution,[status(thm)],[c370,clause40]) ).
cnf(c377,plain,
( ~ accessible_world(skc12,X485)
| present(X485,skf2(X486)) ),
inference(resolution,[status(thm)],[c369,clause44]) ).
cnf(c376,plain,
( ~ accessible_world(skc12,X484)
| specific(X484,skf2(X483)) ),
inference(resolution,[status(thm)],[c368,clause41]) ).
cnf(c373,plain,
( ~ accessible_world(skc12,X481)
| unisex(X481,skf2(X482)) ),
inference(resolution,[status(thm)],[c367,clause43]) ).
cnf(clause42,axiom,
( ~ accessible_world(X105,X107)
| ~ nonexistent(X105,X106)
| nonexistent(X107,X106) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c372,plain,
( ~ accessible_world(skc12,X479)
| nonexistent(X479,skf2(X480)) ),
inference(resolution,[status(thm)],[c366,clause42]) ).
cnf(c371,plain,
( ~ accessible_world(skc12,X478)
| thing(X478,skf2(X477)) ),
inference(resolution,[status(thm)],[c364,clause39]) ).
cnf(clause38,axiom,
( ~ accessible_world(X88,X90)
| ~ eventuality(X88,X89)
| eventuality(X90,X89) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c365,plain,
( ~ accessible_world(skc12,X472)
| eventuality(X472,skf2(X471)) ),
inference(resolution,[status(thm)],[c362,clause38]) ).
cnf(c363,plain,
( ~ accessible_world(skc12,X469)
| event(X469,skf2(X470)) ),
inference(resolution,[status(thm)],[c361,clause37]) ).
cnf(clause36,axiom,
( ~ accessible_world(X77,X79)
| ~ smoke(X77,X78)
| smoke(X79,X78) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c360,plain,
( ~ accessible_world(skc12,X468)
| smoke(X468,skf2(X467)) ),
inference(resolution,[status(thm)],[c359,clause36]) ).
cnf(c533,plain,
( ~ accessible_world(skc12,X466)
| jules_forename(X466,skc11) ),
inference(resolution,[status(thm)],[c531,clause65]) ).
cnf(c523,plain,
( ~ accessible_world(skc12,X465)
| vincent_forename(X465,skc14) ),
inference(resolution,[status(thm)],[c522,clause64]) ).
cnf(clause63,axiom,
( ~ accessible_world(X220,X222)
| ~ relname(X220,X221)
| relname(X222,X221) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
cnf(c506,plain,
( ~ accessible_world(skc12,X460)
| relname(X460,skc11) ),
inference(resolution,[status(thm)],[c503,clause63]) ).
cnf(c502,plain,
( ~ accessible_world(skc12,X459)
| forename(X459,skc11) ),
inference(resolution,[status(thm)],[c501,clause62]) ).
cnf(c499,plain,
( ~ accessible_world(skc12,X458)
| relname(X458,skc14) ),
inference(resolution,[status(thm)],[c498,clause63]) ).
cnf(c497,plain,
( ~ accessible_world(skc12,X457)
| forename(X457,skc14) ),
inference(resolution,[status(thm)],[c485,clause62]) ).
cnf(clause56,axiom,
( ~ accessible_world(X184,X186)
| ~ existent(X184,X185)
| existent(X186,X185) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
cnf(c404,plain,
( ~ accessible_world(skc12,X456)
| existent(X456,skc15) ),
inference(resolution,[status(thm)],[c398,clause56]) ).
cnf(clause58,axiom,
( ~ accessible_world(X197,X199)
| ~ living(X197,X198)
| living(X199,X198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
cnf(c402,plain,
( ~ accessible_world(skc12,X451)
| living(X451,skc15) ),
inference(resolution,[status(thm)],[c394,clause58]) ).
cnf(clause57,axiom,
( ~ accessible_world(X189,X191)
| ~ impartial(X189,X190)
| impartial(X191,X190) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
cnf(c401,plain,
( ~ accessible_world(skc12,X450)
| impartial(X450,skc15) ),
inference(resolution,[status(thm)],[c392,clause57]) ).
cnf(clause55,axiom,
( ~ accessible_world(X179,X181)
| ~ entity(X179,X180)
| entity(X181,X180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
cnf(c397,plain,
( ~ accessible_world(skc12,X449)
| entity(X449,skc15) ),
inference(resolution,[status(thm)],[c391,clause55]) ).
cnf(clause60,axiom,
( ~ accessible_world(X208,X210)
| ~ animate(X208,X209)
| animate(X210,X209) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
cnf(c395,plain,
( ~ accessible_world(skc12,X448)
| animate(X448,skc15) ),
inference(resolution,[status(thm)],[c389,clause60]) ).
cnf(clause54,axiom,
( ~ accessible_world(X173,X175)
| ~ organism(X173,X174)
| organism(X175,X174) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
cnf(c393,plain,
( ~ accessible_world(skc12,X447)
| organism(X447,skc15) ),
inference(resolution,[status(thm)],[c388,clause54]) ).
cnf(clause59,axiom,
( ~ accessible_world(X203,X205)
| ~ human(X203,X204)
| human(X205,X204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
cnf(c390,plain,
( ~ accessible_world(skc12,X442)
| human(X442,skc15) ),
inference(resolution,[status(thm)],[c387,clause59]) ).
cnf(clause53,axiom,
( ~ accessible_world(X166,X168)
| ~ human_person(X166,X167)
| human_person(X168,X167) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(c386,plain,
( ~ accessible_world(skc12,X441)
| human_person(X441,skc15) ),
inference(resolution,[status(thm)],[c382,clause53]) ).
cnf(clause61,axiom,
( ~ accessible_world(X211,X213)
| ~ male(X211,X212)
| male(X213,X212) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
cnf(c385,plain,
( ~ accessible_world(skc12,X440)
| male(X440,skc15) ),
inference(resolution,[status(thm)],[c380,clause61]) ).
cnf(c381,plain,
( ~ accessible_world(skc12,X435)
| man(X435,skc15) ),
inference(resolution,[status(thm)],[c379,clause52]) ).
cnf(c358,plain,
( ~ accessible_world(skc12,X434)
| existent(X434,skc10) ),
inference(resolution,[status(thm)],[c352,clause56]) ).
cnf(c356,plain,
( ~ accessible_world(skc12,X433)
| living(X433,skc10) ),
inference(resolution,[status(thm)],[c347,clause58]) ).
cnf(c355,plain,
( ~ accessible_world(skc12,X432)
| impartial(X432,skc10) ),
inference(resolution,[status(thm)],[c345,clause57]) ).
cnf(c351,plain,
( ~ accessible_world(skc12,X431)
| entity(X431,skc10) ),
inference(resolution,[status(thm)],[c344,clause55]) ).
cnf(c348,plain,
( ~ accessible_world(skc12,X426)
| animate(X426,skc10) ),
inference(resolution,[status(thm)],[c342,clause60]) ).
cnf(c346,plain,
( ~ accessible_world(skc12,X425)
| organism(X425,skc10) ),
inference(resolution,[status(thm)],[c341,clause54]) ).
cnf(c343,plain,
( ~ accessible_world(skc12,X424)
| human(X424,skc10) ),
inference(resolution,[status(thm)],[c340,clause59]) ).
cnf(c339,plain,
( ~ accessible_world(skc12,X423)
| human_person(X423,skc10) ),
inference(resolution,[status(thm)],[c333,clause53]) ).
cnf(c338,plain,
( ~ accessible_world(skc12,X422)
| male(X422,skc10) ),
inference(resolution,[status(thm)],[c332,clause61]) ).
cnf(c334,plain,
( ~ accessible_world(skc12,X417)
| man(X417,skc10) ),
inference(resolution,[status(thm)],[c331,clause52]) ).
cnf(c329,plain,
( ~ accessible_world(skc12,X416)
| state(X416,skc9) ),
inference(resolution,[status(thm)],[c326,clause51]) ).
cnf(clause50,axiom,
( ~ accessible_world(X149,X151)
| ~ general(X149,X150)
| general(X151,X150) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c309,plain,
( ~ accessible_world(skc12,X409)
| general(X409,skc14) ),
inference(resolution,[status(thm)],[c305,clause50]) ).
cnf(clause49,axiom,
( ~ accessible_world(X143,X145)
| ~ nonhuman(X143,X144)
| nonhuman(X145,X144) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c308,plain,
( ~ accessible_world(skc12,X408)
| nonhuman(X408,skc14) ),
inference(resolution,[status(thm)],[c304,clause49]) ).
cnf(clause48,axiom,
( ~ accessible_world(X137,X139)
| ~ abstraction(X137,X138)
| abstraction(X139,X138) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(c302,plain,
( ~ accessible_world(skc12,X403)
| abstraction(X403,skc14) ),
inference(resolution,[status(thm)],[c301,clause48]) ).
cnf(c300,plain,
( ~ accessible_world(skc12,X402)
| relation(X402,skc14) ),
inference(resolution,[status(thm)],[c297,clause47]) ).
cnf(c299,plain,
( ~ accessible_world(skc8,X401)
| relname(X401,skc11) ),
inference(resolution,[status(thm)],[clause63,c84]) ).
cnf(c298,plain,
( ~ accessible_world(skc8,X396)
| relname(X396,skc14) ),
inference(resolution,[status(thm)],[clause63,c83]) ).
cnf(c296,plain,
( ~ accessible_world(skc12,X395)
| general(X395,skc11) ),
inference(resolution,[status(thm)],[c290,clause50]) ).
cnf(c295,plain,
( ~ accessible_world(skc12,X394)
| nonhuman(X394,skc11) ),
inference(resolution,[status(thm)],[c289,clause49]) ).
cnf(c287,plain,
( ~ accessible_world(skc12,X383)
| abstraction(X383,skc11) ),
inference(resolution,[status(thm)],[c286,clause48]) ).
cnf(c285,plain,
( ~ accessible_world(skc12,X382)
| relation(X382,skc11) ),
inference(resolution,[status(thm)],[c284,clause47]) ).
cnf(c283,plain,
( ~ accessible_world(skc8,X381)
| male(X381,skc15) ),
inference(resolution,[status(thm)],[clause61,c82]) ).
cnf(c282,plain,
( ~ accessible_world(skc8,X376)
| male(X376,skc10) ),
inference(resolution,[status(thm)],[clause61,c81]) ).
cnf(c281,plain,
( ~ accessible_world(skc12,X375)
| general(X375,skc12) ),
inference(resolution,[status(thm)],[c275,clause50]) ).
cnf(c280,plain,
( ~ accessible_world(skc12,X374)
| nonhuman(X374,skc12) ),
inference(resolution,[status(thm)],[c274,clause49]) ).
cnf(c278,plain,
( ~ accessible_world(skc8,X369)
| animate(X369,skc15) ),
inference(resolution,[status(thm)],[clause60,c80]) ).
cnf(c277,plain,
( ~ accessible_world(skc8,X368)
| animate(X368,skc10) ),
inference(resolution,[status(thm)],[clause60,c79]) ).
cnf(c272,plain,
( ~ accessible_world(skc12,X367)
| abstraction(X367,skc12) ),
inference(resolution,[status(thm)],[c271,clause48]) ).
cnf(c270,plain,
( ~ accessible_world(skc12,X366)
| relation(X366,skc12) ),
inference(resolution,[status(thm)],[c268,clause47]) ).
cnf(c269,plain,
( ~ accessible_world(skc12,X361)
| proposition(X361,skc12) ),
inference(resolution,[status(thm)],[c267,clause46]) ).
cnf(c266,plain,
( ~ accessible_world(skc8,X360)
| human(X360,skc15) ),
inference(resolution,[status(thm)],[clause59,c78]) ).
cnf(c265,plain,
( ~ accessible_world(skc8,X359)
| human(X359,skc10) ),
inference(resolution,[status(thm)],[clause59,c77]) ).
cnf(c264,plain,
( ~ accessible_world(skc12,X354)
| think_believe_consider(X354,skc13) ),
inference(resolution,[status(thm)],[c263,clause45]) ).
cnf(c262,plain,
( ~ accessible_world(skc12,X353)
| present(X353,skc13) ),
inference(resolution,[status(thm)],[c259,clause44]) ).
cnf(c261,plain,
( ~ accessible_world(skc8,X352)
| living(X352,skc15) ),
inference(resolution,[status(thm)],[clause58,c76]) ).
cnf(c260,plain,
( ~ accessible_world(skc8,X347)
| living(X347,skc10) ),
inference(resolution,[status(thm)],[clause58,c75]) ).
cnf(c258,plain,
( ~ accessible_world(skc8,X346)
| impartial(X346,skc15) ),
inference(resolution,[status(thm)],[clause57,c74]) ).
cnf(c257,plain,
( ~ accessible_world(skc8,X345)
| impartial(X345,skc10) ),
inference(resolution,[status(thm)],[clause57,c73]) ).
cnf(c255,plain,
( ~ accessible_world(skc12,X340)
| unisex(X340,skc11) ),
inference(resolution,[status(thm)],[c254,clause43]) ).
cnf(c253,plain,
( ~ accessible_world(skc8,X339)
| existent(X339,skc10) ),
inference(resolution,[status(thm)],[clause56,c72]) ).
cnf(c252,plain,
( ~ accessible_world(skc8,X338)
| existent(X338,skc15) ),
inference(resolution,[status(thm)],[clause56,c71]) ).
cnf(c249,plain,
( ~ accessible_world(skc12,X333)
| unisex(X333,skc12) ),
inference(resolution,[status(thm)],[c248,clause43]) ).
cnf(c247,plain,
( ~ accessible_world(skc8,X332)
| entity(X332,skc10) ),
inference(resolution,[status(thm)],[clause55,c63]) ).
cnf(c1,axiom,
( X329 != X330
| skf4(X329) = skf4(X330) ),
theory(equality) ).
cnf(c246,plain,
( ~ accessible_world(skc8,X328)
| entity(X328,skc15) ),
inference(resolution,[status(thm)],[clause55,c64]) ).
cnf(c243,plain,
( ~ accessible_world(skc12,X327)
| unisex(X327,skc14) ),
inference(resolution,[status(thm)],[c242,clause43]) ).
cnf(c241,plain,
( ~ accessible_world(skc8,X326)
| organism(X326,skc15) ),
inference(resolution,[status(thm)],[clause54,c62]) ).
cnf(c0,axiom,
( X323 != X324
| skf2(X323) = skf2(X324) ),
theory(equality) ).
cnf(c240,plain,
( ~ accessible_world(skc8,X322)
| organism(X322,skc10) ),
inference(resolution,[status(thm)],[clause54,c61]) ).
cnf(transitivity,axiom,
( X317 != X316
| X316 != X318
| X317 = X318 ),
theory(equality) ).
cnf(c238,plain,
( ~ accessible_world(skc8,X315)
| human_person(X315,skc15) ),
inference(resolution,[status(thm)],[clause53,c59]) ).
cnf(c237,plain,
( ~ accessible_world(skc8,X314)
| human_person(X314,skc10) ),
inference(resolution,[status(thm)],[clause53,c58]) ).
cnf(clause34,axiom,
( ~ nonexistent(X69,X70)
| ~ existent(X69,X70) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c403,plain,
~ nonexistent(skc12,skc15),
inference(resolution,[status(thm)],[c398,clause34]) ).
cnf(clause32,axiom,
( ~ general(X65,X66)
| ~ specific(X65,X66) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c375,plain,
~ general(skc12,skf2(X286)),
inference(resolution,[status(thm)],[c368,clause32]) ).
cnf(clause31,axiom,
( ~ male(X63,X64)
| ~ unisex(X63,X64) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c374,plain,
~ male(skc12,skf2(X285)),
inference(resolution,[status(thm)],[c367,clause31]) ).
cnf(c357,plain,
~ nonexistent(skc12,skc10),
inference(resolution,[status(thm)],[c352,clause34]) ).
cnf(c232,plain,
( ~ accessible_world(skc12,X258)
| specific(X258,skc10) ),
inference(resolution,[status(thm)],[c230,clause41]) ).
cnf(c227,plain,
( ~ accessible_world(skc12,X251)
| specific(X251,skc15) ),
inference(resolution,[status(thm)],[c225,clause41]) ).
cnf(c224,plain,
( ~ accessible_world(skc8,X250)
| general(X250,skc14) ),
inference(resolution,[status(thm)],[clause50,c92]) ).
cnf(c223,plain,
( ~ accessible_world(skc8,X245)
| general(X245,skc11) ),
inference(resolution,[status(thm)],[clause50,c96]) ).
cnf(c222,plain,
( ~ accessible_world(skc8,X244)
| general(X244,skc12) ),
inference(resolution,[status(thm)],[clause50,c49]) ).
cnf(c219,plain,
( ~ accessible_world(skc8,X239)
| nonhuman(X239,skc11) ),
inference(resolution,[status(thm)],[clause49,c95]) ).
cnf(c218,plain,
( ~ accessible_world(skc8,X238)
| nonhuman(X238,skc12) ),
inference(resolution,[status(thm)],[clause49,c48]) ).
cnf(c217,plain,
( ~ accessible_world(skc8,X237)
| nonhuman(X237,skc14) ),
inference(resolution,[status(thm)],[clause49,c91]) ).
cnf(c214,plain,
( ~ accessible_world(skc8,X232)
| abstraction(X232,skc14) ),
inference(resolution,[status(thm)],[clause48,c88]) ).
cnf(c213,plain,
( ~ accessible_world(skc8,X231)
| abstraction(X231,skc12) ),
inference(resolution,[status(thm)],[clause48,c45]) ).
cnf(c212,plain,
( ~ accessible_world(skc8,X227)
| abstraction(X227,skc11) ),
inference(resolution,[status(thm)],[clause48,c89]) ).
cnf(c209,plain,
( ~ accessible_world(skc8,X226)
| relation(X226,skc12) ),
inference(resolution,[status(thm)],[clause47,c44]) ).
cnf(clause33,axiom,
( ~ human(X67,X68)
| ~ nonhuman(X67,X68) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c307,plain,
~ human(skc12,skc14),
inference(resolution,[status(thm)],[c304,clause33]) ).
cnf(c294,plain,
~ human(skc12,skc11),
inference(resolution,[status(thm)],[c289,clause33]) ).
cnf(c205,plain,
( ~ accessible_world(skc12,X214)
| singleton(X214,skc12) ),
inference(resolution,[status(thm)],[c202,clause40]) ).
cnf(c279,plain,
~ human(skc12,skc12),
inference(resolution,[status(thm)],[c274,clause33]) ).
cnf(c203,plain,
( ~ accessible_world(skc12,X206)
| thing(X206,skc12) ),
inference(resolution,[status(thm)],[c201,clause39]) ).
cnf(c197,plain,
( ~ accessible_world(skc12,X201)
| singleton(X201,skc10) ),
inference(resolution,[status(thm)],[c195,clause40]) ).
cnf(c196,plain,
( ~ accessible_world(skc12,X200)
| thing(X200,skc10) ),
inference(resolution,[status(thm)],[c194,clause39]) ).
cnf(c192,plain,
( ~ accessible_world(skc12,X195)
| singleton(X195,skc14) ),
inference(resolution,[status(thm)],[c190,clause40]) ).
cnf(c191,plain,
( ~ accessible_world(skc12,X194)
| thing(X194,skc14) ),
inference(resolution,[status(thm)],[c189,clause39]) ).
cnf(c188,plain,
( ~ accessible_world(skc12,X193)
| singleton(X193,skc15) ),
inference(resolution,[status(thm)],[c186,clause40]) ).
cnf(c187,plain,
( ~ accessible_world(skc12,X192)
| thing(X192,skc15) ),
inference(resolution,[status(thm)],[c178,clause39]) ).
cnf(c185,plain,
( ~ accessible_world(skc12,X188)
| unisex(X188,skc13) ),
inference(resolution,[status(thm)],[clause43,c147]) ).
cnf(c256,plain,
~ male(skc12,skc11),
inference(resolution,[status(thm)],[c254,clause31]) ).
cnf(c183,plain,
( ~ accessible_world(skc8,X183)
| unisex(X183,skc13) ),
inference(resolution,[status(thm)],[clause43,c43]) ).
cnf(c250,plain,
~ male(skc12,skc12),
inference(resolution,[status(thm)],[c248,clause31]) ).
cnf(c181,plain,
( ~ accessible_world(skc8,X178)
| unisex(X178,skc9) ),
inference(resolution,[status(thm)],[clause43,c54]) ).
cnf(c244,plain,
~ male(skc12,skc14),
inference(resolution,[status(thm)],[c242,clause31]) ).
cnf(c179,plain,
( ~ accessible_world(skc12,X176)
| unisex(X176,skc9) ),
inference(resolution,[status(thm)],[clause43,c124]) ).
cnf(c177,plain,
( ~ accessible_world(skc12,X172)
| singleton(X172,skc11) ),
inference(resolution,[status(thm)],[c175,clause40]) ).
cnf(c176,plain,
( ~ accessible_world(skc12,X171)
| thing(X171,skc11) ),
inference(resolution,[status(thm)],[c174,clause39]) ).
cnf(c173,plain,
( ~ accessible_world(skc8,X170)
| nonexistent(X170,skc9) ),
inference(resolution,[status(thm)],[clause42,c53]) ).
cnf(c172,plain,
( ~ accessible_world(skc12,X169)
| nonexistent(X169,skc13) ),
inference(resolution,[status(thm)],[clause42,c146]) ).
cnf(c171,plain,
( ~ accessible_world(skc12,X165)
| nonexistent(X165,skc9) ),
inference(resolution,[status(thm)],[clause42,c123]) ).
cnf(c170,plain,
( ~ accessible_world(skc8,X164)
| nonexistent(X164,skc13) ),
inference(resolution,[status(thm)],[clause42,c42]) ).
cnf(c167,plain,
( ~ accessible_world(skc8,X163)
| specific(X163,skc13) ),
inference(resolution,[status(thm)],[clause41,c41]) ).
cnf(c166,plain,
( ~ accessible_world(skc12,X159)
| specific(X159,skc13) ),
inference(resolution,[status(thm)],[clause41,c148]) ).
cnf(c165,plain,
( ~ accessible_world(skc12,X158)
| specific(X158,skc9) ),
inference(resolution,[status(thm)],[clause41,c125]) ).
cnf(c231,plain,
~ general(skc12,skc10),
inference(resolution,[status(thm)],[c230,clause32]) ).
cnf(c163,plain,
( ~ accessible_world(skc8,X153)
| specific(X153,skc9) ),
inference(resolution,[status(thm)],[clause41,c55]) ).
cnf(c226,plain,
~ general(skc12,skc15),
inference(resolution,[status(thm)],[c225,clause32]) ).
cnf(c161,plain,
( ~ accessible_world(skc12,X148)
| singleton(X148,skc13) ),
inference(resolution,[status(thm)],[c149,clause40]) ).
cnf(c158,plain,
( ~ accessible_world(skc8,X147)
| singleton(X147,skc13) ),
inference(resolution,[status(thm)],[clause40,c40]) ).
cnf(c157,plain,
( ~ accessible_world(skc8,X146)
| singleton(X146,skc11) ),
inference(resolution,[status(thm)],[clause40,c105]) ).
cnf(c156,plain,
( ~ accessible_world(skc12,X142)
| singleton(X142,skc9) ),
inference(resolution,[status(thm)],[clause40,c132]) ).
cnf(c155,plain,
( ~ accessible_world(skc8,X141)
| singleton(X141,skc12) ),
inference(resolution,[status(thm)],[clause40,c47]) ).
cnf(c154,plain,
( ~ accessible_world(skc8,X140)
| singleton(X140,skc9) ),
inference(resolution,[status(thm)],[clause40,c60]) ).
cnf(c153,plain,
( ~ accessible_world(skc8,X136)
| singleton(X136,skc15) ),
inference(resolution,[status(thm)],[clause40,c67]) ).
cnf(c152,plain,
( ~ accessible_world(skc8,X135)
| singleton(X135,skc14) ),
inference(resolution,[status(thm)],[clause40,c99]) ).
cnf(c151,plain,
( ~ accessible_world(skc8,X131)
| singleton(X131,skc10) ),
inference(resolution,[status(thm)],[clause40,c68]) ).
cnf(c150,plain,
( ~ accessible_world(skc12,X130)
| thing(X130,skc13) ),
inference(resolution,[status(thm)],[c144,clause39]) ).
cnf(c145,plain,
( ~ accessible_world(skc12,X129)
| eventuality(X129,skc13) ),
inference(resolution,[status(thm)],[c142,clause38]) ).
cnf(c143,plain,
( ~ accessible_world(skc12,X128)
| event(X128,skc13) ),
inference(resolution,[status(thm)],[c141,clause37]) ).
cnf(c139,plain,
( ~ accessible_world(skc8,X123)
| thing(X123,skc13) ),
inference(resolution,[status(thm)],[clause39,c39]) ).
cnf(c138,plain,
( ~ accessible_world(skc8,X119)
| thing(X119,skc9) ),
inference(resolution,[status(thm)],[clause39,c56]) ).
cnf(c136,plain,
( ~ accessible_world(skc12,X117)
| thing(X117,skc9) ),
inference(resolution,[status(thm)],[clause39,c126]) ).
cnf(c130,plain,
( ~ accessible_world(skc8,X104)
| eventuality(X104,skc9) ),
inference(resolution,[status(thm)],[clause38,c51]) ).
cnf(c129,plain,
( ~ accessible_world(skc12,X103)
| eventuality(X103,skc9) ),
inference(resolution,[status(thm)],[clause38,c121]) ).
cnf(c128,plain,
( ~ accessible_world(skc8,X102)
| eventuality(X102,skc13) ),
inference(resolution,[status(thm)],[clause38,c38]) ).
cnf(c122,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(c159,plain,
~ male(skc12,skc13),
inference(resolution,[status(thm)],[c147,clause31]) ).
cnf(c131,plain,
~ general(skc12,skc9),
inference(resolution,[status(thm)],[c125,clause32]) ).
cnf(c127,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,
( X76 != X75
| X75 = X76 ),
theory(equality) ).
cnf(clause35,axiom,
( ~ be(X71,X74,X73,X72)
| X73 = X72 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c114,plain,
~ nonexistent(skc8,skc10),
inference(resolution,[status(thm)],[clause34,c72]) ).
cnf(c113,plain,
~ nonexistent(skc8,skc15),
inference(resolution,[status(thm)],[clause34,c71]) ).
cnf(c112,plain,
~ human(skc8,skc11),
inference(resolution,[status(thm)],[clause33,c95]) ).
cnf(c111,plain,
~ human(skc8,skc12),
inference(resolution,[status(thm)],[clause33,c48]) ).
cnf(c110,plain,
~ human(skc8,skc14),
inference(resolution,[status(thm)],[clause33,c91]) ).
cnf(c109,plain,
~ general(skc8,skc9),
inference(resolution,[status(thm)],[clause32,c55]) ).
cnf(c108,plain,
~ general(skc8,skc13),
inference(resolution,[status(thm)],[clause32,c41]) ).
cnf(c107,plain,
~ general(skc8,skc10),
inference(resolution,[status(thm)],[clause32,c70]) ).
cnf(c106,plain,
~ general(skc8,skc15),
inference(resolution,[status(thm)],[clause32,c69]) ).
cnf(c104,plain,
~ male(skc8,skc11),
inference(resolution,[status(thm)],[clause31,c94]) ).
cnf(c103,plain,
~ male(skc8,skc13),
inference(resolution,[status(thm)],[clause31,c43]) ).
cnf(c102,plain,
~ male(skc8,skc12),
inference(resolution,[status(thm)],[clause31,c50]) ).
cnf(c101,plain,
~ male(skc8,skc9),
inference(resolution,[status(thm)],[clause31,c54]) ).
cnf(c100,plain,
~ male(skc8,skc14),
inference(resolution,[status(thm)],[clause31,c90]) ).
cnf(clause30,axiom,
( ~ jules_forename(X61,X62)
| forename(X61,X62) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,axiom,
( ~ vincent_forename(X59,X60)
| forename(X59,X60) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(clause72,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP259-1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n003.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:26:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 4.73/4.89 % Version: 1.5
% 4.73/4.89 % SZS status Satisfiable
% 4.73/4.89 % SZS output start Saturation
% See solution above
% 4.73/4.93
% 4.73/4.93 % Initial clauses : 136
% 4.73/4.93 % Processed clauses : 996
% 4.73/4.93 % Factors computed : 71
% 4.73/4.93 % Resolvents computed: 1091
% 4.73/4.93 % Tautologies deleted: 3
% 4.73/4.93 % Forward subsumed : 299
% 4.73/4.93 % Backward subsumed : 63
% 4.73/4.93 % -------- CPU Time ---------
% 4.73/4.93 % User time : 4.566 s
% 4.73/4.93 % System time : 0.015 s
% 4.73/4.93 % Total time : 4.581 s
%------------------------------------------------------------------------------