%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP222-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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 2.14s 2.32s
% Output : Saturation 2.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| be(skc17,skc18,skc21,skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(clause1,negated_conjecture,
actual_world(skc29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause3,negated_conjecture,
( ssSkC0
| proposition(skc29,skc33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
( ssSkC0
| accessible_world(skc29,skc33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
( ssSkC0
| think_believe_consider(skc29,skc34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
( ssSkC0
| present(skc29,skc34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(clause7,negated_conjecture,
( ssSkC0
| event(skc29,skc34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause8,negated_conjecture,
( ssSkC0
| vincent_forename(skc29,skc35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| forename(skc29,skc35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause10,negated_conjecture,
( ssSkC0
| man(skc29,skc36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(clause11,negated_conjecture,
( ssSkC0
| state(skc29,skc30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| man(skc29,skc31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(clause14,negated_conjecture,
( ssSkC0
| jules_forename(skc29,skc32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,negated_conjecture,
( ssSkC0
| forename(skc29,skc32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(clause28,negated_conjecture,
( ssSkC0
| theme(skc29,skc34,skc33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(clause29,negated_conjecture,
( ssSkC0
| agent(skc29,skc34,skc36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( ssSkC0
| of(skc29,skc35,skc36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(clause31,negated_conjecture,
( ssSkC0
| of(skc29,skc32,skc31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(clause40,negated_conjecture,
( ~ man(skc33,X7)
| ssSkC0
| smoke(skc33,skf9(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(clause36,negated_conjecture,
( ssSkC0
| be(skc29,skc30,skc31,skc31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(clause47,negated_conjecture,
( ~ proposition(X25,X28)
| ~ accessible_world(X25,X28)
| ~ think_believe_consider(X25,X30)
| ~ present(X25,X30)
| ~ event(X25,X30)
| ~ theme(X25,X30,X28)
| ~ vincent_forename(X25,X32)
| ~ forename(X25,X32)
| ~ agent(X25,X30,X26)
| ~ man(X25,X26)
| ~ of(X25,X32,X26)
| ~ state(X25,X27)
| ~ man(X25,X24)
| ~ jules_forename(X25,X29)
| ~ forename(X25,X29)
| ~ be(X25,X27,X31,X24)
| ~ man(X25,X31)
| ~ of(X25,X29,X31)
| ~ actual_world(X25)
| ssSkC0
| man(X28,skf11(X28)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c307,plain,
( ~ proposition(skc29,X53)
| ~ accessible_world(skc29,X53)
| ~ think_believe_consider(skc29,X54)
| ~ present(skc29,X54)
| ~ event(skc29,X54)
| ~ theme(skc29,X54,X53)
| ~ vincent_forename(skc29,X56)
| ~ forename(skc29,X56)
| ~ agent(skc29,X54,X55)
| ~ man(skc29,X55)
| ~ of(skc29,X56,X55)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X52)
| ~ forename(skc29,X52)
| ~ of(skc29,X52,skc31)
| ~ actual_world(skc29)
| ssSkC0
| man(X53,skf11(X53)) ),
inference(resolution,[status(thm)],[clause47,clause36]) ).
cnf(c428,plain,
( ~ proposition(skc29,X123)
| ~ accessible_world(skc29,X123)
| ~ think_believe_consider(skc29,X121)
| ~ present(skc29,X121)
| ~ event(skc29,X121)
| ~ theme(skc29,X121,X123)
| ~ vincent_forename(skc29,X124)
| ~ forename(skc29,X124)
| ~ agent(skc29,X121,X122)
| ~ man(skc29,X122)
| ~ of(skc29,X124,X122)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(X123,skf11(X123)) ),
inference(resolution,[status(thm)],[c307,clause31]) ).
cnf(c493,plain,
( ~ proposition(skc29,X186)
| ~ accessible_world(skc29,X186)
| ~ think_believe_consider(skc29,X185)
| ~ present(skc29,X185)
| ~ event(skc29,X185)
| ~ theme(skc29,X185,X186)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ agent(skc29,X185,skc36)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(X186,skf11(X186)) ),
inference(resolution,[status(thm)],[c428,clause30]) ).
cnf(c505,plain,
( ~ proposition(skc29,X187)
| ~ accessible_world(skc29,X187)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ theme(skc29,skc34,X187)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(X187,skf11(X187)) ),
inference(resolution,[status(thm)],[c493,clause29]) ).
cnf(c527,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c505,clause28]) ).
cnf(c548,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c527,clause13]) ).
cnf(c558,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c548,clause14]) ).
cnf(c576,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c558,clause12]) ).
cnf(c591,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c576,clause11]) ).
cnf(c622,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c591,clause10]) ).
cnf(c644,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c622,clause9]) ).
cnf(c659,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c644,clause8]) ).
cnf(c669,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c659,clause7]) ).
cnf(c691,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c669,clause6]) ).
cnf(c715,plain,
( ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c691,clause5]) ).
cnf(c740,plain,
( ~ proposition(skc29,skc33)
| ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c715,clause4]) ).
cnf(c742,plain,
( ~ actual_world(skc29)
| ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c740,clause3]) ).
cnf(c760,plain,
( ssSkC0
| man(skc33,skf11(skc33)) ),
inference(resolution,[status(thm)],[c742,clause1]) ).
cnf(c781,plain,
( ssSkC0
| smoke(skc33,skf9(X205)) ),
inference(resolution,[status(thm)],[c760,clause40]) ).
cnf(clause39,negated_conjecture,
( ~ man(skc33,X5)
| ssSkC0
| present(skc33,skf9(X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c782,plain,
( ssSkC0
| present(skc33,skf9(X212)) ),
inference(resolution,[status(thm)],[c760,clause39]) ).
cnf(clause38,negated_conjecture,
( ~ man(skc33,X3)
| ssSkC0
| event(skc33,skf9(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c779,plain,
( ssSkC0
| event(skc33,skf9(X204)) ),
inference(resolution,[status(thm)],[c760,clause38]) ).
cnf(clause49,negated_conjecture,
( ~ proposition(X43,X46)
| ~ accessible_world(X43,X46)
| ~ smoke(X46,X48)
| ~ present(X46,X48)
| ~ agent(X46,X48,skf11(X46))
| ~ event(X46,X48)
| ~ think_believe_consider(X43,X51)
| ~ present(X43,X51)
| ~ event(X43,X51)
| ~ theme(X43,X51,X46)
| ~ vincent_forename(X43,X44)
| ~ forename(X43,X44)
| ~ agent(X43,X51,X45)
| ~ man(X43,X45)
| ~ of(X43,X44,X45)
| ~ state(X43,X42)
| ~ man(X43,X47)
| ~ jules_forename(X43,X50)
| ~ forename(X43,X50)
| ~ be(X43,X42,X49,X47)
| ~ man(X43,X49)
| ~ of(X43,X50,X49)
| ~ actual_world(X43)
| ssSkC0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c309,plain,
( ~ proposition(skc29,X98)
| ~ accessible_world(skc29,X98)
| ~ smoke(X98,X99)
| ~ present(X98,X99)
| ~ agent(X98,X99,skf11(X98))
| ~ event(X98,X99)
| ~ think_believe_consider(skc29,X100)
| ~ present(skc29,X100)
| ~ event(skc29,X100)
| ~ theme(skc29,X100,X98)
| ~ vincent_forename(skc29,X95)
| ~ forename(skc29,X95)
| ~ agent(skc29,X100,X96)
| ~ man(skc29,X96)
| ~ of(skc29,X95,X96)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X97)
| ~ forename(skc29,X97)
| ~ of(skc29,X97,skc31)
| ~ actual_world(skc29)
| ssSkC0 ),
inference(resolution,[status(thm)],[clause49,clause36]) ).
cnf(clause44,negated_conjecture,
( ~ man(skc33,X14)
| ssSkC0
| agent(skc33,skf9(X14),X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c780,plain,
( ssSkC0
| agent(skc33,skf9(skf11(skc33)),skf11(skc33)) ),
inference(resolution,[status(thm)],[c760,clause44]) ).
cnf(c872,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ smoke(skc33,skf9(skf11(skc33)))
| ~ present(skc33,skf9(skf11(skc33)))
| ~ event(skc33,skf9(skf11(skc33)))
| ~ think_believe_consider(skc29,X980)
| ~ present(skc29,X980)
| ~ event(skc29,X980)
| ~ theme(skc29,X980,skc33)
| ~ vincent_forename(skc29,X979)
| ~ forename(skc29,X979)
| ~ agent(skc29,X980,X981)
| ~ man(skc29,X981)
| ~ of(skc29,X979,X981)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X978)
| ~ forename(skc29,X978)
| ~ of(skc29,X978,skc31)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c780,c309]) ).
cnf(c913,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ smoke(skc33,skf9(skf11(skc33)))
| ~ present(skc33,skf9(skf11(skc33)))
| ~ think_believe_consider(skc29,X983)
| ~ present(skc29,X983)
| ~ event(skc29,X983)
| ~ theme(skc29,X983,skc33)
| ~ vincent_forename(skc29,X982)
| ~ forename(skc29,X982)
| ~ agent(skc29,X983,X984)
| ~ man(skc29,X984)
| ~ of(skc29,X982,X984)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X985)
| ~ forename(skc29,X985)
| ~ of(skc29,X985,skc31)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c872,c779]) ).
cnf(c929,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ smoke(skc33,skf9(skf11(skc33)))
| ~ think_believe_consider(skc29,X986)
| ~ present(skc29,X986)
| ~ event(skc29,X986)
| ~ theme(skc29,X986,skc33)
| ~ vincent_forename(skc29,X988)
| ~ forename(skc29,X988)
| ~ agent(skc29,X986,X987)
| ~ man(skc29,X987)
| ~ of(skc29,X988,X987)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X989)
| ~ forename(skc29,X989)
| ~ of(skc29,X989,skc31)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c913,c782]) ).
cnf(c956,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,X993)
| ~ present(skc29,X993)
| ~ event(skc29,X993)
| ~ theme(skc29,X993,skc33)
| ~ vincent_forename(skc29,X992)
| ~ forename(skc29,X992)
| ~ agent(skc29,X993,X990)
| ~ man(skc29,X990)
| ~ of(skc29,X992,X990)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,X991)
| ~ forename(skc29,X991)
| ~ of(skc29,X991,skc31)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c929,c781]) ).
cnf(c971,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,X1033)
| ~ present(skc29,X1033)
| ~ event(skc29,X1033)
| ~ theme(skc29,X1033,skc33)
| ~ vincent_forename(skc29,X1034)
| ~ forename(skc29,X1034)
| ~ agent(skc29,X1033,X1035)
| ~ man(skc29,X1035)
| ~ of(skc29,X1034,X1035)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c956,clause31]) ).
cnf(c1035,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,X1071)
| ~ present(skc29,X1071)
| ~ event(skc29,X1071)
| ~ theme(skc29,X1071,skc33)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ agent(skc29,X1071,skc36)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c971,clause30]) ).
cnf(c1047,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ theme(skc29,skc34,skc33)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1035,clause29]) ).
cnf(c1069,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ forename(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1047,clause28]) ).
cnf(c1090,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ jules_forename(skc29,skc32)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1069,clause13]) ).
cnf(c1100,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ man(skc29,skc31)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1090,clause14]) ).
cnf(c1118,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ state(skc29,skc30)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1100,clause12]) ).
cnf(c1133,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ man(skc29,skc36)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1118,clause11]) ).
cnf(c1164,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ forename(skc29,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1133,clause10]) ).
cnf(c1186,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ vincent_forename(skc29,skc35)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1164,clause9]) ).
cnf(c1201,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ event(skc29,skc34)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1186,clause8]) ).
cnf(c1211,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ present(skc29,skc34)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1201,clause7]) ).
cnf(c1233,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ think_believe_consider(skc29,skc34)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1211,clause6]) ).
cnf(c1257,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ accessible_world(skc29,skc33)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1233,clause5]) ).
cnf(c1282,plain,
( ssSkC0
| ~ proposition(skc29,skc33)
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1257,clause4]) ).
cnf(c1284,plain,
( ssSkC0
| ~ actual_world(skc29) ),
inference(resolution,[status(thm)],[c1282,clause3]) ).
cnf(c1302,plain,
ssSkC0,
inference(resolution,[status(thm)],[c1284,clause1]) ).
cnf(c1304,plain,
be(skc17,skc18,skc21,skc19),
inference(resolution,[status(thm)],[c1302,clause37]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| theme(skc17,skc23,skc22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c1319,plain,
theme(skc17,skc23,skc22),
inference(resolution,[status(thm)],[c1302,clause32]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| of(skc17,skc24,skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c1318,plain,
of(skc17,skc24,skc25),
inference(resolution,[status(thm)],[c1302,clause34]) ).
cnf(clause35,negated_conjecture,
( ~ ssSkC0
| of(skc17,skc20,skc21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c1316,plain,
of(skc17,skc20,skc21),
inference(resolution,[status(thm)],[c1302,clause35]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| agent(skc17,skc23,skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c1313,plain,
agent(skc17,skc23,skc25),
inference(resolution,[status(thm)],[c1302,clause33]) ).
cnf(clause19,negated_conjecture,
( ~ ssSkC0
| event(skc17,skc23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c1320,plain,
event(skc17,skc23),
inference(resolution,[status(thm)],[c1302,clause19]) ).
cnf(clause15,negated_conjecture,
( ~ ssSkC0
| proposition(skc17,skc22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c1317,plain,
proposition(skc17,skc22),
inference(resolution,[status(thm)],[c1302,clause15]) ).
cnf(clause27,negated_conjecture,
( ~ ssSkC0
| man(skc17,skc21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c1315,plain,
man(skc17,skc21),
inference(resolution,[status(thm)],[c1302,clause27]) ).
cnf(clause18,negated_conjecture,
( ~ ssSkC0
| present(skc17,skc23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c1314,plain,
present(skc17,skc23),
inference(resolution,[status(thm)],[c1302,clause18]) ).
cnf(clause26,negated_conjecture,
( ~ ssSkC0
| forename(skc17,skc20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c1312,plain,
forename(skc17,skc20),
inference(resolution,[status(thm)],[c1302,clause26]) ).
cnf(clause20,negated_conjecture,
( ~ ssSkC0
| vincent_forename(skc17,skc24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c1311,plain,
vincent_forename(skc17,skc24),
inference(resolution,[status(thm)],[c1302,clause20]) ).
cnf(clause22,negated_conjecture,
( ~ ssSkC0
| man(skc17,skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c1310,plain,
man(skc17,skc25),
inference(resolution,[status(thm)],[c1302,clause22]) ).
cnf(clause24,negated_conjecture,
( ~ ssSkC0
| man(skc17,skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c1309,plain,
man(skc17,skc19),
inference(resolution,[status(thm)],[c1302,clause24]) ).
cnf(clause21,negated_conjecture,
( ~ ssSkC0
| forename(skc17,skc24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c1308,plain,
forename(skc17,skc24),
inference(resolution,[status(thm)],[c1302,clause21]) ).
cnf(clause23,negated_conjecture,
( ~ ssSkC0
| state(skc17,skc18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(c1307,plain,
state(skc17,skc18),
inference(resolution,[status(thm)],[c1302,clause23]) ).
cnf(clause25,negated_conjecture,
( ~ ssSkC0
| jules_forename(skc17,skc20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(c1306,plain,
jules_forename(skc17,skc20),
inference(resolution,[status(thm)],[c1302,clause25]) ).
cnf(clause16,negated_conjecture,
( ~ ssSkC0
| accessible_world(skc17,skc22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c1305,plain,
accessible_world(skc17,skc22),
inference(resolution,[status(thm)],[c1302,clause16]) ).
cnf(clause17,negated_conjecture,
( ~ ssSkC0
| think_believe_consider(skc17,skc23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c1303,plain,
think_believe_consider(skc17,skc23),
inference(resolution,[status(thm)],[c1302,clause17]) ).
cnf(clause48,negated_conjecture,
( ~ proposition(X34,X37)
| ~ accessible_world(X34,X37)
| ~ smoke(X37,X39)
| ~ present(X37,X39)
| ~ agent(X37,X39,skf7(X37))
| ~ event(X37,X39)
| ~ think_believe_consider(X34,X41)
| ~ present(X34,X41)
| ~ event(X34,X41)
| ~ theme(X34,X41,X37)
| ~ vincent_forename(X34,X35)
| ~ forename(X34,X35)
| ~ agent(X34,X41,X36)
| ~ man(X34,X36)
| ~ of(X34,X35,X36)
| ~ state(X34,X33)
| ~ man(X34,X38)
| ~ be(X34,X33,X38,X38)
| ~ forename(X34,X40)
| ~ jules_forename(X34,X40)
| ~ of(X34,X40,X38)
| ~ actual_world(X34)
| ~ ssSkC0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(clause46,negated_conjecture,
( ~ proposition(X17,X20)
| ~ accessible_world(X17,X20)
| ~ think_believe_consider(X17,X22)
| ~ present(X17,X22)
| ~ event(X17,X22)
| ~ theme(X17,X22,X20)
| ~ vincent_forename(X17,X23)
| ~ forename(X17,X23)
| ~ agent(X17,X22,X18)
| ~ man(X17,X18)
| ~ of(X17,X23,X18)
| ~ state(X17,X19)
| ~ man(X17,X16)
| ~ be(X17,X19,X16,X16)
| ~ forename(X17,X21)
| ~ jules_forename(X17,X21)
| ~ of(X17,X21,X16)
| ~ actual_world(X17)
| ~ ssSkC0
| man(X20,skf7(X20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(clause45,negated_conjecture,
( ~ man(skc22,X15)
| ~ ssSkC0
| agent(skc22,skf5(X15),X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(clause43,negated_conjecture,
( ~ man(skc22,X13)
| ~ ssSkC0
| smoke(skc22,skf5(X12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(clause42,negated_conjecture,
( ~ man(skc22,X11)
| ~ ssSkC0
| present(skc22,skf5(X10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(clause41,negated_conjecture,
( ~ man(skc22,X9)
| ~ ssSkC0
| event(skc22,skf5(X8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(clause2,negated_conjecture,
actual_world(skc17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NLP222-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n012.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 13:49:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 2.14/2.32 % Version: 1.5
% 2.14/2.32 % SZS status Satisfiable
% 2.14/2.32 % SZS output start Saturation
% See solution above
% 2.14/2.32
% 2.14/2.32 % Initial clauses : 49
% 2.14/2.32 % Processed clauses : 512
% 2.14/2.32 % Factors computed : 3
% 2.14/2.32 % Resolvents computed: 1318
% 2.14/2.32 % Tautologies deleted: 2
% 2.14/2.32 % Forward subsumed : 856
% 2.14/2.32 % Backward subsumed : 485
% 2.14/2.32 % -------- CPU Time ---------
% 2.14/2.32 % User time : 1.952 s
% 2.14/2.32 % System time : 0.015 s
% 2.14/2.32 % Total time : 1.967 s
%------------------------------------------------------------------------------