%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP258-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:55 EDT 2024
% Result : Unsatisfiable 2.55s 2.72s
% Output : Refutation 2.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 25
% Syntax : Number of clauses : 84 ( 28 unt; 0 nHn; 79 RR)
% Number of literals : 767 ( 0 equ; 710 neg)
% Maximal clause size : 33 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-1 aty)
% Number of variables : 122 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause72,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
cnf(clause81,negated_conjecture,
man(skc8,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
cnf(clause79,negated_conjecture,
jules_forename(skc8,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
cnf(clause83,negated_conjecture,
accessible_world(skc8,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
cnf(clause73,negated_conjecture,
man(skc8,skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
cnf(clause74,negated_conjecture,
forename(skc8,skc14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
cnf(clause52,axiom,
( ~ accessible_world(X160,X161)
| ~ man(X160,X162)
| man(X161,X162) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c234,plain,
( ~ accessible_world(skc8,X259)
| man(X259,skc15) ),
inference(resolution,[status(thm)],[clause52,clause73]) ).
cnf(c331,plain,
man(skc12,skc15),
inference(resolution,[status(thm)],[c234,clause83]) ).
cnf(clause90,negated_conjecture,
( ~ man(skc12,X270)
| smoke(skc12,skf2(X271)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
cnf(c359,plain,
smoke(skc12,skf2(X272)),
inference(resolution,[status(thm)],[clause90,c331]) ).
cnf(clause91,negated_conjecture,
( ~ man(skc12,X275)
| present(skc12,skf2(X276)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
cnf(c369,plain,
present(skc12,skf2(X281)),
inference(resolution,[status(thm)],[clause91,c331]) ).
cnf(clause1,axiom,
( ~ smoke(X3,X4)
| event(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(c360,plain,
event(skc12,skf2(X273)),
inference(resolution,[status(thm)],[c359,clause1]) ).
cnf(c235,plain,
( ~ accessible_world(skc8,X287)
| man(X287,skc10) ),
inference(resolution,[status(thm)],[clause52,clause81]) ).
cnf(c379,plain,
man(skc12,skc10),
inference(resolution,[status(thm)],[c235,clause83]) ).
cnf(clause93,negated_conjecture,
( ~ man(skc12,X288)
| agent(skc12,skf2(X288),X288) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
cnf(c384,plain,
agent(skc12,skf2(skc10),skc10),
inference(resolution,[status(thm)],[clause93,c379]) ).
cnf(clause88,negated_conjecture,
of(skc8,skc11,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
cnf(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
cnf(clause86,negated_conjecture,
agent(skc8,skc13,skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
cnf(clause85,negated_conjecture,
of(skc8,skc14,skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
cnf(clause89,negated_conjecture,
be(skc8,skc9,skc10,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
cnf(clause95,negated_conjecture,
( ~ state(X309,X303)
| ~ man(X309,X311)
| ~ be(X309,X303,X311,X311)
| ~ smoke(X310,X300)
| ~ present(X310,X300)
| ~ agent(X310,X300,X311)
| ~ event(X310,X300)
| ~ forename(X309,X305)
| ~ jules_forename(X309,X305)
| ~ of(X309,X305,X311)
| ~ accessible_world(X309,X310)
| ~ proposition(X309,X310)
| ~ proposition(X309,X307)
| ~ accessible_world(X309,X307)
| ~ smoke(X307,X301)
| ~ present(X307,X301)
| ~ agent(X307,X301,skf4(X307))
| ~ event(X307,X301)
| ~ think_believe_consider(X309,X308)
| ~ present(X309,X308)
| ~ event(X309,X308)
| ~ theme(X309,X308,X307)
| ~ agent(X309,X306,X304)
| ~ agent(X309,X308,X304)
| ~ man(X309,X304)
| ~ of(X309,X302,X304)
| ~ vincent_forename(X309,X302)
| ~ forename(X309,X302)
| ~ theme(X309,X306,X310)
| ~ event(X309,X306)
| ~ present(X309,X306)
| ~ think_believe_consider(X309,X306)
| ~ actual_world(X309) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause95) ).
cnf(clause94,negated_conjecture,
( ~ state(X297,X291)
| ~ man(X297,X299)
| ~ be(X297,X291,X299,X299)
| ~ smoke(X298,X289)
| ~ present(X298,X289)
| ~ agent(X298,X289,X299)
| ~ event(X298,X289)
| ~ forename(X297,X293)
| ~ jules_forename(X297,X293)
| ~ of(X297,X293,X299)
| ~ accessible_world(X297,X298)
| ~ proposition(X297,X298)
| ~ proposition(X297,X295)
| ~ accessible_world(X297,X295)
| ~ think_believe_consider(X297,X290)
| ~ present(X297,X290)
| ~ event(X297,X290)
| ~ theme(X297,X290,X295)
| ~ agent(X297,X296,X294)
| ~ agent(X297,X290,X294)
| ~ man(X297,X294)
| ~ of(X297,X292,X294)
| ~ vincent_forename(X297,X292)
| ~ forename(X297,X292)
| ~ theme(X297,X296,X298)
| ~ event(X297,X296)
| ~ present(X297,X296)
| ~ think_believe_consider(X297,X296)
| ~ actual_world(X297)
| man(X295,skf4(X295)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause94) ).
cnf(c396,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(X672,X675)
| ~ present(X672,X675)
| ~ agent(X672,X675,skc10)
| ~ event(X672,X675)
| ~ forename(skc8,X678)
| ~ jules_forename(skc8,X678)
| ~ of(skc8,X678,skc10)
| ~ accessible_world(skc8,X672)
| ~ proposition(skc8,X672)
| ~ proposition(skc8,X673)
| ~ accessible_world(skc8,X673)
| ~ think_believe_consider(skc8,X677)
| ~ present(skc8,X677)
| ~ event(skc8,X677)
| ~ theme(skc8,X677,X673)
| ~ agent(skc8,X671,X674)
| ~ agent(skc8,X677,X674)
| ~ man(skc8,X674)
| ~ of(skc8,X676,X674)
| ~ vincent_forename(skc8,X676)
| ~ forename(skc8,X676)
| ~ theme(skc8,X671,X672)
| ~ event(skc8,X671)
| ~ present(skc8,X671)
| ~ think_believe_consider(skc8,X671)
| ~ actual_world(skc8)
| man(X673,skf4(X673)) ),
inference(resolution,[status(thm)],[clause94,clause89]) ).
cnf(c698,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(X1250,X1247)
| ~ present(X1250,X1247)
| ~ agent(X1250,X1247,skc10)
| ~ event(X1250,X1247)
| ~ forename(skc8,X1246)
| ~ jules_forename(skc8,X1246)
| ~ of(skc8,X1246,skc10)
| ~ accessible_world(skc8,X1250)
| ~ proposition(skc8,X1250)
| ~ think_believe_consider(skc8,X1251)
| ~ present(skc8,X1251)
| ~ event(skc8,X1251)
| ~ theme(skc8,X1251,X1250)
| ~ agent(skc8,X1251,X1248)
| ~ man(skc8,X1248)
| ~ of(skc8,X1249,X1248)
| ~ vincent_forename(skc8,X1249)
| ~ forename(skc8,X1249)
| ~ actual_world(skc8)
| man(X1250,skf4(X1250)) ),
inference(factor,[status(thm)],[c396]) ).
cnf(c1024,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(X1266,X1265)
| ~ present(X1266,X1265)
| ~ agent(X1266,X1265,skc10)
| ~ event(X1266,X1265)
| ~ forename(skc8,X1264)
| ~ jules_forename(skc8,X1264)
| ~ of(skc8,X1264,skc10)
| ~ accessible_world(skc8,X1266)
| ~ proposition(skc8,X1266)
| ~ think_believe_consider(skc8,X1267)
| ~ present(skc8,X1267)
| ~ event(skc8,X1267)
| ~ theme(skc8,X1267,X1266)
| ~ agent(skc8,X1267,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1266,skf4(X1266)) ),
inference(resolution,[status(thm)],[c698,clause85]) ).
cnf(c1028,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(X1274,X1276)
| ~ present(X1274,X1276)
| ~ agent(X1274,X1276,skc10)
| ~ event(X1274,X1276)
| ~ forename(skc8,X1275)
| ~ jules_forename(skc8,X1275)
| ~ of(skc8,X1275,skc10)
| ~ accessible_world(skc8,X1274)
| ~ proposition(skc8,X1274)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,X1274)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1274,skf4(X1274)) ),
inference(resolution,[status(thm)],[c1024,clause86]) ).
cnf(c1032,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1278)
| ~ present(skc12,X1278)
| ~ agent(skc12,X1278,skc10)
| ~ event(skc12,X1278)
| ~ forename(skc8,X1277)
| ~ jules_forename(skc8,X1277)
| ~ of(skc8,X1277,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1028,clause87]) ).
cnf(c1033,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1279)
| ~ present(skc12,X1279)
| ~ agent(skc12,X1279,skc10)
| ~ event(skc12,X1279)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1032,clause88]) ).
cnf(c1034,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1033,c384]) ).
cnf(c1035,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1034,c360]) ).
cnf(c1036,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1035,c369]) ).
cnf(c1037,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1036,c359]) ).
cnf(c1038,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1037,clause74]) ).
cnf(c1039,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1038,clause75]) ).
cnf(c1040,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1039,clause73]) ).
cnf(c1041,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1040,clause76]) ).
cnf(c1042,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1041,clause77]) ).
cnf(c1043,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1042,clause78]) ).
cnf(c1044,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1043,clause84]) ).
cnf(c1045,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1044,clause83]) ).
cnf(c1046,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1045,clause79]) ).
cnf(c1050,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1046,clause80]) ).
cnf(c1051,plain,
( ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1050,clause81]) ).
cnf(c1052,plain,
( ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1051,clause82]) ).
cnf(c1053,plain,
man(skc12,skf4(skc12)),
inference(resolution,[status(thm)],[c1052,clause72]) ).
cnf(c1054,plain,
agent(skc12,skf2(skf4(skc12)),skf4(skc12)),
inference(resolution,[status(thm)],[c1053,clause93]) ).
cnf(c1110,plain,
( ~ state(X1444,X1438)
| ~ man(X1444,X1435)
| ~ be(X1444,X1438,X1435,X1435)
| ~ smoke(X1436,X1439)
| ~ present(X1436,X1439)
| ~ agent(X1436,X1439,X1435)
| ~ event(X1436,X1439)
| ~ forename(X1444,X1442)
| ~ jules_forename(X1444,X1442)
| ~ of(X1444,X1442,X1435)
| ~ accessible_world(X1444,X1436)
| ~ proposition(X1444,X1436)
| ~ proposition(X1444,skc12)
| ~ accessible_world(X1444,skc12)
| ~ smoke(skc12,skf2(skf4(skc12)))
| ~ present(skc12,skf2(skf4(skc12)))
| ~ event(skc12,skf2(skf4(skc12)))
| ~ think_believe_consider(X1444,X1440)
| ~ present(X1444,X1440)
| ~ event(X1444,X1440)
| ~ theme(X1444,X1440,skc12)
| ~ agent(X1444,X1437,X1441)
| ~ agent(X1444,X1440,X1441)
| ~ man(X1444,X1441)
| ~ of(X1444,X1443,X1441)
| ~ vincent_forename(X1444,X1443)
| ~ forename(X1444,X1443)
| ~ theme(X1444,X1437,X1436)
| ~ event(X1444,X1437)
| ~ present(X1444,X1437)
| ~ think_believe_consider(X1444,X1437)
| ~ actual_world(X1444) ),
inference(resolution,[status(thm)],[c1054,clause95]) ).
cnf(c1158,plain,
( ~ state(X1511,X1507)
| ~ man(X1511,X1510)
| ~ be(X1511,X1507,X1510,X1510)
| ~ smoke(X1508,X1512)
| ~ present(X1508,X1512)
| ~ agent(X1508,X1512,X1510)
| ~ event(X1508,X1512)
| ~ forename(X1511,X1509)
| ~ jules_forename(X1511,X1509)
| ~ of(X1511,X1509,X1510)
| ~ accessible_world(X1511,X1508)
| ~ proposition(X1511,X1508)
| ~ proposition(X1511,skc12)
| ~ accessible_world(X1511,skc12)
| ~ smoke(skc12,skf2(skf4(skc12)))
| ~ present(skc12,skf2(skf4(skc12)))
| ~ think_believe_consider(X1511,X1516)
| ~ present(X1511,X1516)
| ~ event(X1511,X1516)
| ~ theme(X1511,X1516,skc12)
| ~ agent(X1511,X1513,X1515)
| ~ agent(X1511,X1516,X1515)
| ~ man(X1511,X1515)
| ~ of(X1511,X1514,X1515)
| ~ vincent_forename(X1511,X1514)
| ~ forename(X1511,X1514)
| ~ theme(X1511,X1513,X1508)
| ~ event(X1511,X1513)
| ~ present(X1511,X1513)
| ~ think_believe_consider(X1511,X1513)
| ~ actual_world(X1511) ),
inference(resolution,[status(thm)],[c1110,c360]) ).
cnf(c1174,plain,
( ~ state(X1519,X1525)
| ~ man(X1519,X1526)
| ~ be(X1519,X1525,X1526,X1526)
| ~ smoke(X1521,X1518)
| ~ present(X1521,X1518)
| ~ agent(X1521,X1518,X1526)
| ~ event(X1521,X1518)
| ~ forename(X1519,X1522)
| ~ jules_forename(X1519,X1522)
| ~ of(X1519,X1522,X1526)
| ~ accessible_world(X1519,X1521)
| ~ proposition(X1519,X1521)
| ~ proposition(X1519,skc12)
| ~ accessible_world(X1519,skc12)
| ~ smoke(skc12,skf2(skf4(skc12)))
| ~ think_believe_consider(X1519,X1523)
| ~ present(X1519,X1523)
| ~ event(X1519,X1523)
| ~ theme(X1519,X1523,skc12)
| ~ agent(X1519,X1520,X1517)
| ~ agent(X1519,X1523,X1517)
| ~ man(X1519,X1517)
| ~ of(X1519,X1524,X1517)
| ~ vincent_forename(X1519,X1524)
| ~ forename(X1519,X1524)
| ~ theme(X1519,X1520,X1521)
| ~ event(X1519,X1520)
| ~ present(X1519,X1520)
| ~ think_believe_consider(X1519,X1520)
| ~ actual_world(X1519) ),
inference(resolution,[status(thm)],[c1158,c369]) ).
cnf(c1176,plain,
( ~ state(X1534,X1536)
| ~ man(X1534,X1531)
| ~ be(X1534,X1536,X1531,X1531)
| ~ smoke(X1538,X1532)
| ~ present(X1538,X1532)
| ~ agent(X1538,X1532,X1531)
| ~ event(X1538,X1532)
| ~ forename(X1534,X1530)
| ~ jules_forename(X1534,X1530)
| ~ of(X1534,X1530,X1531)
| ~ accessible_world(X1534,X1538)
| ~ proposition(X1534,X1538)
| ~ proposition(X1534,skc12)
| ~ accessible_world(X1534,skc12)
| ~ think_believe_consider(X1534,X1535)
| ~ present(X1534,X1535)
| ~ event(X1534,X1535)
| ~ theme(X1534,X1535,skc12)
| ~ agent(X1534,X1537,X1533)
| ~ agent(X1534,X1535,X1533)
| ~ man(X1534,X1533)
| ~ of(X1534,X1539,X1533)
| ~ vincent_forename(X1534,X1539)
| ~ forename(X1534,X1539)
| ~ theme(X1534,X1537,X1538)
| ~ event(X1534,X1537)
| ~ present(X1534,X1537)
| ~ think_believe_consider(X1534,X1537)
| ~ actual_world(X1534) ),
inference(resolution,[status(thm)],[c1174,c359]) ).
cnf(c1178,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(X1647,X1651)
| ~ present(X1647,X1651)
| ~ agent(X1647,X1651,skc10)
| ~ event(X1647,X1651)
| ~ forename(skc8,X1648)
| ~ jules_forename(skc8,X1648)
| ~ of(skc8,X1648,skc10)
| ~ accessible_world(skc8,X1647)
| ~ proposition(skc8,X1647)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ think_believe_consider(skc8,X1646)
| ~ present(skc8,X1646)
| ~ event(skc8,X1646)
| ~ theme(skc8,X1646,skc12)
| ~ agent(skc8,X1645,X1650)
| ~ agent(skc8,X1646,X1650)
| ~ man(skc8,X1650)
| ~ of(skc8,X1649,X1650)
| ~ vincent_forename(skc8,X1649)
| ~ forename(skc8,X1649)
| ~ theme(skc8,X1645,X1647)
| ~ event(skc8,X1645)
| ~ present(skc8,X1645)
| ~ think_believe_consider(skc8,X1645)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1176,clause89]) ).
cnf(c1208,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1656)
| ~ present(skc12,X1656)
| ~ agent(skc12,X1656,skc10)
| ~ event(skc12,X1656)
| ~ forename(skc8,X1655)
| ~ jules_forename(skc8,X1655)
| ~ of(skc8,X1655,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,X1653)
| ~ present(skc8,X1653)
| ~ event(skc8,X1653)
| ~ theme(skc8,X1653,skc12)
| ~ agent(skc8,X1653,X1654)
| ~ man(skc8,X1654)
| ~ of(skc8,X1652,X1654)
| ~ vincent_forename(skc8,X1652)
| ~ forename(skc8,X1652)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c1178]) ).
cnf(c1211,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1670)
| ~ present(skc12,X1670)
| ~ agent(skc12,X1670,skc10)
| ~ event(skc12,X1670)
| ~ forename(skc8,X1668)
| ~ jules_forename(skc8,X1668)
| ~ of(skc8,X1668,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,X1669)
| ~ present(skc8,X1669)
| ~ event(skc8,X1669)
| ~ theme(skc8,X1669,skc12)
| ~ agent(skc8,X1669,skc15)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1208,clause85]) ).
cnf(c1213,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1672)
| ~ present(skc12,X1672)
| ~ agent(skc12,X1672,skc10)
| ~ event(skc12,X1672)
| ~ forename(skc8,X1671)
| ~ jules_forename(skc8,X1671)
| ~ of(skc8,X1671,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ theme(skc8,skc13,skc12)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1211,clause86]) ).
cnf(c1214,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1673)
| ~ present(skc12,X1673)
| ~ agent(skc12,X1673,skc10)
| ~ event(skc12,X1673)
| ~ forename(skc8,X1674)
| ~ jules_forename(skc8,X1674)
| ~ of(skc8,X1674,skc10)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1213,clause87]) ).
cnf(c1215,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,X1675)
| ~ present(skc12,X1675)
| ~ agent(skc12,X1675,skc10)
| ~ event(skc12,X1675)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1214,clause88]) ).
cnf(c1216,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1215,c384]) ).
cnf(c1217,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1216,c360]) ).
cnf(c1218,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ smoke(skc12,skf2(skc10))
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1217,c369]) ).
cnf(c1219,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1218,c359]) ).
cnf(c1220,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1219,clause74]) ).
cnf(c1221,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ man(skc8,skc15)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1220,clause75]) ).
cnf(c1222,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ event(skc8,skc13)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1221,clause73]) ).
cnf(c1223,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ present(skc8,skc13)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1222,clause76]) ).
cnf(c1224,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1223,clause77]) ).
cnf(c1225,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1224,clause78]) ).
cnf(c1226,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ accessible_world(skc8,skc12)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1225,clause84]) ).
cnf(c1227,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1226,clause83]) ).
cnf(c1228,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1227,clause79]) ).
cnf(c1229,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1228,clause80]) ).
cnf(c1230,plain,
( ~ state(skc8,skc9)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1229,clause81]) ).
cnf(c1231,plain,
~ actual_world(skc8),
inference(resolution,[status(thm)],[c1230,clause82]) ).
cnf(c1232,plain,
$false,
inference(resolution,[status(thm)],[c1231,clause72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP258-1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 13:35:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 2.55/2.72 % Version: 1.5
% 2.55/2.72 % SZS status Unsatisfiable
% 2.55/2.72 % SZS output start CNFRefutation
% See solution above
% 2.55/2.73
% 2.55/2.73 % Initial clauses : 136
% 2.55/2.73 % Processed clauses : 1028
% 2.55/2.73 % Factors computed : 65
% 2.55/2.73 % Resolvents computed: 1130
% 2.55/2.73 % Tautologies deleted: 3
% 2.55/2.73 % Forward subsumed : 299
% 2.55/2.73 % Backward subsumed : 82
% 2.55/2.73 % -------- CPU Time ---------
% 2.55/2.73 % User time : 2.364 s
% 2.55/2.73 % System time : 0.017 s
% 2.55/2.73 % Total time : 2.381 s
%------------------------------------------------------------------------------