%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP252+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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 6.83s 7.00s
% Output : Refutation 6.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP252+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:21:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 6.83/7.00 % Version: 1.5
% 6.83/7.00 % SZS status Theorem
% 6.83/7.00 % SZS output start CNFRefutation
% 6.83/7.00 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))&vincent_forename(X5,X7))&forename(X5,X7))&of(X5,X8,X1))&jules_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,X6))&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,X1))&present(X10,X11))&smoke(X10,X11))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 6.83/7.00 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))&vincent_forename(X5,X7))&forename(X5,X7))&of(X5,X8,X1))&jules_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,X6))&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,X1))&present(X10,X11))&smoke(X10,X11)))))))))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 6.83/7.00 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))|~vincent_forename(X5,X7))|~forename(X5,X7))|~of(X5,X8,X1))|~jules_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,X6))|~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,X1))|~present(X10,X11))|~smoke(X10,X11))))))))))))))))))),inference(fof_nnf,[status(thm)],[c36])).
% 6.83/7.00 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))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X21))|~jules_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,X13))|~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,X21))|~present(X24,X27))|~smoke(X24,X27))))))))))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 6.83/7.00 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))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X21))|~jules_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,X13))|~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,X21))|~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))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X21))|~jules_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,X13))|~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,X21))|~present(X24,X27))|~smoke(X24,X27))))))))))))))))))),inference(skolemize,[status(esa)],[c38])).])).
% 6.83/7.00 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))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X21))|~jules_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,X13))|~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,X21))|~present(X24,X27))|~smoke(X24,X27))))&(~actual_world(X12)|(((((((((((((((((((((((((((((((((~of(X12,X14,X13)|~man(X12,X13))|~vincent_forename(X12,X14))|~forename(X12,X14))|~of(X12,X15,X21))|~jules_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,X13))|~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,X21))|~present(X24,X27))|~smoke(X24,X27)))))))))))))))))))))),inference(distribute,[status(thm)],[c40])).
% 6.83/7.00 cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c44,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c45,negated_conjecture,vincent_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c46,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c60,negated_conjecture,jules_forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c61,negated_conjecture,forename(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c47,negated_conjecture,proposition(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c50,negated_conjecture,event(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c51,negated_conjecture,present(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c52,negated_conjecture,think_believe_consider(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c53,negated_conjecture,accessible_world(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c59,negated_conjecture,man(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c63,negated_conjecture,state(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c43,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c58,negated_conjecture,of(skolem0001,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c48,negated_conjecture,agent(skolem0001,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c49,negated_conjecture,theme(skolem0001,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c54,negated_conjecture,~man(skolem0005,X398)|event(skolem0005,skolem0009(X398)),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 6.83/7.00 fof(c134,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 6.83/7.00 fof(c135,plain,(![X103]:(![X104]:(![X105]:((~accessible_world(X104,X105)|~man(X104,X103))|man(X105,X103))))),inference(variable_rename,[status(thm)],[c134])).
% 6.83/7.00 cnf(c136,plain,~accessible_world(X624,X623)|~man(X624,X622)|man(X623,X622),inference(split_conjunct,[status(thm)],[c135])).
% 6.83/7.00 cnf(c655,plain,~accessible_world(skolem0001,X685)|man(X685,skolem0007),inference(resolution,[status(thm)],[c136, c59])).
% 6.83/7.00 cnf(c757,plain,man(skolem0005,skolem0007),inference(resolution,[status(thm)],[c655, c53])).
% 6.83/7.00 cnf(c760,plain,event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c757, c54])).
% 6.83/7.00 cnf(c56,negated_conjecture,~man(skolem0005,X399)|present(skolem0005,skolem0009(X399)),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c765,plain,present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c757, c56])).
% 6.83/7.00 cnf(c57,negated_conjecture,~man(skolem0005,X404)|smoke(skolem0005,skolem0009(X404)),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c762,plain,smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c757, c57])).
% 6.83/7.00 cnf(c55,negated_conjecture,~man(skolem0005,X487)|agent(skolem0005,skolem0009(X487),X487),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c764,plain,agent(skolem0005,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c757, c55])).
% 6.83/7.00 cnf(c64,negated_conjecture,be(skolem0001,skolem0008,skolem0007,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c65,negated_conjecture,~actual_world(X504)|~of(X504,X501,X505)|~man(X504,X505)|~vincent_forename(X504,X501)|~forename(X504,X501)|~of(X504,X502,X496)|~jules_forename(X504,X502)|~forename(X504,X502)|~of(X504,X497,X506)|~man(X504,X506)|~vincent_forename(X504,X497)|~forename(X504,X497)|~proposition(X504,X495)|~agent(X504,X508,X506)|~theme(X504,X508,X495)|~event(X504,X508)|~present(X504,X508)|~think_believe_consider(X504,X508)|~accessible_world(X504,X495)|man(X495,skolem0010(X504,X505,X501,X502,X506,X497,X508,X495,X498,X496,X499,X500,X503))|~of(X504,X498,X496)|~man(X504,X496)|~jules_forename(X504,X498)|~forename(X504,X498)|~man(X504,X496)|~state(X504,X499)|~be(X504,X499,X496,X496)|~proposition(X504,X503)|~agent(X504,X500,X505)|~theme(X504,X500,X503)|~event(X504,X500)|~present(X504,X500)|~think_believe_consider(X504,X500)|~accessible_world(X504,X503)|~event(X503,X507)|~agent(X503,X507,X496)|~present(X503,X507)|~smoke(X503,X507),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.00 cnf(c530,plain,~actual_world(skolem0001)|~of(skolem0001,X1081,X1080)|~man(skolem0001,X1080)|~vincent_forename(skolem0001,X1081)|~forename(skolem0001,X1081)|~of(skolem0001,X1087,skolem0007)|~jules_forename(skolem0001,X1087)|~forename(skolem0001,X1087)|~of(skolem0001,X1086,X1084)|~man(skolem0001,X1084)|~vincent_forename(skolem0001,X1086)|~forename(skolem0001,X1086)|~proposition(skolem0001,X1082)|~agent(skolem0001,X1083,X1084)|~theme(skolem0001,X1083,X1082)|~event(skolem0001,X1083)|~present(skolem0001,X1083)|~think_believe_consider(skolem0001,X1083)|~accessible_world(skolem0001,X1082)|man(X1082,skolem0010(skolem0001,X1080,X1081,X1087,X1084,X1086,X1083,X1082,X1079,skolem0007,skolem0008,X1089,X1085))|~of(skolem0001,X1079,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1079)|~forename(skolem0001,X1079)|~state(skolem0001,skolem0008)|~proposition(skolem0001,X1085)|~agent(skolem0001,X1089,X1080)|~theme(skolem0001,X1089,X1085)|~event(skolem0001,X1089)|~present(skolem0001,X1089)|~think_believe_consider(skolem0001,X1089)|~accessible_world(skolem0001,X1085)|~event(X1085,X1088)|~agent(X1085,X1088,skolem0007)|~present(X1085,X1088)|~smoke(X1085,X1088),inference(resolution,[status(thm)],[c65, c64])).
% 6.83/7.00 cnf(c1093,plain,~actual_world(skolem0001)|~of(skolem0001,X1417,X1420)|~man(skolem0001,X1420)|~vincent_forename(skolem0001,X1417)|~forename(skolem0001,X1417)|~of(skolem0001,X1421,skolem0007)|~jules_forename(skolem0001,X1421)|~forename(skolem0001,X1421)|~of(skolem0001,X1422,X1415)|~man(skolem0001,X1415)|~vincent_forename(skolem0001,X1422)|~forename(skolem0001,X1422)|~proposition(skolem0001,X1419)|~agent(skolem0001,X1416,X1415)|~theme(skolem0001,X1416,X1419)|~event(skolem0001,X1416)|~present(skolem0001,X1416)|~think_believe_consider(skolem0001,X1416)|~accessible_world(skolem0001,X1419)|man(X1419,skolem0010(skolem0001,X1420,X1417,X1421,X1415,X1422,X1416,X1419,X1423,skolem0007,skolem0008,X1418,skolem0005))|~of(skolem0001,X1423,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1423)|~forename(skolem0001,X1423)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1418,X1420)|~theme(skolem0001,X1418,skolem0005)|~event(skolem0001,X1418)|~present(skolem0001,X1418)|~think_believe_consider(skolem0001,X1418)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007))|~smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c530, c764])).
% 6.83/7.00 cnf(c1293,plain,~actual_world(skolem0001)|~of(skolem0001,X1500,X1492)|~man(skolem0001,X1492)|~vincent_forename(skolem0001,X1500)|~forename(skolem0001,X1500)|~of(skolem0001,X1496,skolem0007)|~jules_forename(skolem0001,X1496)|~forename(skolem0001,X1496)|~of(skolem0001,X1499,X1495)|~man(skolem0001,X1495)|~vincent_forename(skolem0001,X1499)|~forename(skolem0001,X1499)|~proposition(skolem0001,X1497)|~agent(skolem0001,X1493,X1495)|~theme(skolem0001,X1493,X1497)|~event(skolem0001,X1493)|~present(skolem0001,X1493)|~think_believe_consider(skolem0001,X1493)|~accessible_world(skolem0001,X1497)|man(X1497,skolem0010(skolem0001,X1492,X1500,X1496,X1495,X1499,X1493,X1497,X1498,skolem0007,skolem0008,X1494,skolem0005))|~of(skolem0001,X1498,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1498)|~forename(skolem0001,X1498)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1494,X1492)|~theme(skolem0001,X1494,skolem0005)|~event(skolem0001,X1494)|~present(skolem0001,X1494)|~think_believe_consider(skolem0001,X1494)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1093, c762])).
% 6.83/7.00 cnf(c1314,plain,~actual_world(skolem0001)|~of(skolem0001,X1581,X1583)|~man(skolem0001,X1583)|~vincent_forename(skolem0001,X1581)|~forename(skolem0001,X1581)|~of(skolem0001,X1584,skolem0007)|~jules_forename(skolem0001,X1584)|~forename(skolem0001,X1584)|~of(skolem0001,X1586,X1582)|~man(skolem0001,X1582)|~vincent_forename(skolem0001,X1586)|~forename(skolem0001,X1586)|~proposition(skolem0001,X1580)|~agent(skolem0001,X1588,X1582)|~theme(skolem0001,X1588,X1580)|~event(skolem0001,X1588)|~present(skolem0001,X1588)|~think_believe_consider(skolem0001,X1588)|~accessible_world(skolem0001,X1580)|man(X1580,skolem0010(skolem0001,X1583,X1581,X1584,X1582,X1586,X1588,X1580,X1585,skolem0007,skolem0008,X1587,skolem0005))|~of(skolem0001,X1585,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1585)|~forename(skolem0001,X1585)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1587,X1583)|~theme(skolem0001,X1587,skolem0005)|~event(skolem0001,X1587)|~present(skolem0001,X1587)|~think_believe_consider(skolem0001,X1587)|~accessible_world(skolem0001,skolem0005)|~event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1293, c765])).
% 6.83/7.00 cnf(c1334,plain,~actual_world(skolem0001)|~of(skolem0001,X1721,X1728)|~man(skolem0001,X1728)|~vincent_forename(skolem0001,X1721)|~forename(skolem0001,X1721)|~of(skolem0001,X1725,skolem0007)|~jules_forename(skolem0001,X1725)|~forename(skolem0001,X1725)|~of(skolem0001,X1722,X1720)|~man(skolem0001,X1720)|~vincent_forename(skolem0001,X1722)|~forename(skolem0001,X1722)|~proposition(skolem0001,X1723)|~agent(skolem0001,X1726,X1720)|~theme(skolem0001,X1726,X1723)|~event(skolem0001,X1726)|~present(skolem0001,X1726)|~think_believe_consider(skolem0001,X1726)|~accessible_world(skolem0001,X1723)|man(X1723,skolem0010(skolem0001,X1728,X1721,X1725,X1720,X1722,X1726,X1723,X1727,skolem0007,skolem0008,X1724,skolem0005))|~of(skolem0001,X1727,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1727)|~forename(skolem0001,X1727)|~state(skolem0001,skolem0008)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1724,X1728)|~theme(skolem0001,X1724,skolem0005)|~event(skolem0001,X1724)|~present(skolem0001,X1724)|~think_believe_consider(skolem0001,X1724)|~accessible_world(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1314, c760])).
% 6.83/7.00 cnf(c1361,plain,~actual_world(skolem0001)|~of(skolem0001,X1730,X1732)|~man(skolem0001,X1732)|~vincent_forename(skolem0001,X1730)|~forename(skolem0001,X1730)|~of(skolem0001,X1729,skolem0007)|~jules_forename(skolem0001,X1729)|~forename(skolem0001,X1729)|~of(skolem0001,X1733,X1734)|~man(skolem0001,X1734)|~vincent_forename(skolem0001,X1733)|~forename(skolem0001,X1733)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1735,X1734)|~theme(skolem0001,X1735,skolem0005)|~event(skolem0001,X1735)|~present(skolem0001,X1735)|~think_believe_consider(skolem0001,X1735)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X1732,X1730,X1729,X1734,X1733,X1735,skolem0005,X1731,skolem0007,skolem0008,X1735,skolem0005))|~of(skolem0001,X1731,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1731)|~forename(skolem0001,X1731)|~state(skolem0001,skolem0008)|~agent(skolem0001,X1735,X1732),inference(factor,[status(thm)],[c1334])).
% 6.83/7.00 cnf(c1363,plain,~actual_world(skolem0001)|~of(skolem0001,X1741,X1740)|~man(skolem0001,X1740)|~vincent_forename(skolem0001,X1741)|~forename(skolem0001,X1741)|~of(skolem0001,X1736,skolem0007)|~jules_forename(skolem0001,X1736)|~forename(skolem0001,X1736)|~of(skolem0001,X1739,X1740)|~vincent_forename(skolem0001,X1739)|~forename(skolem0001,X1739)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1737,X1740)|~theme(skolem0001,X1737,skolem0005)|~event(skolem0001,X1737)|~present(skolem0001,X1737)|~think_believe_consider(skolem0001,X1737)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X1740,X1741,X1736,X1740,X1739,X1737,skolem0005,X1738,skolem0007,skolem0008,X1737,skolem0005))|~of(skolem0001,X1738,skolem0007)|~man(skolem0001,skolem0007)|~jules_forename(skolem0001,X1738)|~forename(skolem0001,X1738)|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1361])).
% 6.83/7.00 cnf(c1366,plain,~actual_world(skolem0001)|~of(skolem0001,X1742,X1746)|~man(skolem0001,X1746)|~vincent_forename(skolem0001,X1742)|~forename(skolem0001,X1742)|~of(skolem0001,X1743,skolem0007)|~jules_forename(skolem0001,X1743)|~forename(skolem0001,X1743)|~of(skolem0001,X1745,X1746)|~vincent_forename(skolem0001,X1745)|~forename(skolem0001,X1745)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,X1744,X1746)|~theme(skolem0001,X1744,skolem0005)|~event(skolem0001,X1744)|~present(skolem0001,X1744)|~think_believe_consider(skolem0001,X1744)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X1746,X1742,X1743,X1746,X1745,X1744,skolem0005,X1743,skolem0007,skolem0008,X1744,skolem0005))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1363])).
% 6.83/7.00 cnf(c1369,plain,~actual_world(skolem0001)|~of(skolem0001,X1758,X1756)|~man(skolem0001,X1756)|~vincent_forename(skolem0001,X1758)|~forename(skolem0001,X1758)|~of(skolem0001,X1757,skolem0007)|~jules_forename(skolem0001,X1757)|~forename(skolem0001,X1757)|~of(skolem0001,X1755,X1756)|~vincent_forename(skolem0001,X1755)|~forename(skolem0001,X1755)|~proposition(skolem0001,skolem0005)|~agent(skolem0001,skolem0004,X1756)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,X1756,X1758,X1757,X1756,X1755,skolem0004,skolem0005,X1757,skolem0007,skolem0008,skolem0004,skolem0005))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1366, c49])).
% 6.83/7.00 cnf(c1371,plain,~actual_world(skolem0001)|~of(skolem0001,X1760,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X1760)|~forename(skolem0001,X1760)|~of(skolem0001,X1761,skolem0007)|~jules_forename(skolem0001,X1761)|~forename(skolem0001,X1761)|~of(skolem0001,X1759,skolem0002)|~vincent_forename(skolem0001,X1759)|~forename(skolem0001,X1759)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,X1760,X1761,skolem0002,X1759,skolem0004,skolem0005,X1761,skolem0007,skolem0008,skolem0004,skolem0005))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1369, c48])).
% 6.83/7.00 cnf(c1372,plain,~actual_world(skolem0001)|~of(skolem0001,X1762,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X1762)|~forename(skolem0001,X1762)|~of(skolem0001,X1763,skolem0007)|~jules_forename(skolem0001,X1763)|~forename(skolem0001,X1763)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|~think_believe_consider(skolem0001,skolem0004)|~accessible_world(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,X1762,X1763,skolem0002,X1762,skolem0004,skolem0005,X1763,skolem0007,skolem0008,skolem0004,skolem0005))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(factor,[status(thm)],[c1371])).
% 6.83/7.00 cnf(c1374,plain,~actual_world(skolem0001)|~of(skolem0001,X1764,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,X1764)|~forename(skolem0001,X1764)|~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,X1764,skolem0006,skolem0002,X1764,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1372, c58])).
% 6.83/7.00 cnf(c1375,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1374, c43])).
% 6.83/7.00 cnf(c1376,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))|~man(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1375, c63])).
% 6.83/7.00 cnf(c1378,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1376, c59])).
% 6.83/7.00 cnf(c1379,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1378, c53])).
% 6.83/7.00 cnf(c1380,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1379, c52])).
% 6.83/7.00 cnf(c1381,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1380, c51])).
% 6.83/7.00 cnf(c1382,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1381, c50])).
% 6.83/7.00 cnf(c1386,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1382, c47])).
% 6.83/7.00 cnf(c1387,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1386, c61])).
% 6.83/7.00 cnf(c1388,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1387, c60])).
% 6.83/7.00 cnf(c1389,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1388, c46])).
% 6.83/7.00 cnf(c1390,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1389, c45])).
% 6.83/7.00 cnf(c1393,plain,~actual_world(skolem0001)|man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1390, c44])).
% 6.83/7.01 cnf(c1394,plain,man(skolem0005,skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1393, c42])).
% 6.83/7.01 cnf(c1397,plain,event(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1394, c54])).
% 6.83/7.01 cnf(c1402,plain,present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1394, c56])).
% 6.83/7.01 cnf(c1399,plain,smoke(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005))),inference(resolution,[status(thm)],[c1394, c57])).
% 6.83/7.01 cnf(c66,negated_conjecture,~actual_world(X520)|~of(X520,X517,X522)|~man(X520,X522)|~vincent_forename(X520,X517)|~forename(X520,X517)|~of(X520,X518,X512)|~jules_forename(X520,X518)|~forename(X520,X518)|~of(X520,X513,X523)|~man(X520,X523)|~vincent_forename(X520,X513)|~forename(X520,X513)|~proposition(X520,X511)|~agent(X520,X525,X523)|~theme(X520,X525,X511)|~event(X520,X525)|~present(X520,X525)|~think_believe_consider(X520,X525)|~accessible_world(X520,X511)|~event(X511,X521)|~agent(X511,X521,skolem0010(X520,X522,X517,X518,X523,X513,X525,X511,X514,X512,X515,X516,X519))|~present(X511,X521)|~smoke(X511,X521)|~of(X520,X514,X512)|~man(X520,X512)|~jules_forename(X520,X514)|~forename(X520,X514)|~man(X520,X512)|~state(X520,X515)|~be(X520,X515,X512,X512)|~proposition(X520,X519)|~agent(X520,X516,X522)|~theme(X520,X516,X519)|~event(X520,X516)|~present(X520,X516)|~think_believe_consider(X520,X516)|~accessible_world(X520,X519)|~event(X519,X524)|~agent(X519,X524,X512)|~present(X519,X524)|~smoke(X519,X524),inference(split_conjunct,[status(thm)],[c41])).
% 6.83/7.01 cnf(c1401,plain,agent(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1394, c55])).
% 6.83/7.01 cnf(c1496,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~smoke(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2136)|~agent(skolem0005,X2136,skolem0007)|~present(skolem0005,X2136)|~smoke(skolem0005,X2136),inference(resolution,[status(thm)],[c1401, c66])).
% 6.83/7.01 cnf(c1583,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~present(skolem0005,skolem0009(skolem0010(skolem0001,skolem0002,skolem0003,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2274)|~agent(skolem0005,X2274,skolem0007)|~present(skolem0005,X2274)|~smoke(skolem0005,X2274),inference(resolution,[status(thm)],[c1496, c1399])).
% 6.83/7.01 cnf(c1608,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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,skolem0006,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,skolem0007,skolem0008,skolem0004,skolem0005)))|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2275)|~agent(skolem0005,X2275,skolem0007)|~present(skolem0005,X2275)|~smoke(skolem0005,X2275),inference(resolution,[status(thm)],[c1583, c1402])).
% 6.83/7.01 cnf(c1610,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~be(skolem0001,skolem0008,skolem0007,skolem0007)|~event(skolem0005,X2276)|~agent(skolem0005,X2276,skolem0007)|~present(skolem0005,X2276)|~smoke(skolem0005,X2276),inference(resolution,[status(thm)],[c1608, c1397])).
% 6.83/7.01 cnf(c1611,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~event(skolem0005,X2277)|~agent(skolem0005,X2277,skolem0007)|~present(skolem0005,X2277)|~smoke(skolem0005,X2277),inference(resolution,[status(thm)],[c1610, c64])).
% 6.83/7.01 cnf(c1612,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007))|~smoke(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1611, c764])).
% 6.83/7.01 cnf(c1613,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~event(skolem0005,skolem0009(skolem0007))|~present(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1612, c762])).
% 6.83/7.01 cnf(c1614,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008)|~event(skolem0005,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c1613, c765])).
% 6.83/7.01 cnf(c1615,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1614, c760])).
% 6.83/7.01 cnf(c1616,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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)|~man(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1615, c49])).
% 6.83/7.01 cnf(c1617,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~of(skolem0001,skolem0006,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(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1616, c48])).
% 6.83/7.01 cnf(c1618,plain,~actual_world(skolem0001)|~of(skolem0001,skolem0003,skolem0002)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1617, c58])).
% 6.83/7.01 cnf(c1619,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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(skolem0001,skolem0007)|~state(skolem0001,skolem0008),inference(resolution,[status(thm)],[c1618, c43])).
% 6.83/7.01 cnf(c1620,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1619, c63])).
% 6.83/7.01 cnf(c1621,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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)],[c1620, c59])).
% 6.83/7.01 cnf(c1622,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~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)],[c1621, c53])).
% 6.83/7.01 cnf(c1623,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004)|~present(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1622, c52])).
% 6.83/7.01 cnf(c1624,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005)|~event(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1623, c51])).
% 6.83/7.01 cnf(c1625,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006)|~proposition(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1624, c50])).
% 6.83/7.01 cnf(c1626,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006)|~forename(skolem0001,skolem0006),inference(resolution,[status(thm)],[c1625, c47])).
% 6.83/7.01 cnf(c1627,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003)|~jules_forename(skolem0001,skolem0006),inference(resolution,[status(thm)],[c1626, c61])).
% 6.83/7.01 cnf(c1628,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003)|~forename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1627, c60])).
% 6.83/7.01 cnf(c1629,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002)|~vincent_forename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1628, c46])).
% 6.83/7.01 cnf(c1630,plain,~actual_world(skolem0001)|~man(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1629, c45])).
% 6.83/7.01 cnf(c1631,plain,~actual_world(skolem0001),inference(resolution,[status(thm)],[c1630, c44])).
% 6.83/7.01 cnf(c1632,plain,$false,inference(resolution,[status(thm)],[c1631, c42])).
% 6.83/7.01 % SZS output end CNFRefutation
% 6.83/7.01
% 6.83/7.01 % Initial clauses : 135
% 6.83/7.01 % Processed clauses : 1143
% 6.83/7.01 % Factors computed : 89
% 6.83/7.01 % Resolvents computed: 1259
% 6.83/7.01 % Tautologies deleted: 3
% 6.83/7.01 % Forward subsumed : 336
% 6.83/7.01 % Backward subsumed : 117
% 6.83/7.01 % -------- CPU Time ---------
% 6.83/7.01 % User time : 6.651 s
% 6.83/7.01 % System time : 0.010 s
% 6.83/7.01 % Total time : 6.661 s
%------------------------------------------------------------------------------