%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NLP117+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 : n004.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:38 AM UTC 2026
% Result : Theorem 12.19s 2.14s
% Output : CNFRefutation 12.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP117+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.09/0.37 % Computer : n004.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 00:53:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.19/2.14 % SZS status Theorem for theBenchmark.p
% 12.19/2.14 % SZS output start CNFRefutation for theBenchmark.p
% 12.19/2.14 fof(co1, conjecture, ~~(((? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((of(X0,X2,X1) & (city(X0,X1) & ('hollywood$uplacename'(X0,X2) & (placename(X0,X2) & (chevy(X0,X3) & (white(X0,X3) & (dirty(X0,X3) & (old(X0,X3) & (street(X0,X4) & (lonely(X0,X4) & (event(X0,X5) & (agent(X0,X5,X3) & (present(X0,X5) & (barrel(X0,X5) & (down(X0,X5,X4) & in(X0,X5,X1))))))))))))))))))) => ? [X6] : (('actual$uworld'(X6) & ? [X7] : ? [X8] : ? [X9] : ? [X10] : ? [X11] : ((of(X6,X8,X7) & (city(X6,X7) & ('hollywood$uplacename'(X6,X8) & (placename(X6,X8) & (street(X6,X9) & (lonely(X6,X9) & (chevy(X6,X10) & (white(X6,X10) & (dirty(X6,X10) & (old(X6,X10) & (event(X6,X11) & (agent(X6,X11,X10) & (present(X6,X11) & (barrel(X6,X11) & (down(X6,X11,X9) & in(X6,X11,X7)))))))))))))))))))) & (? [X6] : (('actual$uworld'(X6) & ? [X7] : ? [X8] : ? [X9] : ? [X10] : ? [X11] : ((of(X6,X8,X7) & (city(X6,X7) & ('hollywood$uplacename'(X6,X8) & (placename(X6,X8) & (street(X6,X9) & (lonely(X6,X9) & (chevy(X6,X10) & (white(X6,X10) & (dirty(X6,X10) & (old(X6,X10) & (event(X6,X11) & (agent(X6,X11,X10) & (present(X6,X11) & (barrel(X6,X11) & (down(X6,X11,X9) & in(X6,X11,X7))))))))))))))))))) => ? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((of(X0,X2,X1) & (city(X0,X1) & ('hollywood$uplacename'(X0,X2) & (placename(X0,X2) & (chevy(X0,X3) & (white(X0,X3) & (dirty(X0,X3) & (old(X0,X3) & (street(X0,X4) & (lonely(X0,X4) & (event(X0,X5) & (agent(X0,X5,X3) & (present(X0,X5) & (barrel(X0,X5) & (down(X0,X5,X4) & in(X0,X5,X1))))))))))))))))))))))).
% 12.19/2.14 fof(negated_conjecture, negated_conjecture, ~~~(((? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((of(X0,X2,X1) & (city(X0,X1) & ('hollywood$uplacename'(X0,X2) & (placename(X0,X2) & (chevy(X0,X3) & (white(X0,X3) & (dirty(X0,X3) & (old(X0,X3) & (street(X0,X4) & (lonely(X0,X4) & (event(X0,X5) & (agent(X0,X5,X3) & (present(X0,X5) & (barrel(X0,X5) & (down(X0,X5,X4) & in(X0,X5,X1))))))))))))))))))) => ? [X6] : (('actual$uworld'(X6) & ? [X7] : ? [X8] : ? [X9] : ? [X10] : ? [X11] : ((of(X6,X8,X7) & (city(X6,X7) & ('hollywood$uplacename'(X6,X8) & (placename(X6,X8) & (street(X6,X9) & (lonely(X6,X9) & (chevy(X6,X10) & (white(X6,X10) & (dirty(X6,X10) & (old(X6,X10) & (event(X6,X11) & (agent(X6,X11,X10) & (present(X6,X11) & (barrel(X6,X11) & (down(X6,X11,X9) & in(X6,X11,X7)))))))))))))))))))) & (? [X6] : (('actual$uworld'(X6) & ? [X7] : ? [X8] : ? [X9] : ? [X10] : ? [X11] : ((of(X6,X8,X7) & (city(X6,X7) & ('hollywood$uplacename'(X6,X8) & (placename(X6,X8) & (street(X6,X9) & (lonely(X6,X9) & (chevy(X6,X10) & (white(X6,X10) & (dirty(X6,X10) & (old(X6,X10) & (event(X6,X11) & (agent(X6,X11,X10) & (present(X6,X11) & (barrel(X6,X11) & (down(X6,X11,X9) & in(X6,X11,X7))))))))))))))))))) => ? [X0] : (('actual$uworld'(X0) & ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((of(X0,X2,X1) & (city(X0,X1) & ('hollywood$uplacename'(X0,X2) & (placename(X0,X2) & (chevy(X0,X3) & (white(X0,X3) & (dirty(X0,X3) & (old(X0,X3) & (street(X0,X4) & (lonely(X0,X4) & (event(X0,X5) & (agent(X0,X5,X3) & (present(X0,X5) & (barrel(X0,X5) & (down(X0,X5,X4) & in(X0,X5,X1)))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])).
% 12.19/2.14 cnf(c0, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c1, plain, X0 | 'actual$uworld'(sK2), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c2, plain, X0 | of(sK2,sK4,sK3), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c3, plain, X0 | city(sK2,sK3), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c4, plain, X0 | 'hollywood$uplacename'(sK2,sK4), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c5, plain, X0 | placename(sK2,sK4), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c6, plain, X0 | chevy(sK2,sK5), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c7, plain, X0 | white(sK2,sK5), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c8, plain, X0 | dirty(sK2,sK5), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c9, plain, X0 | old(sK2,sK5), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c10, plain, X0 | street(sK2,sK6), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c11, plain, X0 | lonely(sK2,sK6), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c12, plain, X0 | event(sK2,sK7), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c13, plain, X0 | agent(sK2,sK7,sK5), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c14, plain, X0 | present(sK2,sK7), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c15, plain, X0 | barrel(sK2,sK7), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c16, plain, X0 | down(sK2,sK7,sK6), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c17, plain, X0 | in(sK2,sK7,sK3), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c18, plain, ~down(X0,X1,X2) | ~chevy(X0,X3) | ~in(X0,X1,X4) | ~dirty(X0,X3) | ~event(X0,X1) | ~'actual$uworld'(X0) | ~of(X0,X5,X4) | ~barrel(X0,X1) | ~city(X0,X4) | ~placename(X0,X5) | ~'hollywood$uplacename'(X0,X5) | ~present(X0,X1) | ~agent(X0,X1,X3) | ~lonely(X0,X2) | ~white(X0,X3) | X6 | ~old(X0,X3) | ~street(X0,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c19, plain, X0 | 'actual$uworld'(sK14), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c20, plain, X0 | of(sK14,sK16,sK15), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c21, plain, X0 | city(sK14,sK15), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c22, plain, X0 | 'hollywood$uplacename'(sK14,sK16), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c23, plain, X0 | placename(sK14,sK16), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c24, plain, X0 | street(sK14,sK17), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c25, plain, X0 | lonely(sK14,sK17), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c26, plain, X0 | chevy(sK14,sK18), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c27, plain, X0 | white(sK14,sK18), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c28, plain, X0 | dirty(sK14,sK18), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c29, plain, X0 | old(sK14,sK18), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c30, plain, X0 | event(sK14,sK19), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c31, plain, X0 | agent(sK14,sK19,sK18), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c32, plain, X0 | present(sK14,sK19), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c33, plain, X0 | barrel(sK14,sK19), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c34, plain, X0 | down(sK14,sK19,sK17), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c35, plain, X0 | in(sK14,sK19,sK15), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(c36, plain, ~in(X0,X1,X2) | ~down(X0,X1,X3) | ~city(X0,X2) | ~present(X0,X1) | ~agent(X0,X1,X4) | ~white(X0,X4) | ~barrel(X0,X1) | ~street(X0,X3) | ~'actual$uworld'(X0) | ~of(X0,X5,X2) | ~'hollywood$uplacename'(X0,X5) | X6 | ~dirty(X0,X4) | ~event(X0,X1) | ~chevy(X0,X4) | ~old(X0,X4) | ~placename(X0,X5) | ~lonely(X0,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.19/2.14 cnf(d0, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~of(sK2,X0,sK3) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,X0) | ~placename(sK2,X0) | ~chevy(sK2,X1) | ~white(sK2,X1) | ~dirty(sK2,X1) | ~old(sK2,X1) | ~street(sK2,X2) | ~lonely(sK2,X2) | ~event(sK2,sK7) | ~agent(sK2,sK7,X1) | ~present(sK2,sK7) | ~barrel(sK2,sK7) | ~down(sK2,sK7,X2) | 'Ts0', inference(resolution, [status(thm)], [c18,c17])).
% 12.19/2.14 cnf(d1, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~of(sK2,X0,sK3) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,X0) | ~placename(sK2,X0) | ~chevy(sK2,X1) | ~white(sK2,X1) | ~dirty(sK2,X1) | ~old(sK2,X1) | ~street(sK2,sK6) | ~lonely(sK2,sK6) | ~event(sK2,sK7) | ~agent(sK2,sK7,X1) | ~present(sK2,sK7) | ~barrel(sK2,sK7) | 'Ts0', inference(resolution, [status(thm)], [d0,c16])).
% 12.19/2.14 cnf(d2, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~of(sK2,X0,sK3) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,X0) | ~placename(sK2,X0) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | ~street(sK2,sK6) | ~lonely(sK2,sK6) | ~event(sK2,sK7) | ~present(sK2,sK7) | ~barrel(sK2,sK7) | 'Ts0', inference(resolution, [status(thm)], [d1,c13])).
% 12.19/2.14 cnf(d3, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | ~street(sK2,sK6) | ~lonely(sK2,sK6) | ~event(sK2,sK7) | ~present(sK2,sK7) | ~barrel(sK2,sK7) | 'Ts0', inference(resolution, [status(thm)], [d2,c2])).
% 12.19/2.14 cnf(d4, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | ~street(sK2,sK6) | ~lonely(sK2,sK6) | ~event(sK2,sK7) | ~present(sK2,sK7) | 'Ts0', inference(resolution, [status(thm)], [d3,c15])).
% 12.19/2.14 cnf(d5, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | ~street(sK2,sK6) | ~lonely(sK2,sK6) | ~event(sK2,sK7) | 'Ts0', inference(resolution, [status(thm)], [d4,c14])).
% 12.19/2.14 cnf(d6, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | ~street(sK2,sK6) | ~lonely(sK2,sK6) | 'Ts0', inference(resolution, [status(thm)], [d5,c12])).
% 12.19/2.14 cnf(d7, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | ~street(sK2,sK6) | 'Ts0', inference(resolution, [status(thm)], [d6,c11])).
% 12.19/2.14 cnf(d8, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | ~old(sK2,sK5) | 'Ts0', inference(resolution, [status(thm)], [d7,c10])).
% 12.19/2.14 cnf(d9, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | ~dirty(sK2,sK5) | 'Ts0', inference(resolution, [status(thm)], [d8,c9])).
% 12.19/2.14 cnf(d10, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | ~white(sK2,sK5) | 'Ts0', inference(resolution, [status(thm)], [d9,c8])).
% 12.19/2.14 cnf(d11, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | ~chevy(sK2,sK5) | 'Ts0', inference(resolution, [status(thm)], [d10,c7])).
% 12.19/2.14 cnf(d12, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | ~placename(sK2,sK4) | 'Ts0', inference(resolution, [status(thm)], [d11,c6])).
% 12.19/2.14 cnf(d13, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | ~'hollywood$uplacename'(sK2,sK4) | 'Ts0', inference(resolution, [status(thm)], [d12,c5])).
% 12.19/2.14 cnf(d14, plain, 'Ts0' | ~'actual$uworld'(sK2) | ~city(sK2,sK3) | 'Ts0', inference(resolution, [status(thm)], [d13,c4])).
% 12.19/2.14 cnf(d15, plain, 'Ts0' | ~'actual$uworld'(sK2) | 'Ts0', inference(resolution, [status(thm)], [d14,c3])).
% 12.19/2.14 cnf(d16, plain, 'Ts0' | 'Ts0', inference(resolution, [status(thm)], [d15,c1])).
% 12.19/2.14 cnf(d17, plain, ~'Ts1', inference(resolution, [status(thm)], [d16,c0])).
% 12.19/2.14 cnf(d18, plain, of(sK14,sK16,sK15), inference(resolution, [status(thm)], [d17,c20])).
% 12.19/2.14 cnf(d19, plain, 'Ts1' | ~'actual$uworld'(sK14) | ~of(sK14,X0,sK15) | ~city(sK14,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,X1) | ~white(sK14,X1) | ~dirty(sK14,X1) | ~old(sK14,X1) | ~street(sK14,X2) | ~lonely(sK14,X2) | ~event(sK14,sK19) | ~agent(sK14,sK19,X1) | ~present(sK14,sK19) | ~barrel(sK14,sK19) | ~down(sK14,sK19,X2) | 'Ts1', inference(resolution, [status(thm)], [c36,c35])).
% 12.19/2.14 cnf(d20, plain, 'Ts1' | ~'actual$uworld'(sK14) | ~of(sK14,X0,sK15) | ~city(sK14,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,X1) | ~white(sK14,X1) | ~dirty(sK14,X1) | ~old(sK14,X1) | ~street(sK14,sK17) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~agent(sK14,sK19,X1) | ~present(sK14,sK19) | ~barrel(sK14,sK19) | 'Ts1', inference(resolution, [status(thm)], [d19,c34])).
% 12.19/2.14 cnf(d21, plain, 'Ts1' | ~'actual$uworld'(sK14) | ~of(sK14,X0,sK15) | ~city(sK14,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~dirty(sK14,sK18) | ~old(sK14,sK18) | ~street(sK14,sK17) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19) | 'Ts1', inference(resolution, [status(thm)], [d20,c31])).
% 12.19/2.14 cnf(d22, plain, ~'actual$uworld'(sK14) | ~of(sK14,X0,sK15) | ~city(sK14,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~dirty(sK14,sK18) | ~old(sK14,sK18) | ~street(sK14,sK17) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d17,d21])).
% 12.19/2.14 cnf(d23, plain, 'actual$uworld'(sK14), inference(resolution, [status(thm)], [d17,c19])).
% 12.19/2.14 cnf(d24, plain, ~of(sK14,X0,sK15) | ~city(sK14,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~dirty(sK14,sK18) | ~old(sK14,sK18) | ~street(sK14,sK17) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d23,d22])).
% 12.19/2.14 cnf(d25, plain, street(sK14,sK17), inference(resolution, [status(thm)], [d17,c24])).
% 12.19/2.14 cnf(d26, plain, ~of(sK14,X0,sK15) | ~city(sK14,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~dirty(sK14,sK18) | ~old(sK14,sK18) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d25,d24])).
% 12.19/2.14 cnf(d27, plain, city(sK14,sK15), inference(resolution, [status(thm)], [d17,c21])).
% 12.19/2.14 cnf(d28, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~dirty(sK14,sK18) | ~old(sK14,sK18) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d27,d26])).
% 12.19/2.14 cnf(d29, plain, dirty(sK14,sK18), inference(resolution, [status(thm)], [d17,c28])).
% 12.19/2.14 cnf(d30, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~old(sK14,sK18) | ~lonely(sK14,sK17) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d29,d28])).
% 12.19/2.14 cnf(d31, plain, lonely(sK14,sK17), inference(resolution, [status(thm)], [d17,c25])).
% 12.19/2.14 cnf(d32, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~chevy(sK14,sK18) | ~white(sK14,sK18) | ~old(sK14,sK18) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d31,d30])).
% 12.19/2.14 cnf(d33, plain, chevy(sK14,sK18), inference(resolution, [status(thm)], [d17,c26])).
% 12.19/2.14 cnf(d34, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~white(sK14,sK18) | ~old(sK14,sK18) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d33,d32])).
% 12.19/2.14 cnf(d35, plain, white(sK14,sK18), inference(resolution, [status(thm)], [d17,c27])).
% 12.19/2.14 cnf(d36, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~old(sK14,sK18) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d35,d34])).
% 12.19/2.14 cnf(d37, plain, old(sK14,sK18), inference(resolution, [status(thm)], [d17,c29])).
% 12.19/2.14 cnf(d38, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~event(sK14,sK19) | ~present(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d37,d36])).
% 12.19/2.14 cnf(d39, plain, present(sK14,sK19), inference(resolution, [status(thm)], [d17,c32])).
% 12.19/2.14 cnf(d40, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~event(sK14,sK19) | ~barrel(sK14,sK19), inference(resolution, [status(thm)], [d39,d38])).
% 12.19/2.14 cnf(d41, plain, barrel(sK14,sK19), inference(resolution, [status(thm)], [d17,c33])).
% 12.19/2.14 cnf(d42, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0) | ~event(sK14,sK19), inference(resolution, [status(thm)], [d41,d40])).
% 12.19/2.14 cnf(d43, plain, event(sK14,sK19), inference(resolution, [status(thm)], [d17,c30])).
% 12.19/2.14 cnf(d44, plain, ~of(sK14,X0,sK15) | ~'hollywood$uplacename'(sK14,X0) | ~placename(sK14,X0), inference(resolution, [status(thm)], [d43,d42])).
% 12.19/2.14 cnf(d45, plain, ~'hollywood$uplacename'(sK14,sK16) | ~placename(sK14,sK16), inference(resolution, [status(thm)], [d44,d18])).
% 12.19/2.14 cnf(d46, plain, placename(sK14,sK16), inference(resolution, [status(thm)], [d17,c23])).
% 12.19/2.14 cnf(d47, plain, ~'hollywood$uplacename'(sK14,sK16), inference(resolution, [status(thm)], [d46,d45])).
% 12.19/2.14 cnf(d48, plain, 'hollywood$uplacename'(sK14,sK16), inference(resolution, [status(thm)], [d17,c22])).
% 12.19/2.14 cnf(d49, plain, $false, inference(resolution, [status(thm)], [d48,d47])).
% 12.19/2.14 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------