%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP254-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:34:53 EDT 2024
% Result : Satisfiable 5.55s 5.78s
% Output : Saturation 5.65s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause83,negated_conjecture,
accessible_world(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
cnf(clause81,negated_conjecture,
man(skc8,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
cnf(clause52,axiom,
( ~ accessible_world(X161,X160)
| ~ man(X161,X162)
| man(X160,X162) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c234,plain,
( ~ accessible_world(skc8,X259)
| man(X259,skc10) ),
inference(resolution,[status(thm)],[clause52,clause81]) ).
cnf(c331,plain,
man(skc12,skc10),
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(skc10),skc10),
inference(resolution,[status(thm)],[clause93,c331]) ).
cnf(clause88,negated_conjecture,
of(skc8,skc11,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
cnf(clause68,axiom,
( ~ accessible_world(X247,X246)
| ~ of(X247,X249,X248)
| of(X246,X249,X248) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
cnf(c324,plain,
( ~ accessible_world(skc8,X504)
| of(X504,skc11,skc10) ),
inference(resolution,[status(thm)],[clause68,clause88]) ).
cnf(c580,plain,
of(skc12,skc11,skc10),
inference(resolution,[status(thm)],[c324,clause83]) ).
cnf(clause94,negated_conjecture,
( ~ accessible_world(X292,X299)
| ~ proposition(X292,X299)
| ~ theme(X292,X302,X299)
| ~ event(X292,X302)
| ~ present(X292,X302)
| ~ think_believe_consider(X292,X302)
| ~ forename(X292,X293)
| ~ vincent_forename(X292,X293)
| ~ of(X292,X293,X289)
| ~ man(X292,X289)
| ~ agent(X292,X302,X289)
| ~ jules_forename(X292,X296)
| ~ forename(X292,X296)
| ~ smoke(X290,X294)
| ~ present(X290,X294)
| ~ agent(X290,X294,X291)
| ~ event(X290,X294)
| ~ man(X292,X291)
| ~ of(X292,X296,X291)
| ~ proposition(X292,X290)
| ~ accessible_world(X292,X290)
| ~ think_believe_consider(X292,X297)
| ~ present(X292,X297)
| ~ event(X292,X297)
| ~ theme(X292,X297,X290)
| ~ state(X292,X298)
| ~ forename(X292,X300)
| ~ vincent_forename(X292,X300)
| ~ of(X292,X300,X301)
| ~ agent(X292,X297,X301)
| ~ be(X292,X298,X301,X301)
| ~ man(X292,X301)
| ~ of(X292,X295,X301)
| ~ jules_forename(X292,X295)
| ~ forename(X292,X295)
| ~ actual_world(X292)
| man(X299,skf4(X299)) ),
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(X254,X256)
| ~ be(X254,X257,X255,X253)
| be(X256,X257,X255,X253) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
cnf(c330,plain,
( ~ accessible_world(skc8,X513)
| be(X513,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[clause69,clause89]) ).
cnf(c587,plain,
be(skc12,skc9,skc10,skc10),
inference(resolution,[status(thm)],[c330,clause83]) ).
cnf(c590,plain,
( ~ accessible_world(skc12,X1059)
| ~ proposition(skc12,X1059)
| ~ theme(skc12,X1061,X1059)
| ~ event(skc12,X1061)
| ~ present(skc12,X1061)
| ~ think_believe_consider(skc12,X1061)
| ~ forename(skc12,X1052)
| ~ vincent_forename(skc12,X1052)
| ~ of(skc12,X1052,X1053)
| ~ man(skc12,X1053)
| ~ agent(skc12,X1061,X1053)
| ~ jules_forename(skc12,X1051)
| ~ forename(skc12,X1051)
| ~ smoke(X1056,X1057)
| ~ present(X1056,X1057)
| ~ agent(X1056,X1057,X1055)
| ~ event(X1056,X1057)
| ~ man(skc12,X1055)
| ~ of(skc12,X1051,X1055)
| ~ proposition(skc12,X1056)
| ~ accessible_world(skc12,X1056)
| ~ think_believe_consider(skc12,X1058)
| ~ present(skc12,X1058)
| ~ event(skc12,X1058)
| ~ theme(skc12,X1058,X1056)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1054)
| ~ vincent_forename(skc12,X1054)
| ~ of(skc12,X1054,skc10)
| ~ agent(skc12,X1058,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1060,skc10)
| ~ jules_forename(skc12,X1060)
| ~ forename(skc12,X1060)
| ~ actual_world(skc12)
| man(X1059,skf4(X1059)) ),
inference(resolution,[status(thm)],[c587,clause94]) ).
cnf(c924,plain,
( ~ accessible_world(skc12,X1541)
| ~ proposition(skc12,X1541)
| ~ theme(skc12,X1540,X1541)
| ~ event(skc12,X1540)
| ~ present(skc12,X1540)
| ~ think_believe_consider(skc12,X1540)
| ~ forename(skc12,X1538)
| ~ vincent_forename(skc12,X1538)
| ~ of(skc12,X1538,X1534)
| ~ man(skc12,X1534)
| ~ agent(skc12,X1540,X1534)
| ~ jules_forename(skc12,X1535)
| ~ forename(skc12,X1535)
| ~ smoke(X1539,X1532)
| ~ present(X1539,X1532)
| ~ agent(X1539,X1532,X1536)
| ~ event(X1539,X1532)
| ~ man(skc12,X1536)
| ~ of(skc12,X1535,X1536)
| ~ proposition(skc12,X1539)
| ~ accessible_world(skc12,X1539)
| ~ think_believe_consider(skc12,X1537)
| ~ present(skc12,X1537)
| ~ event(skc12,X1537)
| ~ theme(skc12,X1537,X1539)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1533)
| ~ vincent_forename(skc12,X1533)
| ~ of(skc12,X1533,skc10)
| ~ agent(skc12,X1537,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1541,skf4(X1541)) ),
inference(resolution,[status(thm)],[c590,c580]) ).
cnf(c1104,plain,
( ~ accessible_world(skc12,X2031)
| ~ proposition(skc12,X2031)
| ~ theme(skc12,X2036,X2031)
| ~ event(skc12,X2036)
| ~ present(skc12,X2036)
| ~ think_believe_consider(skc12,X2036)
| ~ forename(skc12,X2034)
| ~ vincent_forename(skc12,X2034)
| ~ of(skc12,X2034,X2030)
| ~ man(skc12,X2030)
| ~ agent(skc12,X2036,X2030)
| ~ jules_forename(skc12,X2033)
| ~ forename(skc12,X2033)
| ~ smoke(X2032,X2037)
| ~ present(X2032,X2037)
| ~ agent(X2032,X2037,X2038)
| ~ event(X2032,X2037)
| ~ man(skc12,X2038)
| ~ of(skc12,X2033,X2038)
| ~ proposition(skc12,X2032)
| ~ accessible_world(skc12,X2032)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X2032)
| ~ state(skc12,skc9)
| ~ forename(skc12,X2035)
| ~ vincent_forename(skc12,X2035)
| ~ of(skc12,X2035,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X2031,skf4(X2031)) ),
inference(resolution,[status(thm)],[c924,c383]) ).
cnf(c1208,plain,
( ~ accessible_world(skc12,X2131)
| ~ proposition(skc12,X2131)
| ~ theme(skc12,skf2(skc10),X2131)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X2132)
| ~ vincent_forename(skc12,X2132)
| ~ of(skc12,X2132,X2136)
| ~ man(skc12,X2136)
| ~ agent(skc12,skf2(skc10),X2136)
| ~ jules_forename(skc12,X2134)
| ~ forename(skc12,X2134)
| ~ smoke(X2131,X2133)
| ~ present(X2131,X2133)
| ~ agent(X2131,X2133,X2130)
| ~ event(X2131,X2133)
| ~ man(skc12,X2130)
| ~ of(skc12,X2134,X2130)
| ~ state(skc12,skc9)
| ~ forename(skc12,X2135)
| ~ vincent_forename(skc12,X2135)
| ~ of(skc12,X2135,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X2131,skf4(X2131)) ),
inference(factor,[status(thm)],[c1104]) ).
cnf(c1221,plain,
( ~ accessible_world(skc12,X2138)
| ~ proposition(skc12,X2138)
| ~ theme(skc12,skf2(skc10),X2138)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X2141)
| ~ vincent_forename(skc12,X2141)
| ~ of(skc12,X2141,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X2139)
| ~ forename(skc12,X2139)
| ~ smoke(X2138,X2140)
| ~ present(X2138,X2140)
| ~ agent(X2138,X2140,X2137)
| ~ event(X2138,X2140)
| ~ man(skc12,X2137)
| ~ of(skc12,X2139,X2137)
| ~ state(skc12,skc9)
| ~ forename(skc12,X2142)
| ~ vincent_forename(skc12,X2142)
| ~ of(skc12,X2142,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X2138,skf4(X2138)) ),
inference(resolution,[status(thm)],[c1208,c383]) ).
cnf(clause95,negated_conjecture,
( ~ smoke(X307,X314)
| ~ present(X307,X314)
| ~ agent(X307,X314,skf4(X307))
| ~ event(X307,X314)
| ~ accessible_world(X317,X307)
| ~ proposition(X317,X307)
| ~ theme(X317,X308,X307)
| ~ event(X317,X308)
| ~ present(X317,X308)
| ~ think_believe_consider(X317,X308)
| ~ forename(X317,X303)
| ~ vincent_forename(X317,X303)
| ~ of(X317,X303,X311)
| ~ man(X317,X311)
| ~ agent(X317,X308,X311)
| ~ jules_forename(X317,X305)
| ~ forename(X317,X305)
| ~ smoke(X309,X306)
| ~ present(X309,X306)
| ~ agent(X309,X306,X312)
| ~ event(X309,X306)
| ~ man(X317,X312)
| ~ of(X317,X305,X312)
| ~ proposition(X317,X309)
| ~ accessible_world(X317,X309)
| ~ think_believe_consider(X317,X313)
| ~ present(X317,X313)
| ~ event(X317,X313)
| ~ theme(X317,X313,X309)
| ~ state(X317,X315)
| ~ forename(X317,X316)
| ~ vincent_forename(X317,X316)
| ~ of(X317,X316,X310)
| ~ agent(X317,X313,X310)
| ~ be(X317,X315,X310,X310)
| ~ man(X317,X310)
| ~ of(X317,X304,X310)
| ~ jules_forename(X317,X304)
| ~ forename(X317,X304)
| ~ actual_world(X317) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
cnf(c588,plain,
( ~ smoke(X1044,X1037)
| ~ present(X1044,X1037)
| ~ agent(X1044,X1037,skf4(X1044))
| ~ event(X1044,X1037)
| ~ accessible_world(skc12,X1044)
| ~ proposition(skc12,X1044)
| ~ theme(skc12,X1034,X1044)
| ~ event(skc12,X1034)
| ~ present(skc12,X1034)
| ~ think_believe_consider(skc12,X1034)
| ~ forename(skc12,X1043)
| ~ vincent_forename(skc12,X1043)
| ~ of(skc12,X1043,X1041)
| ~ man(skc12,X1041)
| ~ agent(skc12,X1034,X1041)
| ~ jules_forename(skc12,X1045)
| ~ forename(skc12,X1045)
| ~ smoke(X1042,X1038)
| ~ present(X1042,X1038)
| ~ agent(X1042,X1038,X1039)
| ~ event(X1042,X1038)
| ~ man(skc12,X1039)
| ~ of(skc12,X1045,X1039)
| ~ proposition(skc12,X1042)
| ~ accessible_world(skc12,X1042)
| ~ think_believe_consider(skc12,X1035)
| ~ present(skc12,X1035)
| ~ event(skc12,X1035)
| ~ theme(skc12,X1035,X1042)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1036)
| ~ vincent_forename(skc12,X1036)
| ~ of(skc12,X1036,skc10)
| ~ agent(skc12,X1035,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1040,skc10)
| ~ jules_forename(skc12,X1040)
| ~ forename(skc12,X1040)
| ~ actual_world(skc12) ),
inference(resolution,[status(thm)],[c587,clause95]) ).
cnf(c916,plain,
( ~ smoke(skc12,X1388)
| ~ present(skc12,X1388)
| ~ agent(skc12,X1388,skf4(skc12))
| ~ event(skc12,X1388)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1388,skc12)
| ~ think_believe_consider(skc12,X1388)
| ~ forename(skc12,X1391)
| ~ vincent_forename(skc12,X1391)
| ~ of(skc12,X1391,skf4(skc12))
| ~ man(skc12,skf4(skc12))
| ~ jules_forename(skc12,X1389)
| ~ forename(skc12,X1389)
| ~ smoke(X1386,X1385)
| ~ present(X1386,X1385)
| ~ agent(X1386,X1385,X1387)
| ~ event(X1386,X1385)
| ~ man(skc12,X1387)
| ~ of(skc12,X1389,X1387)
| ~ proposition(skc12,X1386)
| ~ accessible_world(skc12,X1386)
| ~ think_believe_consider(skc12,X1393)
| ~ present(skc12,X1393)
| ~ event(skc12,X1393)
| ~ theme(skc12,X1393,X1386)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1392)
| ~ vincent_forename(skc12,X1392)
| ~ of(skc12,X1392,skc10)
| ~ agent(skc12,X1393,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1390,skc10)
| ~ jules_forename(skc12,X1390)
| ~ forename(skc12,X1390)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c588]) ).
cnf(c1064,plain,
( ~ smoke(skc12,X1734)
| ~ present(skc12,X1734)
| ~ agent(skc12,X1734,skf4(skc12))
| ~ event(skc12,X1734)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1734,skc12)
| ~ think_believe_consider(skc12,X1734)
| ~ forename(skc12,X1733)
| ~ vincent_forename(skc12,X1733)
| ~ of(skc12,X1733,skf4(skc12))
| ~ man(skc12,skf4(skc12))
| ~ jules_forename(skc12,X1733)
| ~ smoke(X1736,X1730)
| ~ present(X1736,X1730)
| ~ agent(X1736,X1730,skf4(skc12))
| ~ event(X1736,X1730)
| ~ proposition(skc12,X1736)
| ~ accessible_world(skc12,X1736)
| ~ think_believe_consider(skc12,X1735)
| ~ present(skc12,X1735)
| ~ event(skc12,X1735)
| ~ theme(skc12,X1735,X1736)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1732)
| ~ vincent_forename(skc12,X1732)
| ~ of(skc12,X1732,skc10)
| ~ agent(skc12,X1735,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1731,skc10)
| ~ jules_forename(skc12,X1731)
| ~ forename(skc12,X1731)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c916]) ).
cnf(c1150,plain,
( ~ smoke(skc12,X2122)
| ~ present(skc12,X2122)
| ~ agent(skc12,X2122,skf4(skc12))
| ~ event(skc12,X2122)
| ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X2122,skc12)
| ~ think_believe_consider(skc12,X2122)
| ~ forename(skc12,X2124)
| ~ vincent_forename(skc12,X2124)
| ~ of(skc12,X2124,skf4(skc12))
| ~ man(skc12,skf4(skc12))
| ~ jules_forename(skc12,X2124)
| ~ think_believe_consider(skc12,X2120)
| ~ present(skc12,X2120)
| ~ event(skc12,X2120)
| ~ theme(skc12,X2120,skc12)
| ~ state(skc12,skc9)
| ~ forename(skc12,X2121)
| ~ vincent_forename(skc12,X2121)
| ~ of(skc12,X2121,skc10)
| ~ agent(skc12,X2120,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X2123,skc10)
| ~ jules_forename(skc12,X2123)
| ~ forename(skc12,X2123)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c1064]) ).
cnf(c923,plain,
( ~ accessible_world(skc12,X1521)
| ~ proposition(skc12,X1521)
| ~ theme(skc12,X1520,X1521)
| ~ event(skc12,X1520)
| ~ present(skc12,X1520)
| ~ think_believe_consider(skc12,X1520)
| ~ forename(skc12,X1518)
| ~ vincent_forename(skc12,X1518)
| ~ of(skc12,X1518,X1514)
| ~ man(skc12,X1514)
| ~ agent(skc12,X1520,X1514)
| ~ jules_forename(skc12,X1515)
| ~ forename(skc12,X1515)
| ~ smoke(X1519,X1512)
| ~ present(X1519,X1512)
| ~ agent(X1519,X1512,X1516)
| ~ event(X1519,X1512)
| ~ man(skc12,X1516)
| ~ of(skc12,X1515,X1516)
| ~ proposition(skc12,X1519)
| ~ accessible_world(skc12,X1519)
| ~ think_believe_consider(skc12,X1517)
| ~ present(skc12,X1517)
| ~ event(skc12,X1517)
| ~ theme(skc12,X1517,X1519)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1513)
| ~ vincent_forename(skc12,X1513)
| ~ of(skc12,X1513,skc10)
| ~ agent(skc12,X1517,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1513)
| ~ actual_world(skc12)
| man(X1521,skf4(X1521)) ),
inference(factor,[status(thm)],[c590]) ).
cnf(c1096,plain,
( ~ accessible_world(skc12,X1955)
| ~ proposition(skc12,X1955)
| ~ theme(skc12,X1952,X1955)
| ~ event(skc12,X1952)
| ~ present(skc12,X1952)
| ~ think_believe_consider(skc12,X1952)
| ~ forename(skc12,X1959)
| ~ vincent_forename(skc12,X1959)
| ~ of(skc12,X1959,X1957)
| ~ man(skc12,X1957)
| ~ agent(skc12,X1952,X1957)
| ~ jules_forename(skc12,X1956)
| ~ forename(skc12,X1956)
| ~ smoke(X1958,X1951)
| ~ present(X1958,X1951)
| ~ agent(X1958,X1951,X1954)
| ~ event(X1958,X1951)
| ~ man(skc12,X1954)
| ~ of(skc12,X1956,X1954)
| ~ proposition(skc12,X1958)
| ~ accessible_world(skc12,X1958)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1958)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1953)
| ~ vincent_forename(skc12,X1953)
| ~ of(skc12,X1953,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1953)
| ~ actual_world(skc12)
| man(X1955,skf4(X1955)) ),
inference(resolution,[status(thm)],[c923,c383]) ).
cnf(c1191,plain,
( ~ accessible_world(skc12,X2096)
| ~ proposition(skc12,X2096)
| ~ theme(skc12,skf2(skc10),X2096)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X2098)
| ~ vincent_forename(skc12,X2098)
| ~ of(skc12,X2098,X2093)
| ~ man(skc12,X2093)
| ~ agent(skc12,skf2(skc10),X2093)
| ~ jules_forename(skc12,X2095)
| ~ forename(skc12,X2095)
| ~ smoke(X2096,X2099)
| ~ present(X2096,X2099)
| ~ agent(X2096,X2099,X2094)
| ~ event(X2096,X2099)
| ~ man(skc12,X2094)
| ~ of(skc12,X2095,X2094)
| ~ state(skc12,skc9)
| ~ forename(skc12,X2097)
| ~ vincent_forename(skc12,X2097)
| ~ of(skc12,X2097,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X2097)
| ~ actual_world(skc12)
| man(X2096,skf4(X2096)) ),
inference(factor,[status(thm)],[c1096]) ).
cnf(c1219,plain,
( ~ accessible_world(skc12,X2103)
| ~ proposition(skc12,X2103)
| ~ theme(skc12,skf2(skc10),X2103)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X2102)
| ~ vincent_forename(skc12,X2102)
| ~ of(skc12,X2102,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X2104)
| ~ forename(skc12,X2104)
| ~ smoke(X2103,X2105)
| ~ present(X2103,X2105)
| ~ agent(X2103,X2105,X2101)
| ~ event(X2103,X2105)
| ~ man(skc12,X2101)
| ~ of(skc12,X2104,X2101)
| ~ state(skc12,skc9)
| ~ forename(skc12,X2100)
| ~ vincent_forename(skc12,X2100)
| ~ of(skc12,X2100,skc10)
| ~ jules_forename(skc12,X2100)
| ~ actual_world(skc12)
| man(X2103,skf4(X2103)) ),
inference(resolution,[status(thm)],[c1191,c383]) ).
cnf(c405,plain,
( ~ smoke(X702,X695)
| ~ present(X702,X695)
| ~ agent(X702,X695,skf4(X702))
| ~ event(X702,X695)
| ~ accessible_world(skc8,X702)
| ~ proposition(skc8,X702)
| ~ theme(skc8,X692,X702)
| ~ event(skc8,X692)
| ~ present(skc8,X692)
| ~ think_believe_consider(skc8,X692)
| ~ forename(skc8,X701)
| ~ vincent_forename(skc8,X701)
| ~ of(skc8,X701,X699)
| ~ man(skc8,X699)
| ~ agent(skc8,X692,X699)
| ~ jules_forename(skc8,X703)
| ~ forename(skc8,X703)
| ~ smoke(X700,X696)
| ~ present(X700,X696)
| ~ agent(X700,X696,X697)
| ~ event(X700,X696)
| ~ man(skc8,X697)
| ~ of(skc8,X703,X697)
| ~ proposition(skc8,X700)
| ~ accessible_world(skc8,X700)
| ~ think_believe_consider(skc8,X693)
| ~ present(skc8,X693)
| ~ event(skc8,X693)
| ~ theme(skc8,X693,X700)
| ~ state(skc8,skc9)
| ~ forename(skc8,X694)
| ~ vincent_forename(skc8,X694)
| ~ of(skc8,X694,skc10)
| ~ agent(skc8,X693,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X698,skc10)
| ~ jules_forename(skc8,X698)
| ~ forename(skc8,X698)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[clause95,clause89]) ).
cnf(c705,plain,
( ~ smoke(skc8,X1345)
| ~ present(skc8,X1345)
| ~ agent(skc8,X1345,skf4(skc8))
| ~ event(skc8,X1345)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1345,skc8)
| ~ think_believe_consider(skc8,X1345)
| ~ forename(skc8,X1342)
| ~ vincent_forename(skc8,X1342)
| ~ of(skc8,X1342,skf4(skc8))
| ~ man(skc8,skf4(skc8))
| ~ jules_forename(skc8,X1346)
| ~ forename(skc8,X1346)
| ~ smoke(X1339,X1344)
| ~ present(X1339,X1344)
| ~ agent(X1339,X1344,X1340)
| ~ event(X1339,X1344)
| ~ man(skc8,X1340)
| ~ of(skc8,X1346,X1340)
| ~ proposition(skc8,X1339)
| ~ accessible_world(skc8,X1339)
| ~ think_believe_consider(skc8,X1347)
| ~ present(skc8,X1347)
| ~ event(skc8,X1347)
| ~ theme(skc8,X1347,X1339)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1343)
| ~ vincent_forename(skc8,X1343)
| ~ of(skc8,X1343,skc10)
| ~ agent(skc8,X1347,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1341,skc10)
| ~ jules_forename(skc8,X1341)
| ~ forename(skc8,X1341)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1053,plain,
( ~ smoke(skc8,X1678)
| ~ present(skc8,X1678)
| ~ agent(skc8,X1678,skf4(skc8))
| ~ event(skc8,X1678)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1678,skc8)
| ~ think_believe_consider(skc8,X1678)
| ~ forename(skc8,X1676)
| ~ vincent_forename(skc8,X1676)
| ~ of(skc8,X1676,skf4(skc8))
| ~ man(skc8,skf4(skc8))
| ~ jules_forename(skc8,X1676)
| ~ smoke(X1681,X1680)
| ~ present(X1681,X1680)
| ~ agent(X1681,X1680,skf4(skc8))
| ~ event(X1681,X1680)
| ~ proposition(skc8,X1681)
| ~ accessible_world(skc8,X1681)
| ~ think_believe_consider(skc8,X1682)
| ~ present(skc8,X1682)
| ~ event(skc8,X1682)
| ~ theme(skc8,X1682,X1681)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1677)
| ~ vincent_forename(skc8,X1677)
| ~ of(skc8,X1677,skc10)
| ~ agent(skc8,X1682,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1679,skc10)
| ~ jules_forename(skc8,X1679)
| ~ forename(skc8,X1679)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c705]) ).
cnf(c1144,plain,
( ~ smoke(skc8,X2082)
| ~ present(skc8,X2082)
| ~ agent(skc8,X2082,skf4(skc8))
| ~ event(skc8,X2082)
| ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X2082,skc8)
| ~ think_believe_consider(skc8,X2082)
| ~ forename(skc8,X2081)
| ~ vincent_forename(skc8,X2081)
| ~ of(skc8,X2081,skf4(skc8))
| ~ man(skc8,skf4(skc8))
| ~ jules_forename(skc8,X2081)
| ~ think_believe_consider(skc8,X2084)
| ~ present(skc8,X2084)
| ~ event(skc8,X2084)
| ~ theme(skc8,X2084,skc8)
| ~ state(skc8,skc9)
| ~ forename(skc8,X2083)
| ~ vincent_forename(skc8,X2083)
| ~ of(skc8,X2083,skc10)
| ~ agent(skc8,X2084,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X2085,skc10)
| ~ jules_forename(skc8,X2085)
| ~ forename(skc8,X2085)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c1053]) ).
cnf(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
cnf(clause67,axiom,
( ~ accessible_world(X241,X240)
| ~ theme(X241,X243,X242)
| theme(X240,X243,X242) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
cnf(c320,plain,
( ~ accessible_world(skc8,X498)
| theme(X498,skc13,skc12) ),
inference(resolution,[status(thm)],[clause67,clause87]) ).
cnf(c571,plain,
theme(skc12,skc13,skc12),
inference(resolution,[status(thm)],[c320,clause83]) ).
cnf(c922,plain,
( ~ accessible_world(skc12,X1487)
| ~ proposition(skc12,X1487)
| ~ theme(skc12,X1486,X1487)
| ~ event(skc12,X1486)
| ~ present(skc12,X1486)
| ~ think_believe_consider(skc12,X1486)
| ~ forename(skc12,X1484)
| ~ vincent_forename(skc12,X1484)
| ~ of(skc12,X1484,X1482)
| ~ man(skc12,X1482)
| ~ agent(skc12,X1486,X1482)
| ~ jules_forename(skc12,X1479)
| ~ forename(skc12,X1479)
| ~ smoke(X1485,X1480)
| ~ present(X1485,X1480)
| ~ agent(X1485,X1480,skc10)
| ~ event(X1485,X1480)
| ~ man(skc12,skc10)
| ~ of(skc12,X1479,skc10)
| ~ proposition(skc12,X1485)
| ~ accessible_world(skc12,X1485)
| ~ think_believe_consider(skc12,X1483)
| ~ present(skc12,X1483)
| ~ event(skc12,X1483)
| ~ theme(skc12,X1483,X1485)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1481)
| ~ vincent_forename(skc12,X1481)
| ~ of(skc12,X1481,skc10)
| ~ agent(skc12,X1483,skc10)
| ~ actual_world(skc12)
| man(X1487,skf4(X1487)) ),
inference(factor,[status(thm)],[c590]) ).
cnf(c1082,plain,
( ~ accessible_world(skc12,X1847)
| ~ proposition(skc12,X1847)
| ~ theme(skc12,X1845,X1847)
| ~ event(skc12,X1845)
| ~ present(skc12,X1845)
| ~ think_believe_consider(skc12,X1845)
| ~ forename(skc12,X1844)
| ~ vincent_forename(skc12,X1844)
| ~ of(skc12,X1844,X1846)
| ~ man(skc12,X1846)
| ~ agent(skc12,X1845,X1846)
| ~ jules_forename(skc12,X1843)
| ~ forename(skc12,X1843)
| ~ smoke(skc12,X1841)
| ~ present(skc12,X1841)
| ~ agent(skc12,X1841,skc10)
| ~ event(skc12,X1841)
| ~ man(skc12,skc10)
| ~ of(skc12,X1843,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1841)
| ~ theme(skc12,X1841,skc12)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1842)
| ~ vincent_forename(skc12,X1842)
| ~ of(skc12,X1842,skc10)
| ~ actual_world(skc12)
| man(X1847,skf4(X1847)) ),
inference(factor,[status(thm)],[c922]) ).
cnf(c1175,plain,
( ~ accessible_world(skc12,X2056)
| ~ proposition(skc12,X2056)
| ~ theme(skc12,X2051,X2056)
| ~ event(skc12,X2051)
| ~ present(skc12,X2051)
| ~ think_believe_consider(skc12,X2051)
| ~ forename(skc12,X2053)
| ~ vincent_forename(skc12,X2053)
| ~ of(skc12,X2053,X2054)
| ~ man(skc12,X2054)
| ~ agent(skc12,X2051,X2054)
| ~ jules_forename(skc12,X2055)
| ~ forename(skc12,X2055)
| ~ smoke(skc12,X2052)
| ~ present(skc12,X2052)
| ~ agent(skc12,X2052,skc10)
| ~ event(skc12,X2052)
| ~ man(skc12,skc10)
| ~ of(skc12,X2055,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X2052)
| ~ theme(skc12,X2052,skc12)
| ~ state(skc12,skc9)
| ~ forename(skc12,skc11)
| ~ vincent_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X2056,skf4(X2056)) ),
inference(resolution,[status(thm)],[c1082,c580]) ).
cnf(c1210,plain,
( ~ accessible_world(skc12,X2079)
| ~ proposition(skc12,X2079)
| ~ theme(skc12,X2076,X2079)
| ~ event(skc12,X2076)
| ~ present(skc12,X2076)
| ~ think_believe_consider(skc12,X2076)
| ~ forename(skc12,X2080)
| ~ vincent_forename(skc12,X2080)
| ~ of(skc12,X2080,X2078)
| ~ man(skc12,X2078)
| ~ agent(skc12,X2076,X2078)
| ~ jules_forename(skc12,X2077)
| ~ forename(skc12,X2077)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ man(skc12,skc10)
| ~ of(skc12,X2077,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ forename(skc12,skc11)
| ~ vincent_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X2079,skf4(X2079)) ),
inference(resolution,[status(thm)],[c1175,c571]) ).
cnf(c1209,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X2058,skc12)
| ~ event(skc12,X2058)
| ~ present(skc12,X2058)
| ~ think_believe_consider(skc12,X2058)
| ~ forename(skc12,X2059)
| ~ vincent_forename(skc12,X2059)
| ~ of(skc12,X2059,X2057)
| ~ man(skc12,X2057)
| ~ agent(skc12,X2058,X2057)
| ~ jules_forename(skc12,X2060)
| ~ forename(skc12,X2060)
| ~ smoke(skc12,X2058)
| ~ agent(skc12,X2058,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X2060,skc10)
| ~ state(skc12,skc9)
| ~ forename(skc12,skc11)
| ~ vincent_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1175]) ).
cnf(c1212,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X2070,skc12)
| ~ event(skc12,X2070)
| ~ present(skc12,X2070)
| ~ think_believe_consider(skc12,X2070)
| ~ forename(skc12,X2068)
| ~ vincent_forename(skc12,X2068)
| ~ of(skc12,X2068,X2069)
| ~ man(skc12,X2069)
| ~ agent(skc12,X2070,X2069)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,X2070)
| ~ agent(skc12,X2070,skc10)
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1209,c580]) ).
cnf(c1214,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X2073)
| ~ vincent_forename(skc12,X2073)
| ~ of(skc12,X2073,X2074)
| ~ man(skc12,X2074)
| ~ agent(skc12,skf2(skc10),X2074)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ man(skc12,skc10)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1212,c383]) ).
cnf(clause86,negated_conjecture,
agent(skc8,skc13,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
cnf(clause85,negated_conjecture,
of(skc8,skc14,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
cnf(c323,plain,
( ~ accessible_world(skc8,X503)
| of(X503,skc14,skc15) ),
inference(resolution,[status(thm)],[clause68,clause85]) ).
cnf(c577,plain,
of(skc12,skc14,skc15),
inference(resolution,[status(thm)],[c323,clause83]) ).
cnf(c1102,plain,
( ~ accessible_world(skc12,X1977)
| ~ proposition(skc12,X1977)
| ~ theme(skc12,X1983,X1977)
| ~ event(skc12,X1983)
| ~ present(skc12,X1983)
| ~ think_believe_consider(skc12,X1983)
| ~ forename(skc12,X1980)
| ~ vincent_forename(skc12,X1980)
| ~ of(skc12,X1980,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1983,skc10)
| ~ jules_forename(skc12,X1979)
| ~ forename(skc12,X1979)
| ~ smoke(X1978,X1982)
| ~ present(X1978,X1982)
| ~ agent(X1978,X1982,X1984)
| ~ event(X1978,X1982)
| ~ man(skc12,X1984)
| ~ of(skc12,X1979,X1984)
| ~ proposition(skc12,X1978)
| ~ accessible_world(skc12,X1978)
| ~ theme(skc12,X1983,X1978)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1981)
| ~ vincent_forename(skc12,X1981)
| ~ of(skc12,X1981,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1977,skf4(X1977)) ),
inference(factor,[status(thm)],[c924]) ).
cnf(c1196,plain,
( ~ accessible_world(skc12,X1988)
| ~ proposition(skc12,X1988)
| ~ theme(skc12,X1985,X1988)
| ~ event(skc12,X1985)
| ~ present(skc12,X1985)
| ~ think_believe_consider(skc12,X1985)
| ~ forename(skc12,X1991)
| ~ vincent_forename(skc12,X1991)
| ~ of(skc12,X1991,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1985,skc10)
| ~ jules_forename(skc12,X1990)
| ~ forename(skc12,X1990)
| ~ smoke(X1987,X1986)
| ~ present(X1987,X1986)
| ~ agent(X1987,X1986,X1989)
| ~ event(X1987,X1986)
| ~ man(skc12,X1989)
| ~ of(skc12,X1990,X1989)
| ~ proposition(skc12,X1987)
| ~ accessible_world(skc12,X1987)
| ~ theme(skc12,X1985,X1987)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1988,skf4(X1988)) ),
inference(factor,[status(thm)],[c1102]) ).
cnf(c1199,plain,
( ~ accessible_world(skc12,X1996)
| ~ proposition(skc12,X1996)
| ~ theme(skc12,X1993,X1996)
| ~ event(skc12,X1993)
| ~ present(skc12,X1993)
| ~ think_believe_consider(skc12,X1993)
| ~ forename(skc12,X1992)
| ~ vincent_forename(skc12,X1992)
| ~ of(skc12,X1992,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1993,skc10)
| ~ jules_forename(skc12,X1995)
| ~ forename(skc12,X1995)
| ~ smoke(X1996,X1994)
| ~ present(X1996,X1994)
| ~ agent(X1996,X1994,X1997)
| ~ event(X1996,X1994)
| ~ man(skc12,X1997)
| ~ of(skc12,X1995,X1997)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1996,skf4(X1996)) ),
inference(factor,[status(thm)],[c1196]) ).
cnf(c1203,plain,
( ~ accessible_world(skc12,X2007)
| ~ proposition(skc12,X2007)
| ~ theme(skc12,X2008,X2007)
| ~ event(skc12,X2008)
| ~ present(skc12,X2008)
| ~ think_believe_consider(skc12,X2008)
| ~ forename(skc12,X2006)
| ~ vincent_forename(skc12,X2006)
| ~ of(skc12,X2006,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X2008,skc10)
| ~ jules_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ smoke(X2007,X2009)
| ~ present(X2007,X2009)
| ~ agent(X2007,X2009,skc15)
| ~ event(X2007,X2009)
| ~ man(skc12,skc15)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X2007,skf4(X2007)) ),
inference(resolution,[status(thm)],[c1199,c577]) ).
cnf(c1206,plain,
( ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ theme(skc12,X2019,skc8)
| ~ event(skc12,X2019)
| ~ present(skc12,X2019)
| ~ think_believe_consider(skc12,X2019)
| ~ forename(skc12,X2020)
| ~ vincent_forename(skc12,X2020)
| ~ of(skc12,X2020,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X2019,skc10)
| ~ jules_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1203,clause86]) ).
cnf(c1207,plain,
( ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ theme(skc12,skf2(skc10),skc8)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X2021)
| ~ vincent_forename(skc12,X2021)
| ~ of(skc12,X2021,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1206,c383]) ).
cnf(c396,plain,
( ~ accessible_world(skc8,X685)
| ~ proposition(skc8,X685)
| ~ theme(skc8,X687,X685)
| ~ event(skc8,X687)
| ~ present(skc8,X687)
| ~ think_believe_consider(skc8,X687)
| ~ forename(skc8,X678)
| ~ vincent_forename(skc8,X678)
| ~ of(skc8,X678,X679)
| ~ man(skc8,X679)
| ~ agent(skc8,X687,X679)
| ~ jules_forename(skc8,X677)
| ~ forename(skc8,X677)
| ~ smoke(X682,X683)
| ~ present(X682,X683)
| ~ agent(X682,X683,X681)
| ~ event(X682,X683)
| ~ man(skc8,X681)
| ~ of(skc8,X677,X681)
| ~ proposition(skc8,X682)
| ~ accessible_world(skc8,X682)
| ~ think_believe_consider(skc8,X684)
| ~ present(skc8,X684)
| ~ event(skc8,X684)
| ~ theme(skc8,X684,X682)
| ~ state(skc8,skc9)
| ~ forename(skc8,X680)
| ~ vincent_forename(skc8,X680)
| ~ of(skc8,X680,skc10)
| ~ agent(skc8,X684,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X686,skc10)
| ~ jules_forename(skc8,X686)
| ~ forename(skc8,X686)
| ~ actual_world(skc8)
| man(X685,skf4(X685)) ),
inference(resolution,[status(thm)],[clause94,clause89]) ).
cnf(c699,plain,
( ~ accessible_world(skc8,X1256)
| ~ proposition(skc8,X1256)
| ~ theme(skc8,X1258,X1256)
| ~ event(skc8,X1258)
| ~ present(skc8,X1258)
| ~ think_believe_consider(skc8,X1258)
| ~ forename(skc8,X1261)
| ~ vincent_forename(skc8,X1261)
| ~ of(skc8,X1261,X1260)
| ~ man(skc8,X1260)
| ~ agent(skc8,X1258,X1260)
| ~ jules_forename(skc8,X1259)
| ~ forename(skc8,X1259)
| ~ smoke(X1263,X1262)
| ~ present(X1263,X1262)
| ~ agent(X1263,X1262,skc10)
| ~ event(X1263,X1262)
| ~ man(skc8,skc10)
| ~ of(skc8,X1259,skc10)
| ~ proposition(skc8,X1263)
| ~ accessible_world(skc8,X1263)
| ~ think_believe_consider(skc8,X1257)
| ~ present(skc8,X1257)
| ~ event(skc8,X1257)
| ~ theme(skc8,X1257,X1263)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1255)
| ~ vincent_forename(skc8,X1255)
| ~ of(skc8,X1255,skc10)
| ~ agent(skc8,X1257,skc10)
| ~ actual_world(skc8)
| man(X1256,skf4(X1256)) ),
inference(factor,[status(thm)],[c396]) ).
cnf(c1029,plain,
( ~ accessible_world(skc8,X1556)
| ~ proposition(skc8,X1556)
| ~ theme(skc8,X1553,X1556)
| ~ event(skc8,X1553)
| ~ present(skc8,X1553)
| ~ think_believe_consider(skc8,X1553)
| ~ forename(skc8,X1551)
| ~ vincent_forename(skc8,X1551)
| ~ of(skc8,X1551,X1550)
| ~ man(skc8,X1550)
| ~ agent(skc8,X1553,X1550)
| ~ jules_forename(skc8,X1555)
| ~ forename(skc8,X1555)
| ~ smoke(skc8,X1554)
| ~ present(skc8,X1554)
| ~ agent(skc8,X1554,skc10)
| ~ event(skc8,X1554)
| ~ man(skc8,skc10)
| ~ of(skc8,X1555,skc10)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1554)
| ~ theme(skc8,X1554,skc8)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1552)
| ~ vincent_forename(skc8,X1552)
| ~ of(skc8,X1552,skc10)
| ~ actual_world(skc8)
| man(X1556,skf4(X1556)) ),
inference(factor,[status(thm)],[c699]) ).
cnf(c1111,plain,
( ~ accessible_world(skc8,X1964)
| ~ proposition(skc8,X1964)
| ~ theme(skc8,X1963,X1964)
| ~ event(skc8,X1963)
| ~ present(skc8,X1963)
| ~ think_believe_consider(skc8,X1963)
| ~ forename(skc8,X1960)
| ~ vincent_forename(skc8,X1960)
| ~ of(skc8,X1960,X1961)
| ~ man(skc8,X1961)
| ~ agent(skc8,X1963,X1961)
| ~ jules_forename(skc8,X1962)
| ~ forename(skc8,X1962)
| ~ smoke(skc8,X1965)
| ~ present(skc8,X1965)
| ~ agent(skc8,X1965,skc10)
| ~ event(skc8,X1965)
| ~ man(skc8,skc10)
| ~ of(skc8,X1962,skc10)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1965)
| ~ theme(skc8,X1965,skc8)
| ~ state(skc8,skc9)
| ~ forename(skc8,skc11)
| ~ vincent_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1964,skf4(X1964)) ),
inference(resolution,[status(thm)],[c1029,clause88]) ).
cnf(c1192,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1968,skc8)
| ~ event(skc8,X1968)
| ~ present(skc8,X1968)
| ~ think_believe_consider(skc8,X1968)
| ~ forename(skc8,X1969)
| ~ vincent_forename(skc8,X1969)
| ~ of(skc8,X1969,X1967)
| ~ man(skc8,X1967)
| ~ agent(skc8,X1968,X1967)
| ~ jules_forename(skc8,X1966)
| ~ forename(skc8,X1966)
| ~ smoke(skc8,X1968)
| ~ agent(skc8,X1968,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1966,skc10)
| ~ state(skc8,skc9)
| ~ forename(skc8,skc11)
| ~ vincent_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1111]) ).
cnf(c1194,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1974,skc8)
| ~ event(skc8,X1974)
| ~ present(skc8,X1974)
| ~ think_believe_consider(skc8,X1974)
| ~ forename(skc8,X1972)
| ~ vincent_forename(skc8,X1972)
| ~ of(skc8,X1972,X1973)
| ~ man(skc8,X1973)
| ~ agent(skc8,X1974,X1973)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc8,X1974)
| ~ agent(skc8,X1974,skc10)
| ~ man(skc8,skc10)
| ~ state(skc8,skc9)
| ~ vincent_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1192,clause88]) ).
cnf(c1174,plain,
( ~ accessible_world(skc12,X1914)
| ~ proposition(skc12,X1914)
| ~ theme(skc12,X1910,X1914)
| ~ event(skc12,X1910)
| ~ present(skc12,X1910)
| ~ think_believe_consider(skc12,X1910)
| ~ forename(skc12,X1912)
| ~ vincent_forename(skc12,X1912)
| ~ of(skc12,X1912,X1913)
| ~ man(skc12,X1913)
| ~ agent(skc12,X1910,X1913)
| ~ jules_forename(skc12,X1909)
| ~ forename(skc12,X1909)
| ~ smoke(skc12,X1911)
| ~ present(skc12,X1911)
| ~ agent(skc12,X1911,skc10)
| ~ event(skc12,X1911)
| ~ man(skc12,skc10)
| ~ of(skc12,X1909,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1911)
| ~ theme(skc12,X1911,skc12)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,X1909)
| ~ actual_world(skc12)
| man(X1914,skf4(X1914)) ),
inference(factor,[status(thm)],[c1082]) ).
cnf(c1187,plain,
( ~ accessible_world(skc12,X1920)
| ~ proposition(skc12,X1920)
| ~ theme(skc12,X1922,X1920)
| ~ event(skc12,X1922)
| ~ present(skc12,X1922)
| ~ think_believe_consider(skc12,X1922)
| ~ forename(skc12,X1923)
| ~ vincent_forename(skc12,X1923)
| ~ of(skc12,X1923,X1919)
| ~ man(skc12,X1919)
| ~ agent(skc12,X1922,X1919)
| ~ jules_forename(skc12,X1921)
| ~ forename(skc12,X1921)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ man(skc12,skc10)
| ~ of(skc12,X1921,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,X1921)
| ~ actual_world(skc12)
| man(X1920,skf4(X1920)) ),
inference(resolution,[status(thm)],[c1174,c571]) ).
cnf(c1189,plain,
( ~ accessible_world(skc12,X1934)
| ~ proposition(skc12,X1934)
| ~ theme(skc12,X1936,X1934)
| ~ event(skc12,X1936)
| ~ present(skc12,X1936)
| ~ think_believe_consider(skc12,X1936)
| ~ forename(skc12,X1935)
| ~ vincent_forename(skc12,X1935)
| ~ of(skc12,X1935,X1937)
| ~ man(skc12,X1937)
| ~ agent(skc12,X1936,X1937)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ man(skc12,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ vincent_forename(skc12,skc11)
| ~ actual_world(skc12)
| man(X1934,skf4(X1934)) ),
inference(resolution,[status(thm)],[c1187,c580]) ).
cnf(c1083,plain,
( ~ accessible_world(skc12,X1871)
| ~ proposition(skc12,X1871)
| ~ theme(skc12,X1867,X1871)
| ~ event(skc12,X1867)
| ~ present(skc12,X1867)
| ~ think_believe_consider(skc12,X1867)
| ~ forename(skc12,X1866)
| ~ vincent_forename(skc12,X1866)
| ~ of(skc12,X1866,X1870)
| ~ man(skc12,X1870)
| ~ agent(skc12,X1867,X1870)
| ~ jules_forename(skc12,X1865)
| ~ forename(skc12,X1865)
| ~ smoke(X1868,X1869)
| ~ present(X1868,X1869)
| ~ agent(X1868,X1869,skc10)
| ~ event(X1868,X1869)
| ~ man(skc12,skc10)
| ~ of(skc12,X1865,skc10)
| ~ proposition(skc12,X1868)
| ~ accessible_world(skc12,X1868)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1868)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1864)
| ~ vincent_forename(skc12,X1864)
| ~ of(skc12,X1864,skc10)
| ~ actual_world(skc12)
| man(X1871,skf4(X1871)) ),
inference(resolution,[status(thm)],[c922,c383]) ).
cnf(c1182,plain,
( ~ accessible_world(skc12,X1881)
| ~ proposition(skc12,X1881)
| ~ theme(skc12,skf2(skc10),X1881)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X1884)
| ~ vincent_forename(skc12,X1884)
| ~ of(skc12,X1884,X1883)
| ~ man(skc12,X1883)
| ~ agent(skc12,skf2(skc10),X1883)
| ~ jules_forename(skc12,X1885)
| ~ forename(skc12,X1885)
| ~ smoke(X1881,X1880)
| ~ present(X1881,X1880)
| ~ agent(X1881,X1880,skc10)
| ~ event(X1881,X1880)
| ~ man(skc12,skc10)
| ~ of(skc12,X1885,skc10)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1882)
| ~ vincent_forename(skc12,X1882)
| ~ of(skc12,X1882,skc10)
| ~ actual_world(skc12)
| man(X1881,skf4(X1881)) ),
inference(factor,[status(thm)],[c1083]) ).
cnf(c1185,plain,
( ~ accessible_world(skc12,X1886)
| ~ proposition(skc12,X1886)
| ~ theme(skc12,skf2(skc10),X1886)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X1888)
| ~ vincent_forename(skc12,X1888)
| ~ of(skc12,X1888,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1889)
| ~ forename(skc12,X1889)
| ~ smoke(X1886,X1890)
| ~ present(X1886,X1890)
| ~ agent(X1886,X1890,skc10)
| ~ event(X1886,X1890)
| ~ of(skc12,X1889,skc10)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1887)
| ~ vincent_forename(skc12,X1887)
| ~ of(skc12,X1887,skc10)
| ~ actual_world(skc12)
| man(X1886,skf4(X1886)) ),
inference(resolution,[status(thm)],[c1182,c383]) ).
cnf(c1173,plain,
( ~ accessible_world(skc12,X1852)
| ~ proposition(skc12,X1852)
| ~ theme(skc12,X1849,X1852)
| ~ event(skc12,X1849)
| ~ present(skc12,X1849)
| ~ think_believe_consider(skc12,X1849)
| ~ forename(skc12,X1848)
| ~ vincent_forename(skc12,X1848)
| ~ of(skc12,X1848,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1849,skc10)
| ~ jules_forename(skc12,X1851)
| ~ forename(skc12,X1851)
| ~ smoke(skc12,X1850)
| ~ present(skc12,X1850)
| ~ agent(skc12,X1850,skc10)
| ~ event(skc12,X1850)
| ~ of(skc12,X1851,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1850)
| ~ theme(skc12,X1850,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1852,skf4(X1852)) ),
inference(factor,[status(thm)],[c1082]) ).
cnf(c1177,plain,
( ~ accessible_world(skc12,X1863)
| ~ proposition(skc12,X1863)
| ~ theme(skc12,X1861,X1863)
| ~ event(skc12,X1861)
| ~ present(skc12,X1861)
| ~ think_believe_consider(skc12,X1861)
| ~ forename(skc12,X1860)
| ~ vincent_forename(skc12,X1860)
| ~ of(skc12,X1860,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1861,skc10)
| ~ jules_forename(skc12,X1862)
| ~ forename(skc12,X1862)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ of(skc12,X1862,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1863,skf4(X1863)) ),
inference(resolution,[status(thm)],[c1173,c571]) ).
cnf(c1181,plain,
( ~ accessible_world(skc12,X1875)
| ~ proposition(skc12,X1875)
| ~ theme(skc12,X1876,X1875)
| ~ event(skc12,X1876)
| ~ present(skc12,X1876)
| ~ think_believe_consider(skc12,X1876)
| ~ forename(skc12,X1877)
| ~ vincent_forename(skc12,X1877)
| ~ of(skc12,X1877,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1876,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1875,skf4(X1875)) ),
inference(resolution,[status(thm)],[c1177,c580]) ).
cnf(c1176,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1854,skc12)
| ~ event(skc12,X1854)
| ~ present(skc12,X1854)
| ~ think_believe_consider(skc12,X1854)
| ~ forename(skc12,X1853)
| ~ vincent_forename(skc12,X1853)
| ~ of(skc12,X1853,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1854,skc10)
| ~ jules_forename(skc12,X1855)
| ~ forename(skc12,X1855)
| ~ smoke(skc12,X1854)
| ~ of(skc12,X1855,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1173]) ).
cnf(c921,plain,
( ~ accessible_world(skc12,X1456)
| ~ proposition(skc12,X1456)
| ~ theme(skc12,X1455,X1456)
| ~ event(skc12,X1455)
| ~ present(skc12,X1455)
| ~ think_believe_consider(skc12,X1455)
| ~ forename(skc12,X1448)
| ~ vincent_forename(skc12,X1448)
| ~ of(skc12,X1448,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1455,skc10)
| ~ jules_forename(skc12,X1452)
| ~ forename(skc12,X1452)
| ~ smoke(X1454,X1449)
| ~ present(X1454,X1449)
| ~ agent(X1454,X1449,X1451)
| ~ event(X1454,X1449)
| ~ man(skc12,X1451)
| ~ of(skc12,X1452,X1451)
| ~ proposition(skc12,X1454)
| ~ accessible_world(skc12,X1454)
| ~ think_believe_consider(skc12,X1453)
| ~ present(skc12,X1453)
| ~ event(skc12,X1453)
| ~ theme(skc12,X1453,X1454)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1450)
| ~ vincent_forename(skc12,X1450)
| ~ of(skc12,X1450,skc10)
| ~ agent(skc12,X1453,skc10)
| ~ jules_forename(skc12,X1448)
| ~ actual_world(skc12)
| man(X1456,skf4(X1456)) ),
inference(factor,[status(thm)],[c590]) ).
cnf(c1079,plain,
( ~ accessible_world(skc12,X1797)
| ~ proposition(skc12,X1797)
| ~ theme(skc12,X1794,X1797)
| ~ event(skc12,X1794)
| ~ present(skc12,X1794)
| ~ think_believe_consider(skc12,X1794)
| ~ forename(skc12,X1793)
| ~ vincent_forename(skc12,X1793)
| ~ of(skc12,X1793,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1794,skc10)
| ~ jules_forename(skc12,X1796)
| ~ forename(skc12,X1796)
| ~ smoke(skc12,X1798)
| ~ present(skc12,X1798)
| ~ agent(skc12,X1798,skc10)
| ~ event(skc12,X1798)
| ~ of(skc12,X1796,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1798)
| ~ theme(skc12,X1798,skc12)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1795)
| ~ vincent_forename(skc12,X1795)
| ~ of(skc12,X1795,skc10)
| ~ jules_forename(skc12,X1793)
| ~ actual_world(skc12)
| man(X1797,skf4(X1797)) ),
inference(factor,[status(thm)],[c921]) ).
cnf(c1164,plain,
( ~ accessible_world(skc12,X1814)
| ~ proposition(skc12,X1814)
| ~ theme(skc12,X1813,X1814)
| ~ event(skc12,X1813)
| ~ present(skc12,X1813)
| ~ think_believe_consider(skc12,X1813)
| ~ forename(skc12,X1816)
| ~ vincent_forename(skc12,X1816)
| ~ of(skc12,X1816,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1813,skc10)
| ~ jules_forename(skc12,X1817)
| ~ forename(skc12,X1817)
| ~ smoke(skc12,X1815)
| ~ present(skc12,X1815)
| ~ agent(skc12,X1815,skc10)
| ~ event(skc12,X1815)
| ~ of(skc12,X1817,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,X1815)
| ~ theme(skc12,X1815,skc12)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1816)
| ~ actual_world(skc12)
| man(X1814,skf4(X1814)) ),
inference(factor,[status(thm)],[c1079]) ).
cnf(c1168,plain,
( ~ accessible_world(skc12,X1830)
| ~ proposition(skc12,X1830)
| ~ theme(skc12,X1832,X1830)
| ~ event(skc12,X1832)
| ~ present(skc12,X1832)
| ~ think_believe_consider(skc12,X1832)
| ~ forename(skc12,X1829)
| ~ vincent_forename(skc12,X1829)
| ~ of(skc12,X1829,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1832,skc10)
| ~ jules_forename(skc12,X1831)
| ~ forename(skc12,X1831)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ of(skc12,X1831,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1829)
| ~ actual_world(skc12)
| man(X1830,skf4(X1830)) ),
inference(resolution,[status(thm)],[c1164,c571]) ).
cnf(c1170,plain,
( ~ accessible_world(skc12,X1834)
| ~ proposition(skc12,X1834)
| ~ theme(skc12,X1833,X1834)
| ~ event(skc12,X1833)
| ~ present(skc12,X1833)
| ~ think_believe_consider(skc12,X1833)
| ~ forename(skc12,X1835)
| ~ vincent_forename(skc12,X1835)
| ~ of(skc12,X1835,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1833,skc10)
| ~ jules_forename(skc12,X1835)
| ~ smoke(skc12,skc13)
| ~ present(skc12,skc13)
| ~ agent(skc12,skc13,skc10)
| ~ event(skc12,skc13)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ think_believe_consider(skc12,skc13)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1834,skf4(X1834)) ),
inference(factor,[status(thm)],[c1168]) ).
cnf(c1080,plain,
( ~ accessible_world(skc12,X1825)
| ~ proposition(skc12,X1825)
| ~ theme(skc12,X1822,X1825)
| ~ event(skc12,X1822)
| ~ present(skc12,X1822)
| ~ think_believe_consider(skc12,X1822)
| ~ forename(skc12,X1820)
| ~ vincent_forename(skc12,X1820)
| ~ of(skc12,X1820,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1822,skc10)
| ~ jules_forename(skc12,X1824)
| ~ forename(skc12,X1824)
| ~ smoke(X1818,X1819)
| ~ present(X1818,X1819)
| ~ agent(X1818,X1819,X1821)
| ~ event(X1818,X1819)
| ~ man(skc12,X1821)
| ~ of(skc12,X1824,X1821)
| ~ proposition(skc12,X1818)
| ~ accessible_world(skc12,X1818)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1818)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1823)
| ~ vincent_forename(skc12,X1823)
| ~ of(skc12,X1823,skc10)
| ~ jules_forename(skc12,X1820)
| ~ actual_world(skc12)
| man(X1825,skf4(X1825)) ),
inference(resolution,[status(thm)],[c921,c383]) ).
cnf(c1078,plain,
( ~ accessible_world(skc12,X1755)
| ~ proposition(skc12,X1755)
| ~ theme(skc12,X1756,X1755)
| ~ event(skc12,X1756)
| ~ present(skc12,X1756)
| ~ think_believe_consider(skc12,X1756)
| ~ forename(skc12,X1751)
| ~ vincent_forename(skc12,X1751)
| ~ of(skc12,X1751,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1756,skc10)
| ~ jules_forename(skc12,X1754)
| ~ forename(skc12,X1754)
| ~ smoke(X1749,X1750)
| ~ present(X1749,X1750)
| ~ agent(X1749,X1750,X1752)
| ~ event(X1749,X1750)
| ~ man(skc12,X1752)
| ~ of(skc12,X1754,X1752)
| ~ proposition(skc12,X1749)
| ~ accessible_world(skc12,X1749)
| ~ theme(skc12,X1756,X1749)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1753)
| ~ vincent_forename(skc12,X1753)
| ~ of(skc12,X1753,skc10)
| ~ jules_forename(skc12,X1751)
| ~ actual_world(skc12)
| man(X1755,skf4(X1755)) ),
inference(factor,[status(thm)],[c921]) ).
cnf(c1151,plain,
( ~ accessible_world(skc12,X1761)
| ~ proposition(skc12,X1761)
| ~ theme(skc12,X1760,X1761)
| ~ event(skc12,X1760)
| ~ present(skc12,X1760)
| ~ think_believe_consider(skc12,X1760)
| ~ forename(skc12,X1757)
| ~ vincent_forename(skc12,X1757)
| ~ of(skc12,X1757,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1760,skc10)
| ~ jules_forename(skc12,X1758)
| ~ forename(skc12,X1758)
| ~ smoke(X1759,X1762)
| ~ present(X1759,X1762)
| ~ agent(X1759,X1762,X1763)
| ~ event(X1759,X1762)
| ~ man(skc12,X1763)
| ~ of(skc12,X1758,X1763)
| ~ proposition(skc12,X1759)
| ~ accessible_world(skc12,X1759)
| ~ theme(skc12,X1760,X1759)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1757)
| ~ actual_world(skc12)
| man(X1761,skf4(X1761)) ),
inference(factor,[status(thm)],[c1078]) ).
cnf(c1154,plain,
( ~ accessible_world(skc12,X1765)
| ~ proposition(skc12,X1765)
| ~ theme(skc12,X1767,X1765)
| ~ event(skc12,X1767)
| ~ present(skc12,X1767)
| ~ think_believe_consider(skc12,X1767)
| ~ forename(skc12,X1768)
| ~ vincent_forename(skc12,X1768)
| ~ of(skc12,X1768,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1767,skc10)
| ~ jules_forename(skc12,X1764)
| ~ forename(skc12,X1764)
| ~ smoke(X1765,X1766)
| ~ present(X1765,X1766)
| ~ agent(X1765,X1766,X1769)
| ~ event(X1765,X1766)
| ~ man(skc12,X1769)
| ~ of(skc12,X1764,X1769)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1768)
| ~ actual_world(skc12)
| man(X1765,skf4(X1765)) ),
inference(factor,[status(thm)],[c1151]) ).
cnf(c1158,plain,
( ~ accessible_world(skc12,X1787)
| ~ proposition(skc12,X1787)
| ~ theme(skc12,X1786,X1787)
| ~ event(skc12,X1786)
| ~ present(skc12,X1786)
| ~ think_believe_consider(skc12,X1786)
| ~ forename(skc12,X1788)
| ~ vincent_forename(skc12,X1788)
| ~ of(skc12,X1788,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1786,skc10)
| ~ jules_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ smoke(X1787,X1785)
| ~ present(X1787,X1785)
| ~ agent(X1787,X1785,skc15)
| ~ event(X1787,X1785)
| ~ man(skc12,skc15)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1788)
| ~ actual_world(skc12)
| man(X1787,skf4(X1787)) ),
inference(resolution,[status(thm)],[c1154,c577]) ).
cnf(c1162,plain,
( ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ theme(skc12,X1792,skc8)
| ~ event(skc12,X1792)
| ~ present(skc12,X1792)
| ~ think_believe_consider(skc12,X1792)
| ~ forename(skc12,X1791)
| ~ vincent_forename(skc12,X1791)
| ~ of(skc12,X1791,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1792,skc10)
| ~ jules_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1791)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1158,clause86]) ).
cnf(c1163,plain,
( ~ accessible_world(skc12,skc8)
| ~ proposition(skc12,skc8)
| ~ theme(skc12,skf2(skc10),skc8)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X1799)
| ~ vincent_forename(skc12,X1799)
| ~ of(skc12,X1799,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc14)
| ~ forename(skc12,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc12,skc15)
| ~ state(skc12,skc9)
| ~ jules_forename(skc12,X1799)
| ~ actual_world(skc12)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1162,c383]) ).
cnf(c917,plain,
( ~ smoke(X1420,X1419)
| ~ present(X1420,X1419)
| ~ agent(X1420,X1419,skf4(X1420))
| ~ event(X1420,X1419)
| ~ accessible_world(skc12,X1420)
| ~ proposition(skc12,X1420)
| ~ theme(skc12,X1421,X1420)
| ~ event(skc12,X1421)
| ~ present(skc12,X1421)
| ~ think_believe_consider(skc12,X1421)
| ~ forename(skc12,X1425)
| ~ vincent_forename(skc12,X1425)
| ~ of(skc12,X1425,X1426)
| ~ man(skc12,X1426)
| ~ agent(skc12,X1421,X1426)
| ~ jules_forename(skc12,X1422)
| ~ forename(skc12,X1422)
| ~ man(skc12,skf4(X1420))
| ~ of(skc12,X1422,skf4(X1420))
| ~ think_believe_consider(skc12,X1427)
| ~ present(skc12,X1427)
| ~ event(skc12,X1427)
| ~ theme(skc12,X1427,X1420)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1424)
| ~ vincent_forename(skc12,X1424)
| ~ of(skc12,X1424,skc10)
| ~ agent(skc12,X1427,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1423,skc10)
| ~ jules_forename(skc12,X1423)
| ~ forename(skc12,X1423)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c588]) ).
cnf(c1071,plain,
( ~ smoke(X1774,X1773)
| ~ present(X1774,X1773)
| ~ agent(X1774,X1773,skf4(X1774))
| ~ event(X1774,X1773)
| ~ accessible_world(skc12,X1774)
| ~ proposition(skc12,X1774)
| ~ theme(skc12,X1775,X1774)
| ~ event(skc12,X1775)
| ~ present(skc12,X1775)
| ~ think_believe_consider(skc12,X1775)
| ~ forename(skc12,X1772)
| ~ vincent_forename(skc12,X1772)
| ~ of(skc12,X1772,skf4(X1774))
| ~ man(skc12,skf4(X1774))
| ~ agent(skc12,X1775,skf4(X1774))
| ~ jules_forename(skc12,X1772)
| ~ think_believe_consider(skc12,X1770)
| ~ present(skc12,X1770)
| ~ event(skc12,X1770)
| ~ theme(skc12,X1770,X1774)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1776)
| ~ vincent_forename(skc12,X1776)
| ~ of(skc12,X1776,skc10)
| ~ agent(skc12,X1770,skc10)
| ~ man(skc12,skc10)
| ~ of(skc12,X1771,skc10)
| ~ jules_forename(skc12,X1771)
| ~ forename(skc12,X1771)
| ~ actual_world(skc12) ),
inference(factor,[status(thm)],[c917]) ).
cnf(c1110,plain,
( ~ accessible_world(skc8,X1719)
| ~ proposition(skc8,X1719)
| ~ theme(skc8,X1718,X1719)
| ~ event(skc8,X1718)
| ~ present(skc8,X1718)
| ~ think_believe_consider(skc8,X1718)
| ~ forename(skc8,X1715)
| ~ vincent_forename(skc8,X1715)
| ~ of(skc8,X1715,X1717)
| ~ man(skc8,X1717)
| ~ agent(skc8,X1718,X1717)
| ~ jules_forename(skc8,X1716)
| ~ forename(skc8,X1716)
| ~ smoke(skc8,X1720)
| ~ present(skc8,X1720)
| ~ agent(skc8,X1720,skc10)
| ~ event(skc8,X1720)
| ~ man(skc8,skc10)
| ~ of(skc8,X1716,skc10)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1720)
| ~ theme(skc8,X1720,skc8)
| ~ state(skc8,skc9)
| ~ vincent_forename(skc8,X1716)
| ~ actual_world(skc8)
| man(X1719,skf4(X1719)) ),
inference(factor,[status(thm)],[c1029]) ).
cnf(c706,plain,
( ~ smoke(X1365,X1369)
| ~ present(X1365,X1369)
| ~ agent(X1365,X1369,skf4(X1365))
| ~ event(X1365,X1369)
| ~ accessible_world(skc8,X1365)
| ~ proposition(skc8,X1365)
| ~ theme(skc8,X1371,X1365)
| ~ event(skc8,X1371)
| ~ present(skc8,X1371)
| ~ think_believe_consider(skc8,X1371)
| ~ forename(skc8,X1367)
| ~ vincent_forename(skc8,X1367)
| ~ of(skc8,X1367,X1370)
| ~ man(skc8,X1370)
| ~ agent(skc8,X1371,X1370)
| ~ jules_forename(skc8,X1373)
| ~ forename(skc8,X1373)
| ~ man(skc8,skf4(X1365))
| ~ of(skc8,X1373,skf4(X1365))
| ~ think_believe_consider(skc8,X1372)
| ~ present(skc8,X1372)
| ~ event(skc8,X1372)
| ~ theme(skc8,X1372,X1365)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1368)
| ~ vincent_forename(skc8,X1368)
| ~ of(skc8,X1368,skc10)
| ~ agent(skc8,X1372,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1366,skc10)
| ~ jules_forename(skc8,X1366)
| ~ forename(skc8,X1366)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c1059,plain,
( ~ smoke(X1697,X1699)
| ~ present(X1697,X1699)
| ~ agent(X1697,X1699,skf4(X1697))
| ~ event(X1697,X1699)
| ~ accessible_world(skc8,X1697)
| ~ proposition(skc8,X1697)
| ~ theme(skc8,X1702,X1697)
| ~ event(skc8,X1702)
| ~ present(skc8,X1702)
| ~ think_believe_consider(skc8,X1702)
| ~ forename(skc8,X1698)
| ~ vincent_forename(skc8,X1698)
| ~ of(skc8,X1698,skf4(X1697))
| ~ man(skc8,skf4(X1697))
| ~ agent(skc8,X1702,skf4(X1697))
| ~ jules_forename(skc8,X1698)
| ~ think_believe_consider(skc8,X1703)
| ~ present(skc8,X1703)
| ~ event(skc8,X1703)
| ~ theme(skc8,X1703,X1697)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1700)
| ~ vincent_forename(skc8,X1700)
| ~ of(skc8,X1700,skc10)
| ~ agent(skc8,X1703,skc10)
| ~ man(skc8,skc10)
| ~ of(skc8,X1701,skc10)
| ~ jules_forename(skc8,X1701)
| ~ forename(skc8,X1701)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c706]) ).
cnf(c701,plain,
( ~ accessible_world(skc8,X1320)
| ~ proposition(skc8,X1320)
| ~ theme(skc8,X1323,X1320)
| ~ event(skc8,X1323)
| ~ present(skc8,X1323)
| ~ think_believe_consider(skc8,X1323)
| ~ forename(skc8,X1326)
| ~ vincent_forename(skc8,X1326)
| ~ of(skc8,X1326,X1324)
| ~ man(skc8,X1324)
| ~ agent(skc8,X1323,X1324)
| ~ jules_forename(skc8,X1325)
| ~ forename(skc8,X1325)
| ~ smoke(X1328,X1327)
| ~ present(X1328,X1327)
| ~ agent(X1328,X1327,X1319)
| ~ event(X1328,X1327)
| ~ man(skc8,X1319)
| ~ of(skc8,X1325,X1319)
| ~ proposition(skc8,X1328)
| ~ accessible_world(skc8,X1328)
| ~ think_believe_consider(skc8,X1322)
| ~ present(skc8,X1322)
| ~ event(skc8,X1322)
| ~ theme(skc8,X1322,X1328)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1321)
| ~ vincent_forename(skc8,X1321)
| ~ of(skc8,X1321,skc10)
| ~ agent(skc8,X1322,skc10)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1320,skf4(X1320)) ),
inference(resolution,[status(thm)],[c396,clause88]) ).
cnf(c1048,plain,
( ~ accessible_world(skc8,X1629)
| ~ proposition(skc8,X1629)
| ~ theme(skc8,X1625,X1629)
| ~ event(skc8,X1625)
| ~ present(skc8,X1625)
| ~ think_believe_consider(skc8,X1625)
| ~ forename(skc8,X1628)
| ~ vincent_forename(skc8,X1628)
| ~ of(skc8,X1628,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1625,skc10)
| ~ jules_forename(skc8,X1627)
| ~ forename(skc8,X1627)
| ~ smoke(X1623,X1624)
| ~ present(X1623,X1624)
| ~ agent(X1623,X1624,X1626)
| ~ event(X1623,X1624)
| ~ man(skc8,X1626)
| ~ of(skc8,X1627,X1626)
| ~ proposition(skc8,X1623)
| ~ accessible_world(skc8,X1623)
| ~ theme(skc8,X1625,X1623)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1622)
| ~ vincent_forename(skc8,X1622)
| ~ of(skc8,X1622,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1629,skf4(X1629)) ),
inference(factor,[status(thm)],[c701]) ).
cnf(c1132,plain,
( ~ accessible_world(skc8,X1665)
| ~ proposition(skc8,X1665)
| ~ theme(skc8,X1660,X1665)
| ~ event(skc8,X1660)
| ~ present(skc8,X1660)
| ~ think_believe_consider(skc8,X1660)
| ~ forename(skc8,X1662)
| ~ vincent_forename(skc8,X1662)
| ~ of(skc8,X1662,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1660,skc10)
| ~ jules_forename(skc8,X1663)
| ~ forename(skc8,X1663)
| ~ smoke(X1661,X1664)
| ~ present(X1661,X1664)
| ~ agent(X1661,X1664,X1659)
| ~ event(X1661,X1664)
| ~ man(skc8,X1659)
| ~ of(skc8,X1663,X1659)
| ~ proposition(skc8,X1661)
| ~ accessible_world(skc8,X1661)
| ~ theme(skc8,X1660,X1661)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1665,skf4(X1665)) ),
inference(factor,[status(thm)],[c1048]) ).
cnf(c1139,plain,
( ~ accessible_world(skc8,X1671)
| ~ proposition(skc8,X1671)
| ~ theme(skc8,X1670,X1671)
| ~ event(skc8,X1670)
| ~ present(skc8,X1670)
| ~ think_believe_consider(skc8,X1670)
| ~ forename(skc8,X1668)
| ~ vincent_forename(skc8,X1668)
| ~ of(skc8,X1668,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1670,skc10)
| ~ jules_forename(skc8,X1667)
| ~ forename(skc8,X1667)
| ~ smoke(X1671,X1666)
| ~ present(X1671,X1666)
| ~ agent(X1671,X1666,X1669)
| ~ event(X1671,X1666)
| ~ man(skc8,X1669)
| ~ of(skc8,X1667,X1669)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1671,skf4(X1671)) ),
inference(factor,[status(thm)],[c1132]) ).
cnf(c1142,plain,
( ~ accessible_world(skc8,X1689)
| ~ proposition(skc8,X1689)
| ~ theme(skc8,X1688,X1689)
| ~ event(skc8,X1688)
| ~ present(skc8,X1688)
| ~ think_believe_consider(skc8,X1688)
| ~ forename(skc8,X1687)
| ~ vincent_forename(skc8,X1687)
| ~ of(skc8,X1687,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1688,skc10)
| ~ jules_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ smoke(X1689,X1690)
| ~ present(X1689,X1690)
| ~ agent(X1689,X1690,skc15)
| ~ event(X1689,X1690)
| ~ man(skc8,skc15)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(X1689,skf4(X1689)) ),
inference(resolution,[status(thm)],[c1139,clause85]) ).
cnf(c1147,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1693,skc8)
| ~ event(skc8,X1693)
| ~ present(skc8,X1693)
| ~ think_believe_consider(skc8,X1693)
| ~ forename(skc8,X1694)
| ~ vincent_forename(skc8,X1694)
| ~ of(skc8,X1694,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1693,skc10)
| ~ jules_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1142,clause86]) ).
cnf(c1109,plain,
( ~ accessible_world(skc8,X1643)
| ~ proposition(skc8,X1643)
| ~ theme(skc8,X1642,X1643)
| ~ event(skc8,X1642)
| ~ present(skc8,X1642)
| ~ think_believe_consider(skc8,X1642)
| ~ forename(skc8,X1640)
| ~ vincent_forename(skc8,X1640)
| ~ of(skc8,X1640,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1642,skc10)
| ~ jules_forename(skc8,X1641)
| ~ forename(skc8,X1641)
| ~ smoke(skc8,X1644)
| ~ present(skc8,X1644)
| ~ agent(skc8,X1644,skc10)
| ~ event(skc8,X1644)
| ~ of(skc8,X1641,skc10)
| ~ proposition(skc8,skc8)
| ~ accessible_world(skc8,skc8)
| ~ think_believe_consider(skc8,X1644)
| ~ theme(skc8,X1644,skc8)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1643,skf4(X1643)) ),
inference(factor,[status(thm)],[c1029]) ).
cnf(c1136,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1645,skc8)
| ~ event(skc8,X1645)
| ~ present(skc8,X1645)
| ~ think_believe_consider(skc8,X1645)
| ~ forename(skc8,X1647)
| ~ vincent_forename(skc8,X1647)
| ~ of(skc8,X1647,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1645,skc10)
| ~ jules_forename(skc8,X1646)
| ~ forename(skc8,X1646)
| ~ smoke(skc8,X1645)
| ~ of(skc8,X1646,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1109]) ).
cnf(clause90,negated_conjecture,
( ~ man(skc12,X271)
| smoke(skc12,skf2(X270)) ),
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,X276)
| present(skc12,skf2(X275)) ),
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(X4,X3)
| event(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(c361,plain,
event(skc12,skf2(X273)),
inference(resolution,[status(thm)],[c359,clause1]) ).
cnf(c1081,plain,
( ~ accessible_world(skc12,X1494)
| ~ proposition(skc12,X1494)
| ~ theme(skc12,X1488,X1494)
| ~ event(skc12,X1488)
| ~ present(skc12,X1488)
| ~ think_believe_consider(skc12,X1488)
| ~ forename(skc12,X1491)
| ~ vincent_forename(skc12,X1491)
| ~ of(skc12,X1491,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1488,skc10)
| ~ jules_forename(skc12,X1490)
| ~ forename(skc12,X1490)
| ~ smoke(X1493,X1492)
| ~ present(X1493,X1492)
| ~ agent(X1493,X1492,skc10)
| ~ event(X1493,X1492)
| ~ of(skc12,X1490,skc10)
| ~ proposition(skc12,X1493)
| ~ accessible_world(skc12,X1493)
| ~ theme(skc12,X1488,X1493)
| ~ state(skc12,skc9)
| ~ forename(skc12,X1489)
| ~ vincent_forename(skc12,X1489)
| ~ of(skc12,X1489,skc10)
| ~ actual_world(skc12)
| man(X1494,skf4(X1494)) ),
inference(factor,[status(thm)],[c922]) ).
cnf(c1084,plain,
( ~ accessible_world(skc12,X1500)
| ~ proposition(skc12,X1500)
| ~ theme(skc12,X1498,X1500)
| ~ event(skc12,X1498)
| ~ present(skc12,X1498)
| ~ think_believe_consider(skc12,X1498)
| ~ forename(skc12,X1497)
| ~ vincent_forename(skc12,X1497)
| ~ of(skc12,X1497,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1498,skc10)
| ~ jules_forename(skc12,X1499)
| ~ forename(skc12,X1499)
| ~ smoke(X1495,X1496)
| ~ present(X1495,X1496)
| ~ agent(X1495,X1496,skc10)
| ~ event(X1495,X1496)
| ~ of(skc12,X1499,skc10)
| ~ proposition(skc12,X1495)
| ~ accessible_world(skc12,X1495)
| ~ theme(skc12,X1498,X1495)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1500,skf4(X1500)) ),
inference(factor,[status(thm)],[c1081]) ).
cnf(c1088,plain,
( ~ accessible_world(skc12,X1584)
| ~ proposition(skc12,X1584)
| ~ theme(skc12,skc13,X1584)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1583)
| ~ vincent_forename(skc12,X1583)
| ~ of(skc12,X1583,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,X1581)
| ~ forename(skc12,X1581)
| ~ smoke(skc12,X1582)
| ~ present(skc12,X1582)
| ~ agent(skc12,X1582,skc10)
| ~ event(skc12,X1582)
| ~ of(skc12,X1581,skc10)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1584,skf4(X1584)) ),
inference(resolution,[status(thm)],[c1084,c571]) ).
cnf(c1122,plain,
( ~ accessible_world(skc12,X1614)
| ~ proposition(skc12,X1614)
| ~ theme(skc12,skc13,X1614)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1613)
| ~ vincent_forename(skc12,X1613)
| ~ of(skc12,X1613,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,X1615)
| ~ present(skc12,X1615)
| ~ agent(skc12,X1615,skc10)
| ~ event(skc12,X1615)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1614,skf4(X1614)) ),
inference(resolution,[status(thm)],[c1088,c580]) ).
cnf(c1129,plain,
( ~ accessible_world(skc12,X1618)
| ~ proposition(skc12,X1618)
| ~ theme(skc12,skc13,X1618)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1619)
| ~ vincent_forename(skc12,X1619)
| ~ of(skc12,X1619,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1618,skf4(X1618)) ),
inference(resolution,[status(thm)],[c1122,c383]) ).
cnf(c1130,plain,
( ~ accessible_world(skc12,X1621)
| ~ proposition(skc12,X1621)
| ~ theme(skc12,skc13,X1621)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1620)
| ~ vincent_forename(skc12,X1620)
| ~ of(skc12,X1620,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1621,skf4(X1621)) ),
inference(resolution,[status(thm)],[c1129,c361]) ).
cnf(c1131,plain,
( ~ accessible_world(skc12,X1631)
| ~ proposition(skc12,X1631)
| ~ theme(skc12,skc13,X1631)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1630)
| ~ vincent_forename(skc12,X1630)
| ~ of(skc12,X1630,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1631,skf4(X1631)) ),
inference(resolution,[status(thm)],[c1130,c369]) ).
cnf(c1135,plain,
( ~ accessible_world(skc12,X1633)
| ~ proposition(skc12,X1633)
| ~ theme(skc12,skc13,X1633)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1632)
| ~ vincent_forename(skc12,X1632)
| ~ of(skc12,X1632,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1633,skf4(X1633)) ),
inference(resolution,[status(thm)],[c1131,c359]) ).
cnf(c1121,plain,
( ~ accessible_world(skc12,X1594)
| ~ proposition(skc12,X1594)
| ~ theme(skc12,skc13,X1594)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1595)
| ~ vincent_forename(skc12,X1595)
| ~ of(skc12,X1595,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,X1595)
| ~ smoke(skc12,X1593)
| ~ present(skc12,X1593)
| ~ agent(skc12,X1593,skc10)
| ~ event(skc12,X1593)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1594,skf4(X1594)) ),
inference(factor,[status(thm)],[c1088]) ).
cnf(c1124,plain,
( ~ accessible_world(skc12,X1599)
| ~ proposition(skc12,X1599)
| ~ theme(skc12,skc13,X1599)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1598)
| ~ vincent_forename(skc12,X1598)
| ~ of(skc12,X1598,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,X1598)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1599,skf4(X1599)) ),
inference(resolution,[status(thm)],[c1121,c383]) ).
cnf(c1125,plain,
( ~ accessible_world(skc12,X1601)
| ~ proposition(skc12,X1601)
| ~ theme(skc12,skc13,X1601)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1600)
| ~ vincent_forename(skc12,X1600)
| ~ of(skc12,X1600,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,X1600)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1601,skf4(X1601)) ),
inference(resolution,[status(thm)],[c1124,c361]) ).
cnf(c1126,plain,
( ~ accessible_world(skc12,X1603)
| ~ proposition(skc12,X1603)
| ~ theme(skc12,skc13,X1603)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1602)
| ~ vincent_forename(skc12,X1602)
| ~ of(skc12,X1602,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,X1602)
| ~ smoke(skc12,skf2(skc10))
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1603,skf4(X1603)) ),
inference(resolution,[status(thm)],[c1125,c369]) ).
cnf(c1127,plain,
( ~ accessible_world(skc12,X1611)
| ~ proposition(skc12,X1611)
| ~ theme(skc12,skc13,X1611)
| ~ event(skc12,skc13)
| ~ present(skc12,skc13)
| ~ think_believe_consider(skc12,skc13)
| ~ forename(skc12,X1612)
| ~ vincent_forename(skc12,X1612)
| ~ of(skc12,X1612,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,skc13,skc10)
| ~ jules_forename(skc12,X1612)
| ~ proposition(skc12,skc12)
| ~ accessible_world(skc12,skc12)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1611,skf4(X1611)) ),
inference(resolution,[status(thm)],[c1126,c359]) ).
cnf(c1087,plain,
( ~ accessible_world(skc12,X1502)
| ~ proposition(skc12,X1502)
| ~ theme(skc12,X1504,X1502)
| ~ event(skc12,X1504)
| ~ present(skc12,X1504)
| ~ think_believe_consider(skc12,X1504)
| ~ forename(skc12,X1505)
| ~ vincent_forename(skc12,X1505)
| ~ of(skc12,X1505,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1504,skc10)
| ~ jules_forename(skc12,X1503)
| ~ forename(skc12,X1503)
| ~ smoke(X1502,X1501)
| ~ present(X1502,X1501)
| ~ agent(X1502,X1501,skc10)
| ~ event(X1502,X1501)
| ~ of(skc12,X1503,skc10)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1502,skf4(X1502)) ),
inference(factor,[status(thm)],[c1084]) ).
cnf(c1090,plain,
( ~ accessible_world(skc12,X1526)
| ~ proposition(skc12,X1526)
| ~ theme(skc12,X1525,X1526)
| ~ event(skc12,X1525)
| ~ present(skc12,X1525)
| ~ think_believe_consider(skc12,X1525)
| ~ forename(skc12,X1524)
| ~ vincent_forename(skc12,X1524)
| ~ of(skc12,X1524,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1525,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(X1526,X1523)
| ~ present(X1526,X1523)
| ~ agent(X1526,X1523,skc10)
| ~ event(X1526,X1523)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1526,skf4(X1526)) ),
inference(resolution,[status(thm)],[c1087,c580]) ).
cnf(c1098,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1558,skc12)
| ~ event(skc12,X1558)
| ~ present(skc12,X1558)
| ~ think_believe_consider(skc12,X1558)
| ~ forename(skc12,X1559)
| ~ vincent_forename(skc12,X1559)
| ~ of(skc12,X1559,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1558,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1090,c383]) ).
cnf(c1113,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1561,skc12)
| ~ event(skc12,X1561)
| ~ present(skc12,X1561)
| ~ think_believe_consider(skc12,X1561)
| ~ forename(skc12,X1560)
| ~ vincent_forename(skc12,X1560)
| ~ of(skc12,X1560,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1561,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1098,c361]) ).
cnf(c1115,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1562,skc12)
| ~ event(skc12,X1562)
| ~ present(skc12,X1562)
| ~ think_believe_consider(skc12,X1562)
| ~ forename(skc12,X1563)
| ~ vincent_forename(skc12,X1563)
| ~ of(skc12,X1563,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1562,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1113,c369]) ).
cnf(c1116,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1565,skc12)
| ~ event(skc12,X1565)
| ~ present(skc12,X1565)
| ~ think_believe_consider(skc12,X1565)
| ~ forename(skc12,X1564)
| ~ vincent_forename(skc12,X1564)
| ~ of(skc12,X1564,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1565,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1115,c359]) ).
cnf(c1117,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X1572)
| ~ vincent_forename(skc12,X1572)
| ~ of(skc12,X1572,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,skc11)
| ~ forename(skc12,skc11)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1116,c383]) ).
cnf(c1089,plain,
( ~ accessible_world(skc12,X1509)
| ~ proposition(skc12,X1509)
| ~ theme(skc12,X1507,X1509)
| ~ event(skc12,X1507)
| ~ present(skc12,X1507)
| ~ think_believe_consider(skc12,X1507)
| ~ forename(skc12,X1508)
| ~ vincent_forename(skc12,X1508)
| ~ of(skc12,X1508,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1507,skc10)
| ~ jules_forename(skc12,X1508)
| ~ smoke(X1509,X1506)
| ~ present(X1509,X1506)
| ~ agent(X1509,X1506,skc10)
| ~ event(X1509,X1506)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(X1509,skf4(X1509)) ),
inference(factor,[status(thm)],[c1087]) ).
cnf(c1092,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1531,skc12)
| ~ event(skc12,X1531)
| ~ present(skc12,X1531)
| ~ think_believe_consider(skc12,X1531)
| ~ forename(skc12,X1530)
| ~ vincent_forename(skc12,X1530)
| ~ of(skc12,X1530,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1531,skc10)
| ~ jules_forename(skc12,X1530)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1089,c383]) ).
cnf(c1101,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1542,skc12)
| ~ event(skc12,X1542)
| ~ present(skc12,X1542)
| ~ think_believe_consider(skc12,X1542)
| ~ forename(skc12,X1543)
| ~ vincent_forename(skc12,X1543)
| ~ of(skc12,X1543,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1542,skc10)
| ~ jules_forename(skc12,X1543)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1092,c361]) ).
cnf(c1106,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1544,skc12)
| ~ event(skc12,X1544)
| ~ present(skc12,X1544)
| ~ think_believe_consider(skc12,X1544)
| ~ forename(skc12,X1545)
| ~ vincent_forename(skc12,X1545)
| ~ of(skc12,X1545,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1544,skc10)
| ~ jules_forename(skc12,X1545)
| ~ smoke(skc12,skf2(skc10))
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1101,c369]) ).
cnf(c1107,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,X1547,skc12)
| ~ event(skc12,X1547)
| ~ present(skc12,X1547)
| ~ think_believe_consider(skc12,X1547)
| ~ forename(skc12,X1546)
| ~ vincent_forename(skc12,X1546)
| ~ of(skc12,X1546,skc10)
| ~ man(skc12,skc10)
| ~ agent(skc12,X1547,skc10)
| ~ jules_forename(skc12,X1546)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1106,c359]) ).
cnf(c1108,plain,
( ~ accessible_world(skc12,skc12)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skf2(skc10),skc12)
| ~ event(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ forename(skc12,X1548)
| ~ vincent_forename(skc12,X1548)
| ~ of(skc12,X1548,skc10)
| ~ man(skc12,skc10)
| ~ jules_forename(skc12,X1548)
| ~ state(skc12,skc9)
| ~ actual_world(skc12)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1107,c383]) ).
cnf(c698,plain,
( ~ accessible_world(skc8,X1265)
| ~ proposition(skc8,X1265)
| ~ theme(skc8,X1268,X1265)
| ~ event(skc8,X1268)
| ~ present(skc8,X1268)
| ~ think_believe_consider(skc8,X1268)
| ~ forename(skc8,X1269)
| ~ vincent_forename(skc8,X1269)
| ~ of(skc8,X1269,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1268,skc10)
| ~ jules_forename(skc8,X1270)
| ~ forename(skc8,X1270)
| ~ smoke(X1272,X1271)
| ~ present(X1272,X1271)
| ~ agent(X1272,X1271,X1264)
| ~ event(X1272,X1271)
| ~ man(skc8,X1264)
| ~ of(skc8,X1270,X1264)
| ~ proposition(skc8,X1272)
| ~ accessible_world(skc8,X1272)
| ~ think_believe_consider(skc8,X1267)
| ~ present(skc8,X1267)
| ~ event(skc8,X1267)
| ~ theme(skc8,X1267,X1272)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1266)
| ~ vincent_forename(skc8,X1266)
| ~ of(skc8,X1266,skc10)
| ~ agent(skc8,X1267,skc10)
| ~ jules_forename(skc8,X1269)
| ~ actual_world(skc8)
| man(X1265,skf4(X1265)) ),
inference(factor,[status(thm)],[c396]) ).
cnf(c1030,plain,
( ~ accessible_world(skc8,X1406)
| ~ proposition(skc8,X1406)
| ~ theme(skc8,X1409,X1406)
| ~ event(skc8,X1409)
| ~ present(skc8,X1409)
| ~ think_believe_consider(skc8,X1409)
| ~ forename(skc8,X1411)
| ~ vincent_forename(skc8,X1411)
| ~ of(skc8,X1411,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1409,skc10)
| ~ jules_forename(skc8,X1404)
| ~ forename(skc8,X1404)
| ~ smoke(X1407,X1408)
| ~ present(X1407,X1408)
| ~ agent(X1407,X1408,X1405)
| ~ event(X1407,X1408)
| ~ man(skc8,X1405)
| ~ of(skc8,X1404,X1405)
| ~ proposition(skc8,X1407)
| ~ accessible_world(skc8,X1407)
| ~ theme(skc8,X1409,X1407)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1410)
| ~ vincent_forename(skc8,X1410)
| ~ of(skc8,X1410,skc10)
| ~ jules_forename(skc8,X1411)
| ~ actual_world(skc8)
| man(X1406,skf4(X1406)) ),
inference(factor,[status(thm)],[c698]) ).
cnf(c1066,plain,
( ~ accessible_world(skc8,X1412)
| ~ proposition(skc8,X1412)
| ~ theme(skc8,X1416,X1412)
| ~ event(skc8,X1416)
| ~ present(skc8,X1416)
| ~ think_believe_consider(skc8,X1416)
| ~ forename(skc8,X1418)
| ~ vincent_forename(skc8,X1418)
| ~ of(skc8,X1418,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1416,skc10)
| ~ jules_forename(skc8,X1413)
| ~ forename(skc8,X1413)
| ~ smoke(X1414,X1417)
| ~ present(X1414,X1417)
| ~ agent(X1414,X1417,X1415)
| ~ event(X1414,X1417)
| ~ man(skc8,X1415)
| ~ of(skc8,X1413,X1415)
| ~ proposition(skc8,X1414)
| ~ accessible_world(skc8,X1414)
| ~ theme(skc8,X1416,X1414)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1418)
| ~ actual_world(skc8)
| man(X1412,skf4(X1412)) ),
inference(factor,[status(thm)],[c1030]) ).
cnf(c1069,plain,
( ~ accessible_world(skc8,X1431)
| ~ proposition(skc8,X1431)
| ~ theme(skc8,X1430,X1431)
| ~ event(skc8,X1430)
| ~ present(skc8,X1430)
| ~ think_believe_consider(skc8,X1430)
| ~ forename(skc8,X1428)
| ~ vincent_forename(skc8,X1428)
| ~ of(skc8,X1428,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1430,skc10)
| ~ jules_forename(skc8,X1429)
| ~ forename(skc8,X1429)
| ~ smoke(X1431,X1432)
| ~ present(X1431,X1432)
| ~ agent(X1431,X1432,X1433)
| ~ event(X1431,X1432)
| ~ man(skc8,X1433)
| ~ of(skc8,X1429,X1433)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1428)
| ~ actual_world(skc8)
| man(X1431,skf4(X1431)) ),
inference(factor,[status(thm)],[c1066]) ).
cnf(c1073,plain,
( ~ accessible_world(skc8,X1442)
| ~ proposition(skc8,X1442)
| ~ theme(skc8,X1443,X1442)
| ~ event(skc8,X1443)
| ~ present(skc8,X1443)
| ~ think_believe_consider(skc8,X1443)
| ~ forename(skc8,X1445)
| ~ vincent_forename(skc8,X1445)
| ~ of(skc8,X1445,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1443,skc10)
| ~ jules_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ smoke(X1442,X1444)
| ~ present(X1442,X1444)
| ~ agent(X1442,X1444,skc15)
| ~ event(X1442,X1444)
| ~ man(skc8,skc15)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1445)
| ~ actual_world(skc8)
| man(X1442,skf4(X1442)) ),
inference(resolution,[status(thm)],[c1069,clause85]) ).
cnf(c1077,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1458,skc8)
| ~ event(skc8,X1458)
| ~ present(skc8,X1458)
| ~ think_believe_consider(skc8,X1458)
| ~ forename(skc8,X1457)
| ~ vincent_forename(skc8,X1457)
| ~ of(skc8,X1457,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1458,skc10)
| ~ jules_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ smoke(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ state(skc8,skc9)
| ~ jules_forename(skc8,X1457)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(resolution,[status(thm)],[c1073,clause86]) ).
cnf(c1028,plain,
( ~ accessible_world(skc8,X1279)
| ~ proposition(skc8,X1279)
| ~ theme(skc8,X1276,X1279)
| ~ event(skc8,X1276)
| ~ present(skc8,X1276)
| ~ think_believe_consider(skc8,X1276)
| ~ forename(skc8,X1275)
| ~ vincent_forename(skc8,X1275)
| ~ of(skc8,X1275,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1276,skc10)
| ~ jules_forename(skc8,X1278)
| ~ forename(skc8,X1278)
| ~ smoke(X1274,X1277)
| ~ present(X1274,X1277)
| ~ agent(X1274,X1277,skc10)
| ~ event(X1274,X1277)
| ~ of(skc8,X1278,skc10)
| ~ proposition(skc8,X1274)
| ~ accessible_world(skc8,X1274)
| ~ theme(skc8,X1276,X1274)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1273)
| ~ vincent_forename(skc8,X1273)
| ~ of(skc8,X1273,skc10)
| ~ actual_world(skc8)
| man(X1279,skf4(X1279)) ),
inference(factor,[status(thm)],[c699]) ).
cnf(c1032,plain,
( ~ accessible_world(skc8,X1284)
| ~ proposition(skc8,X1284)
| ~ theme(skc8,X1282,X1284)
| ~ event(skc8,X1282)
| ~ present(skc8,X1282)
| ~ think_believe_consider(skc8,X1282)
| ~ forename(skc8,X1281)
| ~ vincent_forename(skc8,X1281)
| ~ of(skc8,X1281,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1282,skc10)
| ~ jules_forename(skc8,X1283)
| ~ forename(skc8,X1283)
| ~ smoke(X1280,X1285)
| ~ present(X1280,X1285)
| ~ agent(X1280,X1285,skc10)
| ~ event(X1280,X1285)
| ~ of(skc8,X1283,skc10)
| ~ proposition(skc8,X1280)
| ~ accessible_world(skc8,X1280)
| ~ theme(skc8,X1282,X1280)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1284,skf4(X1284)) ),
inference(factor,[status(thm)],[c1028]) ).
cnf(c1036,plain,
( ~ accessible_world(skc8,X1355)
| ~ proposition(skc8,X1355)
| ~ theme(skc8,skc13,X1355)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1354)
| ~ vincent_forename(skc8,X1354)
| ~ of(skc8,X1354,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,X1356)
| ~ forename(skc8,X1356)
| ~ smoke(skc12,X1357)
| ~ present(skc12,X1357)
| ~ agent(skc12,X1357,skc10)
| ~ event(skc12,X1357)
| ~ of(skc8,X1356,skc10)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1355,skf4(X1355)) ),
inference(resolution,[status(thm)],[c1032,clause87]) ).
cnf(c1055,plain,
( ~ accessible_world(skc8,X1378)
| ~ proposition(skc8,X1378)
| ~ theme(skc8,skc13,X1378)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1379)
| ~ vincent_forename(skc8,X1379)
| ~ of(skc8,X1379,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,X1380)
| ~ present(skc12,X1380)
| ~ agent(skc12,X1380,skc10)
| ~ event(skc12,X1380)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1378,skf4(X1378)) ),
inference(resolution,[status(thm)],[c1036,clause88]) ).
cnf(c1061,plain,
( ~ accessible_world(skc8,X1382)
| ~ proposition(skc8,X1382)
| ~ theme(skc8,skc13,X1382)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1381)
| ~ vincent_forename(skc8,X1381)
| ~ of(skc8,X1381,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1382,skf4(X1382)) ),
inference(resolution,[status(thm)],[c1055,c383]) ).
cnf(c1062,plain,
( ~ accessible_world(skc8,X1384)
| ~ proposition(skc8,X1384)
| ~ theme(skc8,skc13,X1384)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1383)
| ~ vincent_forename(skc8,X1383)
| ~ of(skc8,X1383,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1384,skf4(X1384)) ),
inference(resolution,[status(thm)],[c1061,c361]) ).
cnf(c1063,plain,
( ~ accessible_world(skc8,X1394)
| ~ proposition(skc8,X1394)
| ~ theme(skc8,skc13,X1394)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1395)
| ~ vincent_forename(skc8,X1395)
| ~ of(skc8,X1395,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1394,skf4(X1394)) ),
inference(resolution,[status(thm)],[c1062,c369]) ).
cnf(c1065,plain,
( ~ accessible_world(skc8,X1396)
| ~ proposition(skc8,X1396)
| ~ theme(skc8,skc13,X1396)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1397)
| ~ vincent_forename(skc8,X1397)
| ~ of(skc8,X1397,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1396,skf4(X1396)) ),
inference(resolution,[status(thm)],[c1063,c359]) ).
cnf(c1054,plain,
( ~ accessible_world(skc8,X1359)
| ~ proposition(skc8,X1359)
| ~ theme(skc8,skc13,X1359)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1358)
| ~ vincent_forename(skc8,X1358)
| ~ of(skc8,X1358,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,X1358)
| ~ smoke(skc12,X1360)
| ~ present(skc12,X1360)
| ~ agent(skc12,X1360,skc10)
| ~ event(skc12,X1360)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1359,skf4(X1359)) ),
inference(factor,[status(thm)],[c1036]) ).
cnf(c1056,plain,
( ~ accessible_world(skc8,X1362)
| ~ proposition(skc8,X1362)
| ~ theme(skc8,skc13,X1362)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1361)
| ~ vincent_forename(skc8,X1361)
| ~ of(skc8,X1361,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,X1361)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1362,skf4(X1362)) ),
inference(resolution,[status(thm)],[c1054,c383]) ).
cnf(c1057,plain,
( ~ accessible_world(skc8,X1363)
| ~ proposition(skc8,X1363)
| ~ theme(skc8,skc13,X1363)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1364)
| ~ vincent_forename(skc8,X1364)
| ~ of(skc8,X1364,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,X1364)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1363,skf4(X1363)) ),
inference(resolution,[status(thm)],[c1056,c361]) ).
cnf(c1058,plain,
( ~ accessible_world(skc8,X1374)
| ~ proposition(skc8,X1374)
| ~ theme(skc8,skc13,X1374)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1375)
| ~ vincent_forename(skc8,X1375)
| ~ of(skc8,X1375,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,X1375)
| ~ smoke(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1374,skf4(X1374)) ),
inference(resolution,[status(thm)],[c1057,c369]) ).
cnf(c1060,plain,
( ~ accessible_world(skc8,X1376)
| ~ proposition(skc8,X1376)
| ~ theme(skc8,skc13,X1376)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ forename(skc8,X1377)
| ~ vincent_forename(skc8,X1377)
| ~ of(skc8,X1377,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,skc13,skc10)
| ~ jules_forename(skc8,X1377)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1376,skf4(X1376)) ),
inference(resolution,[status(thm)],[c1058,c359]) ).
cnf(c1035,plain,
( ~ accessible_world(skc8,X1290)
| ~ proposition(skc8,X1290)
| ~ theme(skc8,X1286,X1290)
| ~ event(skc8,X1286)
| ~ present(skc8,X1286)
| ~ think_believe_consider(skc8,X1286)
| ~ forename(skc8,X1289)
| ~ vincent_forename(skc8,X1289)
| ~ of(skc8,X1289,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1286,skc10)
| ~ jules_forename(skc8,X1287)
| ~ forename(skc8,X1287)
| ~ smoke(X1290,X1288)
| ~ present(X1290,X1288)
| ~ agent(X1290,X1288,skc10)
| ~ event(X1290,X1288)
| ~ of(skc8,X1287,skc10)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1290,skf4(X1290)) ),
inference(factor,[status(thm)],[c1032]) ).
cnf(c1038,plain,
( ~ accessible_world(skc8,X1307)
| ~ proposition(skc8,X1307)
| ~ theme(skc8,X1308,X1307)
| ~ event(skc8,X1308)
| ~ present(skc8,X1308)
| ~ think_believe_consider(skc8,X1308)
| ~ forename(skc8,X1309)
| ~ vincent_forename(skc8,X1309)
| ~ of(skc8,X1309,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1308,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(X1307,X1310)
| ~ present(X1307,X1310)
| ~ agent(X1307,X1310,skc10)
| ~ event(X1307,X1310)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1307,skf4(X1307)) ),
inference(resolution,[status(thm)],[c1035,clause88]) ).
cnf(c1044,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1331,skc12)
| ~ event(skc8,X1331)
| ~ present(skc8,X1331)
| ~ think_believe_consider(skc8,X1331)
| ~ forename(skc8,X1332)
| ~ vincent_forename(skc8,X1332)
| ~ of(skc8,X1332,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1331,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1038,c383]) ).
cnf(c1050,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1334,skc12)
| ~ event(skc8,X1334)
| ~ present(skc8,X1334)
| ~ think_believe_consider(skc8,X1334)
| ~ forename(skc8,X1333)
| ~ vincent_forename(skc8,X1333)
| ~ of(skc8,X1333,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1334,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1044,c361]) ).
cnf(c1051,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1335,skc12)
| ~ event(skc8,X1335)
| ~ present(skc8,X1335)
| ~ think_believe_consider(skc8,X1335)
| ~ forename(skc8,X1336)
| ~ vincent_forename(skc8,X1336)
| ~ of(skc8,X1336,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1335,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc12,skf2(skc10))
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1050,c369]) ).
cnf(c1052,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1338,skc12)
| ~ event(skc8,X1338)
| ~ present(skc8,X1338)
| ~ think_believe_consider(skc8,X1338)
| ~ forename(skc8,X1337)
| ~ vincent_forename(skc8,X1337)
| ~ of(skc8,X1337,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1338,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1051,c359]) ).
cnf(c1037,plain,
( ~ accessible_world(skc8,X1291)
| ~ proposition(skc8,X1291)
| ~ theme(skc8,X1292,X1291)
| ~ event(skc8,X1292)
| ~ present(skc8,X1292)
| ~ think_believe_consider(skc8,X1292)
| ~ forename(skc8,X1294)
| ~ vincent_forename(skc8,X1294)
| ~ of(skc8,X1294,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1292,skc10)
| ~ jules_forename(skc8,X1294)
| ~ smoke(X1291,X1293)
| ~ present(X1291,X1293)
| ~ agent(X1291,X1293,skc10)
| ~ event(X1291,X1293)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(X1291,skf4(X1291)) ),
inference(factor,[status(thm)],[c1035]) ).
cnf(c1040,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1314,skc12)
| ~ event(skc8,X1314)
| ~ present(skc8,X1314)
| ~ think_believe_consider(skc8,X1314)
| ~ forename(skc8,X1313)
| ~ vincent_forename(skc8,X1313)
| ~ of(skc8,X1313,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1314,skc10)
| ~ jules_forename(skc8,X1313)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1037,c383]) ).
cnf(c1045,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1316,skc12)
| ~ event(skc8,X1316)
| ~ present(skc8,X1316)
| ~ think_believe_consider(skc8,X1316)
| ~ forename(skc8,X1315)
| ~ vincent_forename(skc8,X1315)
| ~ of(skc8,X1315,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1316,skc10)
| ~ jules_forename(skc8,X1315)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1040,c361]) ).
cnf(c1046,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1318,skc12)
| ~ event(skc8,X1318)
| ~ present(skc8,X1318)
| ~ think_believe_consider(skc8,X1318)
| ~ forename(skc8,X1317)
| ~ vincent_forename(skc8,X1317)
| ~ of(skc8,X1317,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1318,skc10)
| ~ jules_forename(skc8,X1317)
| ~ smoke(skc12,skf2(skc10))
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1045,c369]) ).
cnf(c1047,plain,
( ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X1329,skc12)
| ~ event(skc8,X1329)
| ~ present(skc8,X1329)
| ~ think_believe_consider(skc8,X1329)
| ~ forename(skc8,X1330)
| ~ vincent_forename(skc8,X1330)
| ~ of(skc8,X1330,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1329,skc10)
| ~ jules_forename(skc8,X1330)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1046,c359]) ).
cnf(c1043,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1311,skc8)
| ~ event(skc8,X1311)
| ~ present(skc8,X1311)
| ~ think_believe_consider(skc8,X1311)
| ~ forename(skc8,X1312)
| ~ vincent_forename(skc8,X1312)
| ~ of(skc8,X1312,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1311,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ smoke(skc8,X1311)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1038]) ).
cnf(c700,plain,
( ~ accessible_world(skc8,X1298)
| ~ proposition(skc8,X1298)
| ~ theme(skc8,X1300,X1298)
| ~ event(skc8,X1300)
| ~ present(skc8,X1300)
| ~ think_believe_consider(skc8,X1300)
| ~ forename(skc8,X1304)
| ~ vincent_forename(skc8,X1304)
| ~ of(skc8,X1304,X1302)
| ~ man(skc8,X1302)
| ~ agent(skc8,X1300,X1302)
| ~ jules_forename(skc8,X1303)
| ~ forename(skc8,X1303)
| ~ smoke(X1306,X1305)
| ~ present(X1306,X1305)
| ~ agent(X1306,X1305,X1297)
| ~ event(X1306,X1305)
| ~ man(skc8,X1297)
| ~ of(skc8,X1303,X1297)
| ~ proposition(skc8,X1306)
| ~ accessible_world(skc8,X1306)
| ~ think_believe_consider(skc8,X1299)
| ~ present(skc8,X1299)
| ~ event(skc8,X1299)
| ~ theme(skc8,X1299,X1306)
| ~ state(skc8,skc9)
| ~ forename(skc8,X1301)
| ~ vincent_forename(skc8,X1301)
| ~ of(skc8,X1301,skc10)
| ~ agent(skc8,X1299,skc10)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,X1301)
| ~ actual_world(skc8)
| man(X1298,skf4(X1298)) ),
inference(factor,[status(thm)],[c396]) ).
cnf(c1039,plain,
( ~ accessible_world(skc8,skc8)
| ~ proposition(skc8,skc8)
| ~ theme(skc8,X1295,skc8)
| ~ event(skc8,X1295)
| ~ present(skc8,X1295)
| ~ think_believe_consider(skc8,X1295)
| ~ forename(skc8,X1296)
| ~ vincent_forename(skc8,X1296)
| ~ of(skc8,X1296,skc10)
| ~ man(skc8,skc10)
| ~ agent(skc8,X1295,skc10)
| ~ jules_forename(skc8,X1296)
| ~ smoke(skc8,X1295)
| ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc8,skf4(skc8)) ),
inference(factor,[status(thm)],[c1037]) ).
cnf(clause73,negated_conjecture,
man(skc8,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
cnf(c235,plain,
( ~ accessible_world(skc8,X287)
| man(X287,skc15) ),
inference(resolution,[status(thm)],[clause52,clause73]) ).
cnf(c379,plain,
man(skc12,skc15),
inference(resolution,[status(thm)],[c235,clause83]) ).
cnf(c384,plain,
agent(skc12,skf2(skc15),skc15),
inference(resolution,[status(thm)],[clause93,c379]) ).
cnf(clause71,axiom,
( ~ proposition(X265,X268)
| ~ proposition(X265,X269)
| ~ theme(X265,X266,X268)
| ~ think_believe_consider(X265,X266)
| ~ think_believe_consider(X265,X264)
| ~ theme(X265,X264,X269)
| ~ agent(X265,X264,X267)
| ~ agent(X265,X266,X267)
| X268 = X269 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
cnf(clause66,axiom,
( ~ accessible_world(X234,X233)
| ~ agent(X234,X236,X235)
| agent(X233,X236,X235) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
cnf(c316,plain,
( ~ accessible_world(skc8,X497)
| agent(X497,skc13,skc15) ),
inference(resolution,[status(thm)],[clause66,clause86]) ).
cnf(c568,plain,
agent(skc12,skc13,skc15),
inference(resolution,[status(thm)],[c316,clause83]) ).
cnf(c570,plain,
( ~ proposition(skc12,X1008)
| ~ proposition(skc12,X1010)
| ~ theme(skc12,skc13,X1008)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,X1009)
| ~ theme(skc12,X1009,X1010)
| ~ agent(skc12,X1009,skc15)
| X1008 = X1010 ),
inference(resolution,[status(thm)],[c568,clause71]) ).
cnf(c898,plain,
( ~ proposition(skc12,X1253)
| ~ proposition(skc12,X1254)
| ~ theme(skc12,skc13,X1253)
| ~ think_believe_consider(skc12,skc13)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1254)
| X1253 = X1254 ),
inference(resolution,[status(thm)],[c570,c384]) ).
cnf(c349,plain,
( ~ proposition(X659,X658)
| ~ proposition(X659,X661)
| ~ theme(X659,X660,X658)
| ~ think_believe_consider(X659,X660)
| ~ theme(X659,X660,X661)
| ~ agent(X659,X660,X662)
| X658 = X661 ),
inference(factor,[status(thm)],[clause71]) ).
cnf(c689,plain,
( ~ proposition(skc8,X1243)
| ~ proposition(skc8,X1242)
| ~ theme(skc8,skc13,X1243)
| ~ think_believe_consider(skc8,skc13)
| ~ theme(skc8,skc13,X1242)
| X1243 = X1242 ),
inference(resolution,[status(thm)],[c349,clause86]) ).
cnf(c1025,plain,
( ~ proposition(skc8,X1246)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,skc13,X1246)
| ~ think_believe_consider(skc8,skc13)
| X1246 = skc12 ),
inference(resolution,[status(thm)],[c689,clause87]) ).
cnf(c688,plain,
( ~ proposition(skc12,X1233)
| ~ proposition(skc12,X1232)
| ~ theme(skc12,skc13,X1233)
| ~ think_believe_consider(skc12,skc13)
| ~ theme(skc12,skc13,X1232)
| X1233 = X1232 ),
inference(resolution,[status(thm)],[c349,c568]) ).
cnf(c1022,plain,
( ~ proposition(skc12,X1245)
| ~ proposition(skc12,skc12)
| ~ theme(skc12,skc13,X1245)
| ~ think_believe_consider(skc12,skc13)
| X1245 = skc12 ),
inference(resolution,[status(thm)],[c688,c571]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c30,axiom,
( X571 != X575
| X572 != X574
| X570 != X568
| X573 != X569
| ~ be(X571,X572,X570,X573)
| be(X575,X574,X568,X569) ),
theory(equality) ).
cnf(c633,plain,
( skc12 != X1132
| skc9 != X1130
| skc10 != X1131
| skc10 != X1129
| be(X1132,X1130,X1131,X1129) ),
inference(resolution,[status(thm)],[c30,c587]) ).
cnf(c970,plain,
( skc12 != X1234
| skc9 != X1235
| skc10 != X1236
| be(X1234,X1235,X1236,skc10) ),
inference(resolution,[status(thm)],[c633,reflexivity]) ).
cnf(c632,plain,
( skc8 != X1124
| skc9 != X1122
| skc10 != X1123
| skc10 != X1121
| be(X1124,X1122,X1123,X1121) ),
inference(resolution,[status(thm)],[c30,clause89]) ).
cnf(c965,plain,
( skc8 != X1229
| skc9 != X1227
| skc10 != X1228
| be(X1229,X1227,X1228,skc10) ),
inference(resolution,[status(thm)],[c632,reflexivity]) ).
cnf(c969,plain,
( skc12 != X1219
| skc9 != X1220
| skc10 != X1221
| be(X1219,X1220,X1221,X1221) ),
inference(factor,[status(thm)],[c633]) ).
cnf(c1016,plain,
( skc12 != X1225
| skc9 != X1224
| be(X1225,X1224,skc10,skc10) ),
inference(resolution,[status(thm)],[c969,reflexivity]) ).
cnf(c1018,plain,
( skc12 != X1226
| be(X1226,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1016,reflexivity]) ).
cnf(c687,plain,
( ~ proposition(skc12,X1223)
| ~ proposition(skc12,X1222)
| ~ theme(skc12,skf2(skc15),X1223)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ theme(skc12,skf2(skc15),X1222)
| X1223 = X1222 ),
inference(resolution,[status(thm)],[c349,c384]) ).
cnf(c964,plain,
( skc8 != X1214
| skc9 != X1213
| skc10 != X1215
| be(X1214,X1213,X1215,X1215) ),
inference(factor,[status(thm)],[c632]) ).
cnf(c1013,plain,
( skc8 != X1216
| skc9 != X1217
| be(X1216,X1217,skc10,skc10) ),
inference(resolution,[status(thm)],[c964,reflexivity]) ).
cnf(c1014,plain,
( skc8 != X1218
| be(X1218,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c1013,reflexivity]) ).
cnf(c686,plain,
( ~ proposition(skc12,X1212)
| ~ proposition(skc12,X1211)
| ~ theme(skc12,skf2(skc10),X1212)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ theme(skc12,skf2(skc10),X1211)
| X1212 = X1211 ),
inference(resolution,[status(thm)],[c349,c383]) ).
cnf(c36,axiom,
( X630 != X633
| X631 != X632
| X629 != X628
| ~ of(X630,X631,X629)
| of(X633,X632,X628) ),
theory(equality) ).
cnf(c669,plain,
( skc8 != X1205
| skc11 != X1204
| skc10 != X1206
| of(X1205,X1204,X1206) ),
inference(resolution,[status(thm)],[c36,clause88]) ).
cnf(c1008,plain,
( skc8 != X1209
| skc11 != X1208
| of(X1209,X1208,skc10) ),
inference(resolution,[status(thm)],[c669,reflexivity]) ).
cnf(c1010,plain,
( skc8 != X1210
| of(X1210,skc11,skc10) ),
inference(resolution,[status(thm)],[c1008,reflexivity]) ).
cnf(c668,plain,
( skc12 != X1200
| skc14 != X1199
| skc15 != X1201
| of(X1200,X1199,X1201) ),
inference(resolution,[status(thm)],[c36,c577]) ).
cnf(c1006,plain,
( skc12 != X1202
| skc14 != X1203
| of(X1202,X1203,skc15) ),
inference(resolution,[status(thm)],[c668,reflexivity]) ).
cnf(c1007,plain,
( skc12 != X1207
| of(X1207,skc14,skc15) ),
inference(resolution,[status(thm)],[c1006,reflexivity]) ).
cnf(c667,plain,
( skc8 != X1194
| skc14 != X1193
| skc15 != X1195
| of(X1194,X1193,X1195) ),
inference(resolution,[status(thm)],[c36,clause85]) ).
cnf(c1003,plain,
( skc8 != X1197
| skc14 != X1196
| of(X1197,X1196,skc15) ),
inference(resolution,[status(thm)],[c667,reflexivity]) ).
cnf(c1004,plain,
( skc8 != X1198
| of(X1198,skc14,skc15) ),
inference(resolution,[status(thm)],[c1003,reflexivity]) ).
cnf(c666,plain,
( skc12 != X1187
| skc11 != X1186
| skc10 != X1188
| of(X1187,X1186,X1188) ),
inference(resolution,[status(thm)],[c36,c580]) ).
cnf(c999,plain,
( skc12 != X1191
| skc11 != X1190
| of(X1191,X1190,skc10) ),
inference(resolution,[status(thm)],[c666,reflexivity]) ).
cnf(c1001,plain,
( skc12 != X1192
| of(X1192,skc11,skc10) ),
inference(resolution,[status(thm)],[c999,reflexivity]) ).
cnf(c35,axiom,
( X620 != X623
| X621 != X622
| X619 != X618
| ~ theme(X620,X621,X619)
| theme(X623,X622,X618) ),
theory(equality) ).
cnf(c662,plain,
( skc12 != X1180
| skc13 != X1179
| skc12 != X1178
| theme(X1180,X1179,X1178) ),
inference(resolution,[status(thm)],[c35,c571]) ).
cnf(c995,plain,
( skc12 != X1184
| skc13 != X1185
| theme(X1184,X1185,skc12) ),
inference(resolution,[status(thm)],[c662,reflexivity]) ).
cnf(c998,plain,
( skc12 != X1189
| theme(X1189,skc13,skc12) ),
inference(resolution,[status(thm)],[c995,reflexivity]) ).
cnf(c994,plain,
( skc12 != X1181
| skc13 != X1182
| theme(X1181,X1182,X1181) ),
inference(factor,[status(thm)],[c662]) ).
cnf(c996,plain,
( skc12 != X1183
| theme(X1183,skc13,X1183) ),
inference(resolution,[status(thm)],[c994,reflexivity]) ).
cnf(c661,plain,
( skc8 != X1171
| skc13 != X1170
| skc12 != X1169
| theme(X1171,X1170,X1169) ),
inference(resolution,[status(thm)],[c35,clause87]) ).
cnf(c989,plain,
( skc8 != X1175
| skc13 != X1176
| theme(X1175,X1176,skc12) ),
inference(resolution,[status(thm)],[c661,reflexivity]) ).
cnf(c992,plain,
( skc8 != X1177
| theme(X1177,skc13,skc12) ),
inference(resolution,[status(thm)],[c989,reflexivity]) ).
cnf(c34,axiom,
( X609 != X612
| X610 != X611
| X608 != X607
| ~ agent(X609,X610,X608)
| agent(X612,X611,X607) ),
theory(equality) ).
cnf(c657,plain,
( skc8 != X1167
| skc13 != X1166
| skc15 != X1168
| agent(X1167,X1166,X1168) ),
inference(resolution,[status(thm)],[c34,clause86]) ).
cnf(c988,plain,
( skc8 != X1173
| skc13 != X1172
| agent(X1173,X1172,skc15) ),
inference(resolution,[status(thm)],[c657,reflexivity]) ).
cnf(c990,plain,
( skc8 != X1174
| agent(X1174,skc13,skc15) ),
inference(resolution,[status(thm)],[c988,reflexivity]) ).
cnf(c656,plain,
( skc12 != X1161
| skc13 != X1160
| skc15 != X1162
| agent(X1161,X1160,X1162) ),
inference(resolution,[status(thm)],[c34,c568]) ).
cnf(c985,plain,
( skc12 != X1164
| skc13 != X1163
| agent(X1164,X1163,skc15) ),
inference(resolution,[status(thm)],[c656,reflexivity]) ).
cnf(c986,plain,
( skc12 != X1165
| agent(X1165,skc13,skc15) ),
inference(resolution,[status(thm)],[c985,reflexivity]) ).
cnf(c655,plain,
( skc12 != X1152
| skf2(skc15) != X1151
| skc15 != X1153
| agent(X1152,X1151,X1153) ),
inference(resolution,[status(thm)],[c34,c384]) ).
cnf(c980,plain,
( skc12 != X1157
| skc15 != X1158
| agent(X1157,skf2(skc15),X1158) ),
inference(resolution,[status(thm)],[c655,reflexivity]) ).
cnf(c983,plain,
( skc12 != X1159
| agent(X1159,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c980,reflexivity]) ).
cnf(c654,plain,
( skc12 != X1149
| skf2(skc10) != X1148
| skc10 != X1150
| agent(X1149,X1148,X1150) ),
inference(resolution,[status(thm)],[c34,c383]) ).
cnf(c979,plain,
( skc12 != X1155
| skc10 != X1154
| agent(X1155,skf2(skc10),X1154) ),
inference(resolution,[status(thm)],[c654,reflexivity]) ).
cnf(c981,plain,
( skc12 != X1156
| agent(X1156,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c979,reflexivity]) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
cnf(c33,axiom,
( X600 != X599
| X598 != X597
| ~ think_believe_consider(X600,X598)
| think_believe_consider(X599,X597) ),
theory(equality) ).
cnf(c649,plain,
( skc8 != X1145
| skc13 != X1146
| think_believe_consider(X1145,X1146) ),
inference(resolution,[status(thm)],[c33,clause78]) ).
cnf(c977,plain,
( skc8 != X1147
| think_believe_consider(X1147,skc13) ),
inference(resolution,[status(thm)],[c649,reflexivity]) ).
cnf(c32,axiom,
( X592 != X591
| X590 != X589
| ~ present(X592,X590)
| present(X591,X589) ),
theory(equality) ).
cnf(c644,plain,
( skc12 != X1139
| skf2(X1141) != X1140
| present(X1139,X1140) ),
inference(resolution,[status(thm)],[c32,c369]) ).
cnf(c975,plain,
( skc12 != X1143
| present(X1143,skf2(X1142)) ),
inference(resolution,[status(thm)],[c644,reflexivity]) ).
cnf(clause45,axiom,
( ~ accessible_world(X121,X120)
| ~ think_believe_consider(X121,X122)
| think_believe_consider(X120,X122) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(c198,plain,
( ~ accessible_world(skc8,X201)
| think_believe_consider(X201,skc13) ),
inference(resolution,[status(thm)],[clause45,clause78]) ).
cnf(c263,plain,
think_believe_consider(skc12,skc13),
inference(resolution,[status(thm)],[c198,clause83]) ).
cnf(c648,plain,
( skc12 != X1136
| skc13 != X1137
| think_believe_consider(X1136,X1137) ),
inference(resolution,[status(thm)],[c33,c263]) ).
cnf(c973,plain,
( skc12 != X1138
| think_believe_consider(X1138,skc13) ),
inference(resolution,[status(thm)],[c648,reflexivity]) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
cnf(c643,plain,
( skc8 != X1133
| skc13 != X1134
| present(X1133,X1134) ),
inference(resolution,[status(thm)],[c32,clause77]) ).
cnf(c971,plain,
( skc8 != X1135
| present(X1135,skc13) ),
inference(resolution,[status(thm)],[c643,reflexivity]) ).
cnf(clause44,axiom,
( ~ accessible_world(X116,X115)
| ~ present(X116,X117)
| present(X115,X117) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c190,plain,
( ~ accessible_world(skc8,X194)
| present(X194,skc13) ),
inference(resolution,[status(thm)],[clause44,clause77]) ).
cnf(c259,plain,
present(skc12,skc13),
inference(resolution,[status(thm)],[c190,clause83]) ).
cnf(c642,plain,
( skc12 != X1126
| skc13 != X1127
| present(X1126,X1127) ),
inference(resolution,[status(thm)],[c32,c259]) ).
cnf(c967,plain,
( skc12 != X1128
| present(X1128,skc13) ),
inference(resolution,[status(thm)],[c642,reflexivity]) ).
cnf(c31,axiom,
( X583 != X582
| X581 != X580
| ~ accessible_world(X583,X581)
| accessible_world(X582,X580) ),
theory(equality) ).
cnf(c638,plain,
( skc8 != X1120
| skc12 != X1119
| accessible_world(X1120,X1119) ),
inference(resolution,[status(thm)],[c31,clause83]) ).
cnf(c963,plain,
( skc8 != X1125
| accessible_world(X1125,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(X229,X228)
| ~ jules_forename(X229,X230)
| jules_forename(X228,X230) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
cnf(c313,plain,
( ~ accessible_world(skc8,X419)
| jules_forename(X419,skc11) ),
inference(resolution,[status(thm)],[clause65,clause79]) ).
cnf(c529,plain,
jules_forename(skc12,skc11),
inference(resolution,[status(thm)],[c313,clause83]) ).
cnf(c29,axiom,
( X561 != X560
| X559 != X558
| ~ jules_forename(X561,X559)
| jules_forename(X560,X558) ),
theory(equality) ).
cnf(c627,plain,
( skc12 != X1116
| skc11 != X1115
| jules_forename(X1116,X1115) ),
inference(resolution,[status(thm)],[c29,c529]) ).
cnf(c960,plain,
( skc12 != X1118
| jules_forename(X1118,skc11) ),
inference(resolution,[status(thm)],[c627,reflexivity]) ).
cnf(c626,plain,
( skc8 != X1114
| skc11 != X1113
| jules_forename(X1114,X1113) ),
inference(resolution,[status(thm)],[c29,clause79]) ).
cnf(c959,plain,
( skc8 != X1117
| jules_forename(X1117,skc11) ),
inference(resolution,[status(thm)],[c626,reflexivity]) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
cnf(c28,axiom,
( X553 != X552
| X551 != X550
| ~ vincent_forename(X553,X551)
| vincent_forename(X552,X550) ),
theory(equality) ).
cnf(c622,plain,
( skc8 != X1109
| skc14 != X1110
| vincent_forename(X1109,X1110) ),
inference(resolution,[status(thm)],[c28,clause75]) ).
cnf(c956,plain,
( skc8 != X1112
| vincent_forename(X1112,skc14) ),
inference(resolution,[status(thm)],[c622,reflexivity]) ).
cnf(clause64,axiom,
( ~ accessible_world(X225,X224)
| ~ vincent_forename(X225,X226)
| vincent_forename(X224,X226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
cnf(c308,plain,
( ~ accessible_world(skc8,X412)
| vincent_forename(X412,skc14) ),
inference(resolution,[status(thm)],[clause64,clause75]) ).
cnf(c520,plain,
vincent_forename(skc12,skc14),
inference(resolution,[status(thm)],[c308,clause83]) ).
cnf(c621,plain,
( skc12 != X1107
| skc14 != X1108
| vincent_forename(X1107,X1108) ),
inference(resolution,[status(thm)],[c28,c520]) ).
cnf(c955,plain,
( skc12 != X1111
| vincent_forename(X1111,skc14) ),
inference(resolution,[status(thm)],[c621,reflexivity]) ).
cnf(clause74,negated_conjecture,
forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
cnf(clause27,axiom,
( ~ forename(X56,X55)
| relname(X56,X55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c83,plain,
relname(skc8,skc14),
inference(resolution,[status(thm)],[clause27,clause74]) ).
cnf(c27,axiom,
( X544 != X543
| X542 != X541
| ~ relname(X544,X542)
| relname(X543,X541) ),
theory(equality) ).
cnf(c617,plain,
( skc8 != X1104
| skc14 != X1103
| relname(X1104,X1103) ),
inference(resolution,[status(thm)],[c27,c83]) ).
cnf(c952,plain,
( skc8 != X1106
| relname(X1106,skc14) ),
inference(resolution,[status(thm)],[c617,reflexivity]) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
cnf(clause62,axiom,
( ~ accessible_world(X217,X216)
| ~ forename(X217,X218)
| forename(X216,X218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
cnf(c293,plain,
( ~ accessible_world(skc8,X393)
| forename(X393,skc11) ),
inference(resolution,[status(thm)],[clause62,clause80]) ).
cnf(c499,plain,
forename(skc12,skc11),
inference(resolution,[status(thm)],[c293,clause83]) ).
cnf(c501,plain,
relname(skc12,skc11),
inference(resolution,[status(thm)],[c499,clause27]) ).
cnf(c616,plain,
( skc12 != X1102
| skc11 != X1101
| relname(X1102,X1101) ),
inference(resolution,[status(thm)],[c27,c501]) ).
cnf(c951,plain,
( skc12 != X1105
| relname(X1105,skc11) ),
inference(resolution,[status(thm)],[c616,reflexivity]) ).
cnf(c292,plain,
( ~ accessible_world(skc8,X388)
| forename(X388,skc14) ),
inference(resolution,[status(thm)],[clause62,clause74]) ).
cnf(c483,plain,
forename(skc12,skc14),
inference(resolution,[status(thm)],[c292,clause83]) ).
cnf(c496,plain,
relname(skc12,skc14),
inference(resolution,[status(thm)],[c483,clause27]) ).
cnf(c615,plain,
( skc12 != X1098
| skc14 != X1097
| relname(X1098,X1097) ),
inference(resolution,[status(thm)],[c27,c496]) ).
cnf(c948,plain,
( skc12 != X1100
| relname(X1100,skc14) ),
inference(resolution,[status(thm)],[c615,reflexivity]) ).
cnf(c84,plain,
relname(skc8,skc11),
inference(resolution,[status(thm)],[clause27,clause80]) ).
cnf(c614,plain,
( skc8 != X1096
| skc11 != X1095
| relname(X1096,X1095) ),
inference(resolution,[status(thm)],[c27,c84]) ).
cnf(c947,plain,
( skc8 != X1099
| relname(X1099,skc11) ),
inference(resolution,[status(thm)],[c614,reflexivity]) ).
cnf(c26,axiom,
( X534 != X533
| X532 != X531
| ~ forename(X534,X532)
| forename(X533,X531) ),
theory(equality) ).
cnf(c609,plain,
( skc8 != X1091
| skc11 != X1092
| forename(X1091,X1092) ),
inference(resolution,[status(thm)],[c26,clause80]) ).
cnf(c944,plain,
( skc8 != X1094
| forename(X1094,skc11) ),
inference(resolution,[status(thm)],[c609,reflexivity]) ).
cnf(c608,plain,
( skc8 != X1089
| skc14 != X1090
| forename(X1089,X1090) ),
inference(resolution,[status(thm)],[c26,clause74]) ).
cnf(c943,plain,
( skc8 != X1093
| forename(X1093,skc14) ),
inference(resolution,[status(thm)],[c608,reflexivity]) ).
cnf(c607,plain,
( skc12 != X1085
| skc11 != X1086
| forename(X1085,X1086) ),
inference(resolution,[status(thm)],[c26,c499]) ).
cnf(c940,plain,
( skc12 != X1088
| forename(X1088,skc11) ),
inference(resolution,[status(thm)],[c607,reflexivity]) ).
cnf(c606,plain,
( skc12 != X1083
| skc14 != X1084
| forename(X1083,X1084) ),
inference(resolution,[status(thm)],[c26,c483]) ).
cnf(c939,plain,
( skc12 != X1087
| forename(X1087,skc14) ),
inference(resolution,[status(thm)],[c606,reflexivity]) ).
cnf(clause26,axiom,
( ~ man(X54,X53)
| male(X54,X53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c82,plain,
male(skc8,skc15),
inference(resolution,[status(thm)],[clause26,clause73]) ).
cnf(c25,axiom,
( X526 != X525
| X524 != X523
| ~ male(X526,X524)
| male(X525,X523) ),
theory(equality) ).
cnf(c602,plain,
( skc8 != X1080
| skc15 != X1079
| male(X1080,X1079) ),
inference(resolution,[status(thm)],[c25,c82]) ).
cnf(c936,plain,
( skc8 != X1082
| male(X1082,skc15) ),
inference(resolution,[status(thm)],[c602,reflexivity]) ).
cnf(c81,plain,
male(skc8,skc10),
inference(resolution,[status(thm)],[clause26,clause81]) ).
cnf(c601,plain,
( skc8 != X1078
| skc10 != X1077
| male(X1078,X1077) ),
inference(resolution,[status(thm)],[c25,c81]) ).
cnf(c935,plain,
( skc8 != X1081
| male(X1081,skc10) ),
inference(resolution,[status(thm)],[c601,reflexivity]) ).
cnf(c333,plain,
male(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause26]) ).
cnf(c600,plain,
( skc12 != X1074
| skc10 != X1073
| male(X1074,X1073) ),
inference(resolution,[status(thm)],[c25,c333]) ).
cnf(c932,plain,
( skc12 != X1076
| male(X1076,skc10) ),
inference(resolution,[status(thm)],[c600,reflexivity]) ).
cnf(c381,plain,
male(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause26]) ).
cnf(c599,plain,
( skc12 != X1072
| skc15 != X1071
| male(X1072,X1071) ),
inference(resolution,[status(thm)],[c25,c381]) ).
cnf(c931,plain,
( skc12 != X1075
| male(X1075,skc15) ),
inference(resolution,[status(thm)],[c599,reflexivity]) ).
cnf(clause25,axiom,
( ~ human_person(X52,X51)
| animate(X52,X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(clause16,axiom,
( ~ man(X34,X33)
| human_person(X34,X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c380,plain,
human_person(skc12,skc15),
inference(resolution,[status(thm)],[c379,clause16]) ).
cnf(c387,plain,
animate(skc12,skc15),
inference(resolution,[status(thm)],[c380,clause25]) ).
cnf(c24,axiom,
( X517 != X516
| X515 != X514
| ~ animate(X517,X515)
| animate(X516,X514) ),
theory(equality) ).
cnf(c595,plain,
( skc12 != X1068
| skc15 != X1067
| animate(X1068,X1067) ),
inference(resolution,[status(thm)],[c24,c387]) ).
cnf(c928,plain,
( skc12 != X1070
| animate(X1070,skc15) ),
inference(resolution,[status(thm)],[c595,reflexivity]) ).
cnf(c59,plain,
human_person(skc8,skc10),
inference(resolution,[status(thm)],[clause16,clause81]) ).
cnf(c80,plain,
animate(skc8,skc10),
inference(resolution,[status(thm)],[clause25,c59]) ).
cnf(c594,plain,
( skc8 != X1066
| skc10 != X1065
| animate(X1066,X1065) ),
inference(resolution,[status(thm)],[c24,c80]) ).
cnf(c927,plain,
( skc8 != X1069
| animate(X1069,skc10) ),
inference(resolution,[status(thm)],[c594,reflexivity]) ).
cnf(c60,plain,
human_person(skc8,skc15),
inference(resolution,[status(thm)],[clause16,clause73]) ).
cnf(c79,plain,
animate(skc8,skc15),
inference(resolution,[status(thm)],[clause25,c60]) ).
cnf(c593,plain,
( skc8 != X1063
| skc15 != X1062
| animate(X1063,X1062) ),
inference(resolution,[status(thm)],[c24,c79]) ).
cnf(c925,plain,
( skc8 != X1064
| animate(X1064,skc15) ),
inference(resolution,[status(thm)],[c593,reflexivity]) ).
cnf(c332,plain,
human_person(skc12,skc10),
inference(resolution,[status(thm)],[c331,clause16]) ).
cnf(c340,plain,
animate(skc12,skc10),
inference(resolution,[status(thm)],[c332,clause25]) ).
cnf(c592,plain,
( skc12 != X1049
| skc10 != X1048
| animate(X1049,X1048) ),
inference(resolution,[status(thm)],[c24,c340]) ).
cnf(c919,plain,
( skc12 != X1050
| animate(X1050,skc10) ),
inference(resolution,[status(thm)],[c592,reflexivity]) ).
cnf(c591,plain,
( ~ accessible_world(skc12,X1047)
| be(X1047,skc9,skc10,skc10) ),
inference(resolution,[status(thm)],[c587,clause69]) ).
cnf(clause24,axiom,
( ~ human_person(X50,X49)
| human(X50,X49) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c386,plain,
human(skc12,skc15),
inference(resolution,[status(thm)],[c380,clause24]) ).
cnf(c23,axiom,
( X509 != X508
| X507 != X506
| ~ human(X509,X507)
| human(X508,X506) ),
theory(equality) ).
cnf(c586,plain,
( skc12 != X1033
| skc15 != X1032
| human(X1033,X1032) ),
inference(resolution,[status(thm)],[c23,c386]) ).
cnf(c915,plain,
( skc12 != X1046
| human(X1046,skc15) ),
inference(resolution,[status(thm)],[c586,reflexivity]) ).
cnf(c78,plain,
human(skc8,skc10),
inference(resolution,[status(thm)],[clause24,c59]) ).
cnf(c585,plain,
( skc8 != X1030
| skc10 != X1029
| human(X1030,X1029) ),
inference(resolution,[status(thm)],[c23,c78]) ).
cnf(c913,plain,
( skc8 != X1031
| human(X1031,skc10) ),
inference(resolution,[status(thm)],[c585,reflexivity]) ).
cnf(clause70,axiom,
( ~ forename(X261,X260)
| ~ of(X261,X263,X262)
| ~ forename(X261,X263)
| ~ of(X261,X260,X262)
| ~ entity(X261,X262)
| X263 = X260 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
cnf(c581,plain,
( ~ forename(skc12,skc11)
| ~ of(skc12,X1028,skc10)
| ~ forename(skc12,X1028)
| ~ entity(skc12,skc10)
| X1028 = skc11 ),
inference(resolution,[status(thm)],[c580,clause70]) ).
cnf(c339,plain,
human(skc12,skc10),
inference(resolution,[status(thm)],[c332,clause24]) ).
cnf(c584,plain,
( skc12 != X1026
| skc10 != X1025
| human(X1026,X1025) ),
inference(resolution,[status(thm)],[c23,c339]) ).
cnf(c910,plain,
( skc12 != X1027
| human(X1027,skc10) ),
inference(resolution,[status(thm)],[c584,reflexivity]) ).
cnf(c77,plain,
human(skc8,skc15),
inference(resolution,[status(thm)],[clause24,c60]) ).
cnf(c583,plain,
( skc8 != X1023
| skc15 != X1022
| human(X1023,X1022) ),
inference(resolution,[status(thm)],[c23,c77]) ).
cnf(c908,plain,
( skc8 != X1024
| human(X1024,skc15) ),
inference(resolution,[status(thm)],[c583,reflexivity]) ).
cnf(c578,plain,
( ~ forename(skc12,skc14)
| ~ of(skc12,X1021,skc15)
| ~ forename(skc12,X1021)
| ~ entity(skc12,skc15)
| X1021 = skc14 ),
inference(resolution,[status(thm)],[c577,clause70]) ).
cnf(clause17,axiom,
( ~ human_person(X36,X35)
| organism(X36,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c62,plain,
organism(skc8,skc10),
inference(resolution,[status(thm)],[clause17,c59]) ).
cnf(clause23,axiom,
( ~ organism(X48,X47)
| living(X48,X47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(c75,plain,
living(skc8,skc10),
inference(resolution,[status(thm)],[clause23,c62]) ).
cnf(c22,axiom,
( X502 != X501
| X500 != X499
| ~ living(X502,X500)
| living(X501,X499) ),
theory(equality) ).
cnf(c576,plain,
( skc8 != X1018
| skc10 != X1019
| living(X1018,X1019) ),
inference(resolution,[status(thm)],[c22,c75]) ).
cnf(c905,plain,
( skc8 != X1020
| living(X1020,skc10) ),
inference(resolution,[status(thm)],[c576,reflexivity]) ).
cnf(c388,plain,
organism(skc12,skc15),
inference(resolution,[status(thm)],[c380,clause17]) ).
cnf(c395,plain,
living(skc12,skc15),
inference(resolution,[status(thm)],[c388,clause23]) ).
cnf(c575,plain,
( skc12 != X1015
| skc15 != X1016
| living(X1015,X1016) ),
inference(resolution,[status(thm)],[c22,c395]) ).
cnf(c903,plain,
( skc12 != X1017
| living(X1017,skc15) ),
inference(resolution,[status(thm)],[c575,reflexivity]) ).
cnf(c341,plain,
organism(skc12,skc10),
inference(resolution,[status(thm)],[c332,clause17]) ).
cnf(c348,plain,
living(skc12,skc10),
inference(resolution,[status(thm)],[c341,clause23]) ).
cnf(c574,plain,
( skc12 != X1012
| skc10 != X1013
| living(X1012,X1013) ),
inference(resolution,[status(thm)],[c22,c348]) ).
cnf(c901,plain,
( skc12 != X1014
| living(X1014,skc10) ),
inference(resolution,[status(thm)],[c574,reflexivity]) ).
cnf(c61,plain,
organism(skc8,skc15),
inference(resolution,[status(thm)],[clause17,c60]) ).
cnf(c76,plain,
living(skc8,skc15),
inference(resolution,[status(thm)],[clause23,c61]) ).
cnf(c573,plain,
( skc8 != X1006
| skc15 != X1007
| living(X1006,X1007) ),
inference(resolution,[status(thm)],[c22,c76]) ).
cnf(c897,plain,
( skc8 != X1011
| living(X1011,skc15) ),
inference(resolution,[status(thm)],[c573,reflexivity]) ).
cnf(clause22,axiom,
( ~ organism(X46,X45)
| impartial(X46,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c74,plain,
impartial(skc8,skc15),
inference(resolution,[status(thm)],[clause22,c61]) ).
cnf(c21,axiom,
( X494 != X493
| X492 != X491
| ~ impartial(X494,X492)
| impartial(X493,X491) ),
theory(equality) ).
cnf(c567,plain,
( skc8 != X1002
| skc15 != X1003
| impartial(X1002,X1003) ),
inference(resolution,[status(thm)],[c21,c74]) ).
cnf(c894,plain,
( skc8 != X1005
| impartial(X1005,skc15) ),
inference(resolution,[status(thm)],[c567,reflexivity]) ).
cnf(c345,plain,
impartial(skc12,skc10),
inference(resolution,[status(thm)],[c341,clause22]) ).
cnf(c566,plain,
( skc12 != X1000
| skc10 != X1001
| impartial(X1000,X1001) ),
inference(resolution,[status(thm)],[c21,c345]) ).
cnf(c893,plain,
( skc12 != X1004
| impartial(X1004,skc10) ),
inference(resolution,[status(thm)],[c566,reflexivity]) ).
cnf(c73,plain,
impartial(skc8,skc10),
inference(resolution,[status(thm)],[clause22,c62]) ).
cnf(c565,plain,
( skc8 != X996
| skc10 != X997
| impartial(X996,X997) ),
inference(resolution,[status(thm)],[c21,c73]) ).
cnf(c890,plain,
( skc8 != X999
| impartial(X999,skc10) ),
inference(resolution,[status(thm)],[c565,reflexivity]) ).
cnf(c392,plain,
impartial(skc12,skc15),
inference(resolution,[status(thm)],[c388,clause22]) ).
cnf(c564,plain,
( skc12 != X994
| skc15 != X995
| impartial(X994,X995) ),
inference(resolution,[status(thm)],[c21,c392]) ).
cnf(c889,plain,
( skc12 != X998
| impartial(X998,skc15) ),
inference(resolution,[status(thm)],[c564,reflexivity]) ).
cnf(clause18,axiom,
( ~ organism(X38,X37)
| entity(X38,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c64,plain,
entity(skc8,skc15),
inference(resolution,[status(thm)],[clause18,c61]) ).
cnf(clause21,axiom,
( ~ entity(X44,X43)
| existent(X44,X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c72,plain,
existent(skc8,skc15),
inference(resolution,[status(thm)],[clause21,c64]) ).
cnf(c20,axiom,
( X480 != X479
| X478 != X477
| ~ existent(X480,X478)
| existent(X479,X477) ),
theory(equality) ).
cnf(c563,plain,
( skc8 != X991
| skc15 != X990
| existent(X991,X990) ),
inference(resolution,[status(thm)],[c20,c72]) ).
cnf(c886,plain,
( skc8 != X993
| existent(X993,skc15) ),
inference(resolution,[status(thm)],[c563,reflexivity]) ).
cnf(c63,plain,
entity(skc8,skc10),
inference(resolution,[status(thm)],[clause18,c62]) ).
cnf(c71,plain,
existent(skc8,skc10),
inference(resolution,[status(thm)],[clause21,c63]) ).
cnf(c562,plain,
( skc8 != X989
| skc10 != X988
| existent(X989,X988) ),
inference(resolution,[status(thm)],[c20,c71]) ).
cnf(c885,plain,
( skc8 != X992
| existent(X992,skc10) ),
inference(resolution,[status(thm)],[c562,reflexivity]) ).
cnf(c394,plain,
entity(skc12,skc15),
inference(resolution,[status(thm)],[c388,clause18]) ).
cnf(c400,plain,
existent(skc12,skc15),
inference(resolution,[status(thm)],[c394,clause21]) ).
cnf(c561,plain,
( skc12 != X985
| skc15 != X984
| existent(X985,X984) ),
inference(resolution,[status(thm)],[c20,c400]) ).
cnf(c882,plain,
( skc12 != X987
| existent(X987,skc15) ),
inference(resolution,[status(thm)],[c561,reflexivity]) ).
cnf(c347,plain,
entity(skc12,skc10),
inference(resolution,[status(thm)],[c341,clause18]) ).
cnf(c354,plain,
existent(skc12,skc10),
inference(resolution,[status(thm)],[c347,clause21]) ).
cnf(c560,plain,
( skc12 != X983
| skc10 != X982
| existent(X983,X982) ),
inference(resolution,[status(thm)],[c20,c354]) ).
cnf(c881,plain,
( skc12 != X986
| existent(X986,skc10) ),
inference(resolution,[status(thm)],[c560,reflexivity]) ).
cnf(c19,axiom,
( X468 != X467
| X466 != X465
| ~ entity(X468,X466)
| entity(X467,X465) ),
theory(equality) ).
cnf(c559,plain,
( skc8 != X979
| skc15 != X978
| entity(X979,X978) ),
inference(resolution,[status(thm)],[c19,c64]) ).
cnf(c878,plain,
( skc8 != X981
| entity(X981,skc15) ),
inference(resolution,[status(thm)],[c559,reflexivity]) ).
cnf(c558,plain,
( skc12 != X977
| skc15 != X976
| entity(X977,X976) ),
inference(resolution,[status(thm)],[c19,c394]) ).
cnf(c877,plain,
( skc12 != X980
| entity(X980,skc15) ),
inference(resolution,[status(thm)],[c558,reflexivity]) ).
cnf(c557,plain,
( skc12 != X973
| skc10 != X972
| entity(X973,X972) ),
inference(resolution,[status(thm)],[c19,c347]) ).
cnf(c874,plain,
( skc12 != X975
| entity(X975,skc10) ),
inference(resolution,[status(thm)],[c557,reflexivity]) ).
cnf(c556,plain,
( skc8 != X971
| skc10 != X970
| entity(X971,X970) ),
inference(resolution,[status(thm)],[c19,c63]) ).
cnf(c873,plain,
( skc8 != X974
| entity(X974,skc10) ),
inference(resolution,[status(thm)],[c556,reflexivity]) ).
cnf(c18,axiom,
( X459 != X458
| X457 != X456
| ~ organism(X459,X457)
| organism(X458,X456) ),
theory(equality) ).
cnf(c555,plain,
( skc12 != X967
| skc15 != X966
| organism(X967,X966) ),
inference(resolution,[status(thm)],[c18,c388]) ).
cnf(c870,plain,
( skc12 != X969
| organism(X969,skc15) ),
inference(resolution,[status(thm)],[c555,reflexivity]) ).
cnf(c554,plain,
( skc8 != X965
| skc15 != X964
| organism(X965,X964) ),
inference(resolution,[status(thm)],[c18,c61]) ).
cnf(c869,plain,
( skc8 != X968
| organism(X968,skc15) ),
inference(resolution,[status(thm)],[c554,reflexivity]) ).
cnf(c553,plain,
( skc12 != X961
| skc10 != X960
| organism(X961,X960) ),
inference(resolution,[status(thm)],[c18,c341]) ).
cnf(c866,plain,
( skc12 != X963
| organism(X963,skc10) ),
inference(resolution,[status(thm)],[c553,reflexivity]) ).
cnf(c552,plain,
( skc8 != X959
| skc10 != X958
| organism(X959,X958) ),
inference(resolution,[status(thm)],[c18,c62]) ).
cnf(c865,plain,
( skc8 != X962
| organism(X962,skc10) ),
inference(resolution,[status(thm)],[c552,reflexivity]) ).
cnf(c17,axiom,
( X450 != X449
| X448 != X447
| ~ human_person(X450,X448)
| human_person(X449,X447) ),
theory(equality) ).
cnf(c551,plain,
( skc12 != X955
| skc15 != X956
| human_person(X955,X956) ),
inference(resolution,[status(thm)],[c17,c380]) ).
cnf(c863,plain,
( skc12 != X957
| human_person(X957,skc15) ),
inference(resolution,[status(thm)],[c551,reflexivity]) ).
cnf(c547,plain,
( ~ proposition(skc12,X952)
| ~ proposition(skc12,X954)
| ~ theme(skc12,skf2(skc15),X952)
| ~ think_believe_consider(skc12,skf2(skc15))
| ~ think_believe_consider(skc12,X953)
| ~ theme(skc12,X953,X954)
| ~ agent(skc12,X953,skc15)
| X952 = X954 ),
inference(resolution,[status(thm)],[c384,clause71]) ).
cnf(c550,plain,
( skc12 != X949
| skc10 != X950
| human_person(X949,X950) ),
inference(resolution,[status(thm)],[c17,c332]) ).
cnf(c860,plain,
( skc12 != X951
| human_person(X951,skc10) ),
inference(resolution,[status(thm)],[c550,reflexivity]) ).
cnf(c549,plain,
( skc8 != X946
| skc10 != X947
| human_person(X946,X947) ),
inference(resolution,[status(thm)],[c17,c59]) ).
cnf(c858,plain,
( skc8 != X948
| human_person(X948,skc10) ),
inference(resolution,[status(thm)],[c549,reflexivity]) ).
cnf(c545,plain,
( ~ proposition(skc12,X943)
| ~ proposition(skc12,X945)
| ~ theme(skc12,skf2(skc10),X943)
| ~ think_believe_consider(skc12,skf2(skc10))
| ~ think_believe_consider(skc12,X944)
| ~ theme(skc12,X944,X945)
| ~ agent(skc12,X944,skc10)
| X943 = X945 ),
inference(resolution,[status(thm)],[c383,clause71]) ).
cnf(c548,plain,
( skc8 != X940
| skc15 != X941
| human_person(X940,X941) ),
inference(resolution,[status(thm)],[c17,c60]) ).
cnf(c855,plain,
( skc8 != X942
| human_person(X942,skc15) ),
inference(resolution,[status(thm)],[c548,reflexivity]) ).
cnf(c546,plain,
( ~ accessible_world(skc12,X939)
| agent(X939,skf2(skc15),skc15) ),
inference(resolution,[status(thm)],[c384,clause66]) ).
cnf(c544,plain,
( ~ accessible_world(skc12,X938)
| agent(X938,skf2(skc10),skc10) ),
inference(resolution,[status(thm)],[c383,clause66]) ).
cnf(c16,axiom,
( X443 != X442
| X441 != X440
| ~ man(X443,X441)
| man(X442,X440) ),
theory(equality) ).
cnf(c543,plain,
( skc12 != X936
| skc15 != X935
| man(X936,X935) ),
inference(resolution,[status(thm)],[c16,c379]) ).
cnf(c853,plain,
( skc12 != X937
| man(X937,skc15) ),
inference(resolution,[status(thm)],[c543,reflexivity]) ).
cnf(c542,plain,
( skc8 != X933
| skc15 != X932
| man(X933,X932) ),
inference(resolution,[status(thm)],[c16,clause73]) ).
cnf(c851,plain,
( skc8 != X934
| man(X934,skc15) ),
inference(resolution,[status(thm)],[c542,reflexivity]) ).
cnf(c541,plain,
( skc8 != X930
| skc10 != X929
| man(X930,X929) ),
inference(resolution,[status(thm)],[c16,clause81]) ).
cnf(c849,plain,
( skc8 != X931
| man(X931,skc10) ),
inference(resolution,[status(thm)],[c541,reflexivity]) ).
cnf(c540,plain,
( skc12 != X927
| skc10 != X926
| man(X927,X926) ),
inference(resolution,[status(thm)],[c16,c331]) ).
cnf(c847,plain,
( skc12 != X928
| man(X928,skc10) ),
inference(resolution,[status(thm)],[c540,reflexivity]) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
cnf(c15,axiom,
( X434 != X433
| X432 != X431
| ~ state(X434,X432)
| state(X433,X431) ),
theory(equality) ).
cnf(c539,plain,
( skc8 != X924
| skc9 != X923
| state(X924,X923) ),
inference(resolution,[status(thm)],[c15,clause82]) ).
cnf(c845,plain,
( skc8 != X925
| state(X925,skc9) ),
inference(resolution,[status(thm)],[c539,reflexivity]) ).
cnf(clause51,axiom,
( ~ accessible_world(X155,X154)
| ~ state(X155,X156)
| state(X154,X156) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c229,plain,
( ~ accessible_world(skc8,X252)
| state(X252,skc9) ),
inference(resolution,[status(thm)],[clause51,clause82]) ).
cnf(c326,plain,
state(skc12,skc9),
inference(resolution,[status(thm)],[c229,clause83]) ).
cnf(c538,plain,
( skc12 != X921
| skc9 != X920
| state(X921,X920) ),
inference(resolution,[status(thm)],[c15,c326]) ).
cnf(c843,plain,
( skc12 != X922
| state(X922,skc9) ),
inference(resolution,[status(thm)],[c538,reflexivity]) ).
cnf(clause12,axiom,
( ~ abstraction(X26,X25)
| general(X26,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(clause9,axiom,
( ~ relation(X20,X19)
| abstraction(X20,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause28,axiom,
( ~ relname(X58,X57)
| relation(X58,X57) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c85,plain,
relation(skc8,skc11),
inference(resolution,[status(thm)],[clause28,c84]) ).
cnf(c88,plain,
abstraction(skc8,skc11),
inference(resolution,[status(thm)],[c85,clause9]) ).
cnf(c93,plain,
general(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause12]) ).
cnf(c14,axiom,
( X425 != X424
| X423 != X422
| ~ general(X425,X423)
| general(X424,X422) ),
theory(equality) ).
cnf(c537,plain,
( skc8 != X917
| skc11 != X918
| general(X917,X918) ),
inference(resolution,[status(thm)],[c14,c93]) ).
cnf(c841,plain,
( skc8 != X919
| general(X919,skc11) ),
inference(resolution,[status(thm)],[c537,reflexivity]) ).
cnf(c86,plain,
relation(skc8,skc14),
inference(resolution,[status(thm)],[clause28,c83]) ).
cnf(c89,plain,
abstraction(skc8,skc14),
inference(resolution,[status(thm)],[c86,clause9]) ).
cnf(c97,plain,
general(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause12]) ).
cnf(c536,plain,
( skc8 != X914
| skc14 != X915
| general(X914,X915) ),
inference(resolution,[status(thm)],[c14,c97]) ).
cnf(c839,plain,
( skc8 != X916
| general(X916,skc14) ),
inference(resolution,[status(thm)],[c536,reflexivity]) ).
cnf(clause47,axiom,
( ~ accessible_world(X133,X132)
| ~ relation(X133,X134)
| relation(X132,X134) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c207,plain,
( ~ accessible_world(skc8,X215)
| relation(X215,skc11) ),
inference(resolution,[status(thm)],[clause47,c85]) ).
cnf(c284,plain,
relation(skc12,skc11),
inference(resolution,[status(thm)],[c207,clause83]) ).
cnf(c286,plain,
abstraction(skc12,skc11),
inference(resolution,[status(thm)],[c284,clause9]) ).
cnf(c289,plain,
general(skc12,skc11),
inference(resolution,[status(thm)],[c286,clause12]) ).
cnf(c535,plain,
( skc12 != X911
| skc11 != X912
| general(X911,X912) ),
inference(resolution,[status(thm)],[c14,c289]) ).
cnf(c837,plain,
( skc12 != X913
| general(X913,skc11) ),
inference(resolution,[status(thm)],[c535,reflexivity]) ).
cnf(c209,plain,
( ~ accessible_world(skc8,X223)
| relation(X223,skc14) ),
inference(resolution,[status(thm)],[clause47,c86]) ).
cnf(c300,plain,
relation(skc12,skc14),
inference(resolution,[status(thm)],[c209,clause83]) ).
cnf(c302,plain,
abstraction(skc12,skc14),
inference(resolution,[status(thm)],[c300,clause9]) ).
cnf(c305,plain,
general(skc12,skc14),
inference(resolution,[status(thm)],[c302,clause12]) ).
cnf(c534,plain,
( skc12 != X908
| skc14 != X909
| general(X908,X909) ),
inference(resolution,[status(thm)],[c14,c305]) ).
cnf(c835,plain,
( skc12 != X910
| general(X910,skc14) ),
inference(resolution,[status(thm)],[c534,reflexivity]) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
cnf(clause8,axiom,
( ~ proposition(X18,X17)
| relation(X18,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c44,plain,
relation(skc8,skc12),
inference(resolution,[status(thm)],[clause8,clause84]) ).
cnf(c45,plain,
abstraction(skc8,skc12),
inference(resolution,[status(thm)],[clause9,c44]) ).
cnf(c49,plain,
general(skc8,skc12),
inference(resolution,[status(thm)],[clause12,c45]) ).
cnf(c533,plain,
( skc8 != X903
| skc12 != X904
| general(X903,X904) ),
inference(resolution,[status(thm)],[c14,c49]) ).
cnf(c831,plain,
( skc8 != X907
| general(X907,skc12) ),
inference(resolution,[status(thm)],[c533,reflexivity]) ).
cnf(clause46,axiom,
( ~ accessible_world(X126,X125)
| ~ proposition(X126,X127)
| proposition(X125,X127) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(c205,plain,
( ~ accessible_world(skc8,X208)
| proposition(X208,skc12) ),
inference(resolution,[status(thm)],[clause46,clause84]) ).
cnf(c267,plain,
proposition(skc12,skc12),
inference(resolution,[status(thm)],[c205,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(c276,plain,
general(skc12,skc12),
inference(resolution,[status(thm)],[c271,clause12]) ).
cnf(c532,plain,
( skc12 != X901
| skc12 != X902
| general(X901,X902) ),
inference(resolution,[status(thm)],[c14,c276]) ).
cnf(c830,plain,
( skc12 != X906
| general(X906,skc12) ),
inference(resolution,[status(thm)],[c532,reflexivity]) ).
cnf(c829,plain,
( skc12 != X905
| general(X905,X905) ),
inference(factor,[status(thm)],[c532]) ).
cnf(clause11,axiom,
( ~ abstraction(X24,X23)
| nonhuman(X24,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c288,plain,
nonhuman(skc12,skc11),
inference(resolution,[status(thm)],[c286,clause11]) ).
cnf(c13,axiom,
( X418 != X417
| X416 != X415
| ~ nonhuman(X418,X416)
| nonhuman(X417,X415) ),
theory(equality) ).
cnf(c528,plain,
( skc12 != X897
| skc11 != X898
| nonhuman(X897,X898) ),
inference(resolution,[status(thm)],[c13,c288]) ).
cnf(c826,plain,
( skc12 != X900
| nonhuman(X900,skc11) ),
inference(resolution,[status(thm)],[c528,reflexivity]) ).
cnf(c92,plain,
nonhuman(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause11]) ).
cnf(c527,plain,
( skc8 != X895
| skc11 != X896
| nonhuman(X895,X896) ),
inference(resolution,[status(thm)],[c13,c92]) ).
cnf(c825,plain,
( skc8 != X899
| nonhuman(X899,skc11) ),
inference(resolution,[status(thm)],[c527,reflexivity]) ).
cnf(c48,plain,
nonhuman(skc8,skc12),
inference(resolution,[status(thm)],[clause11,c45]) ).
cnf(c526,plain,
( skc8 != X891
| skc12 != X892
| nonhuman(X891,X892) ),
inference(resolution,[status(thm)],[c13,c48]) ).
cnf(c822,plain,
( skc8 != X894
| nonhuman(X894,skc12) ),
inference(resolution,[status(thm)],[c526,reflexivity]) ).
cnf(c304,plain,
nonhuman(skc12,skc14),
inference(resolution,[status(thm)],[c302,clause11]) ).
cnf(c525,plain,
( skc12 != X889
| skc14 != X890
| nonhuman(X889,X890) ),
inference(resolution,[status(thm)],[c13,c304]) ).
cnf(c821,plain,
( skc12 != X893
| nonhuman(X893,skc14) ),
inference(resolution,[status(thm)],[c525,reflexivity]) ).
cnf(c275,plain,
nonhuman(skc12,skc12),
inference(resolution,[status(thm)],[c271,clause11]) ).
cnf(c524,plain,
( skc12 != X885
| skc12 != X886
| nonhuman(X885,X886) ),
inference(resolution,[status(thm)],[c13,c275]) ).
cnf(c818,plain,
( skc12 != X888
| nonhuman(X888,skc12) ),
inference(resolution,[status(thm)],[c524,reflexivity]) ).
cnf(c817,plain,
( skc12 != X887
| nonhuman(X887,X887) ),
inference(factor,[status(thm)],[c524]) ).
cnf(c96,plain,
nonhuman(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause11]) ).
cnf(c523,plain,
( skc8 != X882
| skc14 != X883
| nonhuman(X882,X883) ),
inference(resolution,[status(thm)],[c13,c96]) ).
cnf(c815,plain,
( skc8 != X884
| nonhuman(X884,skc14) ),
inference(resolution,[status(thm)],[c523,reflexivity]) ).
cnf(c12,axiom,
( X411 != X410
| X409 != X408
| ~ abstraction(X411,X409)
| abstraction(X410,X408) ),
theory(equality) ).
cnf(c519,plain,
( skc12 != X880
| skc14 != X879
| abstraction(X880,X879) ),
inference(resolution,[status(thm)],[c12,c302]) ).
cnf(c813,plain,
( skc12 != X881
| abstraction(X881,skc14) ),
inference(resolution,[status(thm)],[c519,reflexivity]) ).
cnf(c518,plain,
( skc8 != X877
| skc14 != X876
| abstraction(X877,X876) ),
inference(resolution,[status(thm)],[c12,c89]) ).
cnf(c811,plain,
( skc8 != X878
| abstraction(X878,skc14) ),
inference(resolution,[status(thm)],[c518,reflexivity]) ).
cnf(c517,plain,
( skc12 != X874
| skc11 != X873
| abstraction(X874,X873) ),
inference(resolution,[status(thm)],[c12,c286]) ).
cnf(c809,plain,
( skc12 != X875
| abstraction(X875,skc11) ),
inference(resolution,[status(thm)],[c517,reflexivity]) ).
cnf(c516,plain,
( skc12 != X870
| skc12 != X869
| abstraction(X870,X869) ),
inference(resolution,[status(thm)],[c12,c271]) ).
cnf(c806,plain,
( skc12 != X872
| abstraction(X872,skc12) ),
inference(resolution,[status(thm)],[c516,reflexivity]) ).
cnf(c805,plain,
( skc12 != X871
| abstraction(X871,X871) ),
inference(factor,[status(thm)],[c516]) ).
cnf(c515,plain,
( skc8 != X867
| skc11 != X866
| abstraction(X867,X866) ),
inference(resolution,[status(thm)],[c12,c88]) ).
cnf(c803,plain,
( skc8 != X868
| abstraction(X868,skc11) ),
inference(resolution,[status(thm)],[c515,reflexivity]) ).
cnf(c514,plain,
( skc8 != X864
| skc12 != X863
| abstraction(X864,X863) ),
inference(resolution,[status(thm)],[c12,c45]) ).
cnf(c801,plain,
( skc8 != X865
| abstraction(X865,skc12) ),
inference(resolution,[status(thm)],[c514,reflexivity]) ).
cnf(c11,axiom,
( X404 != X403
| X402 != X401
| ~ relation(X404,X402)
| relation(X403,X401) ),
theory(equality) ).
cnf(c512,plain,
( skc8 != X861
| skc14 != X860
| relation(X861,X860) ),
inference(resolution,[status(thm)],[c11,c86]) ).
cnf(c799,plain,
( skc8 != X862
| relation(X862,skc14) ),
inference(resolution,[status(thm)],[c512,reflexivity]) ).
cnf(c511,plain,
( skc12 != X858
| skc11 != X857
| relation(X858,X857) ),
inference(resolution,[status(thm)],[c11,c284]) ).
cnf(c797,plain,
( skc12 != X859
| relation(X859,skc11) ),
inference(resolution,[status(thm)],[c511,reflexivity]) ).
cnf(c510,plain,
( skc8 != X853
| skc12 != X852
| relation(X853,X852) ),
inference(resolution,[status(thm)],[c11,c44]) ).
cnf(c793,plain,
( skc8 != X856
| relation(X856,skc12) ),
inference(resolution,[status(thm)],[c510,reflexivity]) ).
cnf(c509,plain,
( skc12 != X851
| skc12 != X850
| relation(X851,X850) ),
inference(resolution,[status(thm)],[c11,c268]) ).
cnf(c792,plain,
( skc12 != X855
| relation(X855,skc12) ),
inference(resolution,[status(thm)],[c509,reflexivity]) ).
cnf(c791,plain,
( skc12 != X854
| relation(X854,X854) ),
inference(factor,[status(thm)],[c509]) ).
cnf(c508,plain,
( skc12 != X847
| skc14 != X846
| relation(X847,X846) ),
inference(resolution,[status(thm)],[c11,c300]) ).
cnf(c788,plain,
( skc12 != X849
| relation(X849,skc14) ),
inference(resolution,[status(thm)],[c508,reflexivity]) ).
cnf(c507,plain,
( skc8 != X845
| skc11 != X844
| relation(X845,X844) ),
inference(resolution,[status(thm)],[c11,c85]) ).
cnf(c787,plain,
( skc8 != X848
| relation(X848,skc11) ),
inference(resolution,[status(thm)],[c507,reflexivity]) ).
cnf(c10,axiom,
( X397 != X396
| X395 != X394
| ~ proposition(X397,X395)
| proposition(X396,X394) ),
theory(equality) ).
cnf(c503,plain,
( skc12 != X840
| skc12 != X841
| proposition(X840,X841) ),
inference(resolution,[status(thm)],[c10,c267]) ).
cnf(c784,plain,
( skc12 != X843
| proposition(X843,skc12) ),
inference(resolution,[status(thm)],[c503,reflexivity]) ).
cnf(c783,plain,
( skc12 != X842
| proposition(X842,X842) ),
inference(factor,[status(thm)],[c503]) ).
cnf(c502,plain,
( skc8 != X837
| skc12 != X838
| proposition(X837,X838) ),
inference(resolution,[status(thm)],[c10,clause84]) ).
cnf(c781,plain,
( skc8 != X839
| proposition(X839,skc12) ),
inference(resolution,[status(thm)],[c502,reflexivity]) ).
cnf(clause7,axiom,
( ~ eventuality(X16,X15)
| unisex(X16,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause14,axiom,
( ~ state(X30,X29)
| eventuality(X30,X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c51,plain,
eventuality(skc8,skc9),
inference(resolution,[status(thm)],[clause14,clause82]) ).
cnf(c56,plain,
unisex(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause7]) ).
cnf(c9,axiom,
( X392 != X391
| X390 != X389
| ~ unisex(X392,X390)
| unisex(X391,X389) ),
theory(equality) ).
cnf(c494,plain,
( skc8 != X834
| skc9 != X835
| unisex(X834,X835) ),
inference(resolution,[status(thm)],[c9,c56]) ).
cnf(c779,plain,
( skc8 != X836
| unisex(X836,skc9) ),
inference(resolution,[status(thm)],[c494,reflexivity]) ).
cnf(clause2,axiom,
( ~ event(X6,X5)
| eventuality(X6,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause15,axiom,
( ~ state(X32,X31)
| event(X32,X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c52,plain,
event(skc8,skc9),
inference(resolution,[status(thm)],[clause15,clause82]) ).
cnf(clause37,axiom,
( ~ accessible_world(X85,X84)
| ~ event(X85,X86)
| event(X84,X86) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c119,plain,
( ~ accessible_world(skc8,X94)
| event(X94,skc9) ),
inference(resolution,[status(thm)],[clause37,c52]) ).
cnf(c141,plain,
event(skc12,skc9),
inference(resolution,[status(thm)],[c119,clause83]) ).
cnf(c142,plain,
eventuality(skc12,skc9),
inference(resolution,[status(thm)],[c141,clause2]) ).
cnf(c146,plain,
unisex(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause7]) ).
cnf(c493,plain,
( skc12 != X831
| skc9 != X832
| unisex(X831,X832) ),
inference(resolution,[status(thm)],[c9,c146]) ).
cnf(c777,plain,
( skc12 != X833
| unisex(X833,skc9) ),
inference(resolution,[status(thm)],[c493,reflexivity]) ).
cnf(c362,plain,
eventuality(skc12,skf2(X274)),
inference(resolution,[status(thm)],[c361,clause2]) ).
cnf(c366,plain,
unisex(skc12,skf2(X279)),
inference(resolution,[status(thm)],[c362,clause7]) ).
cnf(c492,plain,
( skc12 != X825
| skf2(X827) != X826
| unisex(X825,X826) ),
inference(resolution,[status(thm)],[c9,c366]) ).
cnf(c775,plain,
( skc12 != X829
| unisex(X829,skf2(X828)) ),
inference(resolution,[status(thm)],[c492,reflexivity]) ).
cnf(clause13,axiom,
( ~ abstraction(X28,X27)
| unisex(X28,X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c90,plain,
unisex(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause13]) ).
cnf(c491,plain,
( skc8 != X822
| skc11 != X823
| unisex(X822,X823) ),
inference(resolution,[status(thm)],[c9,c90]) ).
cnf(c773,plain,
( skc8 != X824
| unisex(X824,skc11) ),
inference(resolution,[status(thm)],[c491,reflexivity]) ).
cnf(c94,plain,
unisex(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause13]) ).
cnf(c490,plain,
( skc8 != X819
| skc14 != X820
| unisex(X819,X820) ),
inference(resolution,[status(thm)],[c9,c94]) ).
cnf(c771,plain,
( skc8 != X821
| unisex(X821,skc14) ),
inference(resolution,[status(thm)],[c490,reflexivity]) ).
cnf(c50,plain,
unisex(skc8,skc12),
inference(resolution,[status(thm)],[clause13,c45]) ).
cnf(c489,plain,
( skc8 != X815
| skc12 != X816
| unisex(X815,X816) ),
inference(resolution,[status(thm)],[c9,c50]) ).
cnf(c768,plain,
( skc8 != X818
| unisex(X818,skc12) ),
inference(resolution,[status(thm)],[c489,reflexivity]) ).
cnf(clause43,axiom,
( ~ accessible_world(X112,X111)
| ~ unisex(X112,X113)
| unisex(X111,X113) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c178,plain,
( ~ accessible_world(skc8,X176)
| unisex(X176,skc12) ),
inference(resolution,[status(thm)],[clause43,c50]) ).
cnf(c243,plain,
unisex(skc12,skc12),
inference(resolution,[status(thm)],[c178,clause83]) ).
cnf(c488,plain,
( skc12 != X812
| skc12 != X813
| unisex(X812,X813) ),
inference(resolution,[status(thm)],[c9,c243]) ).
cnf(c766,plain,
( skc12 != X817
| unisex(X817,skc12) ),
inference(resolution,[status(thm)],[c488,reflexivity]) ).
cnf(c765,plain,
( skc12 != X814
| unisex(X814,X814) ),
inference(factor,[status(thm)],[c488]) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
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(c487,plain,
( skc8 != X809
| skc13 != X810
| unisex(X809,X810) ),
inference(resolution,[status(thm)],[c9,c43]) ).
cnf(c763,plain,
( skc8 != X811
| unisex(X811,skc13) ),
inference(resolution,[status(thm)],[c487,reflexivity]) ).
cnf(c179,plain,
( ~ accessible_world(skc8,X177)
| unisex(X177,skc14) ),
inference(resolution,[status(thm)],[clause43,c94]) ).
cnf(c246,plain,
unisex(skc12,skc14),
inference(resolution,[status(thm)],[c179,clause83]) ).
cnf(c486,plain,
( skc12 != X806
| skc14 != X807
| unisex(X806,X807) ),
inference(resolution,[status(thm)],[c9,c246]) ).
cnf(c761,plain,
( skc12 != X808
| unisex(X808,skc14) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(c118,plain,
( ~ accessible_world(skc8,X87)
| event(X87,skc13) ),
inference(resolution,[status(thm)],[clause37,clause76]) ).
cnf(c120,plain,
event(skc12,skc13),
inference(resolution,[status(thm)],[c118,clause83]) ).
cnf(c121,plain,
eventuality(skc12,skc13),
inference(resolution,[status(thm)],[c120,clause2]) ).
cnf(c126,plain,
unisex(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause7]) ).
cnf(c485,plain,
( skc12 != X803
| skc13 != X804
| unisex(X803,X804) ),
inference(resolution,[status(thm)],[c9,c126]) ).
cnf(c759,plain,
( skc12 != X805
| unisex(X805,skc13) ),
inference(resolution,[status(thm)],[c485,reflexivity]) ).
cnf(c180,plain,
( ~ accessible_world(skc8,X181)
| unisex(X181,skc11) ),
inference(resolution,[status(thm)],[clause43,c90]) ).
cnf(c251,plain,
unisex(skc12,skc11),
inference(resolution,[status(thm)],[c180,clause83]) ).
cnf(c484,plain,
( skc12 != X800
| skc11 != X801
| unisex(X800,X801) ),
inference(resolution,[status(thm)],[c9,c251]) ).
cnf(c757,plain,
( skc12 != X802
| unisex(X802,skc11) ),
inference(resolution,[status(thm)],[c484,reflexivity]) ).
cnf(clause6,axiom,
( ~ eventuality(X14,X13)
| nonexistent(X14,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c367,plain,
nonexistent(skc12,skf2(X280)),
inference(resolution,[status(thm)],[c362,clause6]) ).
cnf(c8,axiom,
( X384 != X383
| X382 != X381
| ~ nonexistent(X384,X382)
| nonexistent(X383,X381) ),
theory(equality) ).
cnf(c481,plain,
( skc12 != X796
| skf2(X794) != X795
| nonexistent(X796,X795) ),
inference(resolution,[status(thm)],[c8,c367]) ).
cnf(c755,plain,
( skc12 != X798
| nonexistent(X798,skf2(X797)) ),
inference(resolution,[status(thm)],[c481,reflexivity]) ).
cnf(c147,plain,
nonexistent(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause6]) ).
cnf(c480,plain,
( skc12 != X792
| skc9 != X791
| nonexistent(X792,X791) ),
inference(resolution,[status(thm)],[c8,c147]) ).
cnf(c753,plain,
( skc12 != X793
| nonexistent(X793,skc9) ),
inference(resolution,[status(thm)],[c480,reflexivity]) ).
cnf(c42,plain,
nonexistent(skc8,skc13),
inference(resolution,[status(thm)],[clause6,c38]) ).
cnf(c479,plain,
( skc8 != X789
| skc13 != X788
| nonexistent(X789,X788) ),
inference(resolution,[status(thm)],[c8,c42]) ).
cnf(c751,plain,
( skc8 != X790
| nonexistent(X790,skc13) ),
inference(resolution,[status(thm)],[c479,reflexivity]) ).
cnf(c125,plain,
nonexistent(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause6]) ).
cnf(c478,plain,
( skc12 != X786
| skc13 != X785
| nonexistent(X786,X785) ),
inference(resolution,[status(thm)],[c8,c125]) ).
cnf(c749,plain,
( skc12 != X787
| nonexistent(X787,skc13) ),
inference(resolution,[status(thm)],[c478,reflexivity]) ).
cnf(c55,plain,
nonexistent(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause6]) ).
cnf(c477,plain,
( skc8 != X783
| skc9 != X782
| nonexistent(X783,X782) ),
inference(resolution,[status(thm)],[c8,c55]) ).
cnf(c747,plain,
( skc8 != X784
| nonexistent(X784,skc9) ),
inference(resolution,[status(thm)],[c477,reflexivity]) ).
cnf(clause5,axiom,
( ~ eventuality(X12,X11)
| specific(X12,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c144,plain,
specific(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause5]) ).
cnf(c7,axiom,
( X376 != X375
| X374 != X373
| ~ specific(X376,X374)
| specific(X375,X373) ),
theory(equality) ).
cnf(c475,plain,
( skc12 != X780
| skc9 != X779
| specific(X780,X779) ),
inference(resolution,[status(thm)],[c7,c144]) ).
cnf(c745,plain,
( skc12 != X781
| specific(X781,skc9) ),
inference(resolution,[status(thm)],[c475,reflexivity]) ).
cnf(c364,plain,
specific(skc12,skf2(X277)),
inference(resolution,[status(thm)],[c362,clause5]) ).
cnf(c474,plain,
( skc12 != X775
| skf2(X774) != X773
| specific(X775,X773) ),
inference(resolution,[status(thm)],[c7,c364]) ).
cnf(c743,plain,
( skc12 != X777
| specific(X777,skf2(X776)) ),
inference(resolution,[status(thm)],[c474,reflexivity]) ).
cnf(clause20,axiom,
( ~ entity(X42,X41)
| specific(X42,X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c70,plain,
specific(skc8,skc15),
inference(resolution,[status(thm)],[clause20,c64]) ).
cnf(c473,plain,
( skc8 != X771
| skc15 != X770
| specific(X771,X770) ),
inference(resolution,[status(thm)],[c7,c70]) ).
cnf(c741,plain,
( skc8 != X772
| specific(X772,skc15) ),
inference(resolution,[status(thm)],[c473,reflexivity]) ).
cnf(c123,plain,
specific(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause5]) ).
cnf(c472,plain,
( skc12 != X768
| skc13 != X767
| specific(X768,X767) ),
inference(resolution,[status(thm)],[c7,c123]) ).
cnf(c739,plain,
( skc12 != X769
| specific(X769,skc13) ),
inference(resolution,[status(thm)],[c472,reflexivity]) ).
cnf(c41,plain,
specific(skc8,skc13),
inference(resolution,[status(thm)],[clause5,c38]) ).
cnf(c471,plain,
( skc8 != X765
| skc13 != X764
| specific(X765,X764) ),
inference(resolution,[status(thm)],[c7,c41]) ).
cnf(c737,plain,
( skc8 != X766
| specific(X766,skc13) ),
inference(resolution,[status(thm)],[c471,reflexivity]) ).
cnf(c69,plain,
specific(skc8,skc10),
inference(resolution,[status(thm)],[clause20,c63]) ).
cnf(clause41,axiom,
( ~ accessible_world(X99,X98)
| ~ specific(X99,X100)
| specific(X98,X100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c162,plain,
( ~ accessible_world(skc8,X152)
| specific(X152,skc10) ),
inference(resolution,[status(thm)],[clause41,c69]) ).
cnf(c225,plain,
specific(skc12,skc10),
inference(resolution,[status(thm)],[c162,clause83]) ).
cnf(c470,plain,
( skc12 != X762
| skc10 != X761
| specific(X762,X761) ),
inference(resolution,[status(thm)],[c7,c225]) ).
cnf(c735,plain,
( skc12 != X763
| specific(X763,skc10) ),
inference(resolution,[status(thm)],[c470,reflexivity]) ).
cnf(c166,plain,
( ~ accessible_world(skc8,X159)
| specific(X159,skc15) ),
inference(resolution,[status(thm)],[clause41,c70]) ).
cnf(c231,plain,
specific(skc12,skc15),
inference(resolution,[status(thm)],[c166,clause83]) ).
cnf(c469,plain,
( skc12 != X759
| skc15 != X758
| specific(X759,X758) ),
inference(resolution,[status(thm)],[c7,c231]) ).
cnf(c733,plain,
( skc12 != X760
| specific(X760,skc15) ),
inference(resolution,[status(thm)],[c469,reflexivity]) ).
cnf(c53,plain,
specific(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause5]) ).
cnf(c468,plain,
( skc8 != X756
| skc9 != X755
| specific(X756,X755) ),
inference(resolution,[status(thm)],[c7,c53]) ).
cnf(c731,plain,
( skc8 != X757
| specific(X757,skc9) ),
inference(resolution,[status(thm)],[c468,reflexivity]) ).
cnf(c467,plain,
( skc8 != X753
| skc10 != X752
| specific(X753,X752) ),
inference(resolution,[status(thm)],[c7,c69]) ).
cnf(c729,plain,
( skc8 != X754
| specific(X754,skc10) ),
inference(resolution,[status(thm)],[c467,reflexivity]) ).
cnf(clause4,axiom,
( ~ thing(X10,X9)
| singleton(X10,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause3,axiom,
( ~ eventuality(X8,X7)
| thing(X8,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c365,plain,
thing(skc12,skf2(X278)),
inference(resolution,[status(thm)],[c362,clause3]) ).
cnf(c372,plain,
singleton(skc12,skf2(X285)),
inference(resolution,[status(thm)],[c365,clause4]) ).
cnf(c6,axiom,
( X369 != X368
| X367 != X366
| ~ singleton(X369,X367)
| singleton(X368,X366) ),
theory(equality) ).
cnf(c456,plain,
( skc12 != X748
| skf2(X746) != X747
| singleton(X748,X747) ),
inference(resolution,[status(thm)],[c6,c372]) ).
cnf(c727,plain,
( skc12 != X749
| singleton(X749,skf2(X750)) ),
inference(resolution,[status(thm)],[c456,reflexivity]) ).
cnf(clause10,axiom,
( ~ abstraction(X22,X21)
| thing(X22,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c91,plain,
thing(skc8,skc11),
inference(resolution,[status(thm)],[c88,clause10]) ).
cnf(c99,plain,
singleton(skc8,skc11),
inference(resolution,[status(thm)],[c91,clause4]) ).
cnf(c464,plain,
( skc8 != X744
| skc11 != X743
| singleton(X744,X743) ),
inference(resolution,[status(thm)],[c6,c99]) ).
cnf(c725,plain,
( skc8 != X745
| singleton(X745,skc11) ),
inference(resolution,[status(thm)],[c464,reflexivity]) ).
cnf(c5,axiom,
( X362 != X361
| X360 != X359
| ~ thing(X362,X360)
| thing(X361,X359) ),
theory(equality) ).
cnf(c447,plain,
( skc12 != X737
| skf2(X738) != X739
| thing(X737,X739) ),
inference(resolution,[status(thm)],[c5,c365]) ).
cnf(c723,plain,
( skc12 != X740
| thing(X740,skf2(X741)) ),
inference(resolution,[status(thm)],[c447,reflexivity]) ).
cnf(c145,plain,
thing(skc12,skc9),
inference(resolution,[status(thm)],[c142,clause3]) ).
cnf(c150,plain,
singleton(skc12,skc9),
inference(resolution,[status(thm)],[c145,clause4]) ).
cnf(c463,plain,
( skc12 != X735
| skc9 != X734
| singleton(X735,X734) ),
inference(resolution,[status(thm)],[c6,c150]) ).
cnf(c721,plain,
( skc12 != X736
| singleton(X736,skc9) ),
inference(resolution,[status(thm)],[c463,reflexivity]) ).
cnf(c4,axiom,
( X355 != X354
| X353 != X352
| ~ eventuality(X355,X353)
| eventuality(X354,X352) ),
theory(equality) ).
cnf(c428,plain,
( skc12 != X729
| skf2(X730) != X728
| eventuality(X729,X728) ),
inference(resolution,[status(thm)],[c4,c362]) ).
cnf(c719,plain,
( skc12 != X732
| eventuality(X732,skf2(X731)) ),
inference(resolution,[status(thm)],[c428,reflexivity]) ).
cnf(c46,plain,
thing(skc8,skc12),
inference(resolution,[status(thm)],[clause10,c45]) ).
cnf(c47,plain,
singleton(skc8,skc12),
inference(resolution,[status(thm)],[c46,clause4]) ).
cnf(c462,plain,
( skc8 != X726
| skc12 != X725
| singleton(X726,X725) ),
inference(resolution,[status(thm)],[c6,c47]) ).
cnf(c717,plain,
( skc8 != X727
| singleton(X727,skc12) ),
inference(resolution,[status(thm)],[c462,reflexivity]) ).
cnf(c3,axiom,
( X348 != X347
| X346 != X345
| ~ event(X348,X346)
| event(X347,X345) ),
theory(equality) ).
cnf(c423,plain,
( skc12 != X720
| skf2(X719) != X721
| event(X720,X721) ),
inference(resolution,[status(thm)],[c3,c361]) ).
cnf(c715,plain,
( skc12 != X722
| event(X722,skf2(X723)) ),
inference(resolution,[status(thm)],[c423,reflexivity]) ).
cnf(clause19,axiom,
( ~ entity(X40,X39)
| thing(X40,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c66,plain,
thing(skc8,skc15),
inference(resolution,[status(thm)],[clause19,c64]) ).
cnf(c68,plain,
singleton(skc8,skc15),
inference(resolution,[status(thm)],[c66,clause4]) ).
cnf(c461,plain,
( skc8 != X717
| skc15 != X716
| singleton(X717,X716) ),
inference(resolution,[status(thm)],[c6,c68]) ).
cnf(c713,plain,
( skc8 != X718
| singleton(X718,skc15) ),
inference(resolution,[status(thm)],[c461,reflexivity]) ).
cnf(c2,axiom,
( X341 != X340
| X339 != X338
| ~ smoke(X341,X339)
| smoke(X340,X338) ),
theory(equality) ).
cnf(c416,plain,
( skc12 != X710
| skf2(X712) != X711
| smoke(X710,X711) ),
inference(resolution,[status(thm)],[c2,c359]) ).
cnf(c711,plain,
( skc12 != X713
| smoke(X713,skf2(X714)) ),
inference(resolution,[status(thm)],[c416,reflexivity]) ).
cnf(c124,plain,
thing(skc12,skc13),
inference(resolution,[status(thm)],[c121,clause3]) ).
cnf(c128,plain,
singleton(skc12,skc13),
inference(resolution,[status(thm)],[c124,clause4]) ).
cnf(c460,plain,
( skc12 != X708
| skc13 != X707
| singleton(X708,X707) ),
inference(resolution,[status(thm)],[c6,c128]) ).
cnf(c709,plain,
( skc12 != X709
| singleton(X709,skc13) ),
inference(resolution,[status(thm)],[c460,reflexivity]) ).
cnf(c39,plain,
thing(skc8,skc13),
inference(resolution,[status(thm)],[clause3,c38]) ).
cnf(c40,plain,
singleton(skc8,skc13),
inference(resolution,[status(thm)],[clause4,c39]) ).
cnf(c459,plain,
( skc8 != X705
| skc13 != X704
| singleton(X705,X704) ),
inference(resolution,[status(thm)],[c6,c40]) ).
cnf(c707,plain,
( skc8 != X706
| singleton(X706,skc13) ),
inference(resolution,[status(thm)],[c459,reflexivity]) ).
cnf(c95,plain,
thing(skc8,skc14),
inference(resolution,[status(thm)],[c89,clause10]) ).
cnf(c105,plain,
singleton(skc8,skc14),
inference(resolution,[status(thm)],[c95,clause4]) ).
cnf(c458,plain,
( skc8 != X690
| skc14 != X689
| singleton(X690,X689) ),
inference(resolution,[status(thm)],[c6,c105]) ).
cnf(c703,plain,
( skc8 != X691
| singleton(X691,skc14) ),
inference(resolution,[status(thm)],[c458,reflexivity]) ).
cnf(c54,plain,
thing(skc8,skc9),
inference(resolution,[status(thm)],[c51,clause3]) ).
cnf(c58,plain,
singleton(skc8,skc9),
inference(resolution,[status(thm)],[c54,clause4]) ).
cnf(c457,plain,
( skc8 != X676
| skc9 != X675
| singleton(X676,X675) ),
inference(resolution,[status(thm)],[c6,c58]) ).
cnf(c697,plain,
( skc8 != X688
| singleton(X688,skc9) ),
inference(resolution,[status(thm)],[c457,reflexivity]) ).
cnf(clause39,axiom,
( ~ accessible_world(X92,X91)
| ~ thing(X92,X93)
| thing(X91,X93) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c138,plain,
( ~ accessible_world(skc8,X119)
| thing(X119,skc15) ),
inference(resolution,[status(thm)],[clause39,c66]) ).
cnf(c195,plain,
thing(skc12,skc15),
inference(resolution,[status(thm)],[c138,clause83]) ).
cnf(c196,plain,
singleton(skc12,skc15),
inference(resolution,[status(thm)],[c195,clause4]) ).
cnf(c455,plain,
( skc12 != X673
| skc15 != X672
| singleton(X673,X672) ),
inference(resolution,[status(thm)],[c6,c196]) ).
cnf(c695,plain,
( skc12 != X674
| singleton(X674,skc15) ),
inference(resolution,[status(thm)],[c455,reflexivity]) ).
cnf(c350,plain,
( ~ proposition(skc8,X669)
| ~ proposition(skc8,X671)
| ~ theme(skc8,skc13,X669)
| ~ think_believe_consider(skc8,skc13)
| ~ think_believe_consider(skc8,X670)
| ~ theme(skc8,X670,X671)
| ~ agent(skc8,X670,skc15)
| X669 = X671 ),
inference(resolution,[status(thm)],[clause71,clause86]) ).
cnf(c137,plain,
( ~ accessible_world(skc8,X118)
| thing(X118,skc11) ),
inference(resolution,[status(thm)],[clause39,c91]) ).
cnf(c191,plain,
thing(skc12,skc11),
inference(resolution,[status(thm)],[c137,clause83]) ).
cnf(c192,plain,
singleton(skc12,skc11),
inference(resolution,[status(thm)],[c191,clause4]) ).
cnf(c454,plain,
( skc12 != X667
| skc11 != X666
| singleton(X667,X666) ),
inference(resolution,[status(thm)],[c6,c192]) ).
cnf(c692,plain,
( skc12 != X668
| singleton(X668,skc11) ),
inference(resolution,[status(thm)],[c454,reflexivity]) ).
cnf(c136,plain,
( ~ accessible_world(skc8,X114)
| thing(X114,skc14) ),
inference(resolution,[status(thm)],[clause39,c95]) ).
cnf(c186,plain,
thing(skc12,skc14),
inference(resolution,[status(thm)],[c136,clause83]) ).
cnf(c187,plain,
singleton(skc12,skc14),
inference(resolution,[status(thm)],[c186,clause4]) ).
cnf(c453,plain,
( skc12 != X664
| skc14 != X663
| singleton(X664,X663) ),
inference(resolution,[status(thm)],[c6,c187]) ).
cnf(c690,plain,
( skc12 != X665
| singleton(X665,skc14) ),
inference(resolution,[status(thm)],[c453,reflexivity]) ).
cnf(c135,plain,
( ~ accessible_world(skc8,X110)
| thing(X110,skc12) ),
inference(resolution,[status(thm)],[clause39,c46]) ).
cnf(c175,plain,
thing(skc12,skc12),
inference(resolution,[status(thm)],[c135,clause83]) ).
cnf(c183,plain,
singleton(skc12,skc12),
inference(resolution,[status(thm)],[c175,clause4]) ).
cnf(c452,plain,
( skc12 != X655
| skc12 != X654
| singleton(X655,X654) ),
inference(resolution,[status(thm)],[c6,c183]) ).
cnf(c683,plain,
( skc12 != X657
| singleton(X657,skc12) ),
inference(resolution,[status(thm)],[c452,reflexivity]) ).
cnf(c682,plain,
( skc12 != X656
| singleton(X656,X656) ),
inference(factor,[status(thm)],[c452]) ).
cnf(c337,plain,
( ~ forename(skc8,skc11)
| ~ of(skc8,X653,skc10)
| ~ forename(skc8,X653)
| ~ entity(skc8,skc10)
| X653 = skc11 ),
inference(resolution,[status(thm)],[clause70,clause88]) ).
cnf(c65,plain,
thing(skc8,skc10),
inference(resolution,[status(thm)],[clause19,c63]) ).
cnf(c67,plain,
singleton(skc8,skc10),
inference(resolution,[status(thm)],[c65,clause4]) ).
cnf(c451,plain,
( skc8 != X651
| skc10 != X650
| singleton(X651,X650) ),
inference(resolution,[status(thm)],[c6,c67]) ).
cnf(c679,plain,
( skc8 != X652
| singleton(X652,skc10) ),
inference(resolution,[status(thm)],[c451,reflexivity]) ).
cnf(c139,plain,
( ~ accessible_world(skc8,X123)
| thing(X123,skc10) ),
inference(resolution,[status(thm)],[clause39,c65]) ).
cnf(c200,plain,
thing(skc12,skc10),
inference(resolution,[status(thm)],[c139,clause83]) ).
cnf(c201,plain,
singleton(skc12,skc10),
inference(resolution,[status(thm)],[c200,clause4]) ).
cnf(c450,plain,
( skc12 != X647
| skc10 != X646
| singleton(X647,X646) ),
inference(resolution,[status(thm)],[c6,c201]) ).
cnf(c676,plain,
( skc12 != X649
| singleton(X649,skc10) ),
inference(resolution,[status(thm)],[c450,reflexivity]) ).
cnf(c336,plain,
( ~ forename(skc8,skc14)
| ~ of(skc8,X648,skc15)
| ~ forename(skc8,X648)
| ~ entity(skc8,skc15)
| X648 = skc14 ),
inference(resolution,[status(thm)],[clause70,clause85]) ).
cnf(c446,plain,
( skc12 != X643
| skc15 != X644
| thing(X643,X644) ),
inference(resolution,[status(thm)],[c5,c195]) ).
cnf(c674,plain,
( skc12 != X645
| thing(X645,skc15) ),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c445,plain,
( skc12 != X637
| skc11 != X638
| thing(X637,X638) ),
inference(resolution,[status(thm)],[c5,c191]) ).
cnf(c672,plain,
( skc12 != X639
| thing(X639,skc11) ),
inference(resolution,[status(thm)],[c445,reflexivity]) ).
cnf(c444,plain,
( skc8 != X634
| skc9 != X635
| thing(X634,X635) ),
inference(resolution,[status(thm)],[c5,c54]) ).
cnf(c670,plain,
( skc8 != X636
| thing(X636,skc9) ),
inference(resolution,[status(thm)],[c444,reflexivity]) ).
cnf(c443,plain,
( skc12 != X625
| skc14 != X626
| thing(X625,X626) ),
inference(resolution,[status(thm)],[c5,c186]) ).
cnf(c664,plain,
( skc12 != X627
| thing(X627,skc14) ),
inference(resolution,[status(thm)],[c443,reflexivity]) ).
cnf(c442,plain,
( skc12 != X616
| skc10 != X617
| thing(X616,X617) ),
inference(resolution,[status(thm)],[c5,c200]) ).
cnf(c660,plain,
( skc12 != X624
| thing(X624,skc10) ),
inference(resolution,[status(thm)],[c442,reflexivity]) ).
cnf(c441,plain,
( skc8 != X613
| skc10 != X614
| thing(X613,X614) ),
inference(resolution,[status(thm)],[c5,c65]) ).
cnf(c658,plain,
( skc8 != X615
| thing(X615,skc10) ),
inference(resolution,[status(thm)],[c441,reflexivity]) ).
cnf(c440,plain,
( skc12 != X604
| skc9 != X605
| thing(X604,X605) ),
inference(resolution,[status(thm)],[c5,c145]) ).
cnf(c652,plain,
( skc12 != X606
| thing(X606,skc9) ),
inference(resolution,[status(thm)],[c440,reflexivity]) ).
cnf(c439,plain,
( skc8 != X601
| skc15 != X602
| thing(X601,X602) ),
inference(resolution,[status(thm)],[c5,c66]) ).
cnf(c650,plain,
( skc8 != X603
| thing(X603,skc15) ),
inference(resolution,[status(thm)],[c439,reflexivity]) ).
cnf(c438,plain,
( skc8 != X594
| skc11 != X595
| thing(X594,X595) ),
inference(resolution,[status(thm)],[c5,c91]) ).
cnf(c646,plain,
( skc8 != X596
| thing(X596,skc11) ),
inference(resolution,[status(thm)],[c438,reflexivity]) ).
cnf(c437,plain,
( skc8 != X587
| skc14 != X588
| thing(X587,X588) ),
inference(resolution,[status(thm)],[c5,c95]) ).
cnf(c641,plain,
( skc8 != X593
| thing(X593,skc14) ),
inference(resolution,[status(thm)],[c437,reflexivity]) ).
cnf(c436,plain,
( skc8 != X584
| skc12 != X585
| thing(X584,X585) ),
inference(resolution,[status(thm)],[c5,c46]) ).
cnf(c639,plain,
( skc8 != X586
| thing(X586,skc12) ),
inference(resolution,[status(thm)],[c436,reflexivity]) ).
cnf(c435,plain,
( skc12 != X576
| skc12 != X577
| thing(X576,X577) ),
inference(resolution,[status(thm)],[c5,c175]) ).
cnf(c635,plain,
( skc12 != X579
| thing(X579,skc12) ),
inference(resolution,[status(thm)],[c435,reflexivity]) ).
cnf(c634,plain,
( skc12 != X578
| thing(X578,X578) ),
inference(factor,[status(thm)],[c435]) ).
cnf(c434,plain,
( skc12 != X565
| skc13 != X566
| thing(X565,X566) ),
inference(resolution,[status(thm)],[c5,c124]) ).
cnf(c630,plain,
( skc12 != X567
| thing(X567,skc13) ),
inference(resolution,[status(thm)],[c434,reflexivity]) ).
cnf(c433,plain,
( skc8 != X562
| skc13 != X563
| thing(X562,X563) ),
inference(resolution,[status(thm)],[c5,c39]) ).
cnf(c628,plain,
( skc8 != X564
| thing(X564,skc13) ),
inference(resolution,[status(thm)],[c433,reflexivity]) ).
cnf(c430,plain,
( skc12 != X556
| skc9 != X555
| eventuality(X556,X555) ),
inference(resolution,[status(thm)],[c4,c142]) ).
cnf(c624,plain,
( skc12 != X557
| eventuality(X557,skc9) ),
inference(resolution,[status(thm)],[c430,reflexivity]) ).
cnf(c429,plain,
( skc8 != X549
| skc13 != X548
| eventuality(X549,X548) ),
inference(resolution,[status(thm)],[c4,c38]) ).
cnf(c620,plain,
( skc8 != X554
| eventuality(X554,skc13) ),
inference(resolution,[status(thm)],[c429,reflexivity]) ).
cnf(c427,plain,
( skc12 != X546
| skc13 != X545
| eventuality(X546,X545) ),
inference(resolution,[status(thm)],[c4,c121]) ).
cnf(c618,plain,
( skc12 != X547
| eventuality(X547,skc13) ),
inference(resolution,[status(thm)],[c427,reflexivity]) ).
cnf(c426,plain,
( skc8 != X539
| skc9 != X538
| eventuality(X539,X538) ),
inference(resolution,[status(thm)],[c4,c51]) ).
cnf(c612,plain,
( skc8 != X540
| eventuality(X540,skc9) ),
inference(resolution,[status(thm)],[c426,reflexivity]) ).
cnf(c422,plain,
( skc12 != X535
| skc9 != X536
| event(X535,X536) ),
inference(resolution,[status(thm)],[c3,c141]) ).
cnf(c610,plain,
( skc12 != X537
| event(X537,skc9) ),
inference(resolution,[status(thm)],[c422,reflexivity]) ).
cnf(c421,plain,
( skc8 != X528
| skc9 != X529
| event(X528,X529) ),
inference(resolution,[status(thm)],[c3,c52]) ).
cnf(c604,plain,
( skc8 != X530
| event(X530,skc9) ),
inference(resolution,[status(thm)],[c421,reflexivity]) ).
cnf(c420,plain,
( skc12 != X521
| skc13 != X522
| event(X521,X522) ),
inference(resolution,[status(thm)],[c3,c120]) ).
cnf(c598,plain,
( skc12 != X527
| event(X527,skc13) ),
inference(resolution,[status(thm)],[c420,reflexivity]) ).
cnf(c419,plain,
( skc8 != X518
| skc13 != X519
| event(X518,X519) ),
inference(resolution,[status(thm)],[c3,clause76]) ).
cnf(c596,plain,
( skc8 != X520
| event(X520,skc13) ),
inference(resolution,[status(thm)],[c419,reflexivity]) ).
cnf(c582,plain,
( ~ accessible_world(skc12,X512)
| of(X512,skc11,skc10) ),
inference(resolution,[status(thm)],[c580,clause68]) ).
cnf(c579,plain,
( ~ accessible_world(skc12,X511)
| of(X511,skc14,skc15) ),
inference(resolution,[status(thm)],[c577,clause68]) ).
cnf(c572,plain,
( ~ accessible_world(skc12,X510)
| theme(X510,skc13,skc12) ),
inference(resolution,[status(thm)],[c571,clause67]) ).
cnf(c569,plain,
( ~ accessible_world(skc12,X505)
| agent(X505,skc13,skc15) ),
inference(resolution,[status(thm)],[c568,clause66]) ).
cnf(clause40,axiom,
( ~ accessible_world(X96,X95)
| ~ singleton(X96,X97)
| singleton(X95,X97) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c378,plain,
( ~ accessible_world(skc12,X495)
| singleton(X495,skf2(X496)) ),
inference(resolution,[status(thm)],[c372,clause40]) ).
cnf(c377,plain,
( ~ accessible_world(skc12,X489)
| present(X489,skf2(X490)) ),
inference(resolution,[status(thm)],[c369,clause44]) ).
cnf(clause42,axiom,
( ~ accessible_world(X106,X105)
| ~ nonexistent(X106,X107)
| nonexistent(X105,X107) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c376,plain,
( ~ accessible_world(skc12,X488)
| nonexistent(X488,skf2(X487)) ),
inference(resolution,[status(thm)],[c367,clause42]) ).
cnf(c374,plain,
( ~ accessible_world(skc12,X485)
| unisex(X485,skf2(X486)) ),
inference(resolution,[status(thm)],[c366,clause43]) ).
cnf(c373,plain,
( ~ accessible_world(skc12,X483)
| thing(X483,skf2(X484)) ),
inference(resolution,[status(thm)],[c365,clause39]) ).
cnf(c370,plain,
( ~ accessible_world(skc12,X481)
| specific(X481,skf2(X482)) ),
inference(resolution,[status(thm)],[c364,clause41]) ).
cnf(clause38,axiom,
( ~ accessible_world(X89,X88)
| ~ eventuality(X89,X90)
| eventuality(X88,X90) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c368,plain,
( ~ accessible_world(skc12,X475)
| eventuality(X475,skf2(X476)) ),
inference(resolution,[status(thm)],[c362,clause38]) ).
cnf(c363,plain,
( ~ accessible_world(skc12,X474)
| event(X474,skf2(X473)) ),
inference(resolution,[status(thm)],[c361,clause37]) ).
cnf(clause36,axiom,
( ~ accessible_world(X78,X77)
| ~ smoke(X78,X79)
| smoke(X77,X79) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c360,plain,
( ~ accessible_world(skc12,X472)
| smoke(X472,skf2(X471)) ),
inference(resolution,[status(thm)],[c359,clause36]) ).
cnf(c530,plain,
( ~ accessible_world(skc12,X470)
| jules_forename(X470,skc11) ),
inference(resolution,[status(thm)],[c529,clause65]) ).
cnf(c522,plain,
( ~ accessible_world(skc12,X469)
| vincent_forename(X469,skc14) ),
inference(resolution,[status(thm)],[c520,clause64]) ).
cnf(clause63,axiom,
( ~ accessible_world(X221,X220)
| ~ relname(X221,X222)
| relname(X220,X222) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
cnf(c504,plain,
( ~ accessible_world(skc12,X464)
| relname(X464,skc11) ),
inference(resolution,[status(thm)],[c501,clause63]) ).
cnf(c500,plain,
( ~ accessible_world(skc12,X463)
| forename(X463,skc11) ),
inference(resolution,[status(thm)],[c499,clause62]) ).
cnf(c497,plain,
( ~ accessible_world(skc12,X462)
| relname(X462,skc14) ),
inference(resolution,[status(thm)],[c496,clause63]) ).
cnf(c495,plain,
( ~ accessible_world(skc12,X461)
| forename(X461,skc14) ),
inference(resolution,[status(thm)],[c483,clause62]) ).
cnf(clause56,axiom,
( ~ accessible_world(X183,X182)
| ~ existent(X183,X184)
| existent(X182,X184) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
cnf(c404,plain,
( ~ accessible_world(skc12,X460)
| existent(X460,skc15) ),
inference(resolution,[status(thm)],[c400,clause56]) ).
cnf(clause58,axiom,
( ~ accessible_world(X197,X196)
| ~ living(X197,X198)
| living(X196,X198) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
cnf(c402,plain,
( ~ accessible_world(skc12,X455)
| living(X455,skc15) ),
inference(resolution,[status(thm)],[c395,clause58]) ).
cnf(clause55,axiom,
( ~ accessible_world(X179,X178)
| ~ entity(X179,X180)
| entity(X178,X180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
cnf(c399,plain,
( ~ accessible_world(skc12,X454)
| entity(X454,skc15) ),
inference(resolution,[status(thm)],[c394,clause55]) ).
cnf(clause57,axiom,
( ~ accessible_world(X190,X189)
| ~ impartial(X190,X191)
| impartial(X189,X191) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
cnf(c397,plain,
( ~ accessible_world(skc12,X453)
| impartial(X453,skc15) ),
inference(resolution,[status(thm)],[c392,clause57]) ).
cnf(clause54,axiom,
( ~ accessible_world(X174,X173)
| ~ organism(X174,X175)
| organism(X173,X175) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
cnf(c393,plain,
( ~ accessible_world(skc12,X452)
| organism(X452,skc15) ),
inference(resolution,[status(thm)],[c388,clause54]) ).
cnf(clause60,axiom,
( ~ accessible_world(X210,X209)
| ~ animate(X210,X211)
| animate(X209,X211) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
cnf(c391,plain,
( ~ accessible_world(skc12,X451)
| animate(X451,skc15) ),
inference(resolution,[status(thm)],[c387,clause60]) ).
cnf(clause59,axiom,
( ~ accessible_world(X204,X203)
| ~ human(X204,X205)
| human(X203,X205) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
cnf(c390,plain,
( ~ accessible_world(skc12,X446)
| human(X446,skc15) ),
inference(resolution,[status(thm)],[c386,clause59]) ).
cnf(clause61,axiom,
( ~ accessible_world(X213,X212)
| ~ male(X213,X214)
| male(X212,X214) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
cnf(c389,plain,
( ~ accessible_world(skc12,X445)
| male(X445,skc15) ),
inference(resolution,[status(thm)],[c381,clause61]) ).
cnf(clause53,axiom,
( ~ accessible_world(X167,X166)
| ~ human_person(X167,X168)
| human_person(X166,X168) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(c385,plain,
( ~ accessible_world(skc12,X444)
| human_person(X444,skc15) ),
inference(resolution,[status(thm)],[c380,clause53]) ).
cnf(c382,plain,
( ~ accessible_world(skc12,X439)
| man(X439,skc15) ),
inference(resolution,[status(thm)],[c379,clause52]) ).
cnf(c358,plain,
( ~ accessible_world(skc12,X438)
| existent(X438,skc10) ),
inference(resolution,[status(thm)],[c354,clause56]) ).
cnf(c356,plain,
( ~ accessible_world(skc12,X437)
| living(X437,skc10) ),
inference(resolution,[status(thm)],[c348,clause58]) ).
cnf(c353,plain,
( ~ accessible_world(skc12,X436)
| entity(X436,skc10) ),
inference(resolution,[status(thm)],[c347,clause55]) ).
cnf(c351,plain,
( ~ accessible_world(skc12,X435)
| impartial(X435,skc10) ),
inference(resolution,[status(thm)],[c345,clause57]) ).
cnf(c346,plain,
( ~ accessible_world(skc12,X430)
| organism(X430,skc10) ),
inference(resolution,[status(thm)],[c341,clause54]) ).
cnf(c344,plain,
( ~ accessible_world(skc12,X429)
| animate(X429,skc10) ),
inference(resolution,[status(thm)],[c340,clause60]) ).
cnf(c343,plain,
( ~ accessible_world(skc12,X428)
| human(X428,skc10) ),
inference(resolution,[status(thm)],[c339,clause59]) ).
cnf(c342,plain,
( ~ accessible_world(skc12,X427)
| male(X427,skc10) ),
inference(resolution,[status(thm)],[c333,clause61]) ).
cnf(c338,plain,
( ~ accessible_world(skc12,X426)
| human_person(X426,skc10) ),
inference(resolution,[status(thm)],[c332,clause53]) ).
cnf(c334,plain,
( ~ accessible_world(skc12,X421)
| man(X421,skc10) ),
inference(resolution,[status(thm)],[c331,clause52]) ).
cnf(c327,plain,
( ~ accessible_world(skc12,X420)
| state(X420,skc9) ),
inference(resolution,[status(thm)],[c326,clause51]) ).
cnf(clause50,axiom,
( ~ accessible_world(X150,X149)
| ~ general(X150,X151)
| general(X149,X151) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c311,plain,
( ~ accessible_world(skc12,X414)
| general(X414,skc14) ),
inference(resolution,[status(thm)],[c305,clause50]) ).
cnf(clause49,axiom,
( ~ accessible_world(X144,X143)
| ~ nonhuman(X144,X145)
| nonhuman(X143,X145) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c309,plain,
( ~ accessible_world(skc12,X413)
| nonhuman(X413,skc14) ),
inference(resolution,[status(thm)],[c304,clause49]) ).
cnf(clause48,axiom,
( ~ accessible_world(X138,X137)
| ~ abstraction(X138,X139)
| abstraction(X137,X139) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(c306,plain,
( ~ accessible_world(skc12,X407)
| abstraction(X407,skc14) ),
inference(resolution,[status(thm)],[c302,clause48]) ).
cnf(c301,plain,
( ~ accessible_world(skc12,X406)
| relation(X406,skc14) ),
inference(resolution,[status(thm)],[c300,clause47]) ).
cnf(c299,plain,
( ~ accessible_world(skc8,X405)
| relname(X405,skc14) ),
inference(resolution,[status(thm)],[clause63,c83]) ).
cnf(c298,plain,
( ~ accessible_world(skc8,X400)
| relname(X400,skc11) ),
inference(resolution,[status(thm)],[clause63,c84]) ).
cnf(c296,plain,
( ~ accessible_world(skc12,X399)
| general(X399,skc11) ),
inference(resolution,[status(thm)],[c289,clause50]) ).
cnf(c294,plain,
( ~ accessible_world(skc12,X398)
| nonhuman(X398,skc11) ),
inference(resolution,[status(thm)],[c288,clause49]) ).
cnf(c290,plain,
( ~ accessible_world(skc12,X387)
| abstraction(X387,skc11) ),
inference(resolution,[status(thm)],[c286,clause48]) ).
cnf(c285,plain,
( ~ accessible_world(skc12,X386)
| relation(X386,skc11) ),
inference(resolution,[status(thm)],[c284,clause47]) ).
cnf(c283,plain,
( ~ accessible_world(skc8,X385)
| male(X385,skc15) ),
inference(resolution,[status(thm)],[clause61,c82]) ).
cnf(c282,plain,
( ~ accessible_world(skc8,X380)
| male(X380,skc10) ),
inference(resolution,[status(thm)],[clause61,c81]) ).
cnf(c281,plain,
( ~ accessible_world(skc12,X379)
| general(X379,skc12) ),
inference(resolution,[status(thm)],[c276,clause50]) ).
cnf(c279,plain,
( ~ accessible_world(skc12,X378)
| nonhuman(X378,skc12) ),
inference(resolution,[status(thm)],[c275,clause49]) ).
cnf(c277,plain,
( ~ accessible_world(skc12,X377)
| abstraction(X377,skc12) ),
inference(resolution,[status(thm)],[c271,clause48]) ).
cnf(c273,plain,
( ~ accessible_world(skc8,X372)
| animate(X372,skc10) ),
inference(resolution,[status(thm)],[clause60,c80]) ).
cnf(c272,plain,
( ~ accessible_world(skc8,X371)
| animate(X371,skc15) ),
inference(resolution,[status(thm)],[clause60,c79]) ).
cnf(c270,plain,
( ~ accessible_world(skc12,X370)
| relation(X370,skc12) ),
inference(resolution,[status(thm)],[c268,clause47]) ).
cnf(c269,plain,
( ~ accessible_world(skc12,X365)
| proposition(X365,skc12) ),
inference(resolution,[status(thm)],[c267,clause46]) ).
cnf(c266,plain,
( ~ accessible_world(skc8,X364)
| human(X364,skc10) ),
inference(resolution,[status(thm)],[clause59,c78]) ).
cnf(c265,plain,
( ~ accessible_world(skc8,X363)
| human(X363,skc15) ),
inference(resolution,[status(thm)],[clause59,c77]) ).
cnf(c264,plain,
( ~ accessible_world(skc12,X358)
| think_believe_consider(X358,skc13) ),
inference(resolution,[status(thm)],[c263,clause45]) ).
cnf(c262,plain,
( ~ accessible_world(skc8,X357)
| living(X357,skc10) ),
inference(resolution,[status(thm)],[clause58,c75]) ).
cnf(c261,plain,
( ~ accessible_world(skc8,X356)
| living(X356,skc15) ),
inference(resolution,[status(thm)],[clause58,c76]) ).
cnf(c260,plain,
( ~ accessible_world(skc12,X351)
| present(X351,skc13) ),
inference(resolution,[status(thm)],[c259,clause44]) ).
cnf(c258,plain,
( ~ accessible_world(skc8,X350)
| impartial(X350,skc15) ),
inference(resolution,[status(thm)],[clause57,c74]) ).
cnf(c257,plain,
( ~ accessible_world(skc8,X349)
| impartial(X349,skc10) ),
inference(resolution,[status(thm)],[clause57,c73]) ).
cnf(c255,plain,
( ~ accessible_world(skc8,X344)
| existent(X344,skc15) ),
inference(resolution,[status(thm)],[clause56,c72]) ).
cnf(c254,plain,
( ~ accessible_world(skc8,X343)
| existent(X343,skc10) ),
inference(resolution,[status(thm)],[clause56,c71]) ).
cnf(c252,plain,
( ~ accessible_world(skc12,X342)
| unisex(X342,skc11) ),
inference(resolution,[status(thm)],[c251,clause43]) ).
cnf(c249,plain,
( ~ accessible_world(skc12,X337)
| unisex(X337,skc14) ),
inference(resolution,[status(thm)],[c246,clause43]) ).
cnf(c248,plain,
( ~ accessible_world(skc8,X336)
| entity(X336,skc15) ),
inference(resolution,[status(thm)],[clause55,c64]) ).
cnf(c1,axiom,
( X334 != X333
| skf4(X334) = skf4(X333) ),
theory(equality) ).
cnf(c247,plain,
( ~ accessible_world(skc8,X332)
| entity(X332,skc10) ),
inference(resolution,[status(thm)],[clause55,c63]) ).
cnf(c244,plain,
( ~ accessible_world(skc12,X331)
| unisex(X331,skc12) ),
inference(resolution,[status(thm)],[c243,clause43]) ).
cnf(c242,plain,
( ~ accessible_world(skc8,X330)
| organism(X330,skc15) ),
inference(resolution,[status(thm)],[clause54,c61]) ).
cnf(c0,axiom,
( X328 != X327
| skf2(X328) = skf2(X327) ),
theory(equality) ).
cnf(c241,plain,
( ~ accessible_world(skc8,X326)
| organism(X326,skc10) ),
inference(resolution,[status(thm)],[clause54,c62]) ).
cnf(transitivity,axiom,
( X320 != X321
| X321 != X322
| X320 = X322 ),
theory(equality) ).
cnf(c239,plain,
( ~ accessible_world(skc8,X319)
| human_person(X319,skc10) ),
inference(resolution,[status(thm)],[clause53,c59]) ).
cnf(c238,plain,
( ~ accessible_world(skc8,X318)
| human_person(X318,skc15) ),
inference(resolution,[status(thm)],[clause53,c60]) ).
cnf(clause34,axiom,
( ~ nonexistent(X70,X69)
| ~ existent(X70,X69) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c403,plain,
~ nonexistent(skc12,skc15),
inference(resolution,[status(thm)],[c400,clause34]) ).
cnf(clause31,axiom,
( ~ male(X64,X63)
| ~ unisex(X64,X63) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c375,plain,
~ male(skc12,skf2(X286)),
inference(resolution,[status(thm)],[c366,clause31]) ).
cnf(clause32,axiom,
( ~ general(X66,X65)
| ~ specific(X66,X65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c371,plain,
~ general(skc12,skf2(X284)),
inference(resolution,[status(thm)],[c364,clause32]) ).
cnf(c357,plain,
~ nonexistent(skc12,skc10),
inference(resolution,[status(thm)],[c354,clause34]) ).
cnf(c232,plain,
( ~ accessible_world(skc12,X258)
| specific(X258,skc15) ),
inference(resolution,[status(thm)],[c231,clause41]) ).
cnf(c226,plain,
( ~ accessible_world(skc12,X251)
| specific(X251,skc10) ),
inference(resolution,[status(thm)],[c225,clause41]) ).
cnf(c224,plain,
( ~ accessible_world(skc8,X250)
| general(X250,skc11) ),
inference(resolution,[status(thm)],[clause50,c93]) ).
cnf(c223,plain,
( ~ accessible_world(skc8,X245)
| general(X245,skc12) ),
inference(resolution,[status(thm)],[clause50,c49]) ).
cnf(c222,plain,
( ~ accessible_world(skc8,X244)
| general(X244,skc14) ),
inference(resolution,[status(thm)],[clause50,c97]) ).
cnf(c219,plain,
( ~ accessible_world(skc8,X239)
| nonhuman(X239,skc14) ),
inference(resolution,[status(thm)],[clause49,c96]) ).
cnf(c218,plain,
( ~ accessible_world(skc8,X238)
| nonhuman(X238,skc11) ),
inference(resolution,[status(thm)],[clause49,c92]) ).
cnf(c217,plain,
( ~ accessible_world(skc8,X237)
| nonhuman(X237,skc12) ),
inference(resolution,[status(thm)],[clause49,c48]) ).
cnf(c214,plain,
( ~ accessible_world(skc8,X232)
| abstraction(X232,skc14) ),
inference(resolution,[status(thm)],[clause48,c89]) ).
cnf(c213,plain,
( ~ accessible_world(skc8,X231)
| abstraction(X231,skc11) ),
inference(resolution,[status(thm)],[clause48,c88]) ).
cnf(c212,plain,
( ~ accessible_world(skc8,X227)
| abstraction(X227,skc12) ),
inference(resolution,[status(thm)],[clause48,c45]) ).
cnf(clause33,axiom,
( ~ human(X68,X67)
| ~ nonhuman(X68,X67) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c310,plain,
~ human(skc12,skc14),
inference(resolution,[status(thm)],[c304,clause33]) ).
cnf(c208,plain,
( ~ accessible_world(skc8,X219)
| relation(X219,skc12) ),
inference(resolution,[status(thm)],[clause47,c44]) ).
cnf(c295,plain,
~ human(skc12,skc11),
inference(resolution,[status(thm)],[c288,clause33]) ).
cnf(c280,plain,
~ human(skc12,skc12),
inference(resolution,[status(thm)],[c275,clause33]) ).
cnf(c203,plain,
( ~ accessible_world(skc12,X207)
| singleton(X207,skc10) ),
inference(resolution,[status(thm)],[c201,clause40]) ).
cnf(c202,plain,
( ~ accessible_world(skc12,X206)
| thing(X206,skc10) ),
inference(resolution,[status(thm)],[c200,clause39]) ).
cnf(c199,plain,
( ~ accessible_world(skc12,X202)
| singleton(X202,skc15) ),
inference(resolution,[status(thm)],[c196,clause40]) ).
cnf(c197,plain,
( ~ accessible_world(skc12,X200)
| thing(X200,skc15) ),
inference(resolution,[status(thm)],[c195,clause39]) ).
cnf(c194,plain,
( ~ accessible_world(skc12,X199)
| singleton(X199,skc11) ),
inference(resolution,[status(thm)],[c192,clause40]) ).
cnf(c193,plain,
( ~ accessible_world(skc12,X195)
| thing(X195,skc11) ),
inference(resolution,[status(thm)],[c191,clause39]) ).
cnf(c189,plain,
( ~ accessible_world(skc12,X193)
| singleton(X193,skc14) ),
inference(resolution,[status(thm)],[c187,clause40]) ).
cnf(c188,plain,
( ~ accessible_world(skc12,X192)
| thing(X192,skc14) ),
inference(resolution,[status(thm)],[c186,clause39]) ).
cnf(c185,plain,
( ~ accessible_world(skc12,X188)
| singleton(X188,skc12) ),
inference(resolution,[status(thm)],[c183,clause40]) ).
cnf(c184,plain,
( ~ accessible_world(skc12,X187)
| thing(X187,skc12) ),
inference(resolution,[status(thm)],[c175,clause39]) ).
cnf(c182,plain,
( ~ accessible_world(skc8,X186)
| unisex(X186,skc9) ),
inference(resolution,[status(thm)],[clause43,c56]) ).
cnf(c181,plain,
( ~ accessible_world(skc12,X185)
| unisex(X185,skc9) ),
inference(resolution,[status(thm)],[clause43,c146]) ).
cnf(c253,plain,
~ male(skc12,skc11),
inference(resolution,[status(thm)],[c251,clause31]) ).
cnf(c250,plain,
~ male(skc12,skc14),
inference(resolution,[status(thm)],[c246,clause31]) ).
cnf(c245,plain,
~ male(skc12,skc12),
inference(resolution,[status(thm)],[c243,clause31]) ).
cnf(c177,plain,
( ~ accessible_world(skc8,X172)
| unisex(X172,skc13) ),
inference(resolution,[status(thm)],[clause43,c43]) ).
cnf(c176,plain,
( ~ accessible_world(skc12,X171)
| unisex(X171,skc13) ),
inference(resolution,[status(thm)],[clause43,c126]) ).
cnf(c173,plain,
( ~ accessible_world(skc12,X170)
| nonexistent(X170,skc9) ),
inference(resolution,[status(thm)],[clause42,c147]) ).
cnf(c172,plain,
( ~ accessible_world(skc12,X169)
| nonexistent(X169,skc13) ),
inference(resolution,[status(thm)],[clause42,c125]) ).
cnf(c171,plain,
( ~ accessible_world(skc8,X165)
| nonexistent(X165,skc13) ),
inference(resolution,[status(thm)],[clause42,c42]) ).
cnf(c170,plain,
( ~ accessible_world(skc8,X164)
| nonexistent(X164,skc9) ),
inference(resolution,[status(thm)],[clause42,c55]) ).
cnf(c167,plain,
( ~ accessible_world(skc12,X163)
| specific(X163,skc9) ),
inference(resolution,[status(thm)],[clause41,c144]) ).
cnf(c233,plain,
~ general(skc12,skc15),
inference(resolution,[status(thm)],[c231,clause32]) ).
cnf(c165,plain,
( ~ accessible_world(skc12,X158)
| specific(X158,skc13) ),
inference(resolution,[status(thm)],[clause41,c123]) ).
cnf(c164,plain,
( ~ accessible_world(skc8,X157)
| specific(X157,skc13) ),
inference(resolution,[status(thm)],[clause41,c41]) ).
cnf(c163,plain,
( ~ accessible_world(skc8,X153)
| specific(X153,skc9) ),
inference(resolution,[status(thm)],[clause41,c53]) ).
cnf(c227,plain,
~ general(skc12,skc10),
inference(resolution,[status(thm)],[c225,clause32]) ).
cnf(c161,plain,
( ~ accessible_world(skc12,X148)
| singleton(X148,skc9) ),
inference(resolution,[status(thm)],[c150,clause40]) ).
cnf(c159,plain,
( ~ accessible_world(skc8,X147)
| singleton(X147,skc11) ),
inference(resolution,[status(thm)],[clause40,c99]) ).
cnf(c158,plain,
( ~ accessible_world(skc8,X146)
| singleton(X146,skc12) ),
inference(resolution,[status(thm)],[clause40,c47]) ).
cnf(c157,plain,
( ~ accessible_world(skc8,X142)
| singleton(X142,skc15) ),
inference(resolution,[status(thm)],[clause40,c68]) ).
cnf(c156,plain,
( ~ accessible_world(skc12,X141)
| singleton(X141,skc13) ),
inference(resolution,[status(thm)],[clause40,c128]) ).
cnf(c155,plain,
( ~ accessible_world(skc8,X140)
| singleton(X140,skc13) ),
inference(resolution,[status(thm)],[clause40,c40]) ).
cnf(c154,plain,
( ~ accessible_world(skc8,X136)
| singleton(X136,skc14) ),
inference(resolution,[status(thm)],[clause40,c105]) ).
cnf(c153,plain,
( ~ accessible_world(skc8,X135)
| singleton(X135,skc9) ),
inference(resolution,[status(thm)],[clause40,c58]) ).
cnf(c152,plain,
( ~ accessible_world(skc8,X131)
| singleton(X131,skc10) ),
inference(resolution,[status(thm)],[clause40,c67]) ).
cnf(c151,plain,
( ~ accessible_world(skc12,X130)
| thing(X130,skc9) ),
inference(resolution,[status(thm)],[c145,clause39]) ).
cnf(c148,plain,
( ~ accessible_world(skc12,X129)
| eventuality(X129,skc9) ),
inference(resolution,[status(thm)],[c142,clause38]) ).
cnf(c143,plain,
( ~ accessible_world(skc12,X128)
| event(X128,skc9) ),
inference(resolution,[status(thm)],[c141,clause37]) ).
cnf(c140,plain,
( ~ accessible_world(skc8,X124)
| thing(X124,skc9) ),
inference(resolution,[status(thm)],[clause39,c54]) ).
cnf(c134,plain,
( ~ accessible_world(skc12,X109)
| thing(X109,skc13) ),
inference(resolution,[status(thm)],[clause39,c124]) ).
cnf(c133,plain,
( ~ accessible_world(skc8,X108)
| thing(X108,skc13) ),
inference(resolution,[status(thm)],[clause39,c39]) ).
cnf(c131,plain,
( ~ accessible_world(skc8,X104)
| eventuality(X104,skc13) ),
inference(resolution,[status(thm)],[clause38,c38]) ).
cnf(c130,plain,
( ~ accessible_world(skc8,X103)
| eventuality(X103,skc9) ),
inference(resolution,[status(thm)],[clause38,c51]) ).
cnf(c129,plain,
( ~ accessible_world(skc12,X102)
| eventuality(X102,skc13) ),
inference(resolution,[status(thm)],[clause38,c121]) ).
cnf(c122,plain,
( ~ accessible_world(skc12,X101)
| event(X101,skc13) ),
inference(resolution,[status(thm)],[c120,clause37]) ).
cnf(c160,plain,
~ male(skc12,skc9),
inference(resolution,[status(thm)],[c146,clause31]) ).
cnf(c149,plain,
~ general(skc12,skc9),
inference(resolution,[status(thm)],[c144,clause32]) ).
cnf(c132,plain,
~ male(skc12,skc13),
inference(resolution,[status(thm)],[c126,clause31]) ).
cnf(c127,plain,
~ general(skc12,skc13),
inference(resolution,[status(thm)],[c123,clause32]) ).
cnf(c37,axiom,
( X82 != X81
| ~ actual_world(X82)
| actual_world(X81) ),
theory(equality) ).
cnf(symmetry,axiom,
( X75 != X76
| X76 = X75 ),
theory(equality) ).
cnf(clause35,axiom,
( ~ be(X72,X71,X74,X73)
| X74 = X73 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c114,plain,
~ nonexistent(skc8,skc15),
inference(resolution,[status(thm)],[clause34,c72]) ).
cnf(c113,plain,
~ nonexistent(skc8,skc10),
inference(resolution,[status(thm)],[clause34,c71]) ).
cnf(c112,plain,
~ human(skc8,skc14),
inference(resolution,[status(thm)],[clause33,c96]) ).
cnf(c111,plain,
~ human(skc8,skc11),
inference(resolution,[status(thm)],[clause33,c92]) ).
cnf(c110,plain,
~ human(skc8,skc12),
inference(resolution,[status(thm)],[clause33,c48]) ).
cnf(c109,plain,
~ general(skc8,skc10),
inference(resolution,[status(thm)],[clause32,c69]) ).
cnf(c108,plain,
~ general(skc8,skc13),
inference(resolution,[status(thm)],[clause32,c41]) ).
cnf(c107,plain,
~ general(skc8,skc15),
inference(resolution,[status(thm)],[clause32,c70]) ).
cnf(c106,plain,
~ general(skc8,skc9),
inference(resolution,[status(thm)],[clause32,c53]) ).
cnf(c104,plain,
~ male(skc8,skc9),
inference(resolution,[status(thm)],[clause31,c56]) ).
cnf(c103,plain,
~ male(skc8,skc11),
inference(resolution,[status(thm)],[clause31,c90]) ).
cnf(c102,plain,
~ male(skc8,skc14),
inference(resolution,[status(thm)],[clause31,c94]) ).
cnf(c101,plain,
~ male(skc8,skc12),
inference(resolution,[status(thm)],[clause31,c50]) ).
cnf(c100,plain,
~ male(skc8,skc13),
inference(resolution,[status(thm)],[clause31,c43]) ).
cnf(clause30,axiom,
( ~ jules_forename(X62,X61)
| forename(X62,X61) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,axiom,
( ~ vincent_forename(X60,X59)
| forename(X60,X59) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(clause72,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : NLP254-1 : TPTP v8.1.2. Released v2.4.0.
% 0.12/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n020.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 13:25:53 EDT 2024
% 0.15/0.37 % CPUTime :
% 5.55/5.78 % Version: 1.5
% 5.55/5.78 % SZS status Satisfiable
% 5.55/5.78 % SZS output start Saturation
% See solution above
% 5.65/5.82
% 5.65/5.82 % Initial clauses : 136
% 5.65/5.82 % Processed clauses : 982
% 5.65/5.82 % Factors computed : 125
% 5.65/5.82 % Resolvents computed: 1059
% 5.65/5.82 % Tautologies deleted: 3
% 5.65/5.82 % Forward subsumed : 335
% 5.65/5.82 % Backward subsumed : 46
% 5.65/5.82 % -------- CPU Time ---------
% 5.65/5.82 % User time : 5.424 s
% 5.65/5.82 % System time : 0.020 s
% 5.65/5.82 % Total time : 5.444 s
%------------------------------------------------------------------------------