%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NLP079+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:05:32 AM UTC 2026
% Result : Theorem 16.99s 4.54s
% Output : CNFRefutation 16.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP079+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.41 % Computer : n013.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sat Sep 26 00:44:42 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.99/4.54 % SZS status Theorem for theBenchmark.p
% 16.99/4.54 % SZS output start CNFRefutation for theBenchmark.p
% 16.99/4.54 fof(co1, conjecture, ~~(((? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ((male(X0,X1) & (male(X0,X2) & (man(X0,X2) & (of(X0,X3,X2) & (cannon(X0,X3) & (! [X8] : ((member(X0,X8,X4) => ? [X9] : ((event(X0,X9) & (agent(X0,X9,X2) & (patient(X0,X9,X8) & (present(X0,X9) & (nonreflexive(X0,X9) & (fire(X0,X9) & 'from$uloc'(X0,X9,X3)))))))))) & (six(X0,X4) & (group(X0,X4) & (! [X10] : ((member(X0,X10,X4) => shot(X0,X10))) & (revenge(X0,X5) & (cry(X0,X6) & (event(X0,X7) & (agent(X0,X7,X1) & (patient(X0,X7,X6) & (present(X0,X7) & (nonreflexive(X0,X7) & (scream(X0,X7) & of(X0,X7,X5))))))))))))))))))))) => ? [X11] : (('actual$uworld'(X11) & ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ? [X18] : ((male(X11,X12) & (male(X11,X13) & (man(X11,X13) & (of(X11,X14,X13) & (cannon(X11,X14) & (! [X19] : ((member(X11,X19,X15) => ? [X20] : ((event(X11,X20) & (agent(X11,X20,X13) & (patient(X11,X20,X19) & (present(X11,X20) & (nonreflexive(X11,X20) & (fire(X11,X20) & 'from$uloc'(X11,X20,X14)))))))))) & (six(X11,X15) & (group(X11,X15) & (! [X21] : ((member(X11,X21,X15) => shot(X11,X21))) & (cry(X11,X16) & (revenge(X11,X17) & (event(X11,X18) & (agent(X11,X18,X12) & (patient(X11,X18,X16) & (present(X11,X18) & (nonreflexive(X11,X18) & (scream(X11,X18) & of(X11,X18,X17)))))))))))))))))))))) & (? [X11] : (('actual$uworld'(X11) & ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ? [X18] : ((male(X11,X12) & (male(X11,X13) & (man(X11,X13) & (of(X11,X14,X13) & (cannon(X11,X14) & (! [X19] : ((member(X11,X19,X15) => ? [X20] : ((event(X11,X20) & (agent(X11,X20,X13) & (patient(X11,X20,X19) & (present(X11,X20) & (nonreflexive(X11,X20) & (fire(X11,X20) & 'from$uloc'(X11,X20,X14)))))))))) & (six(X11,X15) & (group(X11,X15) & (! [X21] : ((member(X11,X21,X15) => shot(X11,X21))) & (cry(X11,X16) & (revenge(X11,X17) & (event(X11,X18) & (agent(X11,X18,X12) & (patient(X11,X18,X16) & (present(X11,X18) & (nonreflexive(X11,X18) & (scream(X11,X18) & of(X11,X18,X17))))))))))))))))))))) => ? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ((male(X0,X1) & (male(X0,X2) & (man(X0,X2) & (of(X0,X3,X2) & (cannon(X0,X3) & (! [X8] : ((member(X0,X8,X4) => ? [X9] : ((event(X0,X9) & (agent(X0,X9,X2) & (patient(X0,X9,X8) & (present(X0,X9) & (nonreflexive(X0,X9) & (fire(X0,X9) & 'from$uloc'(X0,X9,X3)))))))))) & (six(X0,X4) & (group(X0,X4) & (! [X10] : ((member(X0,X10,X4) => shot(X0,X10))) & (revenge(X0,X5) & (cry(X0,X6) & (event(X0,X7) & (agent(X0,X7,X1) & (patient(X0,X7,X6) & (present(X0,X7) & (nonreflexive(X0,X7) & (scream(X0,X7) & of(X0,X7,X5))))))))))))))))))))))))).
% 16.99/4.54 fof(negated_conjecture, negated_conjecture, ~~~(((? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ((male(X0,X1) & (male(X0,X2) & (man(X0,X2) & (of(X0,X3,X2) & (cannon(X0,X3) & (! [X8] : ((member(X0,X8,X4) => ? [X9] : ((event(X0,X9) & (agent(X0,X9,X2) & (patient(X0,X9,X8) & (present(X0,X9) & (nonreflexive(X0,X9) & (fire(X0,X9) & 'from$uloc'(X0,X9,X3)))))))))) & (six(X0,X4) & (group(X0,X4) & (! [X10] : ((member(X0,X10,X4) => shot(X0,X10))) & (revenge(X0,X5) & (cry(X0,X6) & (event(X0,X7) & (agent(X0,X7,X1) & (patient(X0,X7,X6) & (present(X0,X7) & (nonreflexive(X0,X7) & (scream(X0,X7) & of(X0,X7,X5))))))))))))))))))))) => ? [X11] : (('actual$uworld'(X11) & ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ? [X18] : ((male(X11,X12) & (male(X11,X13) & (man(X11,X13) & (of(X11,X14,X13) & (cannon(X11,X14) & (! [X19] : ((member(X11,X19,X15) => ? [X20] : ((event(X11,X20) & (agent(X11,X20,X13) & (patient(X11,X20,X19) & (present(X11,X20) & (nonreflexive(X11,X20) & (fire(X11,X20) & 'from$uloc'(X11,X20,X14)))))))))) & (six(X11,X15) & (group(X11,X15) & (! [X21] : ((member(X11,X21,X15) => shot(X11,X21))) & (cry(X11,X16) & (revenge(X11,X17) & (event(X11,X18) & (agent(X11,X18,X12) & (patient(X11,X18,X16) & (present(X11,X18) & (nonreflexive(X11,X18) & (scream(X11,X18) & of(X11,X18,X17)))))))))))))))))))))) & (? [X11] : (('actual$uworld'(X11) & ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ? [X18] : ((male(X11,X12) & (male(X11,X13) & (man(X11,X13) & (of(X11,X14,X13) & (cannon(X11,X14) & (! [X19] : ((member(X11,X19,X15) => ? [X20] : ((event(X11,X20) & (agent(X11,X20,X13) & (patient(X11,X20,X19) & (present(X11,X20) & (nonreflexive(X11,X20) & (fire(X11,X20) & 'from$uloc'(X11,X20,X14)))))))))) & (six(X11,X15) & (group(X11,X15) & (! [X21] : ((member(X11,X21,X15) => shot(X11,X21))) & (cry(X11,X16) & (revenge(X11,X17) & (event(X11,X18) & (agent(X11,X18,X12) & (patient(X11,X18,X16) & (present(X11,X18) & (nonreflexive(X11,X18) & (scream(X11,X18) & of(X11,X18,X17))))))))))))))))))))) => ? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ((male(X0,X1) & (male(X0,X2) & (man(X0,X2) & (of(X0,X3,X2) & (cannon(X0,X3) & (! [X8] : ((member(X0,X8,X4) => ? [X9] : ((event(X0,X9) & (agent(X0,X9,X2) & (patient(X0,X9,X8) & (present(X0,X9) & (nonreflexive(X0,X9) & (fire(X0,X9) & 'from$uloc'(X0,X9,X3)))))))))) & (six(X0,X4) & (group(X0,X4) & (! [X10] : ((member(X0,X10,X4) => shot(X0,X10))) & (revenge(X0,X5) & (cry(X0,X6) & (event(X0,X7) & (agent(X0,X7,X1) & (patient(X0,X7,X6) & (present(X0,X7) & (nonreflexive(X0,X7) & (scream(X0,X7) & of(X0,X7,X5)))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])).
% 16.99/4.54 cnf(c0, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c1, plain, ~X0(X1,X2,X3,X4) | event(X1,sK4(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c2, plain, ~X0(X1,X2,X3,X4) | agent(X1,sK4(X2,X1,X3,X4),X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c3, plain, ~X0(X1,X2,X3,X4) | patient(X1,sK4(X2,X1,X3,X4),X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c4, plain, ~X0(X1,X2,X3,X4) | present(X1,sK4(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c5, plain, ~X0(X1,X2,X3,X4) | nonreflexive(X1,sK4(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c6, plain, ~X0(X1,X2,X3,X4) | fire(X1,sK4(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c7, plain, ~X0(X1,X2,X3,X4) | 'from$uloc'(X1,sK4(X2,X1,X3,X4),X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c8, plain, ~X0(X1,X2,X3,X4) | event(X2,sK5(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c9, plain, ~X0(X1,X2,X3,X4) | agent(X2,sK5(X2,X1,X3,X4),X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c10, plain, ~X0(X1,X2,X3,X4) | patient(X2,sK5(X2,X1,X3,X4),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c11, plain, ~X0(X1,X2,X3,X4) | present(X2,sK5(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c12, plain, ~X0(X1,X2,X3,X4) | nonreflexive(X2,sK5(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c13, plain, ~X0(X1,X2,X3,X4) | fire(X2,sK5(X2,X1,X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c14, plain, ~X0(X1,X2,X3,X4) | 'from$uloc'(X2,sK5(X2,X1,X3,X4),X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c15, plain, X0 | 'actual$uworld'(sK6), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c16, plain, X0 | male(sK6,sK7), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c17, plain, X0 | male(sK6,sK8), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c18, plain, X0 | man(sK6,sK8), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c19, plain, X0 | of(sK6,sK9,sK8), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c20, plain, X0 | cannon(sK6,sK9), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c21, plain, X0 | ~member(sK6,X1,sK10) | X2(sK6,sK8,sK9,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c22, plain, X0 | six(sK6,sK10), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c23, plain, X0 | group(sK6,sK10), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c24, plain, X0 | ~member(sK6,X1,sK10) | shot(sK6,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c25, plain, X0 | revenge(sK6,sK11), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c26, plain, X0 | cry(sK6,sK12), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c27, plain, X0 | event(sK6,sK13), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c28, plain, X0 | agent(sK6,sK13,sK7), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c29, plain, X0 | patient(sK6,sK13,sK12), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c30, plain, X0 | present(sK6,sK13), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c31, plain, X0 | nonreflexive(sK6,sK13), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c32, plain, X0 | scream(sK6,sK13), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c33, plain, X0 | of(sK6,sK13,sK11), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c34, plain, ~revenge(X0,X1) | member(X0,sK26(X0,X2),X2) | ~group(X0,X2) | ~of(X0,X3,X4) | ~male(X0,X5) | ~male(X0,X4) | ~present(X0,X6) | ~cannon(X0,X3) | ~'actual$uworld'(X0) | ~patient(X0,X6,X7) | ~cry(X0,X7) | ~man(X0,X4) | X8 | ~scream(X0,X6) | ~of(X0,X6,X1) | ~event(X0,X6) | ~nonreflexive(X0,X6) | member(X0,sK24(X0,X4,X3,X2),X2) | ~agent(X0,X6,X5) | ~six(X0,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c35, plain, ~revenge(X0,X1) | ~group(X0,X2) | ~of(X0,X3,X4) | ~male(X0,X5) | ~male(X0,X4) | ~shot(X0,sK26(X0,X2)) | ~present(X0,X6) | ~cannon(X0,X3) | ~'actual$uworld'(X0) | ~patient(X0,X6,X7) | ~cry(X0,X7) | ~man(X0,X4) | X8 | ~scream(X0,X6) | ~of(X0,X6,X1) | ~event(X0,X6) | ~nonreflexive(X0,X6) | member(X0,sK24(X0,X4,X3,X2),X2) | ~agent(X0,X6,X5) | ~six(X0,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c36, plain, ~revenge(X0,X1) | member(X0,sK26(X0,X2),X2) | ~'from$uloc'(X0,X3,X4) | ~nonreflexive(X0,X3) | ~patient(X0,X3,sK24(X0,X5,X4,X2)) | ~event(X0,X3) | ~group(X0,X2) | ~male(X0,X6) | ~agent(X0,X3,X5) | ~male(X0,X5) | ~present(X0,X7) | ~cannon(X0,X4) | ~'actual$uworld'(X0) | ~patient(X0,X7,X8) | ~cry(X0,X8) | ~man(X0,X5) | X9 | ~scream(X0,X7) | ~present(X0,X3) | ~fire(X0,X3) | ~of(X0,X4,X5) | ~of(X0,X7,X1) | ~event(X0,X7) | ~nonreflexive(X0,X7) | ~agent(X0,X7,X6) | ~six(X0,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c37, plain, ~revenge(X0,X1) | ~'from$uloc'(X0,X2,X3) | ~nonreflexive(X0,X2) | ~patient(X0,X2,sK24(X0,X4,X3,X5)) | ~event(X0,X2) | ~group(X0,X5) | ~male(X0,X6) | ~agent(X0,X2,X4) | ~male(X0,X4) | ~shot(X0,sK26(X0,X5)) | ~present(X0,X7) | ~cannon(X0,X3) | ~'actual$uworld'(X0) | ~patient(X0,X7,X8) | ~cry(X0,X8) | ~man(X0,X4) | X9 | ~scream(X0,X7) | ~present(X0,X2) | ~fire(X0,X2) | ~of(X0,X3,X4) | ~of(X0,X7,X1) | ~event(X0,X7) | ~nonreflexive(X0,X7) | ~agent(X0,X7,X6) | ~six(X0,X5), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c38, plain, X0 | 'actual$uworld'(sK27), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c39, plain, X0 | male(sK27,sK28), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c40, plain, X0 | male(sK27,sK29), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c41, plain, X0 | man(sK27,sK29), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c42, plain, X0 | of(sK27,sK30,sK29), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c43, plain, X0 | cannon(sK27,sK30), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c44, plain, X0 | ~member(sK27,X1,sK31) | X2(X1,sK27,sK29,sK30), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c45, plain, X0 | six(sK27,sK31), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c46, plain, X0 | group(sK27,sK31), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c47, plain, X0 | ~member(sK27,X1,sK31) | shot(sK27,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c48, plain, X0 | cry(sK27,sK32), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c49, plain, X0 | revenge(sK27,sK33), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c50, plain, X0 | event(sK27,sK34), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c51, plain, X0 | agent(sK27,sK34,sK28), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c52, plain, X0 | patient(sK27,sK34,sK32), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c53, plain, X0 | present(sK27,sK34), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c54, plain, X0 | nonreflexive(sK27,sK34), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c55, plain, X0 | scream(sK27,sK34), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c56, plain, X0 | of(sK27,sK34,sK33), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c57, plain, ~event(X0,X1) | ~six(X0,X2) | member(X0,sK45(X0,X3,X4,X2),X2) | ~cannon(X0,X4) | ~man(X0,X3) | ~patient(X0,X1,X5) | ~'actual$uworld'(X0) | ~revenge(X0,X6) | ~of(X0,X4,X3) | ~of(X0,X1,X6) | X7 | ~agent(X0,X1,X8) | ~present(X0,X1) | member(X0,sK47(X0,X2),X2) | ~group(X0,X2) | ~male(X0,X3) | ~scream(X0,X1) | ~male(X0,X8) | ~cry(X0,X5) | ~nonreflexive(X0,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c58, plain, ~event(X0,X1) | ~present(X0,X1) | ~shot(X0,sK47(X0,X2)) | ~six(X0,X2) | member(X0,sK45(X0,X3,X4,X2),X2) | ~cannon(X0,X4) | ~man(X0,X3) | ~patient(X0,X1,X5) | ~'actual$uworld'(X0) | ~revenge(X0,X6) | ~of(X0,X4,X3) | ~of(X0,X1,X6) | X7 | ~agent(X0,X1,X8) | ~group(X0,X2) | ~male(X0,X3) | ~scream(X0,X1) | ~male(X0,X8) | ~cry(X0,X5) | ~nonreflexive(X0,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c59, plain, ~event(X0,X1) | ~patient(X0,X2,sK45(X0,X3,X4,X5)) | ~agent(X0,X2,X3) | ~six(X0,X5) | ~cannon(X0,X4) | ~event(X0,X2) | ~man(X0,X3) | ~patient(X0,X1,X6) | ~'actual$uworld'(X0) | ~revenge(X0,X7) | ~of(X0,X4,X3) | ~of(X0,X1,X7) | X8 | ~agent(X0,X1,X9) | ~present(X0,X1) | member(X0,sK47(X0,X5),X5) | ~nonreflexive(X0,X2) | ~present(X0,X2) | ~group(X0,X5) | ~male(X0,X3) | ~'from$uloc'(X0,X2,X4) | ~fire(X0,X2) | ~scream(X0,X1) | ~male(X0,X9) | ~cry(X0,X6) | ~nonreflexive(X0,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(c60, plain, ~event(X0,X1) | ~present(X0,X1) | ~patient(X0,X2,sK45(X0,X3,X4,X5)) | ~six(X0,X5) | ~cannon(X0,X4) | ~event(X0,X2) | ~man(X0,X3) | ~patient(X0,X1,X6) | ~'actual$uworld'(X0) | ~revenge(X0,X7) | ~of(X0,X4,X3) | ~of(X0,X1,X7) | X8 | ~agent(X0,X1,X9) | ~nonreflexive(X0,X2) | ~present(X0,X2) | ~group(X0,X5) | ~male(X0,X3) | ~agent(X0,X2,X3) | ~shot(X0,sK47(X0,X5)) | ~'from$uloc'(X0,X2,X4) | ~fire(X0,X2) | ~scream(X0,X1) | ~male(X0,X9) | ~cry(X0,X6) | ~nonreflexive(X0,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.99/4.54 cnf(d0, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~patient(sK6,sK13,X1) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,X2) | ~man(sK6,X2) | ~of(sK6,X3,X2) | ~cannon(sK6,X3) | member(sK6,sK24(sK6,X2,X3,X4),X4) | member(sK6,sK26(sK6,X4),X4) | ~six(sK6,X4) | ~group(sK6,X4) | ~revenge(sK6,sK11) | ~cry(sK6,X1) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [c34,c33])).
% 16.99/4.54 cnf(d1, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~patient(sK6,sK13,X1) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK8) | ~male(sK6,X0) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,sK8,sK9,X2),X2) | member(sK6,sK26(sK6,X2),X2) | ~six(sK6,X2) | ~group(sK6,X2) | ~revenge(sK6,sK11) | ~cry(sK6,X1) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d0,c19])).
% 16.99/4.54 cnf(d2, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,sK8,sK9,X1),X1) | member(sK6,sK26(sK6,X1),X1) | ~six(sK6,X1) | ~group(sK6,X1) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d1,c29])).
% 16.99/4.54 cnf(d3, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,sK8,sK9,X0),X0) | member(sK6,sK26(sK6,X0),X0) | ~six(sK6,X0) | ~group(sK6,X0) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d2,c28])).
% 16.99/4.54 cnf(d4, plain, 'Ts2' | ~event(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~event(X0,X6) | ~agent(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5)),X3) | ~agent(X0,X6,X7) | ~patient(X0,X6,X8) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~present(X0,X6) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~nonreflexive(X0,X6) | ~fire(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~'from$uloc'(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5)),X4) | ~'actual$uworld'(X0) | ~male(X0,X7) | ~male(X0,X3) | ~man(X0,X3) | ~of(X0,X4,X3) | ~of(X0,X6,X9) | ~cannon(X0,X4) | member(X0,sK26(X0,X5),X5) | ~six(X0,X5) | ~group(X0,X5) | ~revenge(X0,X9) | ~cry(X0,X8) | ~scream(X0,X6) | ~'Ts0'(X0,X1,X2,sK24(X0,X3,X4,X5)), inference(resolution, [status(thm)], [c36,c3])).
% 16.99/4.54 cnf(d5, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X3,X2,X4)) | ~event(X0,X5) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~agent(X0,X5,X6) | ~agent(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4)),X3) | ~patient(X0,X5,X7) | ~present(X0,X5) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~nonreflexive(X0,X5) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~fire(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~'actual$uworld'(X0) | ~male(X0,X6) | ~male(X0,X3) | ~man(X0,X3) | ~of(X0,X5,X8) | ~of(X0,X2,X3) | ~cannon(X0,X2) | member(X0,sK26(X0,X4),X4) | ~six(X0,X4) | ~group(X0,X4) | ~revenge(X0,X8) | ~cry(X0,X7) | ~scream(X0,X5) | ~'Ts0'(X0,X1,X2,sK24(X0,X3,X2,X4)), inference(resolution, [status(thm)], [d4,c7])).
% 16.99/4.54 cnf(d6, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~nonreflexive(X0,X4) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~fire(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | member(X0,sK26(X0,X3),X3) | ~six(X0,X3) | ~group(X0,X3) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d5,c2])).
% 16.99/4.54 cnf(d7, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~nonreflexive(X0,X4) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | member(X0,sK26(X0,X3),X3) | ~six(X0,X3) | ~group(X0,X3) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d6,c6])).
% 16.99/4.54 cnf(d8, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~nonreflexive(X0,X4) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | member(X0,sK26(X0,X3),X3) | ~six(X0,X3) | ~group(X0,X3) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d7,c5])).
% 16.99/4.54 cnf(d9, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~nonreflexive(X0,X4) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | member(X0,sK26(X0,X3),X3) | ~six(X0,X3) | ~group(X0,X3) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d8,c4])).
% 16.99/4.54 cnf(d10, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~nonreflexive(X0,X4) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | member(X0,sK26(X0,X3),X3) | ~six(X0,X3) | ~group(X0,X3) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d9,c1])).
% 16.99/4.54 cnf(d11, plain, 'Ts2' | ~event(sK6,X0) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~nonreflexive(sK6,X0) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~of(sK6,sK9,sK8) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,X4),X4) | ~six(sK6,X4) | ~group(sK6,X4) | ~revenge(sK6,X3) | ~cry(sK6,X2) | ~scream(sK6,X0) | 'Ts2' | ~member(sK6,sK24(sK6,sK8,sK9,X4),sK10), inference(resolution, [status(thm)], [d10,c21])).
% 16.99/4.54 cnf(d12, plain, 'Ts2' | ~event(sK6,X0) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~nonreflexive(sK6,X0) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~of(sK6,sK9,sK8) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,X3) | ~cry(sK6,X2) | ~scream(sK6,X0) | 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13), inference(resolution, [status(thm)], [d11,d3])).
% 16.99/4.54 cnf(d13, plain, 'Ts2' | ~event(sK6,X0) | ~event(sK6,sK13) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,X0) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,X3) | ~revenge(sK6,sK11) | ~cry(sK6,X2) | ~cry(sK6,sK12) | ~scream(sK6,X0) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d12,c19])).
% 16.99/4.54 cnf(d14, plain, 'Ts2' | ~event(sK6,sK13) | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~patient(sK6,sK13,X1) | ~present(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~revenge(sK6,sK11) | ~cry(sK6,X1) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d13,c33])).
% 16.99/4.54 cnf(d15, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d14,c29])).
% 16.99/4.54 cnf(d16, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK26(sK6,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d15,c28])).
% 16.99/4.54 cnf(d17, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2' | shot(sK6,sK26(sK6,sK10)), inference(resolution, [status(thm)], [d16,c24])).
% 16.99/4.54 cnf(d18, plain, 'Ts2' | ~event(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~event(X0,X6) | ~agent(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5)),X3) | ~agent(X0,X6,X7) | ~patient(X0,X6,X8) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~present(X0,X6) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~nonreflexive(X0,X6) | ~fire(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5))) | ~'from$uloc'(X0,sK4(X1,X0,X2,sK24(X0,X3,X4,X5)),X4) | ~'actual$uworld'(X0) | ~male(X0,X7) | ~male(X0,X3) | ~man(X0,X3) | ~of(X0,X4,X3) | ~of(X0,X6,X9) | ~cannon(X0,X4) | ~six(X0,X5) | ~group(X0,X5) | ~shot(X0,sK26(X0,X5)) | ~revenge(X0,X9) | ~cry(X0,X8) | ~scream(X0,X6) | ~'Ts0'(X0,X1,X2,sK24(X0,X3,X4,X5)), inference(resolution, [status(thm)], [c37,c3])).
% 16.99/4.54 cnf(d19, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X3,X2,X4)) | ~event(X0,X5) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~agent(X0,X5,X6) | ~agent(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4)),X3) | ~patient(X0,X5,X7) | ~present(X0,X5) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~nonreflexive(X0,X5) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~fire(X0,sK4(X1,X0,X2,sK24(X0,X3,X2,X4))) | ~'actual$uworld'(X0) | ~male(X0,X6) | ~male(X0,X3) | ~man(X0,X3) | ~of(X0,X5,X8) | ~of(X0,X2,X3) | ~cannon(X0,X2) | ~six(X0,X4) | ~group(X0,X4) | ~shot(X0,sK26(X0,X4)) | ~revenge(X0,X8) | ~cry(X0,X7) | ~scream(X0,X5) | ~'Ts0'(X0,X1,X2,sK24(X0,X3,X2,X4)), inference(resolution, [status(thm)], [d18,c7])).
% 16.99/4.54 cnf(d20, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~nonreflexive(X0,X4) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~fire(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | ~six(X0,X3) | ~group(X0,X3) | ~shot(X0,sK26(X0,X3)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d19,c2])).
% 16.99/4.54 cnf(d21, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~nonreflexive(X0,X4) | ~nonreflexive(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | ~six(X0,X3) | ~group(X0,X3) | ~shot(X0,sK26(X0,X3)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d20,c6])).
% 16.99/4.54 cnf(d22, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~present(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~nonreflexive(X0,X4) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | ~six(X0,X3) | ~group(X0,X3) | ~shot(X0,sK26(X0,X3)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d21,c5])).
% 16.99/4.54 cnf(d23, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~event(X0,sK4(X1,X0,X2,sK24(X0,X1,X2,X3))) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~nonreflexive(X0,X4) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | ~six(X0,X3) | ~group(X0,X3) | ~shot(X0,sK26(X0,X3)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d22,c4])).
% 16.99/4.54 cnf(d24, plain, 'Ts2' | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)) | ~event(X0,X4) | ~agent(X0,X4,X5) | ~patient(X0,X4,X6) | ~present(X0,X4) | ~nonreflexive(X0,X4) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X1) | ~man(X0,X1) | ~of(X0,X4,X7) | ~of(X0,X2,X1) | ~cannon(X0,X2) | ~six(X0,X3) | ~group(X0,X3) | ~shot(X0,sK26(X0,X3)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X4) | ~'Ts0'(X0,X1,X2,sK24(X0,X1,X2,X3)), inference(resolution, [status(thm)], [d23,c1])).
% 16.99/4.54 cnf(d25, plain, 'Ts2' | ~event(sK6,X0) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~nonreflexive(sK6,X0) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~of(sK6,sK9,sK8) | ~cannon(sK6,sK9) | ~six(sK6,X4) | ~group(sK6,X4) | ~shot(sK6,sK26(sK6,X4)) | ~revenge(sK6,X3) | ~cry(sK6,X2) | ~scream(sK6,X0) | 'Ts2' | ~member(sK6,sK24(sK6,sK8,sK9,X4),sK10), inference(resolution, [status(thm)], [d24,c21])).
% 16.99/4.54 cnf(d26, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2' | ~event(sK6,X0) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~nonreflexive(sK6,X0) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,X3) | ~man(sK6,X3) | ~of(sK6,X4,X3) | ~of(sK6,X0,X5) | ~cannon(sK6,X4) | member(sK6,sK24(sK6,X3,X4,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,X5) | ~cry(sK6,X2) | ~scream(sK6,X0), inference(resolution, [status(thm)], [d17,c35])).
% 16.99/4.54 cnf(d27, plain, 'Ts2' | ~event(sK6,sK13) | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~patient(sK6,sK13,X1) | ~present(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X2) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,X2) | ~man(sK6,sK8) | ~of(sK6,X3,X2) | ~cannon(sK6,X3) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,X2,X3,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~revenge(sK6,sK11) | ~cry(sK6,X1) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d26,c33])).
% 16.99/4.54 cnf(d28, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~patient(sK6,sK13,X1) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK8) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,sK8,sK9,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,X1) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d27,c19])).
% 16.99/4.54 cnf(d29, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,sK8,sK9,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d28,c29])).
% 16.99/4.54 cnf(d30, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | member(sK6,sK24(sK6,sK8,sK9,sK10),sK10) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d29,c28])).
% 16.99/4.54 cnf(d31, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2' | ~event(sK6,X0) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~nonreflexive(sK6,X0) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~of(sK6,sK9,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~shot(sK6,sK26(sK6,sK10)) | ~revenge(sK6,X3) | ~cry(sK6,X2) | ~scream(sK6,X0), inference(resolution, [status(thm)], [d30,d25])).
% 16.99/4.54 cnf(d32, plain, 'Ts2' | ~event(sK6,X0) | ~event(sK6,sK13) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,X0) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~of(sK6,sK9,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,X3) | ~revenge(sK6,sK11) | ~cry(sK6,X2) | ~cry(sK6,sK12) | ~scream(sK6,X0) | ~scream(sK6,sK13) | 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13), inference(resolution, [status(thm)], [d31,d17])).
% 16.99/4.54 cnf(d33, plain, 'Ts2' | ~event(sK6,X0) | ~event(sK6,sK13) | ~agent(sK6,X0,X1) | ~patient(sK6,X0,X2) | ~present(sK6,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,X0) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X1) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~of(sK6,X0,X3) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,X3) | ~revenge(sK6,sK11) | ~cry(sK6,X2) | ~cry(sK6,sK12) | ~scream(sK6,X0) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d32,c19])).
% 16.99/4.54 cnf(d34, plain, 'Ts2' | ~event(sK6,sK13) | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~patient(sK6,sK13,X1) | ~present(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~revenge(sK6,sK11) | ~cry(sK6,X1) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d33,c33])).
% 16.99/4.54 cnf(d35, plain, 'Ts2' | ~event(sK6,sK13) | ~agent(sK6,sK13,X0) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,X0) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d34,c29])).
% 16.99/4.54 cnf(d36, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | ~scream(sK6,sK13) | 'Ts2', inference(resolution, [status(thm)], [d35,c28])).
% 16.99/4.54 cnf(d37, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | ~cry(sK6,sK12) | 'Ts2', inference(resolution, [status(thm)], [d36,c32])).
% 16.99/4.54 cnf(d38, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | ~revenge(sK6,sK11) | 'Ts2', inference(resolution, [status(thm)], [d37,c26])).
% 16.99/4.54 cnf(d39, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | ~group(sK6,sK10) | 'Ts2', inference(resolution, [status(thm)], [d38,c25])).
% 16.99/4.54 cnf(d40, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | ~six(sK6,sK10) | 'Ts2', inference(resolution, [status(thm)], [d39,c23])).
% 16.99/4.54 cnf(d41, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | ~cannon(sK6,sK9) | 'Ts2', inference(resolution, [status(thm)], [d40,c22])).
% 16.99/4.54 cnf(d42, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | ~man(sK6,sK8) | 'Ts2', inference(resolution, [status(thm)], [d41,c20])).
% 16.99/4.54 cnf(d43, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | ~male(sK6,sK8) | 'Ts2', inference(resolution, [status(thm)], [d42,c18])).
% 16.99/4.54 cnf(d44, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | ~male(sK6,sK7) | 'Ts2', inference(resolution, [status(thm)], [d43,c17])).
% 16.99/4.54 cnf(d45, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~nonreflexive(sK6,sK13) | ~'actual$uworld'(sK6) | 'Ts2', inference(resolution, [status(thm)], [d44,c16])).
% 16.99/4.54 cnf(d46, plain, 'Ts2' | ~event(sK6,sK13) | ~present(sK6,sK13) | ~'actual$uworld'(sK6) | 'Ts2', inference(resolution, [status(thm)], [d45,c31])).
% 16.99/4.54 cnf(d47, plain, 'Ts2' | ~event(sK6,sK13) | ~'actual$uworld'(sK6) | 'Ts2', inference(resolution, [status(thm)], [d46,c30])).
% 16.99/4.54 cnf(d48, plain, 'Ts2' | ~'actual$uworld'(sK6) | 'Ts2', inference(resolution, [status(thm)], [d47,c27])).
% 16.99/4.54 cnf(d49, plain, 'Ts2' | 'Ts2', inference(resolution, [status(thm)], [d48,c15])).
% 16.99/4.54 cnf(d50, plain, ~'Ts3', inference(resolution, [status(thm)], [d49,c0])).
% 16.99/4.54 cnf(d51, plain, 'actual$uworld'(sK27), inference(resolution, [status(thm)], [d50,c38])).
% 16.99/4.54 cnf(d52, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~patient(sK27,sK34,X1) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X2) | ~male(sK27,X0) | ~man(sK27,X2) | ~of(sK27,X3,X2) | ~cannon(sK27,X3) | member(sK27,sK45(sK27,X2,X3,X4),X4) | member(sK27,sK47(sK27,X4),X4) | ~six(sK27,X4) | ~group(sK27,X4) | ~revenge(sK27,sK33) | ~cry(sK27,X1) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [c57,c56])).
% 16.99/4.54 cnf(d53, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~patient(sK27,sK34,X1) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK29) | ~male(sK27,X0) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,sK29,sK30,X2),X2) | member(sK27,sK47(sK27,X2),X2) | ~six(sK27,X2) | ~group(sK27,X2) | ~revenge(sK27,sK33) | ~cry(sK27,X1) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d52,c42])).
% 16.99/4.54 cnf(d54, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X0) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,sK29,sK30,X1),X1) | member(sK27,sK47(sK27,X1),X1) | ~six(sK27,X1) | ~group(sK27,X1) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d53,c52])).
% 16.99/4.54 cnf(d55, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,sK29,sK30,X0),X0) | member(sK27,sK47(sK27,X0),X0) | ~six(sK27,X0) | ~group(sK27,X0) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d54,c51])).
% 16.99/4.54 cnf(d56, plain, 'Ts3' | ~event(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~event(X0,X6) | ~agent(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5),X1) | ~agent(X0,X6,X7) | ~patient(X0,X6,X8) | ~present(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~present(X0,X6) | ~nonreflexive(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~nonreflexive(X0,X6) | ~fire(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~'from$uloc'(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5),X2) | ~'actual$uworld'(X0) | ~male(X0,X1) | ~male(X0,X7) | ~man(X0,X1) | ~of(X0,X2,X1) | ~of(X0,X6,X9) | ~cannon(X0,X2) | member(X0,sK47(X0,X3),X3) | ~six(X0,X3) | ~group(X0,X3) | ~revenge(X0,X9) | ~cry(X0,X8) | ~scream(X0,X6) | ~'Ts1'(sK45(X0,X1,X2,X3),X0,X4,X5), inference(resolution, [status(thm)], [c59,c10])).
% 16.99/4.54 cnf(d57, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~agent(X0,X1,X6) | ~agent(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3),X2) | ~patient(X0,X1,X7) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~nonreflexive(X0,X1) | ~nonreflexive(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~fire(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X5,X3) | ~'actual$uworld'(X0) | ~male(X0,X6) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X1,X8) | ~of(X0,X3,X2) | ~cannon(X0,X3) | member(X0,sK47(X0,X4),X4) | ~six(X0,X4) | ~group(X0,X4) | ~revenge(X0,X8) | ~cry(X0,X7) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X5,X3), inference(resolution, [status(thm)], [d56,c14])).
% 16.99/4.54 cnf(d58, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~nonreflexive(X0,X1) | ~nonreflexive(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~fire(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | member(X0,sK47(X0,X4),X4) | ~six(X0,X4) | ~group(X0,X4) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d57,c9])).
% 16.99/4.54 cnf(d59, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~nonreflexive(X0,X1) | ~nonreflexive(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | member(X0,sK47(X0,X4),X4) | ~six(X0,X4) | ~group(X0,X4) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d58,c13])).
% 16.99/4.54 cnf(d60, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~nonreflexive(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | member(X0,sK47(X0,X4),X4) | ~six(X0,X4) | ~group(X0,X4) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d59,c12])).
% 16.99/4.54 cnf(d61, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~nonreflexive(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | member(X0,sK47(X0,X4),X4) | ~six(X0,X4) | ~group(X0,X4) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d60,c11])).
% 16.99/4.54 cnf(d62, plain, 'Ts3' | ~event(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X3) | ~present(X0,X1) | ~nonreflexive(X0,X1) | ~'Ts1'(sK45(X0,X4,X5,X6),X0,X4,X5) | ~'actual$uworld'(X0) | ~male(X0,X2) | ~male(X0,X4) | ~man(X0,X4) | ~of(X0,X5,X4) | ~of(X0,X1,X7) | ~cannon(X0,X5) | member(X0,sK47(X0,X6),X6) | ~six(X0,X6) | ~group(X0,X6) | ~revenge(X0,X7) | ~cry(X0,X3) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X4,X5,X6),X0,X4,X5), inference(resolution, [status(thm)], [d61,c8])).
% 16.99/4.54 cnf(d63, plain, 'Ts3' | ~event(sK27,X0) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~nonreflexive(sK27,X0) | ~'actual$uworld'(sK27) | ~male(sK27,sK29) | ~male(sK27,X1) | ~man(sK27,sK29) | ~of(sK27,sK30,sK29) | ~of(sK27,X0,X3) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,X4),X4) | ~six(sK27,X4) | ~group(sK27,X4) | ~revenge(sK27,X3) | ~cry(sK27,X2) | ~scream(sK27,X0) | 'Ts3' | ~member(sK27,sK45(sK27,sK29,sK30,X4),sK31), inference(resolution, [status(thm)], [d62,c44])).
% 16.99/4.54 cnf(d64, plain, 'Ts3' | ~event(sK27,X0) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~nonreflexive(sK27,X0) | ~'actual$uworld'(sK27) | ~male(sK27,X1) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~of(sK27,X0,X3) | ~of(sK27,sK30,sK29) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,X3) | ~cry(sK27,X2) | ~scream(sK27,X0) | 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34), inference(resolution, [status(thm)], [d63,d55])).
% 16.99/4.54 cnf(d65, plain, 'Ts3' | ~event(sK27,X0) | ~event(sK27,sK34) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,X0) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X1) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~of(sK27,X0,X3) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,X3) | ~revenge(sK27,sK33) | ~cry(sK27,X2) | ~cry(sK27,sK32) | ~scream(sK27,X0) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d64,c42])).
% 16.99/4.54 cnf(d66, plain, 'Ts3' | ~event(sK27,sK34) | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~patient(sK27,sK34,X1) | ~present(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~revenge(sK27,sK33) | ~cry(sK27,X1) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d65,c56])).
% 16.99/4.54 cnf(d67, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d66,c52])).
% 16.99/4.54 cnf(d68, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK47(sK27,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d67,c51])).
% 16.99/4.54 cnf(d69, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3' | shot(sK27,sK47(sK27,sK31)), inference(resolution, [status(thm)], [d68,c47])).
% 16.99/4.54 cnf(d70, plain, 'Ts3' | ~event(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~event(X0,X6) | ~agent(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5),X1) | ~agent(X0,X6,X7) | ~patient(X0,X6,X8) | ~present(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~present(X0,X6) | ~nonreflexive(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~nonreflexive(X0,X6) | ~fire(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5)) | ~'from$uloc'(X0,sK5(X0,sK45(X0,X1,X2,X3),X4,X5),X2) | ~'actual$uworld'(X0) | ~male(X0,X1) | ~male(X0,X7) | ~man(X0,X1) | ~of(X0,X2,X1) | ~of(X0,X6,X9) | ~cannon(X0,X2) | ~six(X0,X3) | ~group(X0,X3) | ~shot(X0,sK47(X0,X3)) | ~revenge(X0,X9) | ~cry(X0,X8) | ~scream(X0,X6) | ~'Ts1'(sK45(X0,X1,X2,X3),X0,X4,X5), inference(resolution, [status(thm)], [c60,c10])).
% 16.99/4.54 cnf(d71, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~agent(X0,X1,X6) | ~agent(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3),X2) | ~patient(X0,X1,X7) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~nonreflexive(X0,X1) | ~nonreflexive(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~fire(X0,sK5(X0,sK45(X0,X2,X3,X4),X5,X3)) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X5,X3) | ~'actual$uworld'(X0) | ~male(X0,X6) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X1,X8) | ~of(X0,X3,X2) | ~cannon(X0,X3) | ~six(X0,X4) | ~group(X0,X4) | ~shot(X0,sK47(X0,X4)) | ~revenge(X0,X8) | ~cry(X0,X7) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X5,X3), inference(resolution, [status(thm)], [d70,c14])).
% 16.99/4.54 cnf(d72, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~nonreflexive(X0,X1) | ~nonreflexive(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~fire(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | ~six(X0,X4) | ~group(X0,X4) | ~shot(X0,sK47(X0,X4)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d71,c9])).
% 16.99/4.54 cnf(d73, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~nonreflexive(X0,X1) | ~nonreflexive(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | ~six(X0,X4) | ~group(X0,X4) | ~shot(X0,sK47(X0,X4)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d72,c13])).
% 16.99/4.54 cnf(d74, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~present(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~nonreflexive(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | ~six(X0,X4) | ~group(X0,X4) | ~shot(X0,sK47(X0,X4)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d73,c12])).
% 16.99/4.54 cnf(d75, plain, 'Ts3' | ~event(X0,X1) | ~event(X0,sK5(X0,sK45(X0,X2,X3,X4),X2,X3)) | ~agent(X0,X1,X5) | ~patient(X0,X1,X6) | ~present(X0,X1) | ~nonreflexive(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3) | ~'actual$uworld'(X0) | ~male(X0,X5) | ~male(X0,X2) | ~man(X0,X2) | ~of(X0,X3,X2) | ~of(X0,X1,X7) | ~cannon(X0,X3) | ~six(X0,X4) | ~group(X0,X4) | ~shot(X0,sK47(X0,X4)) | ~revenge(X0,X7) | ~cry(X0,X6) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X2,X3,X4),X0,X2,X3), inference(resolution, [status(thm)], [d74,c11])).
% 16.99/4.54 cnf(d76, plain, 'Ts3' | ~event(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X3) | ~present(X0,X1) | ~nonreflexive(X0,X1) | ~'Ts1'(sK45(X0,X4,X5,X6),X0,X4,X5) | ~'actual$uworld'(X0) | ~male(X0,X2) | ~male(X0,X4) | ~man(X0,X4) | ~of(X0,X5,X4) | ~of(X0,X1,X7) | ~cannon(X0,X5) | ~six(X0,X6) | ~group(X0,X6) | ~shot(X0,sK47(X0,X6)) | ~revenge(X0,X7) | ~cry(X0,X3) | ~scream(X0,X1) | ~'Ts1'(sK45(X0,X4,X5,X6),X0,X4,X5), inference(resolution, [status(thm)], [d75,c8])).
% 16.99/4.54 cnf(d77, plain, 'Ts3' | ~event(sK27,X0) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~nonreflexive(sK27,X0) | ~'actual$uworld'(sK27) | ~male(sK27,sK29) | ~male(sK27,X1) | ~man(sK27,sK29) | ~of(sK27,sK30,sK29) | ~of(sK27,X0,X3) | ~cannon(sK27,sK30) | ~six(sK27,X4) | ~group(sK27,X4) | ~shot(sK27,sK47(sK27,X4)) | ~revenge(sK27,X3) | ~cry(sK27,X2) | ~scream(sK27,X0) | 'Ts3' | ~member(sK27,sK45(sK27,sK29,sK30,X4),sK31), inference(resolution, [status(thm)], [d76,c44])).
% 16.99/4.54 cnf(d78, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3' | ~event(sK27,X0) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~nonreflexive(sK27,X0) | ~'actual$uworld'(sK27) | ~male(sK27,X3) | ~male(sK27,X1) | ~man(sK27,X3) | ~of(sK27,X4,X3) | ~of(sK27,X0,X5) | ~cannon(sK27,X4) | member(sK27,sK45(sK27,X3,X4,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,X5) | ~cry(sK27,X2) | ~scream(sK27,X0), inference(resolution, [status(thm)], [d69,c58])).
% 16.99/4.54 cnf(d79, plain, 'Ts3' | ~event(sK27,sK34) | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~patient(sK27,sK34,X1) | ~present(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X2) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,X2) | ~man(sK27,sK29) | ~of(sK27,X3,X2) | ~cannon(sK27,X3) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,X2,X3,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~revenge(sK27,sK33) | ~cry(sK27,X1) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d78,c56])).
% 16.99/4.54 cnf(d80, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~patient(sK27,sK34,X1) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK29) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,sK29,sK30,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,X1) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d79,c42])).
% 16.99/4.54 cnf(d81, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,sK29,sK30,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d80,c52])).
% 16.99/4.54 cnf(d82, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | member(sK27,sK45(sK27,sK29,sK30,sK31),sK31) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d81,c51])).
% 16.99/4.54 cnf(d83, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3' | ~event(sK27,X0) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~nonreflexive(sK27,X0) | ~'actual$uworld'(sK27) | ~male(sK27,X1) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~of(sK27,X0,X3) | ~of(sK27,sK30,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~shot(sK27,sK47(sK27,sK31)) | ~revenge(sK27,X3) | ~cry(sK27,X2) | ~scream(sK27,X0), inference(resolution, [status(thm)], [d82,d77])).
% 16.99/4.54 cnf(d84, plain, 'Ts3' | ~event(sK27,X0) | ~event(sK27,sK34) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,X0) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X1) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~of(sK27,X0,X3) | ~of(sK27,sK30,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,X3) | ~revenge(sK27,sK33) | ~cry(sK27,X2) | ~cry(sK27,sK32) | ~scream(sK27,X0) | ~scream(sK27,sK34) | 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34), inference(resolution, [status(thm)], [d83,d69])).
% 16.99/4.54 cnf(d85, plain, 'Ts3' | ~event(sK27,X0) | ~event(sK27,sK34) | ~agent(sK27,X0,X1) | ~patient(sK27,X0,X2) | ~present(sK27,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,X0) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X1) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~of(sK27,X0,X3) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,X3) | ~revenge(sK27,sK33) | ~cry(sK27,X2) | ~cry(sK27,sK32) | ~scream(sK27,X0) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d84,c42])).
% 16.99/4.54 cnf(d86, plain, 'Ts3' | ~event(sK27,sK34) | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~patient(sK27,sK34,X1) | ~present(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~revenge(sK27,sK33) | ~cry(sK27,X1) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d85,c56])).
% 16.99/4.54 cnf(d87, plain, 'Ts3' | ~event(sK27,sK34) | ~agent(sK27,sK34,X0) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,X0) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d86,c52])).
% 16.99/4.54 cnf(d88, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | ~scream(sK27,sK34) | 'Ts3', inference(resolution, [status(thm)], [d87,c51])).
% 16.99/4.54 cnf(d89, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | ~cry(sK27,sK32) | 'Ts3', inference(resolution, [status(thm)], [d88,c55])).
% 16.99/4.54 cnf(d90, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | ~revenge(sK27,sK33) | 'Ts3', inference(resolution, [status(thm)], [d89,c48])).
% 16.99/4.54 cnf(d91, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | ~group(sK27,sK31) | 'Ts3', inference(resolution, [status(thm)], [d90,c49])).
% 16.99/4.54 cnf(d92, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | ~six(sK27,sK31) | 'Ts3', inference(resolution, [status(thm)], [d91,c46])).
% 16.99/4.54 cnf(d93, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | ~cannon(sK27,sK30) | 'Ts3', inference(resolution, [status(thm)], [d92,c45])).
% 16.99/4.54 cnf(d94, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | ~man(sK27,sK29) | 'Ts3', inference(resolution, [status(thm)], [d93,c43])).
% 16.99/4.54 cnf(d95, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | ~male(sK27,sK29) | 'Ts3', inference(resolution, [status(thm)], [d94,c41])).
% 16.99/4.54 cnf(d96, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | ~male(sK27,sK28) | 'Ts3', inference(resolution, [status(thm)], [d95,c40])).
% 16.99/4.54 cnf(d97, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~nonreflexive(sK27,sK34) | ~'actual$uworld'(sK27) | 'Ts3', inference(resolution, [status(thm)], [d96,c39])).
% 16.99/4.54 cnf(d98, plain, 'Ts3' | ~event(sK27,sK34) | ~present(sK27,sK34) | ~'actual$uworld'(sK27) | 'Ts3', inference(resolution, [status(thm)], [d97,c54])).
% 16.99/4.54 cnf(d99, plain, 'Ts3' | ~event(sK27,sK34) | ~'actual$uworld'(sK27) | 'Ts3', inference(resolution, [status(thm)], [d98,c53])).
% 16.99/4.54 cnf(d100, plain, 'Ts3' | ~'actual$uworld'(sK27) | 'Ts3', inference(resolution, [status(thm)], [d99,c50])).
% 16.99/4.54 cnf(d101, plain, ~'actual$uworld'(sK27), inference(resolution, [status(thm)], [d50,d100])).
% 16.99/4.54 cnf(d102, plain, $false, inference(resolution, [status(thm)], [d101,d51])).
% 16.99/4.54 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------