%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP251+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:52 EDT 2024
% Result : Theorem 19.01s 19.21s
% Output : Refutation 19.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP251+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 13:26:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 19.01/19.21 % Version: 1.5
% 19.01/19.21 % SZS status Theorem
% 19.01/19.21 % SZS output start CNFRefutation
% 19.01/19.21 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]:(?[X9]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X10]:(?[X11]:((((((((((((((((((((((((((((((((((of(X5,X7,X6)&man(X5,X6))&vincent_forename(X5,X7))&forename(X5,X7))&of(X5,X9,X8))&man(X5,X8))&jules_forename(X5,X9))&forename(X5,X9))&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,X11))&agent(X5,X10,X6))&theme(X5,X10,X11))&event(X5,X10))&present(X5,X10))&think_believe_consider(X5,X10))&accessible_world(X5,X11))&(?[X12]:(((event(X11,X12)&agent(X11,X12,X8))&present(X11,X12))&smoke(X11,X12)))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 19.01/19.21 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]:(?[X9]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X10]:(?[X11]:((((((((((((((((((((((((((((((((((of(X5,X7,X6)&man(X5,X6))&vincent_forename(X5,X7))&forename(X5,X7))&of(X5,X9,X8))&man(X5,X8))&jules_forename(X5,X9))&forename(X5,X9))&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,X11))&agent(X5,X10,X6))&theme(X5,X10,X11))&event(X5,X10))&present(X5,X10))&think_believe_consider(X5,X10))&accessible_world(X5,X11))&(?[X12]:(((event(X11,X12)&agent(X11,X12,X8))&present(X11,X12))&smoke(X11,X12))))))))))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 19.01/19.21 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]:(![X9]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(![X2]:(![X10]:(![X11]:((((((((((((((((((((((((((((((((((~of(X5,X7,X6)|~man(X5,X6))|~vincent_forename(X5,X7))|~forename(X5,X7))|~of(X5,X9,X8))|~man(X5,X8))|~jules_forename(X5,X9))|~forename(X5,X9))|~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,X11))|~agent(X5,X10,X6))|~theme(X5,X10,X11))|~event(X5,X10))|~present(X5,X10))|~think_believe_consider(X5,X10))|~accessible_world(X5,X11))|(![X12]:(((~event(X11,X12)|~agent(X11,X12,X8))|~present(X11,X12))|~smoke(X11,X12)))))))))))))))))))),inference(fof_nnf,[status(thm)],[c36])).
% 19.01/19.21 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]:(![X25]:((((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X16,X15))|~man(X12,X15))|~jules_forename(X12,X16))|~forename(X12,X16))|~of(X12,X18,X17))|~man(X12,X17))|~vincent_forename(X12,X18))|~forename(X12,X18))|~proposition(X12,X20))|~agent(X12,X19,X17))|~theme(X12,X19,X20))|~event(X12,X19))|~present(X12,X19))|~think_believe_consider(X12,X19))|~accessible_world(X12,X20))|(?[X26]:(man(X20,X26)&(![X27]:(((~event(X20,X27)|~agent(X20,X27,X26))|~present(X20,X27))|~smoke(X20,X27))))))|~of(X12,X21,X22))|~man(X12,X22))|~jules_forename(X12,X21))|~forename(X12,X21))|~man(X12,X22))|~state(X12,X23))|~be(X12,X23,X22,X22))|~proposition(X12,X25))|~agent(X12,X24,X13))|~theme(X12,X24,X25))|~event(X12,X24))|~present(X12,X24))|~think_believe_consider(X12,X24))|~accessible_world(X12,X25))|(![X28]:(((~event(X25,X28)|~agent(X25,X28,X15))|~present(X25,X28))|~smoke(X25,X28)))))))))))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 19.01/19.21 fof(c40,negated_conjecture,(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X27]:(![X28]:((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))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X16,X15))|~man(X12,X15))|~jules_forename(X12,X16))|~forename(X12,X16))|~of(X12,X18,X17))|~man(X12,X17))|~vincent_forename(X12,X18))|~forename(X12,X18))|~proposition(X12,X20))|~agent(X12,X19,X17))|~theme(X12,X19,X20))|~event(X12,X19))|~present(X12,X19))|~think_believe_consider(X12,X19))|~accessible_world(X12,X20))|(man(X20,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25))&(((~event(X20,X27)|~agent(X20,X27,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25)))|~present(X20,X27))|~smoke(X20,X27))))|~of(X12,X21,X22))|~man(X12,X22))|~jules_forename(X12,X21))|~forename(X12,X21))|~man(X12,X22))|~state(X12,X23))|~be(X12,X23,X22,X22))|~proposition(X12,X25))|~agent(X12,X24,X13))|~theme(X12,X24,X25))|~event(X12,X24))|~present(X12,X24))|~think_believe_consider(X12,X24))|~accessible_world(X12,X25))|(((~event(X25,X28)|~agent(X25,X28,X15))|~present(X25,X28))|~smoke(X25,X28)))))))))))))))))))))),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]:(![X25]:((((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X16,X15))|~man(X12,X15))|~jules_forename(X12,X16))|~forename(X12,X16))|~of(X12,X18,X17))|~man(X12,X17))|~vincent_forename(X12,X18))|~forename(X12,X18))|~proposition(X12,X20))|~agent(X12,X19,X17))|~theme(X12,X19,X20))|~event(X12,X19))|~present(X12,X19))|~think_believe_consider(X12,X19))|~accessible_world(X12,X20))|(man(X20,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25))&(![X27]:(((~event(X20,X27)|~agent(X20,X27,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25)))|~present(X20,X27))|~smoke(X20,X27)))))|~of(X12,X21,X22))|~man(X12,X22))|~jules_forename(X12,X21))|~forename(X12,X21))|~man(X12,X22))|~state(X12,X23))|~be(X12,X23,X22,X22))|~proposition(X12,X25))|~agent(X12,X24,X13))|~theme(X12,X24,X25))|~event(X12,X24))|~present(X12,X24))|~think_believe_consider(X12,X24))|~accessible_world(X12,X25))|(![X28]:(((~event(X25,X28)|~agent(X25,X28,X15))|~present(X25,X28))|~smoke(X25,X28)))))))))))))))))))),inference(skolemize,[status(esa)],[c38])).])).
% 19.01/19.21 fof(c41,negated_conjecture,(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X27]:(![X28]:((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))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X16,X15))|~man(X12,X15))|~jules_forename(X12,X16))|~forename(X12,X16))|~of(X12,X18,X17))|~man(X12,X17))|~vincent_forename(X12,X18))|~forename(X12,X18))|~proposition(X12,X20))|~agent(X12,X19,X17))|~theme(X12,X19,X20))|~event(X12,X19))|~present(X12,X19))|~think_believe_consider(X12,X19))|~accessible_world(X12,X20))|man(X20,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25)))|~of(X12,X21,X22))|~man(X12,X22))|~jules_forename(X12,X21))|~forename(X12,X21))|~man(X12,X22))|~state(X12,X23))|~be(X12,X23,X22,X22))|~proposition(X12,X25))|~agent(X12,X24,X13))|~theme(X12,X24,X25))|~event(X12,X24))|~present(X12,X24))|~think_believe_consider(X12,X24))|~accessible_world(X12,X25))|(((~event(X25,X28)|~agent(X25,X28,X15))|~present(X25,X28))|~smoke(X25,X28))))&(~actual_world(X12)|((((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X16,X15))|~man(X12,X15))|~jules_forename(X12,X16))|~forename(X12,X16))|~of(X12,X18,X17))|~man(X12,X17))|~vincent_forename(X12,X18))|~forename(X12,X18))|~proposition(X12,X20))|~agent(X12,X19,X17))|~theme(X12,X19,X20))|~event(X12,X19))|~present(X12,X19))|~think_believe_consider(X12,X19))|~accessible_world(X12,X20))|(((~event(X20,X27)|~agent(X20,X27,skolem0010(X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25)))|~present(X20,X27))|~smoke(X20,X27)))|~of(X12,X21,X22))|~man(X12,X22))|~jules_forename(X12,X21))|~forename(X12,X21))|~man(X12,X22))|~state(X12,X23))|~be(X12,X23,X22,X22))|~proposition(X12,X25))|~agent(X12,X24,X13))|~theme(X12,X24,X25))|~event(X12,X24))|~present(X12,X24))|~think_believe_consider(X12,X24))|~accessible_world(X12,X25))|(((~event(X25,X28)|~agent(X25,X28,X15))|~present(X25,X28))|~smoke(X25,X28))))))))))))))))))))))),inference(distribute,[status(thm)],[c40])).
% 19.01/19.21 cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c44,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c45,negated_conjecture,vincent_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c46,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c59,negated_conjecture,man(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c60,negated_conjecture,jules_forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c61,negated_conjecture,forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c47,negated_conjecture,proposition(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c50,negated_conjecture,event(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c51,negated_conjecture,present(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c52,negated_conjecture,think_believe_consider(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c53,negated_conjecture,accessible_world(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c63,negated_conjecture,state(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c43,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c58,negated_conjecture,of(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c48,negated_conjecture,agent(skolem0001,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c49,negated_conjecture,theme(skolem0001,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c54,negated_conjecture,~man(skolem0005,X399)|event(skolem0005,skolem0009(X399)),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 19.01/19.21 fof(c134,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 19.01/19.21 fof(c135,plain,(![X104]:(![X105]:(![X106]:((~accessible_world(X105,X106)|~man(X105,X104))|man(X106,X104))))),inference(variable_rename,[status(thm)],[c134])).
% 19.01/19.21 cnf(c136,plain,~accessible_world(X626,X625)|~man(X626,X627)|man(X625,X627),inference(split_conjunct,[status(thm)],[c135])).
% 19.01/19.21 cnf(c654,plain,~accessible_world(skolem0001,X672)|man(X672,skolem0007),inference(resolution,[status(thm)],[c136, c59])).
% 19.01/19.21 cnf(c684,plain,man(skolem0005,skolem0007),inference(resolution,[status(thm)],[c654, c53])).
% 19.01/19.21 cnf(c692,plain,event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c684, c54])).
% 19.01/19.21 cnf(c56,negated_conjecture,~man(skolem0005,X400)|present(skolem0005,skolem0009(X400)),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c691,plain,present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c684, c56])).
% 19.01/19.21 cnf(c57,negated_conjecture,~man(skolem0005,X405)|smoke(skolem0005,skolem0009(X405)),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c685,plain,smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c684, c57])).
% 19.01/19.21 cnf(c55,negated_conjecture,~man(skolem0005,X488)|agent(skolem0005,skolem0009(X488),X488),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c689,plain,agent(skolem0005,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c684, c55])).
% 19.01/19.21 cnf(c64,negated_conjecture,be(skolem0001,skolem0008,skolem0007,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c65,negated_conjecture,~actual_world(X507)|~of(X507,X505,X509)|~man(X507,X509)|~vincent_forename(X507,X505)|~forename(X507,X505)|~of(X507,X508,X495)|~man(X507,X495)|~jules_forename(X507,X508)|~forename(X507,X508)|~of(X507,X499,X502)|~man(X507,X502)|~vincent_forename(X507,X499)|~forename(X507,X499)|~proposition(X507,X504)|~agent(X507,X503,X502)|~theme(X507,X503,X504)|~event(X507,X503)|~present(X507,X503)|~think_believe_consider(X507,X503)|~accessible_world(X507,X504)|man(X504,skolem0010(X507,X509,X505,X495,X508,X502,X499,X503,X504,X506,X496,X498,X497,X500))|~of(X507,X506,X496)|~man(X507,X496)|~jules_forename(X507,X506)|~forename(X507,X506)|~man(X507,X496)|~state(X507,X498)|~be(X507,X498,X496,X496)|~proposition(X507,X500)|~agent(X507,X497,X509)|~theme(X507,X497,X500)|~event(X507,X497)|~present(X507,X497)|~think_believe_consider(X507,X497)|~accessible_world(X507,X500)|~event(X500,X501)|~agent(X500,X501,X495)|~present(X500,X501)|~smoke(X500,X501),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c530,plain,~actual_world(skolem0001)|~of(skolem0001,X1086,X1089)|~man(skolem0001,X1089)|~vincent_forename(skolem0001,X1086)|~forename(skolem0001,X1086)|~of(skolem0001,X1087,X1092)|~man(skolem0001,X1092)|~jules_forename(skolem0001,X1087)|~forename(skolem0001,X1087)|~of(skolem0001,X1091,X1085)|~man(skolem0001,X1085)|~vincent_forename(skolem0001,X1091)|~forename(skolem0001,X1091)|~proposition(skolem0001,X1083)|~agent(skolem0001,X1084,X1085)|~theme(skolem0001,X1084,X1083)|~event(skolem0001,X1084)|~present(skolem0001,X1084)|~think_believe_consider(skolem0001,X1084)|~accessible_world(skolem0001,X1083)|man(X1083,skolem0010(skolem0001,X1089,X1086,X1092,X1087,X1085,X1091,X1084,X1083,X1090,skolem0007,skolem0008,X1093,X1082))|~of(skolem0001,X1090,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1090)|~forename(skolem0001,X1090)|~state(skolem0001,skolem0008)|~proposition(skolem0001,X1082)|~agent(skolem0001,X1093,X1089)|~theme(skolem0001,X1093,X1082)|~event(skolem0001,X1093)|~present(skolem0001,X1093)|~think_believe_consider(skolem0001,X1093)|~accessible_world(skolem0001,X1082)|~event(X1082,X1088)|~agent(X1082,X1088,X1092)|~present(X1082,X1088)|~smoke(X1082,X1088),inference(resolution,[status(thm)],[c65, c64])).
% 19.01/19.21 cnf(c1096,plain,~actual_world(skolem0001)|~of(skolem0001,X1483,X1476)|~man(skolem0001,X1476)|~vincent_forename(skolem0001,X1483)|~forename(skolem0001,X1483)|~of(skolem0001,X1480,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1480)|~forename(skolem0001,X1480)|~of(skolem0001,X1481,X1478)|~man(skolem0001,X1478)|~vincent_forename(skolem0001,X1481)|~forename(skolem0001,X1481)|~proposition(skolem0001,X1484)|~agent(skolem0001,X1477,X1478)|~theme(skolem0001,X1477,X1484)|~event(skolem0001,X1477)|~present(skolem0001,X1477)|~think_believe_consider(skolem0001,X1477)|~accessible_world(skolem0001,X1484)|man(X1484,skolem0010(skolem0001,X1476,X1483,skolem0007,X1480,X1478,X1481,X1477,X1484,X1479,skolem0007,skolem0008,X1482,skolem0005))|~of(skolem0001,X1479,skolem0007)|~jules_forename(skolem0001,X1479)|~forename(skolem0001,X1479)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1482,X1476)|~theme(skolem0001,X1482,skolem0005)|~event(skolem0001,X1482)|~present(skolem0001,X1482)|~think_believe_consider(skolem0001,X1482)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007))|~smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c530, c689])).
% 19.01/19.21 cnf(c1313,plain,~actual_world(skolem0001)|~of(skolem0001,X1630,X1628)|~man(skolem0001,X1628)|~vincent_forename(skolem0001,X1630)|~forename(skolem0001,X1630)|~of(skolem0001,X1632,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1632)|~forename(skolem0001,X1632)|~of(skolem0001,X1625,X1626)|~man(skolem0001,X1626)|~vincent_forename(skolem0001,X1625)|~forename(skolem0001,X1625)|~proposition(skolem0001,X1631)|~agent(skolem0001,X1633,X1626)|~theme(skolem0001,X1633,X1631)|~event(skolem0001,X1633)|~present(skolem0001,X1633)|~think_believe_consider(skolem0001,X1633)|~accessible_world(skolem0001,X1631)|man(X1631,skolem0010(skolem0001,X1628,X1630,skolem0007,X1632,X1626,X1625,X1633,X1631,X1627,skolem0007,skolem0008,X1629,skolem0005))|~of(skolem0001,X1627,skolem0007)|~jules_forename(skolem0001,X1627)|~forename(skolem0001,X1627)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1629,X1628)|~theme(skolem0001,X1629,skolem0005)|~event(skolem0001,X1629)|~present(skolem0001,X1629)|~think_believe_consider(skolem0001,X1629)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1096, c685])).
% 19.01/19.21 cnf(c1351,plain,~actual_world(skolem0001)|~of(skolem0001,X1884,X1889)|~man(skolem0001,X1889)|~vincent_forename(skolem0001,X1884)|~forename(skolem0001,X1884)|~of(skolem0001,X1888,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1888)|~forename(skolem0001,X1888)|~of(skolem0001,X1885,X1891)|~man(skolem0001,X1891)|~vincent_forename(skolem0001,X1885)|~forename(skolem0001,X1885)|~proposition(skolem0001,X1890)|~agent(skolem0001,X1887,X1891)|~theme(skolem0001,X1887,X1890)|~event(skolem0001,X1887)|~present(skolem0001,X1887)|~think_believe_consider(skolem0001,X1887)|~accessible_world(skolem0001,X1890)|man(X1890,skolem0010(skolem0001,X1889,X1884,skolem0007,X1888,X1891,X1885,X1887,X1890,X1886,skolem0007,skolem0008,X1892,skolem0005))|~of(skolem0001,X1886,skolem0007)|~jules_forename(skolem0001,X1886)|~forename(skolem0001,X1886)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1892,X1889)|~theme(skolem0001,X1892,skolem0005)|~event(skolem0001,X1892)|~present(skolem0001,X1892)|~think_believe_consider(skolem0001,X1892)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1313, c691])).
% 19.01/19.21 cnf(c1420,plain,~actual_world(skolem0001)|~of(skolem0001,X2174,X2169)|~man(skolem0001,X2169)|~vincent_forename(skolem0001,X2174)|~forename(skolem0001,X2174)|~of(skolem0001,X2177,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2177)|~forename(skolem0001,X2177)|~of(skolem0001,X2171,X2175)|~man(skolem0001,X2175)|~vincent_forename(skolem0001,X2171)|~forename(skolem0001,X2171)|~proposition(skolem0001,X2172)|~agent(skolem0001,X2173,X2175)|~theme(skolem0001,X2173,X2172)|~event(skolem0001,X2173)|~present(skolem0001,X2173)|~think_believe_consider(skolem0001,X2173)|~accessible_world(skolem0001,X2172)|man(X2172,skolem0010(skolem0001,X2169,X2174,skolem0007,X2177,X2175,X2171,X2173,X2172,X2170,skolem0007,skolem0008,X2176,skolem0005))|~of(skolem0001,X2170,skolem0007)|~jules_forename(skolem0001,X2170)|~forename(skolem0001,X2170)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X2176,X2169)|~theme(skolem0001,X2176,skolem0005)|~event(skolem0001,X2176)|~present(skolem0001,X2176)|~think_believe_consider(skolem0001,X2176)|~accessible_world(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1351, c692])).
% 19.01/19.21 cnf(c1477,plain,~actual_world(skolem0001)|~of(skolem0001,X2187,X2190)|~man(skolem0001,X2190)|~vincent_forename(skolem0001,X2187)|~forename(skolem0001,X2187)|~of(skolem0001,X2188,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2188)|~forename(skolem0001,X2188)|~of(skolem0001,X2184,X2186)|~man(skolem0001,X2186)|~vincent_forename(skolem0001,X2184)|~forename(skolem0001,X2184)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X2189,X2186)|~theme(skolem0001,X2189,skolem0005)|~event(skolem0001,X2189)|~present(skolem0001,X2189)|~think_believe_consider(skolem0001,X2189)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X2190,X2187,skolem0007,X2188,X2186,X2184,X2189,skolem0005,X2185,skolem0007,skolem0008,X2189,skolem0005))|~of(skolem0001,X2185,skolem0007)|~jules_forename(skolem0001,X2185)|~forename(skolem0001,X2185)|~state(skolem0001,skolem0008)|~agent(skolem0001,X2189,X2190),inference(factor,[status(thm)],[c1420])).
% 19.01/19.21 cnf(c1480,plain,~actual_world(skolem0001)|~of(skolem0001,X2191,X2193)|~man(skolem0001,X2193)|~vincent_forename(skolem0001,X2191)|~forename(skolem0001,X2191)|~of(skolem0001,X2196,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2196)|~forename(skolem0001,X2196)|~of(skolem0001,X2194,X2193)|~vincent_forename(skolem0001,X2194)|~forename(skolem0001,X2194)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X2195,X2193)|~theme(skolem0001,X2195,skolem0005)|~event(skolem0001,X2195)|~present(skolem0001,X2195)|~think_believe_consider(skolem0001,X2195)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X2193,X2191,skolem0007,X2196,X2193,X2194,X2195,skolem0005,X2192,skolem0007,skolem0008,X2195,skolem0005))|~of(skolem0001,X2192,skolem0007)|~jules_forename(skolem0001,X2192)|~forename(skolem0001,X2192)|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1477])).
% 19.01/19.21 cnf(c1483,plain,~actual_world(skolem0001)|~of(skolem0001,X2200,X2199)|~man(skolem0001,X2199)|~vincent_forename(skolem0001,X2200)|~forename(skolem0001,X2200)|~of(skolem0001,X2197,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2197)|~forename(skolem0001,X2197)|~of(skolem0001,X2201,X2199)|~vincent_forename(skolem0001,X2201)|~forename(skolem0001,X2201)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X2198,X2199)|~theme(skolem0001,X2198,skolem0005)|~event(skolem0001,X2198)|~present(skolem0001,X2198)|~think_believe_consider(skolem0001,X2198)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X2199,X2200,skolem0007,X2197,X2199,X2201,X2198,skolem0005,X2197,skolem0007,skolem0008,X2198,skolem0005))|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1480])).
% 19.01/19.21 cnf(c1486,plain,~actual_world(skolem0001)|~of(skolem0001,X2205,X2202)|~man(skolem0001,X2202)|~vincent_forename(skolem0001,X2205)|~forename(skolem0001,X2205)|~of(skolem0001,X2203,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2203)|~forename(skolem0001,X2203)|~of(skolem0001,X2204,X2202)|~vincent_forename(skolem0001,X2204)|~forename(skolem0001,X2204)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,X2202)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X2202,X2205,skolem0007,X2203,X2202,X2204,skolem0004,skolem0005,X2203,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1483, c49])).
% 19.01/19.21 cnf(c1487,plain,~actual_world(skolem0001)|~of(skolem0001,X2207,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X2207)|~forename(skolem0001,X2207)|~of(skolem0001,X2208,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2208)|~forename(skolem0001,X2208)|~of(skolem0001,X2206,skolem0002)|~vincent_forename(skolem0001,X2206)|~forename(skolem0001,X2206)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,X2207,skolem0007,X2208,skolem0002,X2206,skolem0004,skolem0005,X2208,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1486, c48])).
% 19.01/19.21 cnf(c1488,plain,~actual_world(skolem0001)|~of(skolem0001,X2219,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X2219)|~forename(skolem0001,X2219)|~of(skolem0001,X2218,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X2218)|~forename(skolem0001,X2218)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,X2219,skolem0007,X2218,skolem0002,X2219,skolem0004,skolem0005,X2218,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1487])).
% 19.01/19.21 cnf(c1492,plain,~actual_world(skolem0001)|~of(skolem0001,X2220,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X2220)|~forename(skolem0001,X2220)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,X2220,skolem0007,skolem0006,skolem0002,X2220,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1488, c58])).
% 19.01/19.21 cnf(c1493,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1492, c43])).
% 19.01/19.21 cnf(c1494,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1493, c63])).
% 19.01/19.21 cnf(c1495,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1494, c53])).
% 19.01/19.21 cnf(c1496,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1495, c52])).
% 19.01/19.21 cnf(c1499,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1496, c51])).
% 19.01/19.21 cnf(c1500,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1499, c50])).
% 19.01/19.21 cnf(c1501,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1500, c47])).
% 19.01/19.21 cnf(c1502,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1501, c61])).
% 19.01/19.21 cnf(c1503,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1502, c60])).
% 19.01/19.21 cnf(c1504,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1503, c59])).
% 19.01/19.21 cnf(c1505,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1504, c46])).
% 19.01/19.21 cnf(c1506,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1505, c45])).
% 19.01/19.21 cnf(c1507,plain,~actual_world(skolem0001)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1506, c44])).
% 19.01/19.21 cnf(c1508,plain,man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1507, c42])).
% 19.01/19.21 cnf(c1516,plain,event(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1508, c54])).
% 19.01/19.21 cnf(c1515,plain,present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1508, c56])).
% 19.01/19.21 cnf(c1509,plain,smoke(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1508, c57])).
% 19.01/19.21 cnf(c66,negated_conjecture,~actual_world(X526)|~of(X526,X524,X528)|~man(X526,X528)|~vincent_forename(X526,X524)|~forename(X526,X524)|~of(X526,X527,X513)|~man(X526,X513)|~jules_forename(X526,X527)|~forename(X526,X527)|~of(X526,X517,X520)|~man(X526,X520)|~vincent_forename(X526,X517)|~forename(X526,X517)|~proposition(X526,X523)|~agent(X526,X521,X520)|~theme(X526,X521,X523)|~event(X526,X521)|~present(X526,X521)|~think_believe_consider(X526,X521)|~accessible_world(X526,X523)|~event(X523,X522)|~agent(X523,X522,skolem0010(X526,X528,X524,X513,X527,X520,X517,X521,X523,X525,X514,X516,X515,X518))|~present(X523,X522)|~smoke(X523,X522)|~of(X526,X525,X514)|~man(X526,X514)|~jules_forename(X526,X525)|~forename(X526,X525)|~man(X526,X514)|~state(X526,X516)|~be(X526,X516,X514,X514)|~proposition(X526,X518)|~agent(X526,X515,X528)|~theme(X526,X515,X518)|~event(X526,X515)|~present(X526,X515)|~think_believe_consider(X526,X515)|~accessible_world(X526,X518)|~event(X518,X519)|~agent(X518,X519,X513)|~present(X518,X519)|~smoke(X518,X519),inference(split_conjunct,[status(thm)],[c41])).
% 19.01/19.21 cnf(c1513,plain,agent(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1508, c55])).
% 19.01/19.21 cnf(c1642,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~smoke(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2745)|~agent(skolem0005,X2745,skolem0007)|~present(skolem0005,X2745)|~smoke(skolem0005,X2745),inference(resolution,[status(thm)],[c1513, c66])).
% 19.01/19.21 cnf(c1746,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X3152)|~agent(skolem0005,X3152,skolem0007)|~present(skolem0005,X3152)|~smoke(skolem0005,X3152),inference(resolution,[status(thm)],[c1642, c1509])).
% 19.01/19.21 cnf(c1837,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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,skolem0002,skolem0003,skolem0007,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X3171)|~agent(skolem0005,X3171,skolem0007)|~present(skolem0005,X3171)|~smoke(skolem0005,X3171),inference(resolution,[status(thm)],[c1746, c1515])).
% 19.01/19.21 cnf(c1841,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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,X3181)|~agent(skolem0005,X3181,skolem0007)|~present(skolem0005,X3181)|~smoke(skolem0005,X3181),inference(resolution,[status(thm)],[c1837, c1516])).
% 19.01/19.21 cnf(c1845,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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,X3182)|~agent(skolem0005,X3182,skolem0007)|~present(skolem0005,X3182)|~smoke(skolem0005,X3182),inference(resolution,[status(thm)],[c1841, c64])).
% 19.01/19.21 cnf(c1846,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1845, c689])).
% 19.01/19.21 cnf(c1847,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1846, c685])).
% 19.01/19.21 cnf(c1848,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1847, c691])).
% 19.01/19.21 cnf(c1849,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1848, c692])).
% 19.01/19.21 cnf(c1851,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1849, c49])).
% 19.01/19.21 cnf(c1852,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1851, c48])).
% 19.01/19.21 cnf(c1853,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1852, c58])).
% 19.01/19.21 cnf(c1854,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~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)],[c1853, c43])).
% 19.01/19.21 cnf(c1855,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1854, c63])).
% 19.01/19.21 cnf(c1856,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1855, c53])).
% 19.01/19.21 cnf(c1857,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1856, c52])).
% 19.01/19.21 cnf(c1858,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1857, c51])).
% 19.01/19.21 cnf(c1859,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1858, c50])).
% 19.01/19.21 cnf(c1860,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006),inference(resolution,[status(thm)],[c1859, c47])).
% 19.01/19.21 cnf(c1862,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,skolem0006),inference(resolution,[status(thm)],[c1860, c61])).
% 19.01/19.21 cnf(c1863,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~man(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1862, c60])).
% 19.01/19.21 cnf(c1864,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1863, c59])).
% 19.01/19.21 cnf(c1865,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1864, c46])).
% 19.01/19.21 cnf(c1866,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1865, c45])).
% 19.01/19.21 cnf(c1867,plain,~actual_world(skolem0001),inference(resolution,[status(thm)],[c1866, c44])).
% 19.01/19.21 cnf(c1868,plain,$false,inference(resolution,[status(thm)],[c1867, c42])).
% 19.01/19.21 % SZS output end CNFRefutation
% 19.01/19.21
% 19.01/19.21 % Initial clauses : 135
% 19.01/19.21 % Processed clauses : 1321
% 19.01/19.21 % Factors computed : 164
% 19.01/19.21 % Resolvents computed: 1420
% 19.01/19.21 % Tautologies deleted: 3
% 19.01/19.21 % Forward subsumed : 388
% 19.01/19.21 % Backward subsumed : 248
% 19.01/19.21 % -------- CPU Time ---------
% 19.01/19.21 % User time : 18.848 s
% 19.01/19.21 % System time : 0.024 s
% 19.01/19.21 % Total time : 18.872 s
%------------------------------------------------------------------------------