%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP257-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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 6.23s 6.42s
% Output : Refutation 6.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 25
% Syntax : Number of clauses : 84 ( 27 unt; 0 nHn; 79 RR)
% Number of literals : 865 ( 0 equ; 809 neg)
% Maximal clause size : 37 ( 10 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 : 163 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause72,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
cnf(clause82,negated_conjecture,
state(skc8,skc9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
cnf(clause81,negated_conjecture,
man(skc8,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
cnf(clause79,negated_conjecture,
jules_forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
cnf(clause84,negated_conjecture,
proposition(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
cnf(clause83,negated_conjecture,
accessible_world(skc8,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
cnf(clause76,negated_conjecture,
event(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
cnf(clause77,negated_conjecture,
present(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
cnf(clause78,negated_conjecture,
think_believe_consider(skc8,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
cnf(clause73,negated_conjecture,
man(skc8,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
cnf(clause74,negated_conjecture,
forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
cnf(clause75,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
cnf(clause88,negated_conjecture,
of(skc8,skc11,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
cnf(clause52,axiom,
( ~ accessible_world(X162,X161)
| ~ man(X162,X160)
| man(X161,X160) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c233,plain,
( ~ accessible_world(skc8,X259)
| man(X259,skc10) ),
inference(resolution,[status(thm)],[clause52,clause81]) ).
cnf(c331,plain,
man(skc12,skc10),
inference(resolution,[status(thm)],[c233,clause83]) ).
cnf(clause90,negated_conjecture,
( ~ man(skc12,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(c360,plain,
event(skc12,skf2(X273)),
inference(resolution,[status(thm)],[c359,clause1]) ).
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(clause87,negated_conjecture,
theme(skc8,skc13,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
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(clause89,negated_conjecture,
be(skc8,skc9,skc10,skc10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
cnf(clause95,negated_conjecture,
( ~ state(X305,X314)
| ~ be(X305,X314,X310,X310)
| ~ man(X305,X310)
| ~ of(X305,X303,X310)
| ~ jules_forename(X305,X303)
| ~ forename(X305,X303)
| ~ jules_forename(X305,X302)
| ~ forename(X305,X302)
| ~ smoke(X312,X309)
| ~ present(X312,X309)
| ~ agent(X312,X309,X306)
| ~ event(X312,X309)
| ~ man(X305,X306)
| ~ of(X305,X302,X306)
| ~ proposition(X305,X312)
| ~ accessible_world(X305,X312)
| ~ smoke(X308,X311)
| ~ present(X308,X311)
| ~ agent(X308,X311,skf4(X308))
| ~ event(X308,X311)
| ~ accessible_world(X305,X308)
| ~ proposition(X305,X308)
| ~ theme(X305,X304,X308)
| ~ event(X305,X304)
| ~ present(X305,X304)
| ~ think_believe_consider(X305,X304)
| ~ man(X305,X315)
| ~ agent(X305,X304,X315)
| ~ agent(X305,X307,X315)
| ~ forename(X305,X313)
| ~ vincent_forename(X305,X313)
| ~ of(X305,X313,X315)
| ~ think_believe_consider(X305,X307)
| ~ present(X305,X307)
| ~ event(X305,X307)
| ~ theme(X305,X307,X312)
| ~ actual_world(X305) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
cnf(clause94,negated_conjecture,
( ~ state(X292,X300)
| ~ be(X292,X300,X297,X297)
| ~ man(X292,X297)
| ~ of(X292,X290,X297)
| ~ jules_forename(X292,X290)
| ~ forename(X292,X290)
| ~ jules_forename(X292,X289)
| ~ forename(X292,X289)
| ~ smoke(X299,X296)
| ~ present(X299,X296)
| ~ agent(X299,X296,X293)
| ~ event(X299,X296)
| ~ man(X292,X293)
| ~ of(X292,X289,X293)
| ~ proposition(X292,X299)
| ~ accessible_world(X292,X299)
| ~ accessible_world(X292,X295)
| ~ proposition(X292,X295)
| ~ theme(X292,X298,X295)
| ~ event(X292,X298)
| ~ present(X292,X298)
| ~ think_believe_consider(X292,X298)
| ~ man(X292,X291)
| ~ agent(X292,X298,X291)
| ~ agent(X292,X301,X291)
| ~ forename(X292,X294)
| ~ vincent_forename(X292,X294)
| ~ of(X292,X294,X291)
| ~ think_believe_consider(X292,X301)
| ~ present(X292,X301)
| ~ event(X292,X301)
| ~ theme(X292,X301,X299)
| ~ actual_world(X292)
| man(X295,skf4(X295)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
cnf(c396,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X684,skc10)
| ~ jules_forename(skc8,X684)
| ~ forename(skc8,X684)
| ~ jules_forename(skc8,X679)
| ~ forename(skc8,X679)
| ~ smoke(X680,X677)
| ~ present(X680,X677)
| ~ agent(X680,X677,X675)
| ~ event(X680,X677)
| ~ man(skc8,X675)
| ~ of(skc8,X679,X675)
| ~ proposition(skc8,X680)
| ~ accessible_world(skc8,X680)
| ~ accessible_world(skc8,X683)
| ~ proposition(skc8,X683)
| ~ theme(skc8,X678,X683)
| ~ event(skc8,X678)
| ~ present(skc8,X678)
| ~ think_believe_consider(skc8,X678)
| ~ man(skc8,X682)
| ~ agent(skc8,X678,X682)
| ~ agent(skc8,X676,X682)
| ~ forename(skc8,X681)
| ~ vincent_forename(skc8,X681)
| ~ of(skc8,X681,X682)
| ~ think_believe_consider(skc8,X676)
| ~ present(skc8,X676)
| ~ event(skc8,X676)
| ~ theme(skc8,X676,X680)
| ~ actual_world(skc8)
| man(X683,skf4(X683)) ),
inference(resolution,[status(thm)],[clause94,clause89]) ).
cnf(c698,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1263,skc10)
| ~ jules_forename(skc8,X1263)
| ~ forename(skc8,X1263)
| ~ jules_forename(skc8,X1266)
| ~ forename(skc8,X1266)
| ~ smoke(X1262,X1260)
| ~ present(X1262,X1260)
| ~ agent(X1262,X1260,X1265)
| ~ event(X1262,X1260)
| ~ man(skc8,X1265)
| ~ of(skc8,X1266,X1265)
| ~ proposition(skc8,X1262)
| ~ accessible_world(skc8,X1262)
| ~ theme(skc8,X1267,X1262)
| ~ event(skc8,X1267)
| ~ present(skc8,X1267)
| ~ think_believe_consider(skc8,X1267)
| ~ man(skc8,X1261)
| ~ agent(skc8,X1267,X1261)
| ~ forename(skc8,X1264)
| ~ vincent_forename(skc8,X1264)
| ~ of(skc8,X1264,X1261)
| ~ actual_world(skc8)
| man(X1262,skf4(X1262)) ),
inference(factor,[status(thm)],[c396]) ).
cnf(c1029,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1401,skc10)
| ~ jules_forename(skc8,X1401)
| ~ forename(skc8,X1401)
| ~ jules_forename(skc8,X1402)
| ~ forename(skc8,X1402)
| ~ smoke(X1397,X1399)
| ~ present(X1397,X1399)
| ~ agent(X1397,X1399,X1400)
| ~ event(X1397,X1399)
| ~ man(skc8,X1400)
| ~ of(skc8,X1402,X1400)
| ~ proposition(skc8,X1397)
| ~ accessible_world(skc8,X1397)
| ~ theme(skc8,X1398,X1397)
| ~ event(skc8,X1398)
| ~ present(skc8,X1398)
| ~ think_believe_consider(skc8,X1398)
| ~ man(skc8,skc15)
| ~ agent(skc8,X1398,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1397,skf4(X1397)) ),
inference(resolution,[status(thm)],[c698,clause85]) ).
cnf(c1070,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1406,skc10)
| ~ jules_forename(skc8,X1406)
| ~ forename(skc8,X1406)
| ~ jules_forename(skc8,X1407)
| ~ forename(skc8,X1407)
| ~ smoke(X1408,X1410)
| ~ present(X1408,X1410)
| ~ agent(X1408,X1410,X1409)
| ~ event(X1408,X1410)
| ~ man(skc8,X1409)
| ~ of(skc8,X1407,X1409)
| ~ proposition(skc8,X1408)
| ~ accessible_world(skc8,X1408)
| ~ theme(skc8,skc13,X1408)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(X1408,skf4(X1408)) ),
inference(resolution,[status(thm)],[c1029,clause86]) ).
cnf(c1071,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1511,skc10)
| ~ jules_forename(skc8,X1511)
| ~ forename(skc8,X1511)
| ~ jules_forename(skc8,X1512)
| ~ forename(skc8,X1512)
| ~ smoke(skc12,X1514)
| ~ present(skc12,X1514)
| ~ agent(skc12,X1514,X1513)
| ~ event(skc12,X1514)
| ~ man(skc8,X1513)
| ~ of(skc8,X1512,X1513)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1070,clause87]) ).
cnf(c1116,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1515,skc10)
| ~ jules_forename(skc8,X1515)
| ~ forename(skc8,X1515)
| ~ smoke(skc12,X1516)
| ~ present(skc12,X1516)
| ~ agent(skc12,X1516,skc10)
| ~ event(skc12,X1516)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(factor,[status(thm)],[c1071]) ).
cnf(c1119,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1517,skc10)
| ~ jules_forename(skc8,X1517)
| ~ forename(skc8,X1517)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1116,c383]) ).
cnf(c1120,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1518,skc10)
| ~ jules_forename(skc8,X1518)
| ~ forename(skc8,X1518)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1119,c360]) ).
cnf(c1121,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1519,skc10)
| ~ jules_forename(skc8,X1519)
| ~ forename(skc8,X1519)
| ~ smoke(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1120,c369]) ).
cnf(c1122,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X1520,skc10)
| ~ jules_forename(skc8,X1520)
| ~ forename(skc8,X1520)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1121,c359]) ).
cnf(c1123,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1122,clause88]) ).
cnf(c1127,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1123,clause75]) ).
cnf(c1128,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1127,clause74]) ).
cnf(c1129,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1128,clause73]) ).
cnf(c1130,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1129,clause78]) ).
cnf(c1131,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1130,clause77]) ).
cnf(c1132,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1131,clause76]) ).
cnf(c1133,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1132,clause83]) ).
cnf(c1134,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1133,clause84]) ).
cnf(c1135,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1134,clause80]) ).
cnf(c1136,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1135,clause79]) ).
cnf(c1139,plain,
( ~ state(skc8,skc9)
| ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1136,clause81]) ).
cnf(c1140,plain,
( ~ actual_world(skc8)
| man(skc12,skf4(skc12)) ),
inference(resolution,[status(thm)],[c1139,clause82]) ).
cnf(c1141,plain,
man(skc12,skf4(skc12)),
inference(resolution,[status(thm)],[c1140,clause72]) ).
cnf(c1144,plain,
agent(skc12,skf2(skf4(skc12)),skf4(skc12)),
inference(resolution,[status(thm)],[c1141,clause93]) ).
cnf(c1193,plain,
( ~ state(X1852,X1857)
| ~ be(X1852,X1857,X1860,X1860)
| ~ man(X1852,X1860)
| ~ of(X1852,X1855,X1860)
| ~ jules_forename(X1852,X1855)
| ~ forename(X1852,X1855)
| ~ jules_forename(X1852,X1856)
| ~ forename(X1852,X1856)
| ~ smoke(X1854,X1858)
| ~ present(X1854,X1858)
| ~ agent(X1854,X1858,X1863)
| ~ event(X1854,X1858)
| ~ man(X1852,X1863)
| ~ of(X1852,X1856,X1863)
| ~ proposition(X1852,X1854)
| ~ accessible_world(X1852,X1854)
| ~ smoke(skc12,skf2(skf4(skc12)))
| ~ present(skc12,skf2(skf4(skc12)))
| ~ event(skc12,skf2(skf4(skc12)))
| ~ accessible_world(X1852,skc12)
| ~ proposition(X1852,skc12)
| ~ theme(X1852,X1862,skc12)
| ~ event(X1852,X1862)
| ~ present(X1852,X1862)
| ~ think_believe_consider(X1852,X1862)
| ~ man(X1852,X1853)
| ~ agent(X1852,X1862,X1853)
| ~ agent(X1852,X1861,X1853)
| ~ forename(X1852,X1859)
| ~ vincent_forename(X1852,X1859)
| ~ of(X1852,X1859,X1853)
| ~ think_believe_consider(X1852,X1861)
| ~ present(X1852,X1861)
| ~ event(X1852,X1861)
| ~ theme(X1852,X1861,X1854)
| ~ actual_world(X1852) ),
inference(resolution,[status(thm)],[c1144,clause95]) ).
cnf(c1271,plain,
( ~ state(X1923,X1922)
| ~ be(X1923,X1922,X1924,X1924)
| ~ man(X1923,X1924)
| ~ of(X1923,X1917,X1924)
| ~ jules_forename(X1923,X1917)
| ~ forename(X1923,X1917)
| ~ jules_forename(X1923,X1925)
| ~ forename(X1923,X1925)
| ~ smoke(X1926,X1927)
| ~ present(X1926,X1927)
| ~ agent(X1926,X1927,X1928)
| ~ event(X1926,X1927)
| ~ man(X1923,X1928)
| ~ of(X1923,X1925,X1928)
| ~ proposition(X1923,X1926)
| ~ accessible_world(X1923,X1926)
| ~ smoke(skc12,skf2(skf4(skc12)))
| ~ present(skc12,skf2(skf4(skc12)))
| ~ accessible_world(X1923,skc12)
| ~ proposition(X1923,skc12)
| ~ theme(X1923,X1920,skc12)
| ~ event(X1923,X1920)
| ~ present(X1923,X1920)
| ~ think_believe_consider(X1923,X1920)
| ~ man(X1923,X1919)
| ~ agent(X1923,X1920,X1919)
| ~ agent(X1923,X1918,X1919)
| ~ forename(X1923,X1921)
| ~ vincent_forename(X1923,X1921)
| ~ of(X1923,X1921,X1919)
| ~ think_believe_consider(X1923,X1918)
| ~ present(X1923,X1918)
| ~ event(X1923,X1918)
| ~ theme(X1923,X1918,X1926)
| ~ actual_world(X1923) ),
inference(resolution,[status(thm)],[c1193,c360]) ).
cnf(c1283,plain,
( ~ state(X1935,X1929)
| ~ be(X1935,X1929,X1936,X1936)
| ~ man(X1935,X1936)
| ~ of(X1935,X1940,X1936)
| ~ jules_forename(X1935,X1940)
| ~ forename(X1935,X1940)
| ~ jules_forename(X1935,X1939)
| ~ forename(X1935,X1939)
| ~ smoke(X1938,X1934)
| ~ present(X1938,X1934)
| ~ agent(X1938,X1934,X1931)
| ~ event(X1938,X1934)
| ~ man(X1935,X1931)
| ~ of(X1935,X1939,X1931)
| ~ proposition(X1935,X1938)
| ~ accessible_world(X1935,X1938)
| ~ smoke(skc12,skf2(skf4(skc12)))
| ~ accessible_world(X1935,skc12)
| ~ proposition(X1935,skc12)
| ~ theme(X1935,X1932,skc12)
| ~ event(X1935,X1932)
| ~ present(X1935,X1932)
| ~ think_believe_consider(X1935,X1932)
| ~ man(X1935,X1933)
| ~ agent(X1935,X1932,X1933)
| ~ agent(X1935,X1930,X1933)
| ~ forename(X1935,X1937)
| ~ vincent_forename(X1935,X1937)
| ~ of(X1935,X1937,X1933)
| ~ think_believe_consider(X1935,X1930)
| ~ present(X1935,X1930)
| ~ event(X1935,X1930)
| ~ theme(X1935,X1930,X1938)
| ~ actual_world(X1935) ),
inference(resolution,[status(thm)],[c1271,c369]) ).
cnf(c1285,plain,
( ~ state(X1957,X1954)
| ~ be(X1957,X1954,X1953,X1953)
| ~ man(X1957,X1953)
| ~ of(X1957,X1951,X1953)
| ~ jules_forename(X1957,X1951)
| ~ forename(X1957,X1951)
| ~ jules_forename(X1957,X1949)
| ~ forename(X1957,X1949)
| ~ smoke(X1950,X1956)
| ~ present(X1950,X1956)
| ~ agent(X1950,X1956,X1948)
| ~ event(X1950,X1956)
| ~ man(X1957,X1948)
| ~ of(X1957,X1949,X1948)
| ~ proposition(X1957,X1950)
| ~ accessible_world(X1957,X1950)
| ~ accessible_world(X1957,skc12)
| ~ proposition(X1957,skc12)
| ~ theme(X1957,X1955,skc12)
| ~ event(X1957,X1955)
| ~ present(X1957,X1955)
| ~ think_believe_consider(X1957,X1955)
| ~ man(X1957,X1952)
| ~ agent(X1957,X1955,X1952)
| ~ agent(X1957,X1946,X1952)
| ~ forename(X1957,X1947)
| ~ vincent_forename(X1957,X1947)
| ~ of(X1957,X1947,X1952)
| ~ think_believe_consider(X1957,X1946)
| ~ present(X1957,X1946)
| ~ event(X1957,X1946)
| ~ theme(X1957,X1946,X1950)
| ~ actual_world(X1957) ),
inference(resolution,[status(thm)],[c1283,c359]) ).
cnf(c1287,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2110,skc10)
| ~ jules_forename(skc8,X2110)
| ~ forename(skc8,X2110)
| ~ jules_forename(skc8,X2105)
| ~ forename(skc8,X2105)
| ~ smoke(X2104,X2109)
| ~ present(X2104,X2109)
| ~ agent(X2104,X2109,X2107)
| ~ event(X2104,X2109)
| ~ man(skc8,X2107)
| ~ of(skc8,X2105,X2107)
| ~ proposition(skc8,X2104)
| ~ accessible_world(skc8,X2104)
| ~ accessible_world(skc8,skc12)
| ~ proposition(skc8,skc12)
| ~ theme(skc8,X2112,skc12)
| ~ event(skc8,X2112)
| ~ present(skc8,X2112)
| ~ think_believe_consider(skc8,X2112)
| ~ man(skc8,X2106)
| ~ agent(skc8,X2112,X2106)
| ~ agent(skc8,X2108,X2106)
| ~ forename(skc8,X2111)
| ~ vincent_forename(skc8,X2111)
| ~ of(skc8,X2111,X2106)
| ~ think_believe_consider(skc8,X2108)
| ~ present(skc8,X2108)
| ~ event(skc8,X2108)
| ~ theme(skc8,X2108,X2104)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1285,clause89]) ).
cnf(c1325,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2172,skc10)
| ~ jules_forename(skc8,X2172)
| ~ forename(skc8,X2172)
| ~ jules_forename(skc8,X2173)
| ~ forename(skc8,X2173)
| ~ smoke(skc12,X2169)
| ~ present(skc12,X2169)
| ~ agent(skc12,X2169,X2168)
| ~ event(skc12,X2169)
| ~ man(skc8,X2168)
| ~ of(skc8,X2173,X2168)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ theme(skc8,X2174,skc12)
| ~ event(skc8,X2174)
| ~ present(skc8,X2174)
| ~ think_believe_consider(skc8,X2174)
| ~ man(skc8,X2170)
| ~ agent(skc8,X2174,X2170)
| ~ forename(skc8,X2171)
| ~ vincent_forename(skc8,X2171)
| ~ of(skc8,X2171,X2170)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c1287]) ).
cnf(c1349,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2211,skc10)
| ~ jules_forename(skc8,X2211)
| ~ forename(skc8,X2211)
| ~ jules_forename(skc8,X2210)
| ~ forename(skc8,X2210)
| ~ smoke(skc12,X2212)
| ~ present(skc12,X2212)
| ~ agent(skc12,X2212,X2213)
| ~ event(skc12,X2212)
| ~ man(skc8,X2213)
| ~ of(skc8,X2210,X2213)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ theme(skc8,X2209,skc12)
| ~ event(skc8,X2209)
| ~ present(skc8,X2209)
| ~ think_believe_consider(skc8,X2209)
| ~ man(skc8,skc15)
| ~ agent(skc8,X2209,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1325,clause85]) ).
cnf(c1363,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2224,skc10)
| ~ jules_forename(skc8,X2224)
| ~ forename(skc8,X2224)
| ~ jules_forename(skc8,X2225)
| ~ forename(skc8,X2225)
| ~ smoke(skc12,X2223)
| ~ present(skc12,X2223)
| ~ agent(skc12,X2223,X2222)
| ~ event(skc12,X2223)
| ~ man(skc8,X2222)
| ~ of(skc8,X2225,X2222)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ theme(skc8,skc13,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1349,clause86]) ).
cnf(c1373,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2230,skc10)
| ~ jules_forename(skc8,X2230)
| ~ forename(skc8,X2230)
| ~ jules_forename(skc8,X2229)
| ~ forename(skc8,X2229)
| ~ smoke(skc12,X2228)
| ~ present(skc12,X2228)
| ~ agent(skc12,X2228,X2227)
| ~ event(skc12,X2228)
| ~ man(skc8,X2227)
| ~ of(skc8,X2229,X2227)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1363,clause87]) ).
cnf(c1379,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2231,skc10)
| ~ jules_forename(skc8,X2231)
| ~ forename(skc8,X2231)
| ~ smoke(skc12,X2232)
| ~ present(skc12,X2232)
| ~ agent(skc12,X2232,skc10)
| ~ event(skc12,X2232)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(factor,[status(thm)],[c1373]) ).
cnf(c1386,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2233,skc10)
| ~ jules_forename(skc8,X2233)
| ~ forename(skc8,X2233)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ event(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1379,c383]) ).
cnf(c1387,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2234,skc10)
| ~ jules_forename(skc8,X2234)
| ~ forename(skc8,X2234)
| ~ smoke(skc12,skf2(skc10))
| ~ present(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1386,c360]) ).
cnf(c1388,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2235,skc10)
| ~ jules_forename(skc8,X2235)
| ~ forename(skc8,X2235)
| ~ smoke(skc12,skf2(skc10))
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1387,c369]) ).
cnf(c1389,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ of(skc8,X2236,skc10)
| ~ jules_forename(skc8,X2236)
| ~ forename(skc8,X2236)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1388,c359]) ).
cnf(c1390,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ vincent_forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1389,clause88]) ).
cnf(c1391,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ forename(skc8,skc14)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1390,clause75]) ).
cnf(c1392,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ man(skc8,skc15)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1391,clause74]) ).
cnf(c1393,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ think_believe_consider(skc8,skc13)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1392,clause73]) ).
cnf(c1394,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ present(skc8,skc13)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1393,clause78]) ).
cnf(c1395,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ event(skc8,skc13)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1394,clause77]) ).
cnf(c1396,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ accessible_world(skc8,skc12)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1395,clause76]) ).
cnf(c1397,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ proposition(skc8,skc12)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1396,clause83]) ).
cnf(c1398,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ forename(skc8,skc11)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1397,clause84]) ).
cnf(c1399,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ jules_forename(skc8,skc11)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1398,clause80]) ).
cnf(c1400,plain,
( ~ state(skc8,skc9)
| ~ man(skc8,skc10)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1399,clause79]) ).
cnf(c1401,plain,
( ~ state(skc8,skc9)
| ~ actual_world(skc8) ),
inference(resolution,[status(thm)],[c1400,clause81]) ).
cnf(c1402,plain,
~ actual_world(skc8),
inference(resolution,[status(thm)],[c1401,clause82]) ).
cnf(c1403,plain,
$false,
inference(resolution,[status(thm)],[c1402,clause72]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NLP257-1 : TPTP v8.1.2. Released v2.4.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n013.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 13:22:53 EDT 2024
% 0.13/0.33 % CPUTime :
% 6.23/6.42 % Version: 1.5
% 6.23/6.42 % SZS status Unsatisfiable
% 6.23/6.42 % SZS output start CNFRefutation
% See solution above
% 6.23/6.42
% 6.23/6.42 % Initial clauses : 136
% 6.23/6.42 % Processed clauses : 1171
% 6.23/6.42 % Factors computed : 104
% 6.23/6.42 % Resolvents computed: 1262
% 6.23/6.42 % Tautologies deleted: 3
% 6.23/6.42 % Forward subsumed : 327
% 6.23/6.42 % Backward subsumed : 207
% 6.23/6.42 % -------- CPU Time ---------
% 6.23/6.42 % User time : 6.060 s
% 6.23/6.42 % System time : 0.021 s
% 6.23/6.42 % Total time : 6.081 s
%------------------------------------------------------------------------------