%------------------------------------------------------------------------------
% 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 : n014.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 : Theorem 11.07s 11.27s
% Output : Refutation 11.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NLP257+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n014.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 13:43:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 11.07/11.27 % Version: 1.5
% 11.07/11.27 % SZS status Theorem
% 11.07/11.27 % SZS output start CNFRefutation
% 11.07/11.27 fof(co1,conjecture,(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]:(man(Y,X3)=>(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1)))))))))))&(~(?[X5]:(actual_world(X5)&(?[X6]:(?[X7]:(?[X8]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X9]:(?[X10]:(((((((((((((((((((((((((((((((((of(X5,X7,X6)&man(X5,X6))&jules_forename(X5,X7))&forename(X5,X7))&of(X5,X8,V))&vincent_forename(X5,X8))&forename(X5,X8))&of(X5,W,V))&man(X5,V))&vincent_forename(X5,W))&forename(X5,W))&proposition(X5,Y))&agent(X5,X,V))&theme(X5,X,Y))&event(X5,X))&present(X5,X))&think_believe_consider(X5,X))&accessible_world(X5,Y))&(![X3]:(man(Y,X3)=>(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(X5,Z,X1))&man(X5,X1))&jules_forename(X5,Z))&forename(X5,Z))&man(X5,X1))&state(X5,X2))&be(X5,X2,X1,X1))&proposition(X5,X10))&agent(X5,X9,V))&theme(X5,X9,X10))&event(X5,X9))&present(X5,X9))&think_believe_consider(X5,X9))&accessible_world(X5,X10))&(?[X11]:(((event(X10,X11)&agent(X10,X11,X6))&present(X10,X11))&smoke(X10,X11))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 11.07/11.27 fof(c36,negated_conjecture,(~(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]:(man(Y,X3)=>(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1)))))))))))&(~(?[X5]:(actual_world(X5)&(?[X6]:(?[X7]:(?[X8]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X9]:(?[X10]:(((((((((((((((((((((((((((((((((of(X5,X7,X6)&man(X5,X6))&jules_forename(X5,X7))&forename(X5,X7))&of(X5,X8,V))&vincent_forename(X5,X8))&forename(X5,X8))&of(X5,W,V))&man(X5,V))&vincent_forename(X5,W))&forename(X5,W))&proposition(X5,Y))&agent(X5,X,V))&theme(X5,X,Y))&event(X5,X))&present(X5,X))&think_believe_consider(X5,X))&accessible_world(X5,Y))&(![X3]:(man(Y,X3)=>(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(X5,Z,X1))&man(X5,X1))&jules_forename(X5,Z))&forename(X5,Z))&man(X5,X1))&state(X5,X2))&be(X5,X2,X1,X1))&proposition(X5,X10))&agent(X5,X9,V))&theme(X5,X9,X10))&event(X5,X9))&present(X5,X9))&think_believe_consider(X5,X9))&accessible_world(X5,X10))&(?[X11]:(((event(X10,X11)&agent(X10,X11,X6))&present(X10,X11))&smoke(X10,X11)))))))))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 11.07/11.27 fof(c37,negated_conjecture,((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:((((((((((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![X3]:(~man(Y,X3)|(?[X4]:(((event(Y,X4)&agent(Y,X4,X3))&present(Y,X4))&smoke(Y,X4))))))&of(U,Z,X1))&man(U,X1))&jules_forename(U,Z))&forename(U,Z))&man(U,X1))&state(U,X2))&be(U,X2,X1,X1)))))))))))&(![X5]:(~actual_world(X5)|(![X6]:(![X7]:(![X8]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(![X2]:(![X9]:(![X10]:(((((((((((((((((((((((((((((((((~of(X5,X7,X6)|~man(X5,X6))|~jules_forename(X5,X7))|~forename(X5,X7))|~of(X5,X8,V))|~vincent_forename(X5,X8))|~forename(X5,X8))|~of(X5,W,V))|~man(X5,V))|~vincent_forename(X5,W))|~forename(X5,W))|~proposition(X5,Y))|~agent(X5,X,V))|~theme(X5,X,Y))|~event(X5,X))|~present(X5,X))|~think_believe_consider(X5,X))|~accessible_world(X5,Y))|(?[X3]:(man(Y,X3)&(![X4]:(((~event(Y,X4)|~agent(Y,X4,X3))|~present(Y,X4))|~smoke(Y,X4))))))|~of(X5,Z,X1))|~man(X5,X1))|~jules_forename(X5,Z))|~forename(X5,Z))|~man(X5,X1))|~state(X5,X2))|~be(X5,X2,X1,X1))|~proposition(X5,X10))|~agent(X5,X9,V))|~theme(X5,X9,X10))|~event(X5,X9))|~present(X5,X9))|~think_believe_consider(X5,X9))|~accessible_world(X5,X10))|(![X11]:(((~event(X10,X11)|~agent(X10,X11,X6))|~present(X10,X11))|~smoke(X10,X11))))))))))))))))))),inference(fof_nnf,[status(thm)],[c36])).
% 11.07/11.27 fof(c38,negated_conjecture,((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((((((((((of(X2,X4,X3)&man(X2,X3))&vincent_forename(X2,X4))&forename(X2,X4))&proposition(X2,X6))&agent(X2,X5,X3))&theme(X2,X5,X6))&event(X2,X5))&present(X2,X5))&think_believe_consider(X2,X5))&accessible_world(X2,X6))&(![X10]:(~man(X6,X10)|(?[X11]:(((event(X6,X11)&agent(X6,X11,X10))&present(X6,X11))&smoke(X6,X11))))))&of(X2,X7,X8))&man(X2,X8))&jules_forename(X2,X7))&forename(X2,X7))&man(X2,X8))&state(X2,X9))&be(X2,X9,X8,X8)))))))))))&(![X12]:(~actual_world(X12)|(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~jules_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X16))|~vincent_forename(X12,X15))|~forename(X12,X15))|~of(X12,X17,X16))|~man(X12,X16))|~vincent_forename(X12,X17))|~forename(X12,X17))|~proposition(X12,X19))|~agent(X12,X18,X16))|~theme(X12,X18,X19))|~event(X12,X18))|~present(X12,X18))|~think_believe_consider(X12,X18))|~accessible_world(X12,X19))|(?[X25]:(man(X19,X25)&(![X26]:(((~event(X19,X26)|~agent(X19,X26,X25))|~present(X19,X26))|~smoke(X19,X26))))))|~of(X12,X20,X21))|~man(X12,X21))|~jules_forename(X12,X20))|~forename(X12,X20))|~man(X12,X21))|~state(X12,X22))|~be(X12,X22,X21,X21))|~proposition(X12,X24))|~agent(X12,X23,X16))|~theme(X12,X23,X24))|~event(X12,X23))|~present(X12,X23))|~think_believe_consider(X12,X23))|~accessible_world(X12,X24))|(![X27]:(((~event(X24,X27)|~agent(X24,X27,X13))|~present(X24,X27))|~smoke(X24,X27))))))))))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 11.07/11.27 fof(c40,negated_conjecture,(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X26]:(![X27]:((actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&(~man(skolem0005,X10)|(((event(skolem0005,skolem0009(X10))&agent(skolem0005,skolem0009(X10),X10))&present(skolem0005,skolem0009(X10)))&smoke(skolem0005,skolem0009(X10)))))&of(skolem0001,skolem0006,skolem0007))&man(skolem0001,skolem0007))&jules_forename(skolem0001,skolem0006))&forename(skolem0001,skolem0006))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0007,skolem0007)))&(~actual_world(X12)|(((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~jules_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X16))|~vincent_forename(X12,X15))|~forename(X12,X15))|~of(X12,X17,X16))|~man(X12,X16))|~vincent_forename(X12,X17))|~forename(X12,X17))|~proposition(X12,X19))|~agent(X12,X18,X16))|~theme(X12,X18,X19))|~event(X12,X18))|~present(X12,X18))|~think_believe_consider(X12,X18))|~accessible_world(X12,X19))|(man(X19,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24))&(((~event(X19,X26)|~agent(X19,X26,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)))|~present(X19,X26))|~smoke(X19,X26))))|~of(X12,X20,X21))|~man(X12,X21))|~jules_forename(X12,X20))|~forename(X12,X20))|~man(X12,X21))|~state(X12,X22))|~be(X12,X22,X21,X21))|~proposition(X12,X24))|~agent(X12,X23,X16))|~theme(X12,X23,X24))|~event(X12,X23))|~present(X12,X23))|~think_believe_consider(X12,X23))|~accessible_world(X12,X24))|(((~event(X24,X27)|~agent(X24,X27,X13))|~present(X24,X27))|~smoke(X24,X27))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c39,negated_conjecture,((actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&(![X10]:(~man(skolem0005,X10)|(((event(skolem0005,skolem0009(X10))&agent(skolem0005,skolem0009(X10),X10))&present(skolem0005,skolem0009(X10)))&smoke(skolem0005,skolem0009(X10))))))&of(skolem0001,skolem0006,skolem0007))&man(skolem0001,skolem0007))&jules_forename(skolem0001,skolem0006))&forename(skolem0001,skolem0006))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0007,skolem0007)))&(![X12]:(~actual_world(X12)|(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~jules_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X16))|~vincent_forename(X12,X15))|~forename(X12,X15))|~of(X12,X17,X16))|~man(X12,X16))|~vincent_forename(X12,X17))|~forename(X12,X17))|~proposition(X12,X19))|~agent(X12,X18,X16))|~theme(X12,X18,X19))|~event(X12,X18))|~present(X12,X18))|~think_believe_consider(X12,X18))|~accessible_world(X12,X19))|(man(X19,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24))&(![X26]:(((~event(X19,X26)|~agent(X19,X26,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)))|~present(X19,X26))|~smoke(X19,X26)))))|~of(X12,X20,X21))|~man(X12,X21))|~jules_forename(X12,X20))|~forename(X12,X20))|~man(X12,X21))|~state(X12,X22))|~be(X12,X22,X21,X21))|~proposition(X12,X24))|~agent(X12,X23,X16))|~theme(X12,X23,X24))|~event(X12,X23))|~present(X12,X23))|~think_believe_consider(X12,X23))|~accessible_world(X12,X24))|(![X27]:(((~event(X24,X27)|~agent(X24,X27,X13))|~present(X24,X27))|~smoke(X24,X27))))))))))))))))))),inference(skolemize,[status(esa)],[c38])).])).
% 11.07/11.27 fof(c41,negated_conjecture,(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X26]:(![X27]:((actual_world(skolem0001)&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&((((~man(skolem0005,X10)|event(skolem0005,skolem0009(X10)))&(~man(skolem0005,X10)|agent(skolem0005,skolem0009(X10),X10)))&(~man(skolem0005,X10)|present(skolem0005,skolem0009(X10))))&(~man(skolem0005,X10)|smoke(skolem0005,skolem0009(X10)))))&of(skolem0001,skolem0006,skolem0007))&man(skolem0001,skolem0007))&jules_forename(skolem0001,skolem0006))&forename(skolem0001,skolem0006))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0007,skolem0007)))&((~actual_world(X12)|(((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~jules_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X16))|~vincent_forename(X12,X15))|~forename(X12,X15))|~of(X12,X17,X16))|~man(X12,X16))|~vincent_forename(X12,X17))|~forename(X12,X17))|~proposition(X12,X19))|~agent(X12,X18,X16))|~theme(X12,X18,X19))|~event(X12,X18))|~present(X12,X18))|~think_believe_consider(X12,X18))|~accessible_world(X12,X19))|man(X19,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)))|~of(X12,X20,X21))|~man(X12,X21))|~jules_forename(X12,X20))|~forename(X12,X20))|~man(X12,X21))|~state(X12,X22))|~be(X12,X22,X21,X21))|~proposition(X12,X24))|~agent(X12,X23,X16))|~theme(X12,X23,X24))|~event(X12,X23))|~present(X12,X23))|~think_believe_consider(X12,X23))|~accessible_world(X12,X24))|(((~event(X24,X27)|~agent(X24,X27,X13))|~present(X24,X27))|~smoke(X24,X27))))&(~actual_world(X12)|(((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~jules_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X16))|~vincent_forename(X12,X15))|~forename(X12,X15))|~of(X12,X17,X16))|~man(X12,X16))|~vincent_forename(X12,X17))|~forename(X12,X17))|~proposition(X12,X19))|~agent(X12,X18,X16))|~theme(X12,X18,X19))|~event(X12,X18))|~present(X12,X18))|~think_believe_consider(X12,X18))|~accessible_world(X12,X19))|(((~event(X19,X26)|~agent(X19,X26,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24)))|~present(X19,X26))|~smoke(X19,X26)))|~of(X12,X20,X21))|~man(X12,X21))|~jules_forename(X12,X20))|~forename(X12,X20))|~man(X12,X21))|~state(X12,X22))|~be(X12,X22,X21,X21))|~proposition(X12,X24))|~agent(X12,X23,X16))|~theme(X12,X23,X24))|~event(X12,X23))|~present(X12,X23))|~think_believe_consider(X12,X23))|~accessible_world(X12,X24))|(((~event(X24,X27)|~agent(X24,X27,X13))|~present(X24,X27))|~smoke(X24,X27)))))))))))))))))))))),inference(distribute,[status(thm)],[c40])).
% 11.07/11.27 cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c59,negated_conjecture,man(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c60,negated_conjecture,jules_forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c61,negated_conjecture,forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c45,negated_conjecture,vincent_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c46,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c44,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c47,negated_conjecture,proposition(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c50,negated_conjecture,event(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c51,negated_conjecture,present(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c52,negated_conjecture,think_believe_consider(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c53,negated_conjecture,accessible_world(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c63,negated_conjecture,state(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c58,negated_conjecture,of(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c43,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c48,negated_conjecture,agent(skolem0001,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c49,negated_conjecture,theme(skolem0001,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c54,negated_conjecture,~man(skolem0005,X398)|event(skolem0005,skolem0009(X398)),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 11.07/11.27 fof(c134,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 11.07/11.27 fof(c135,plain,(![X103]:(![X104]:(![X105]:((~accessible_world(X104,X105)|~man(X104,X103))|man(X105,X103))))),inference(variable_rename,[status(thm)],[c134])).
% 11.07/11.27 cnf(c136,plain,~accessible_world(X624,X622)|~man(X624,X623)|man(X622,X623),inference(split_conjunct,[status(thm)],[c135])).
% 11.07/11.27 cnf(c655,plain,~accessible_world(skolem0001,X685)|man(X685,skolem0007),inference(resolution,[status(thm)],[c136, c59])).
% 11.07/11.27 cnf(c757,plain,man(skolem0005,skolem0007),inference(resolution,[status(thm)],[c655, c53])).
% 11.07/11.27 cnf(c765,plain,event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c757, c54])).
% 11.07/11.27 cnf(c56,negated_conjecture,~man(skolem0005,X399)|present(skolem0005,skolem0009(X399)),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c761,plain,present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c757, c56])).
% 11.07/11.27 cnf(c57,negated_conjecture,~man(skolem0005,X404)|smoke(skolem0005,skolem0009(X404)),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c760,plain,smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c757, c57])).
% 11.07/11.27 cnf(c55,negated_conjecture,~man(skolem0005,X487)|agent(skolem0005,skolem0009(X487),X487),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c758,plain,agent(skolem0005,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c757, c55])).
% 11.07/11.27 cnf(c64,negated_conjecture,be(skolem0001,skolem0008,skolem0007,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c65,negated_conjecture,~actual_world(X500)|~of(X500,X498,X501)|~man(X500,X501)|~jules_forename(X500,X498)|~forename(X500,X498)|~of(X500,X499,X508)|~vincent_forename(X500,X499)|~forename(X500,X499)|~of(X500,X507,X508)|~man(X500,X508)|~vincent_forename(X500,X507)|~forename(X500,X507)|~proposition(X500,X502)|~agent(X500,X506,X508)|~theme(X500,X506,X502)|~event(X500,X506)|~present(X500,X506)|~think_believe_consider(X500,X506)|~accessible_world(X500,X502)|man(X502,skolem0010(X500,X501,X498,X499,X508,X507,X506,X502,X505,X495,X496,X497,X504))|~of(X500,X505,X495)|~man(X500,X495)|~jules_forename(X500,X505)|~forename(X500,X505)|~man(X500,X495)|~state(X500,X496)|~be(X500,X496,X495,X495)|~proposition(X500,X504)|~agent(X500,X497,X508)|~theme(X500,X497,X504)|~event(X500,X497)|~present(X500,X497)|~think_believe_consider(X500,X497)|~accessible_world(X500,X504)|~event(X504,X503)|~agent(X504,X503,X501)|~present(X504,X503)|~smoke(X504,X503),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c529,plain,~actual_world(skolem0001)|~of(skolem0001,X1086,X1082)|~man(skolem0001,X1082)|~jules_forename(skolem0001,X1086)|~forename(skolem0001,X1086)|~of(skolem0001,X1085,X1080)|~vincent_forename(skolem0001,X1085)|~forename(skolem0001,X1085)|~of(skolem0001,X1088,X1080)|~man(skolem0001,X1080)|~vincent_forename(skolem0001,X1088)|~forename(skolem0001,X1088)|~proposition(skolem0001,X1083)|~agent(skolem0001,X1079,X1080)|~theme(skolem0001,X1079,X1083)|~event(skolem0001,X1079)|~present(skolem0001,X1079)|~think_believe_consider(skolem0001,X1079)|~accessible_world(skolem0001,X1083)|man(X1083,skolem0010(skolem0001,X1082,X1086,X1085,X1080,X1088,X1079,X1083,X1084,skolem0007,skolem0008,X1087,X1081))|~of(skolem0001,X1084,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1084)|~forename(skolem0001,X1084)|~state(skolem0001,skolem0008)|~proposition(skolem0001,X1081)|~agent(skolem0001,X1087,X1080)|~theme(skolem0001,X1087,X1081)|~event(skolem0001,X1087)|~present(skolem0001,X1087)|~think_believe_consider(skolem0001,X1087)|~accessible_world(skolem0001,X1081)|~event(X1081,X1089)|~agent(X1081,X1089,X1082)|~present(X1081,X1089)|~smoke(X1081,X1089),inference(resolution,[status(thm)],[c65, c64])).
% 11.07/11.27 cnf(c1096,plain,~actual_world(skolem0001)|~of(skolem0001,X1470,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1470)|~forename(skolem0001,X1470)|~of(skolem0001,X1464,X1468)|~vincent_forename(skolem0001,X1464)|~forename(skolem0001,X1464)|~of(skolem0001,X1467,X1468)|~man(skolem0001,X1468)|~vincent_forename(skolem0001,X1467)|~forename(skolem0001,X1467)|~proposition(skolem0001,X1466)|~agent(skolem0001,X1465,X1468)|~theme(skolem0001,X1465,X1466)|~event(skolem0001,X1465)|~present(skolem0001,X1465)|~think_believe_consider(skolem0001,X1465)|~accessible_world(skolem0001,X1466)|man(X1466,skolem0010(skolem0001,skolem0007,X1470,X1464,X1468,X1467,X1465,X1466,X1469,skolem0007,skolem0008,X1471,skolem0005))|~of(skolem0001,X1469,skolem0007)|~jules_forename(skolem0001,X1469)|~forename(skolem0001,X1469)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1471,X1468)|~theme(skolem0001,X1471,skolem0005)|~event(skolem0001,X1471)|~present(skolem0001,X1471)|~think_believe_consider(skolem0001,X1471)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007))|~smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c529, c758])).
% 11.07/11.27 cnf(c1311,plain,~actual_world(skolem0001)|~of(skolem0001,X1577,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1577)|~forename(skolem0001,X1577)|~of(skolem0001,X1572,X1575)|~vincent_forename(skolem0001,X1572)|~forename(skolem0001,X1572)|~of(skolem0001,X1576,X1575)|~man(skolem0001,X1575)|~vincent_forename(skolem0001,X1576)|~forename(skolem0001,X1576)|~proposition(skolem0001,X1574)|~agent(skolem0001,X1573,X1575)|~theme(skolem0001,X1573,X1574)|~event(skolem0001,X1573)|~present(skolem0001,X1573)|~think_believe_consider(skolem0001,X1573)|~accessible_world(skolem0001,X1574)|man(X1574,skolem0010(skolem0001,skolem0007,X1577,X1572,X1575,X1576,X1573,X1574,X1579,skolem0007,skolem0008,X1578,skolem0005))|~of(skolem0001,X1579,skolem0007)|~jules_forename(skolem0001,X1579)|~forename(skolem0001,X1579)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1578,X1575)|~theme(skolem0001,X1578,skolem0005)|~event(skolem0001,X1578)|~present(skolem0001,X1578)|~think_believe_consider(skolem0001,X1578)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1096, c760])).
% 11.07/11.27 cnf(c1338,plain,~actual_world(skolem0001)|~of(skolem0001,X1787,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1787)|~forename(skolem0001,X1787)|~of(skolem0001,X1783,X1789)|~vincent_forename(skolem0001,X1783)|~forename(skolem0001,X1783)|~of(skolem0001,X1785,X1789)|~man(skolem0001,X1789)|~vincent_forename(skolem0001,X1785)|~forename(skolem0001,X1785)|~proposition(skolem0001,X1790)|~agent(skolem0001,X1784,X1789)|~theme(skolem0001,X1784,X1790)|~event(skolem0001,X1784)|~present(skolem0001,X1784)|~think_believe_consider(skolem0001,X1784)|~accessible_world(skolem0001,X1790)|man(X1790,skolem0010(skolem0001,skolem0007,X1787,X1783,X1789,X1785,X1784,X1790,X1788,skolem0007,skolem0008,X1786,skolem0005))|~of(skolem0001,X1788,skolem0007)|~jules_forename(skolem0001,X1788)|~forename(skolem0001,X1788)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1786,X1789)|~theme(skolem0001,X1786,skolem0005)|~event(skolem0001,X1786)|~present(skolem0001,X1786)|~think_believe_consider(skolem0001,X1786)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1311, c761])).
% 11.07/11.27 cnf(c1394,plain,~actual_world(skolem0001)|~of(skolem0001,X1795,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1795)|~forename(skolem0001,X1795)|~of(skolem0001,X1801,X1800)|~vincent_forename(skolem0001,X1801)|~forename(skolem0001,X1801)|~of(skolem0001,X1799,X1800)|~man(skolem0001,X1800)|~vincent_forename(skolem0001,X1799)|~forename(skolem0001,X1799)|~proposition(skolem0001,X1802)|~agent(skolem0001,X1798,X1800)|~theme(skolem0001,X1798,X1802)|~event(skolem0001,X1798)|~present(skolem0001,X1798)|~think_believe_consider(skolem0001,X1798)|~accessible_world(skolem0001,X1802)|man(X1802,skolem0010(skolem0001,skolem0007,X1795,X1801,X1800,X1799,X1798,X1802,X1797,skolem0007,skolem0008,X1796,skolem0005))|~of(skolem0001,X1797,skolem0007)|~jules_forename(skolem0001,X1797)|~forename(skolem0001,X1797)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1796,X1800)|~theme(skolem0001,X1796,skolem0005)|~event(skolem0001,X1796)|~present(skolem0001,X1796)|~think_believe_consider(skolem0001,X1796)|~accessible_world(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1338, c765])).
% 11.07/11.27 cnf(c1395,plain,~actual_world(skolem0001)|~of(skolem0001,X1805,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1805)|~forename(skolem0001,X1805)|~of(skolem0001,X1803,X1807)|~vincent_forename(skolem0001,X1803)|~forename(skolem0001,X1803)|~of(skolem0001,X1806,X1807)|~man(skolem0001,X1807)|~vincent_forename(skolem0001,X1806)|~forename(skolem0001,X1806)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1804,X1807)|~theme(skolem0001,X1804,skolem0005)|~event(skolem0001,X1804)|~present(skolem0001,X1804)|~think_believe_consider(skolem0001,X1804)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,X1805,X1803,X1807,X1806,X1804,skolem0005,X1808,skolem0007,skolem0008,X1804,skolem0005))|~of(skolem0001,X1808,skolem0007)|~jules_forename(skolem0001,X1808)|~forename(skolem0001,X1808)|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1394])).
% 11.07/11.27 cnf(c1397,plain,~actual_world(skolem0001)|~of(skolem0001,X1812,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1812)|~forename(skolem0001,X1812)|~of(skolem0001,X1809,X1811)|~vincent_forename(skolem0001,X1809)|~forename(skolem0001,X1809)|~of(skolem0001,X1813,X1811)|~man(skolem0001,X1811)|~vincent_forename(skolem0001,X1813)|~forename(skolem0001,X1813)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1810,X1811)|~theme(skolem0001,X1810,skolem0005)|~event(skolem0001,X1810)|~present(skolem0001,X1810)|~think_believe_consider(skolem0001,X1810)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,X1812,X1809,X1811,X1813,X1810,skolem0005,X1812,skolem0007,skolem0008,X1810,skolem0005))|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1395])).
% 11.07/11.27 cnf(c1401,plain,~actual_world(skolem0001)|~of(skolem0001,X1816,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1816)|~forename(skolem0001,X1816)|~of(skolem0001,X1815,X1814)|~vincent_forename(skolem0001,X1815)|~forename(skolem0001,X1815)|~of(skolem0001,X1817,X1814)|~man(skolem0001,X1814)|~vincent_forename(skolem0001,X1817)|~forename(skolem0001,X1817)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,X1814)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,X1816,X1815,X1814,X1817,skolem0004,skolem0005,X1816,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1397, c49])).
% 11.07/11.27 cnf(c1402,plain,~actual_world(skolem0001)|~of(skolem0001,X1825,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1825)|~forename(skolem0001,X1825)|~of(skolem0001,X1827,skolem0002)|~vincent_forename(skolem0001,X1827)|~forename(skolem0001,X1827)|~of(skolem0001,X1826,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X1826)|~forename(skolem0001,X1826)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,X1825,X1827,skolem0002,X1826,skolem0004,skolem0005,X1825,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1401, c48])).
% 11.07/11.27 cnf(c1405,plain,~actual_world(skolem0001)|~of(skolem0001,X1828,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1828)|~forename(skolem0001,X1828)|~of(skolem0001,X1829,skolem0002)|~vincent_forename(skolem0001,X1829)|~forename(skolem0001,X1829)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,X1828,X1829,skolem0002,X1829,skolem0004,skolem0005,X1828,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1402])).
% 11.07/11.27 cnf(c1407,plain,~actual_world(skolem0001)|~of(skolem0001,X1830,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1830)|~forename(skolem0001,X1830)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,X1830,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,X1830,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1405, c43])).
% 11.07/11.27 cnf(c1408,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1407, c58])).
% 11.07/11.27 cnf(c1409,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1408, c63])).
% 11.07/11.27 cnf(c1410,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1409, c53])).
% 11.07/11.27 cnf(c1413,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1410, c52])).
% 11.07/11.27 cnf(c1414,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1413, c51])).
% 11.07/11.27 cnf(c1415,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1414, c50])).
% 11.07/11.27 cnf(c1416,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1415, c47])).
% 11.07/11.27 cnf(c1417,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1416, c44])).
% 11.07/11.27 cnf(c1421,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1417, c46])).
% 11.07/11.27 cnf(c1422,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1421, c45])).
% 11.07/11.27 cnf(c1423,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1422, c61])).
% 11.07/11.27 cnf(c1424,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1423, c60])).
% 11.07/11.27 cnf(c1425,plain,~actual_world(skolem0001)|man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1424, c59])).
% 11.07/11.27 cnf(c1428,plain,man(skolem0005,skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1425, c42])).
% 11.07/11.27 cnf(c1436,plain,event(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1428, c54])).
% 11.07/11.27 cnf(c1432,plain,present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1428, c56])).
% 11.07/11.27 cnf(c1431,plain,smoke(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1428, c57])).
% 11.07/11.27 cnf(c66,negated_conjecture,~actual_world(X518)|~of(X518,X515,X519)|~man(X518,X519)|~jules_forename(X518,X515)|~forename(X518,X515)|~of(X518,X517,X526)|~vincent_forename(X518,X517)|~forename(X518,X517)|~of(X518,X525,X526)|~man(X518,X526)|~vincent_forename(X518,X525)|~forename(X518,X525)|~proposition(X518,X520)|~agent(X518,X524,X526)|~theme(X518,X524,X520)|~event(X518,X524)|~present(X518,X524)|~think_believe_consider(X518,X524)|~accessible_world(X518,X520)|~event(X520,X516)|~agent(X520,X516,skolem0010(X518,X519,X515,X517,X526,X525,X524,X520,X523,X512,X513,X514,X522))|~present(X520,X516)|~smoke(X520,X516)|~of(X518,X523,X512)|~man(X518,X512)|~jules_forename(X518,X523)|~forename(X518,X523)|~man(X518,X512)|~state(X518,X513)|~be(X518,X513,X512,X512)|~proposition(X518,X522)|~agent(X518,X514,X526)|~theme(X518,X514,X522)|~event(X518,X514)|~present(X518,X514)|~think_believe_consider(X518,X514)|~accessible_world(X518,X522)|~event(X522,X521)|~agent(X522,X521,X519)|~present(X522,X521)|~smoke(X522,X521),inference(split_conjunct,[status(thm)],[c41])).
% 11.07/11.27 cnf(c1429,plain,agent(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1428, c55])).
% 11.07/11.27 cnf(c1556,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~smoke(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2366)|~agent(skolem0005,X2366,skolem0007)|~present(skolem0005,X2366)|~smoke(skolem0005,X2366),inference(resolution,[status(thm)],[c1429, c66])).
% 11.07/11.27 cnf(c1672,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2550)|~agent(skolem0005,X2550,skolem0007)|~present(skolem0005,X2550)|~smoke(skolem0005,X2550),inference(resolution,[status(thm)],[c1556, c1431])).
% 11.07/11.27 cnf(c1718,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0010(skolem0001,skolem0007,skolem0006,skolem0003,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2555)|~agent(skolem0005,X2555,skolem0007)|~present(skolem0005,X2555)|~smoke(skolem0005,X2555),inference(resolution,[status(thm)],[c1672, c1432])).
% 11.07/11.27 cnf(c1720,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2556)|~agent(skolem0005,X2556,skolem0007)|~present(skolem0005,X2556)|~smoke(skolem0005,X2556),inference(resolution,[status(thm)],[c1718, c1436])).
% 11.07/11.27 cnf(c1721,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008)|~event(skolem0005,X2557)|~agent(skolem0005,X2557,skolem0007)|~present(skolem0005,X2557)|~smoke(skolem0005,X2557),inference(resolution,[status(thm)],[c1720, c64])).
% 11.07/11.27 cnf(c1722,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007))|~smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1721, c758])).
% 11.07/11.27 cnf(c1723,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1722, c760])).
% 11.07/11.27 cnf(c1726,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008)|~event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1723, c761])).
% 11.07/11.27 cnf(c1727,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~theme(skolem0001,skolem0004,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1726, c765])).
% 11.07/11.28 cnf(c1728,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,skolem0002)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1727, c49])).
% 11.07/11.28 cnf(c1729,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~of(skolem0001,skolem0003,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1728, c48])).
% 11.07/11.28 cnf(c1730,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1729, c43])).
% 11.07/11.28 cnf(c1732,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1730, c58])).
% 11.07/11.28 cnf(c1733,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1732, c63])).
% 11.07/11.28 cnf(c1734,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1733, c53])).
% 11.07/11.28 cnf(c1735,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1734, c52])).
% 11.07/11.28 cnf(c1736,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1735, c51])).
% 11.07/11.28 cnf(c1738,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002)|~proposition(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1736, c50])).
% 11.07/11.28 cnf(c1739,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1738, c47])).
% 11.07/11.28 cnf(c1740,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1739, c44])).
% 11.07/11.28 cnf(c1741,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~vincent_forename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1740, c46])).
% 11.07/11.28 cnf(c1742,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006),inference(resolution,[status(thm)],[c1741, c45])).
% 11.07/11.28 cnf(c1744,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006),inference(resolution,[status(thm)],[c1742, c61])).
% 11.07/11.28 cnf(c1745,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1744, c60])).
% 11.07/11.28 cnf(c1746,plain,~actual_world(skolem0001),inference(resolution,[status(thm)],[c1745, c59])).
% 11.07/11.28 cnf(c1747,plain,$false,inference(resolution,[status(thm)],[c1746, c42])).
% 11.07/11.28 % SZS output end CNFRefutation
% 11.07/11.28
% 11.07/11.28 % Initial clauses : 135
% 11.07/11.28 % Processed clauses : 1227
% 11.07/11.28 % Factors computed : 125
% 11.07/11.28 % Resolvents computed: 1338
% 11.07/11.28 % Tautologies deleted: 3
% 11.07/11.28 % Forward subsumed : 358
% 11.07/11.28 % Backward subsumed : 194
% 11.07/11.28 % -------- CPU Time ---------
% 11.07/11.28 % User time : 10.905 s
% 11.07/11.28 % System time : 0.015 s
% 11.07/11.28 % Total time : 10.920 s
%------------------------------------------------------------------------------