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