%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP221-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:40 EDT 2024
% Result : Satisfiable 13.67s 13.83s
% Output : Saturation 13.68s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause48,negated_conjecture,
( ~ state(X33,X36)
| ~ man(X33,X34)
| ~ smoke(X39,X38)
| ~ present(X39,X38)
| ~ agent(X39,X38,skf7(X39))
| ~ event(X39,X38)
| ~ accessible_world(X33,X39)
| ~ proposition(X33,X39)
| ~ theme(X33,X41,X39)
| ~ event(X33,X41)
| ~ present(X33,X41)
| ~ think_believe_consider(X33,X41)
| ~ forename(X33,X40)
| ~ vincent_forename(X33,X40)
| ~ of(X33,X40,X35)
| ~ man(X33,X35)
| ~ agent(X33,X41,X35)
| ~ be(X33,X36,X35,X34)
| ~ forename(X33,X37)
| ~ jules_forename(X33,X37)
| ~ of(X33,X37,X35)
| ~ actual_world(X33)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| be(skc17,skc18,skc21,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(clause1,negated_conjecture,
actual_world(skc29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause6,negated_conjecture,
( ssSkC0
| proposition(skc29,skc32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(clause5,negated_conjecture,
( ssSkC0
| accessible_world(skc29,skc32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| think_believe_consider(skc29,skc33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause8,negated_conjecture,
( ssSkC0
| present(skc29,skc33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(clause7,negated_conjecture,
( ssSkC0
| event(skc29,skc33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause11,negated_conjecture,
( ssSkC0
| vincent_forename(skc29,skc34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
( ssSkC0
| forename(skc29,skc34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| man(skc29,skc35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause3,negated_conjecture,
( ssSkC0
| state(skc29,skc30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
( ssSkC0
| man(skc29,skc31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause14,negated_conjecture,
( ssSkC0
| jules_forename(skc29,skc36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,negated_conjecture,
( ssSkC0
| forename(skc29,skc36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause28,negated_conjecture,
( ssSkC0
| theme(skc29,skc33,skc32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(clause30,negated_conjecture,
( ssSkC0
| agent(skc29,skc33,skc35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,negated_conjecture,
( ssSkC0
| of(skc29,skc34,skc35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause31,negated_conjecture,
( ssSkC0
| of(skc29,skc36,skc35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(clause40,negated_conjecture,
( ~ man(skc32,X6)
| ssSkC0
| smoke(skc32,skf11(X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(clause36,negated_conjecture,
( ssSkC0
| be(skc29,skc30,skc35,skc31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(clause47,negated_conjecture,
( ~ proposition(X24,X27)
| ~ accessible_world(X24,X27)
| ~ think_believe_consider(X24,X25)
| ~ present(X24,X25)
| ~ event(X24,X25)
| ~ theme(X24,X25,X27)
| ~ vincent_forename(X24,X30)
| ~ forename(X24,X30)
| ~ agent(X24,X25,X29)
| ~ man(X24,X29)
| ~ of(X24,X30,X29)
| ~ state(X24,X32)
| ~ man(X24,X31)
| ~ jules_forename(X24,X26)
| ~ forename(X24,X26)
| ~ be(X24,X32,X28,X31)
| ~ man(X24,X28)
| ~ of(X24,X26,X28)
| ~ actual_world(X24)
| ssSkC0
| man(X27,skf13(X27)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(c307,plain,
( ~ proposition(skc29,X59)
| ~ accessible_world(skc29,X59)
| ~ think_believe_consider(skc29,X60)
| ~ present(skc29,X60)
| ~ event(skc29,X60)
| ~ theme(skc29,X60,X59)
| ~ vincent_forename(skc29,X56)
| ~ forename(skc29,X56)
| ~ agent(skc29,X60,X58)
| ~ man(skc29,X58)
| ~ of(skc29,X56,X58)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X57)
| ~ forename(skc29,X57)
| ~ man(skc29,skc35)
| ~ of(skc29,X57,skc35)
| ~ actual_world(skc29)
| ssSkC0
| man(X59,skf13(X59)) ),
inference(resolution,[status(thm)],[clause47,clause36]) ).
cnf(c487,plain,
( ~ proposition(skc29,X556)
| ~ accessible_world(skc29,X556)
| ~ think_believe_consider(skc29,X554)
| ~ present(skc29,X554)
| ~ event(skc29,X554)
| ~ theme(skc29,X554,X556)
| ~ vincent_forename(skc29,X555)
| ~ forename(skc29,X555)
| ~ agent(skc29,X554,X553)
| ~ man(skc29,X553)
| ~ of(skc29,X555,X553)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| ssSkC0
| man(X556,skf13(X556)) ),
inference(resolution,[status(thm)],[c307,clause31]) ).
cnf(c801,plain,
( ~ proposition(skc29,X589)
| ~ accessible_world(skc29,X589)
| ~ think_believe_consider(skc29,X590)
| ~ present(skc29,X590)
| ~ event(skc29,X590)
| ~ theme(skc29,X590,X589)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ agent(skc29,X590,skc35)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| ssSkC0
| man(X589,skf13(X589)) ),
inference(resolution,[status(thm)],[c487,clause29]) ).
cnf(c822,plain,
( ~ proposition(skc29,X591)
| ~ accessible_world(skc29,X591)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ theme(skc29,skc33,X591)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| ssSkC0
| man(X591,skf13(X591)) ),
inference(resolution,[status(thm)],[c801,clause30]) ).
cnf(c837,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c822,clause28]) ).
cnf(c861,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c837,clause13]) ).
cnf(c870,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c861,clause14]) ).
cnf(c900,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c870,clause4]) ).
cnf(c921,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c900,clause3]) ).
cnf(c938,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c921,clause12]) ).
cnf(c962,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c938,clause10]) ).
cnf(c974,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c962,clause11]) ).
cnf(c1000,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c974,clause7]) ).
cnf(c1007,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c1000,clause8]) ).
cnf(c1029,plain,
( ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c1007,clause9]) ).
cnf(c1042,plain,
( ~ proposition(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c1029,clause5]) ).
cnf(c1075,plain,
( ~ actual_world(skc29)
| ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c1042,clause6]) ).
cnf(c1079,plain,
( ssSkC0
| man(skc32,skf13(skc32)) ),
inference(resolution,[status(thm)],[c1075,clause1]) ).
cnf(c1099,plain,
( ssSkC0
| smoke(skc32,skf11(X608)) ),
inference(resolution,[status(thm)],[c1079,clause40]) ).
cnf(clause39,negated_conjecture,
( ~ man(skc32,X4)
| ssSkC0
| present(skc32,skf11(X5)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c1098,plain,
( ssSkC0
| present(skc32,skf11(X607)) ),
inference(resolution,[status(thm)],[c1079,clause39]) ).
cnf(clause38,negated_conjecture,
( ~ man(skc32,X2)
| ssSkC0
| event(skc32,skf11(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c1100,plain,
( ssSkC0
| event(skc32,skf11(X614)) ),
inference(resolution,[status(thm)],[c1079,clause38]) ).
cnf(clause49,negated_conjecture,
( ~ proposition(X42,X45)
| ~ accessible_world(X42,X45)
| ~ smoke(X45,X43)
| ~ present(X45,X43)
| ~ agent(X45,X43,skf13(X45))
| ~ event(X45,X43)
| ~ think_believe_consider(X42,X49)
| ~ present(X42,X49)
| ~ event(X42,X49)
| ~ theme(X42,X49,X45)
| ~ vincent_forename(X42,X47)
| ~ forename(X42,X47)
| ~ agent(X42,X49,X51)
| ~ man(X42,X51)
| ~ of(X42,X47,X51)
| ~ state(X42,X50)
| ~ man(X42,X44)
| ~ jules_forename(X42,X46)
| ~ forename(X42,X46)
| ~ be(X42,X50,X48,X44)
| ~ man(X42,X48)
| ~ of(X42,X46,X48)
| ~ actual_world(X42)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c309,plain,
( ~ proposition(skc29,X78)
| ~ accessible_world(skc29,X78)
| ~ smoke(X78,X80)
| ~ present(X78,X80)
| ~ agent(X78,X80,skf13(X78))
| ~ event(X78,X80)
| ~ think_believe_consider(skc29,X75)
| ~ present(skc29,X75)
| ~ event(skc29,X75)
| ~ theme(skc29,X75,X78)
| ~ vincent_forename(skc29,X76)
| ~ forename(skc29,X76)
| ~ agent(skc29,X75,X77)
| ~ man(skc29,X77)
| ~ of(skc29,X76,X77)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X79)
| ~ forename(skc29,X79)
| ~ man(skc29,skc35)
| ~ of(skc29,X79,skc35)
| ~ actual_world(skc29)
| ssSkC0 ),
inference(resolution,[status(thm)],[clause49,clause36]) ).
cnf(clause44,negated_conjecture,
( ~ man(skc32,X14)
| ssSkC0
| agent(skc32,skf11(X14),X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c1101,plain,
( ssSkC0
| agent(skc32,skf11(skf13(skc32)),skf13(skc32)) ),
inference(resolution,[status(thm)],[c1079,clause44]) ).
cnf(c1257,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ present(skc32,skf11(skf13(skc32)))
| ~ event(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X1948)
| ~ present(skc29,X1948)
| ~ event(skc29,X1948)
| ~ theme(skc29,X1948,skc32)
| ~ vincent_forename(skc29,X1951)
| ~ forename(skc29,X1951)
| ~ agent(skc29,X1948,X1950)
| ~ man(skc29,X1950)
| ~ of(skc29,X1951,X1950)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X1949)
| ~ forename(skc29,X1949)
| ~ man(skc29,skc35)
| ~ of(skc29,X1949,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1101,c309]) ).
cnf(c1729,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ present(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3200)
| ~ present(skc29,X3200)
| ~ event(skc29,X3200)
| ~ theme(skc29,X3200,skc32)
| ~ vincent_forename(skc29,X3202)
| ~ forename(skc29,X3202)
| ~ agent(skc29,X3200,X3201)
| ~ man(skc29,X3201)
| ~ of(skc29,X3202,X3201)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3203)
| ~ forename(skc29,X3203)
| ~ man(skc29,skc35)
| ~ of(skc29,X3203,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1257,c1100]) ).
cnf(c2276,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X4937)
| ~ present(skc29,X4937)
| ~ event(skc29,X4937)
| ~ theme(skc29,X4937,skc32)
| ~ vincent_forename(skc29,X4939)
| ~ forename(skc29,X4939)
| ~ agent(skc29,X4937,X4938)
| ~ man(skc29,X4938)
| ~ of(skc29,X4939,X4938)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X4936)
| ~ forename(skc29,X4936)
| ~ man(skc29,skc35)
| ~ of(skc29,X4936,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1729,c1098]) ).
cnf(c4799,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X5002)
| ~ present(skc29,X5002)
| ~ event(skc29,X5002)
| ~ theme(skc29,X5002,skc32)
| ~ vincent_forename(skc29,X5001)
| ~ forename(skc29,X5001)
| ~ agent(skc29,X5002,X4999)
| ~ man(skc29,X4999)
| ~ of(skc29,X5001,X4999)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X5000)
| ~ forename(skc29,X5000)
| ~ man(skc29,skc35)
| ~ of(skc29,X5000,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c2276,c1099]) ).
cnf(c4849,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X5249)
| ~ present(skc29,X5249)
| ~ event(skc29,X5249)
| ~ theme(skc29,X5249,skc32)
| ~ vincent_forename(skc29,X5250)
| ~ forename(skc29,X5250)
| ~ agent(skc29,X5249,X5248)
| ~ man(skc29,X5248)
| ~ of(skc29,X5250,X5248)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ man(skc29,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c4799,clause31]) ).
cnf(c5098,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X5269)
| ~ present(skc29,X5269)
| ~ event(skc29,X5269)
| ~ theme(skc29,X5269,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ agent(skc29,X5269,skc35)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c4849,clause29]) ).
cnf(c5114,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ theme(skc29,skc33,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5098,clause30]) ).
cnf(c5127,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5114,clause28]) ).
cnf(c5146,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5127,clause13]) ).
cnf(c5155,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5146,clause14]) ).
cnf(c5179,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5155,clause4]) ).
cnf(c5199,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5179,clause3]) ).
cnf(c5211,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5199,clause12]) ).
cnf(c5232,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5211,clause10]) ).
cnf(c5242,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5232,clause11]) ).
cnf(c5265,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5242,clause7]) ).
cnf(c5270,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5265,clause8]) ).
cnf(c5290,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5270,clause9]) ).
cnf(c5300,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5290,clause5]) ).
cnf(c5327,plain,
( ssSkC0
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c5300,clause6]) ).
cnf(c5331,plain,
ssSkC0,
inference(resolution,[status(thm)],[c5327,clause1]) ).
cnf(c5334,plain,
be(skc17,skc18,skc21,skc19),
inference(resolution,[status(thm)],[c5331,clause37]) ).
cnf(c5370,plain,
( ~ state(skc17,skc18)
| ~ man(skc17,skc19)
| ~ smoke(X6868,X6869)
| ~ present(X6868,X6869)
| ~ agent(X6868,X6869,skf7(X6868))
| ~ event(X6868,X6869)
| ~ accessible_world(skc17,X6868)
| ~ proposition(skc17,X6868)
| ~ theme(skc17,X6871,X6868)
| ~ event(skc17,X6871)
| ~ present(skc17,X6871)
| ~ think_believe_consider(skc17,X6871)
| ~ forename(skc17,X6867)
| ~ vincent_forename(skc17,X6867)
| ~ of(skc17,X6867,skc21)
| ~ man(skc17,skc21)
| ~ agent(skc17,X6871,skc21)
| ~ forename(skc17,X6870)
| ~ jules_forename(skc17,X6870)
| ~ of(skc17,X6870,skc21)
| ~ actual_world(skc17)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c5334,clause48]) ).
cnf(clause35,negated_conjecture,
( ~ ssSkC0
| of(skc17,skc20,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c5335,plain,
of(skc17,skc20,skc21),
inference(resolution,[status(thm)],[c5331,clause35]) ).
cnf(clause46,negated_conjecture,
( ~ state(X16,X19)
| ~ man(X16,X17)
| ~ accessible_world(X16,X21)
| ~ proposition(X16,X21)
| ~ theme(X16,X20,X21)
| ~ event(X16,X20)
| ~ present(X16,X20)
| ~ think_believe_consider(X16,X20)
| ~ forename(X16,X23)
| ~ vincent_forename(X16,X23)
| ~ of(X16,X23,X22)
| ~ man(X16,X22)
| ~ agent(X16,X20,X22)
| ~ be(X16,X19,X22,X17)
| ~ forename(X16,X18)
| ~ jules_forename(X16,X18)
| ~ of(X16,X18,X22)
| ~ actual_world(X16)
| ~ ssSkC0
| man(X21,skf7(X21)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c5369,plain,
( ~ state(skc17,skc18)
| ~ man(skc17,skc19)
| ~ accessible_world(skc17,X5481)
| ~ proposition(skc17,X5481)
| ~ theme(skc17,X5483,X5481)
| ~ event(skc17,X5483)
| ~ present(skc17,X5483)
| ~ think_believe_consider(skc17,X5483)
| ~ forename(skc17,X5484)
| ~ vincent_forename(skc17,X5484)
| ~ of(skc17,X5484,skc21)
| ~ man(skc17,skc21)
| ~ agent(skc17,X5483,skc21)
| ~ forename(skc17,X5482)
| ~ jules_forename(skc17,X5482)
| ~ of(skc17,X5482,skc21)
| ~ actual_world(skc17)
| ~ ssSkC0
| man(X5481,skf7(X5481)) ),
inference(resolution,[status(thm)],[c5334,clause46]) ).
cnf(c5372,plain,
( ~ state(skc17,skc18)
| ~ man(skc17,skc19)
| ~ accessible_world(skc17,X5491)
| ~ proposition(skc17,X5491)
| ~ theme(skc17,X5493,X5491)
| ~ event(skc17,X5493)
| ~ present(skc17,X5493)
| ~ think_believe_consider(skc17,X5493)
| ~ forename(skc17,X5492)
| ~ vincent_forename(skc17,X5492)
| ~ of(skc17,X5492,skc21)
| ~ man(skc17,skc21)
| ~ agent(skc17,X5493,skc21)
| ~ forename(skc17,skc20)
| ~ jules_forename(skc17,skc20)
| ~ actual_world(skc17)
| ~ ssSkC0
| man(X5491,skf7(X5491)) ),
inference(resolution,[status(thm)],[c5369,c5335]) ).
cnf(c5371,plain,
( ~ state(skc17,skc18)
| ~ man(skc17,skc19)
| ~ accessible_world(skc17,X5485)
| ~ proposition(skc17,X5485)
| ~ theme(skc17,X5486,X5485)
| ~ event(skc17,X5486)
| ~ present(skc17,X5486)
| ~ think_believe_consider(skc17,X5486)
| ~ forename(skc17,X5487)
| ~ vincent_forename(skc17,X5487)
| ~ of(skc17,X5487,skc21)
| ~ man(skc17,skc21)
| ~ agent(skc17,X5486,skc21)
| ~ jules_forename(skc17,X5487)
| ~ actual_world(skc17)
| ~ ssSkC0
| man(X5485,skf7(X5485)) ),
inference(factor,[status(thm)],[c5369]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| agent(skc17,skc23,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c5346,plain,
agent(skc17,skc23,skc25),
inference(resolution,[status(thm)],[c5331,clause33]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| theme(skc17,skc23,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c5341,plain,
theme(skc17,skc23,skc22),
inference(resolution,[status(thm)],[c5331,clause32]) ).
cnf(clause27,negated_conjecture,
( ~ ssSkC0
| man(skc17,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c5345,plain,
man(skc17,skc21),
inference(resolution,[status(thm)],[c5331,clause27]) ).
cnf(clause16,negated_conjecture,
( ~ ssSkC0
| accessible_world(skc17,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c5344,plain,
accessible_world(skc17,skc22),
inference(resolution,[status(thm)],[c5331,clause16]) ).
cnf(clause18,negated_conjecture,
( ~ ssSkC0
| present(skc17,skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c5343,plain,
present(skc17,skc23),
inference(resolution,[status(thm)],[c5331,clause18]) ).
cnf(clause17,negated_conjecture,
( ~ ssSkC0
| think_believe_consider(skc17,skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c5342,plain,
think_believe_consider(skc17,skc23),
inference(resolution,[status(thm)],[c5331,clause17]) ).
cnf(clause26,negated_conjecture,
( ~ ssSkC0
| forename(skc17,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c5340,plain,
forename(skc17,skc20),
inference(resolution,[status(thm)],[c5331,clause26]) ).
cnf(clause25,negated_conjecture,
( ~ ssSkC0
| jules_forename(skc17,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c5339,plain,
jules_forename(skc17,skc20),
inference(resolution,[status(thm)],[c5331,clause25]) ).
cnf(clause21,negated_conjecture,
( ~ ssSkC0
| forename(skc17,skc24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c5338,plain,
forename(skc17,skc24),
inference(resolution,[status(thm)],[c5331,clause21]) ).
cnf(clause23,negated_conjecture,
( ~ ssSkC0
| state(skc17,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c5337,plain,
state(skc17,skc18),
inference(resolution,[status(thm)],[c5331,clause23]) ).
cnf(clause24,negated_conjecture,
( ~ ssSkC0
| man(skc17,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c5336,plain,
man(skc17,skc19),
inference(resolution,[status(thm)],[c5331,clause24]) ).
cnf(clause20,negated_conjecture,
( ~ ssSkC0
| vincent_forename(skc17,skc24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c5333,plain,
vincent_forename(skc17,skc24),
inference(resolution,[status(thm)],[c5331,clause20]) ).
cnf(clause22,negated_conjecture,
( ~ ssSkC0
| man(skc17,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c5332,plain,
man(skc17,skc25),
inference(resolution,[status(thm)],[c5331,clause22]) ).
cnf(clause15,negated_conjecture,
( ~ ssSkC0
| proposition(skc17,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c6,plain,
( proposition(skc17,skc22)
| proposition(skc29,skc32) ),
inference(resolution,[status(thm)],[clause15,clause6]) ).
cnf(c9,plain,
( proposition(skc17,skc22)
| event(skc29,skc33) ),
inference(resolution,[status(thm)],[clause15,clause7]) ).
cnf(c2,plain,
( proposition(skc17,skc22)
| vincent_forename(skc29,skc34) ),
inference(resolution,[status(thm)],[clause15,clause11]) ).
cnf(c8,plain,
( proposition(skc17,skc22)
| forename(skc29,skc34) ),
inference(resolution,[status(thm)],[clause15,clause10]) ).
cnf(c1,plain,
( proposition(skc17,skc22)
| man(skc29,skc35) ),
inference(resolution,[status(thm)],[clause15,clause12]) ).
cnf(c4,plain,
( proposition(skc17,skc22)
| man(skc29,skc31) ),
inference(resolution,[status(thm)],[clause15,clause4]) ).
cnf(c10,plain,
( proposition(skc17,skc22)
| forename(skc29,skc36) ),
inference(resolution,[status(thm)],[clause15,clause13]) ).
cnf(c158,plain,
( theme(skc29,skc33,skc32)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[clause28,clause15]) ).
cnf(c184,plain,
( agent(skc29,skc33,skc35)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[clause30,clause15]) ).
cnf(c197,plain,
( of(skc29,skc36,skc35)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[clause31,clause15]) ).
cnf(c1142,plain,
( event(skc32,skf11(X669))
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c1100,clause15]) ).
cnf(c1717,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ present(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3152)
| ~ present(skc29,X3152)
| ~ event(skc29,X3152)
| ~ theme(skc29,X3152,skc32)
| ~ vincent_forename(skc29,X3154)
| ~ forename(skc29,X3154)
| ~ agent(skc29,X3152,X3153)
| ~ man(skc29,X3153)
| ~ of(skc29,X3154,X3153)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3155)
| ~ forename(skc29,X3155)
| ~ man(skc29,skc35)
| ~ of(skc29,X3155,skc35)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c1257,c1142]) ).
cnf(c2048,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3740)
| ~ present(skc29,X3740)
| ~ event(skc29,X3740)
| ~ theme(skc29,X3740,skc32)
| ~ vincent_forename(skc29,X3741)
| ~ forename(skc29,X3741)
| ~ agent(skc29,X3740,X3739)
| ~ man(skc29,X3739)
| ~ of(skc29,X3741,X3739)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3738)
| ~ forename(skc29,X3738)
| ~ man(skc29,skc35)
| ~ of(skc29,X3738,skc35)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c1717,c1098]) ).
cnf(c3133,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X4204)
| ~ present(skc29,X4204)
| ~ event(skc29,X4204)
| ~ theme(skc29,X4204,skc32)
| ~ vincent_forename(skc29,X4202)
| ~ forename(skc29,X4202)
| ~ agent(skc29,X4204,X4205)
| ~ man(skc29,X4205)
| ~ of(skc29,X4202,X4205)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X4203)
| ~ forename(skc29,X4203)
| ~ man(skc29,skc35)
| ~ of(skc29,X4203,skc35)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c2048,c1099]) ).
cnf(c3713,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X4467)
| ~ present(skc29,X4467)
| ~ event(skc29,X4467)
| ~ theme(skc29,X4467,skc32)
| ~ vincent_forename(skc29,X4466)
| ~ forename(skc29,X4466)
| ~ agent(skc29,X4467,X4468)
| ~ man(skc29,X4468)
| ~ of(skc29,X4466,X4468)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c3133,c197]) ).
cnf(c4118,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X4492)
| ~ present(skc29,X4492)
| ~ event(skc29,X4492)
| ~ theme(skc29,X4492,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ agent(skc29,X4492,skc35)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c3713,clause29]) ).
cnf(c4150,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ theme(skc29,skc33,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4118,c184]) ).
cnf(c4166,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4150,c158]) ).
cnf(c4186,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4166,c10]) ).
cnf(c4197,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4186,clause14]) ).
cnf(c4220,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4197,c4]) ).
cnf(c4243,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4220,clause3]) ).
cnf(c4254,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4243,c1]) ).
cnf(c4269,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4254,c8]) ).
cnf(c4285,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4269,c2]) ).
cnf(c4299,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4285,c9]) ).
cnf(c4319,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4299,clause8]) ).
cnf(c4340,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4319,clause9]) ).
cnf(c4351,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4340,clause5]) ).
cnf(c4375,plain,
( ssSkC0
| ~ actual_world(skc29)
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4351,c6]) ).
cnf(c4384,plain,
( ssSkC0
| proposition(skc17,skc22) ),
inference(resolution,[status(thm)],[c4375,clause1]) ).
cnf(c4389,plain,
proposition(skc17,skc22),
inference(resolution,[status(thm)],[c4384,clause15]) ).
cnf(clause19,negated_conjecture,
( ~ ssSkC0
| event(skc17,skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c54,plain,
( event(skc17,skc23)
| proposition(skc29,skc32) ),
inference(resolution,[status(thm)],[clause19,clause6]) ).
cnf(c50,plain,
( event(skc17,skc23)
| vincent_forename(skc29,skc34) ),
inference(resolution,[status(thm)],[clause19,clause11]) ).
cnf(c56,plain,
( event(skc17,skc23)
| forename(skc29,skc34) ),
inference(resolution,[status(thm)],[clause19,clause10]) ).
cnf(c49,plain,
( event(skc17,skc23)
| man(skc29,skc35) ),
inference(resolution,[status(thm)],[clause19,clause12]) ).
cnf(c55,plain,
( event(skc17,skc23)
| state(skc29,skc30) ),
inference(resolution,[status(thm)],[clause19,clause3]) ).
cnf(c52,plain,
( event(skc17,skc23)
| man(skc29,skc31) ),
inference(resolution,[status(thm)],[clause19,clause4]) ).
cnf(c58,plain,
( event(skc17,skc23)
| forename(skc29,skc36) ),
inference(resolution,[status(thm)],[clause19,clause13]) ).
cnf(c177,plain,
( of(skc29,skc34,skc35)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[clause29,clause19]) ).
cnf(c203,plain,
( of(skc29,skc36,skc35)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[clause31,clause19]) ).
cnf(c1131,plain,
( smoke(skc32,skf11(X656))
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c1099,clause19]) ).
cnf(c1113,plain,
( present(skc32,skf11(X629))
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c1098,clause19]) ).
cnf(c1149,plain,
( event(skc32,skf11(X684))
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c1100,clause19]) ).
cnf(c1715,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ present(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3137)
| ~ present(skc29,X3137)
| ~ event(skc29,X3137)
| ~ theme(skc29,X3137,skc32)
| ~ vincent_forename(skc29,X3139)
| ~ forename(skc29,X3139)
| ~ agent(skc29,X3137,X3138)
| ~ man(skc29,X3138)
| ~ of(skc29,X3139,X3138)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3140)
| ~ forename(skc29,X3140)
| ~ man(skc29,skc35)
| ~ of(skc29,X3140,skc35)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c1257,c1149]) ).
cnf(c1798,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3433)
| ~ present(skc29,X3433)
| ~ event(skc29,X3433)
| ~ theme(skc29,X3433,skc32)
| ~ vincent_forename(skc29,X3435)
| ~ forename(skc29,X3435)
| ~ agent(skc29,X3433,X3432)
| ~ man(skc29,X3432)
| ~ of(skc29,X3435,X3432)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3434)
| ~ forename(skc29,X3434)
| ~ man(skc29,skc35)
| ~ of(skc29,X3434,skc35)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c1715,c1113]) ).
cnf(c2714,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X3623)
| ~ present(skc29,X3623)
| ~ event(skc29,X3623)
| ~ theme(skc29,X3623,skc32)
| ~ vincent_forename(skc29,X3622)
| ~ forename(skc29,X3622)
| ~ agent(skc29,X3623,X3625)
| ~ man(skc29,X3625)
| ~ of(skc29,X3622,X3625)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3624)
| ~ forename(skc29,X3624)
| ~ man(skc29,skc35)
| ~ of(skc29,X3624,skc35)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c1798,c1131]) ).
cnf(c2738,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X3897)
| ~ present(skc29,X3897)
| ~ event(skc29,X3897)
| ~ theme(skc29,X3897,skc32)
| ~ vincent_forename(skc29,X3899)
| ~ forename(skc29,X3899)
| ~ agent(skc29,X3897,X3898)
| ~ man(skc29,X3898)
| ~ of(skc29,X3899,X3898)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c2714,c203]) ).
cnf(c3241,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X3916)
| ~ present(skc29,X3916)
| ~ event(skc29,X3916)
| ~ theme(skc29,X3916,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ agent(skc29,X3916,skc35)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c2738,c177]) ).
cnf(c3271,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ theme(skc29,skc33,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3241,clause30]) ).
cnf(c3286,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3271,clause28]) ).
cnf(c3301,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3286,c58]) ).
cnf(c3317,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3301,clause14]) ).
cnf(c3344,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3317,c52]) ).
cnf(c3364,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3344,c55]) ).
cnf(c3372,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3364,c49]) ).
cnf(c3393,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3372,c56]) ).
cnf(c3409,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3393,c50]) ).
cnf(c3440,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3409,clause7]) ).
cnf(c3446,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3440,clause8]) ).
cnf(c3468,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3446,clause9]) ).
cnf(c3480,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3468,clause5]) ).
cnf(c3504,plain,
( ssSkC0
| ~ actual_world(skc29)
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3480,c54]) ).
cnf(c3515,plain,
( ssSkC0
| event(skc17,skc23) ),
inference(resolution,[status(thm)],[c3504,clause1]) ).
cnf(c3527,plain,
event(skc17,skc23),
inference(resolution,[status(thm)],[c3515,clause19]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| of(skc17,skc24,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c247,plain,
( of(skc17,skc24,skc25)
| proposition(skc29,skc32) ),
inference(resolution,[status(thm)],[clause34,clause6]) ).
cnf(c246,plain,
( of(skc17,skc24,skc25)
| present(skc29,skc33) ),
inference(resolution,[status(thm)],[clause34,clause8]) ).
cnf(c252,plain,
( of(skc17,skc24,skc25)
| event(skc29,skc33) ),
inference(resolution,[status(thm)],[clause34,clause7]) ).
cnf(c249,plain,
( of(skc17,skc24,skc25)
| forename(skc29,skc34) ),
inference(resolution,[status(thm)],[clause34,clause10]) ).
cnf(c241,plain,
( of(skc17,skc24,skc25)
| man(skc29,skc35) ),
inference(resolution,[status(thm)],[clause34,clause12]) ).
cnf(c244,plain,
( of(skc17,skc24,skc25)
| man(skc29,skc31) ),
inference(resolution,[status(thm)],[clause34,clause4]) ).
cnf(c253,plain,
( of(skc17,skc24,skc25)
| forename(skc29,skc36) ),
inference(resolution,[status(thm)],[clause34,clause13]) ).
cnf(c250,plain,
( of(skc17,skc24,skc25)
| agent(skc29,skc33,skc35) ),
inference(resolution,[status(thm)],[clause34,clause30]) ).
cnf(c251,plain,
( of(skc17,skc24,skc25)
| of(skc29,skc36,skc35) ),
inference(resolution,[status(thm)],[clause34,clause31]) ).
cnf(c1119,plain,
( present(skc32,skf11(X712))
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1098,clause34]) ).
cnf(c1155,plain,
( event(skc32,skf11(X725))
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1100,clause34]) ).
cnf(c1714,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ present(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3117)
| ~ present(skc29,X3117)
| ~ event(skc29,X3117)
| ~ theme(skc29,X3117,skc32)
| ~ vincent_forename(skc29,X3119)
| ~ forename(skc29,X3119)
| ~ agent(skc29,X3117,X3118)
| ~ man(skc29,X3118)
| ~ of(skc29,X3119,X3118)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3120)
| ~ forename(skc29,X3120)
| ~ man(skc29,skc35)
| ~ of(skc29,X3120,skc35)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1257,c1155]) ).
cnf(c1757,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ smoke(skc32,skf11(skf13(skc32)))
| ~ think_believe_consider(skc29,X3134)
| ~ present(skc29,X3134)
| ~ event(skc29,X3134)
| ~ theme(skc29,X3134,skc32)
| ~ vincent_forename(skc29,X3135)
| ~ forename(skc29,X3135)
| ~ agent(skc29,X3134,X3133)
| ~ man(skc29,X3133)
| ~ of(skc29,X3135,X3133)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3136)
| ~ forename(skc29,X3136)
| ~ man(skc29,skc35)
| ~ of(skc29,X3136,skc35)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1714,c1119]) ).
cnf(c1789,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X3141)
| ~ present(skc29,X3141)
| ~ event(skc29,X3141)
| ~ theme(skc29,X3141,skc32)
| ~ vincent_forename(skc29,X3144)
| ~ forename(skc29,X3144)
| ~ agent(skc29,X3141,X3143)
| ~ man(skc29,X3143)
| ~ of(skc29,X3144,X3143)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X3142)
| ~ forename(skc29,X3142)
| ~ man(skc29,skc35)
| ~ of(skc29,X3142,skc35)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1757,c1099]) ).
cnf(c1835,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X3353)
| ~ present(skc29,X3353)
| ~ event(skc29,X3353)
| ~ theme(skc29,X3353,skc32)
| ~ vincent_forename(skc29,X3354)
| ~ forename(skc29,X3354)
| ~ agent(skc29,X3353,X3352)
| ~ man(skc29,X3352)
| ~ of(skc29,X3354,X3352)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1789,c251]) ).
cnf(c2353,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,X3375)
| ~ present(skc29,X3375)
| ~ event(skc29,X3375)
| ~ theme(skc29,X3375,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ agent(skc29,X3375,skc35)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c1835,clause29]) ).
cnf(c2370,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ theme(skc29,skc33,skc32)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2353,c250]) ).
cnf(c2389,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ forename(skc29,skc36)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2370,clause28]) ).
cnf(c2403,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc36)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2389,c253]) ).
cnf(c2422,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2403,clause14]) ).
cnf(c2443,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ state(skc29,skc30)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2422,c244]) ).
cnf(c2473,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ man(skc29,skc35)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2443,clause3]) ).
cnf(c2489,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ forename(skc29,skc34)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2473,c241]) ).
cnf(c2508,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ vincent_forename(skc29,skc34)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2489,c249]) ).
cnf(c2526,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ event(skc29,skc33)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2508,clause11]) ).
cnf(c2536,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ present(skc29,skc33)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2526,c252]) ).
cnf(c2556,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ think_believe_consider(skc29,skc33)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2536,c246]) ).
cnf(c2581,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ accessible_world(skc29,skc32)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2556,clause9]) ).
cnf(c2594,plain,
( ssSkC0
| ~ proposition(skc29,skc32)
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2581,clause5]) ).
cnf(c2624,plain,
( ssSkC0
| ~ actual_world(skc29)
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2594,c247]) ).
cnf(c2631,plain,
( ssSkC0
| of(skc17,skc24,skc25) ),
inference(resolution,[status(thm)],[c2624,clause1]) ).
cnf(c2649,plain,
of(skc17,skc24,skc25),
inference(resolution,[status(thm)],[c2631,clause34]) ).
cnf(clause45,negated_conjecture,
( ~ man(skc22,X15)
| ~ ssSkC0
| agent(skc22,skf5(X15),X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(clause43,negated_conjecture,
( ~ man(skc22,X12)
| ~ ssSkC0
| smoke(skc22,skf5(X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(clause42,negated_conjecture,
( ~ man(skc22,X10)
| ~ ssSkC0
| present(skc22,skf5(X11)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(clause41,negated_conjecture,
( ~ man(skc22,X8)
| ~ ssSkC0
| event(skc22,skf5(X9)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(clause2,negated_conjecture,
actual_world(skc17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP221-1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 13:36:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 13.67/13.83 % Version: 1.5
% 13.67/13.83 % SZS status Satisfiable
% 13.67/13.83 % SZS output start Saturation
% See solution above
% 13.68/13.84
% 13.68/13.84 % Initial clauses : 49
% 13.68/13.84 % Processed clauses : 800
% 13.68/13.84 % Factors computed : 30
% 13.68/13.84 % Resolvents computed: 5343
% 13.68/13.84 % Tautologies deleted: 2
% 13.68/13.84 % Forward subsumed : 4620
% 13.68/13.84 % Backward subsumed : 769
% 13.68/13.84 % -------- CPU Time ---------
% 13.68/13.84 % User time : 13.475 s
% 13.68/13.84 % System time : 0.023 s
% 13.68/13.84 % Total time : 13.498 s
%------------------------------------------------------------------------------