%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NLP007+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 : n008.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:22 AM UTC 2026 % Result : Theorem 27.50s 4.06s % Output : CNFRefutation 27.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP007+1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n008.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 26 00:23:39 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.50/4.06 % SZS status Theorem for theBenchmark.p % 27.50/4.06 % SZS output start CNFRefutation for theBenchmark.p % 27.50/4.06 fof(co1, conjecture, ((? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ? [X9] : ((seat(X0) & (furniture(X0) & (front(X0) & (hollywood(X1) & (city(X1) & (event(X2) & (chevy(X3) & (car(X3) & (white(X3) & (dirty(X3) & (old(X3) & (street(X4) & (way(X4) & (lonely(X4) & (barrel(X2,X3) & (down(X2,X4) & (in(X2,X1) & (seat(X7) & (furniture(X7) & (front(X7) & (X5 != X6 & (fellow(X5) & (man(X5) & (young(X5) & (fellow(X6) & (man(X6) & (young(X6) & (X5 = X8 & (in(X8,X7) & (X6 = X9 & in(X9,X0)))))))))))))))))))))))))))))))) => ? [X10] : ? [X11] : ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ? [X18] : ? [X19] : ((seat(X10) & (furniture(X10) & (front(X10) & (hollywood(X11) & (city(X11) & (event(X12) & (chevy(X13) & (car(X13) & (white(X13) & (dirty(X13) & (old(X13) & (street(X14) & (way(X14) & (lonely(X14) & (barrel(X12,X13) & (down(X12,X14) & (in(X12,X11) & (seat(X17) & (furniture(X17) & (front(X17) & (X15 != X16 & (fellow(X15) & (man(X15) & (young(X15) & (fellow(X16) & (man(X16) & (young(X16) & (X15 = X18 & (in(X18,X10) & (X16 = X19 & in(X19,X17))))))))))))))))))))))))))))))))) & (? [X20] : ? [X21] : ? [X22] : ? [X23] : ? [X24] : ? [X25] : ? [X26] : ? [X27] : ? [X28] : ? [X29] : ((seat(X20) & (furniture(X20) & (front(X20) & (hollywood(X21) & (city(X21) & (event(X22) & (chevy(X23) & (car(X23) & (white(X23) & (dirty(X23) & (old(X23) & (street(X24) & (way(X24) & (lonely(X24) & (barrel(X22,X23) & (down(X22,X24) & (in(X22,X21) & (seat(X27) & (furniture(X27) & (front(X27) & (X25 != X26 & (fellow(X25) & (man(X25) & (young(X25) & (fellow(X26) & (man(X26) & (young(X26) & (X25 = X28 & (in(X28,X20) & (X26 = X29 & in(X29,X27)))))))))))))))))))))))))))))))) => ? [X30] : ? [X31] : ? [X32] : ? [X33] : ? [X34] : ? [X35] : ? [X36] : ? [X37] : ? [X38] : ? [X39] : ((seat(X30) & (furniture(X30) & (front(X30) & (hollywood(X31) & (city(X31) & (event(X32) & (chevy(X33) & (car(X33) & (white(X33) & (dirty(X33) & (old(X33) & (street(X34) & (way(X34) & (lonely(X34) & (barrel(X32,X33) & (down(X32,X34) & (in(X32,X31) & (seat(X37) & (furniture(X37) & (front(X37) & (X35 != X36 & (fellow(X35) & (man(X35) & (young(X35) & (fellow(X36) & (man(X36) & (young(X36) & (X35 = X38 & (in(X38,X37) & (X36 = X39 & in(X39,X30))))))))))))))))))))))))))))))))))). % 27.50/4.06 fof(negated_conjecture, negated_conjecture, ~(((? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ? [X9] : ((seat(X0) & (furniture(X0) & (front(X0) & (hollywood(X1) & (city(X1) & (event(X2) & (chevy(X3) & (car(X3) & (white(X3) & (dirty(X3) & (old(X3) & (street(X4) & (way(X4) & (lonely(X4) & (barrel(X2,X3) & (down(X2,X4) & (in(X2,X1) & (seat(X7) & (furniture(X7) & (front(X7) & (X5 != X6 & (fellow(X5) & (man(X5) & (young(X5) & (fellow(X6) & (man(X6) & (young(X6) & (X5 = X8 & (in(X8,X7) & (X6 = X9 & in(X9,X0)))))))))))))))))))))))))))))))) => ? [X10] : ? [X11] : ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ? [X18] : ? [X19] : ((seat(X10) & (furniture(X10) & (front(X10) & (hollywood(X11) & (city(X11) & (event(X12) & (chevy(X13) & (car(X13) & (white(X13) & (dirty(X13) & (old(X13) & (street(X14) & (way(X14) & (lonely(X14) & (barrel(X12,X13) & (down(X12,X14) & (in(X12,X11) & (seat(X17) & (furniture(X17) & (front(X17) & (X15 != X16 & (fellow(X15) & (man(X15) & (young(X15) & (fellow(X16) & (man(X16) & (young(X16) & (X15 = X18 & (in(X18,X10) & (X16 = X19 & in(X19,X17))))))))))))))))))))))))))))))))) & (? [X20] : ? [X21] : ? [X22] : ? [X23] : ? [X24] : ? [X25] : ? [X26] : ? [X27] : ? [X28] : ? [X29] : ((seat(X20) & (furniture(X20) & (front(X20) & (hollywood(X21) & (city(X21) & (event(X22) & (chevy(X23) & (car(X23) & (white(X23) & (dirty(X23) & (old(X23) & (street(X24) & (way(X24) & (lonely(X24) & (barrel(X22,X23) & (down(X22,X24) & (in(X22,X21) & (seat(X27) & (furniture(X27) & (front(X27) & (X25 != X26 & (fellow(X25) & (man(X25) & (young(X25) & (fellow(X26) & (man(X26) & (young(X26) & (X25 = X28 & (in(X28,X20) & (X26 = X29 & in(X29,X27)))))))))))))))))))))))))))))))) => ? [X30] : ? [X31] : ? [X32] : ? [X33] : ? [X34] : ? [X35] : ? [X36] : ? [X37] : ? [X38] : ? [X39] : ((seat(X30) & (furniture(X30) & (front(X30) & (hollywood(X31) & (city(X31) & (event(X32) & (chevy(X33) & (car(X33) & (white(X33) & (dirty(X33) & (old(X33) & (street(X34) & (way(X34) & (lonely(X34) & (barrel(X32,X33) & (down(X32,X34) & (in(X32,X31) & (seat(X37) & (furniture(X37) & (front(X37) & (X35 != X36 & (fellow(X35) & (man(X35) & (young(X35) & (fellow(X36) & (man(X36) & (young(X36) & (X35 = X38 & (in(X38,X37) & (X36 = X39 & in(X39,X30))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 27.50/4.06 cnf(c0, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c1, plain, X0 | seat(sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c2, plain, X0 | furniture(sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c3, plain, X0 | front(sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c4, plain, X0 | hollywood(sK3), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c5, plain, X0 | city(sK3), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c6, plain, X0 | event(sK4), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c7, plain, X0 | chevy(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c8, plain, X0 | car(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c9, plain, X0 | white(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c10, plain, X0 | dirty(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c11, plain, X0 | old(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c12, plain, X0 | street(sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c13, plain, X0 | way(sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c14, plain, X0 | lonely(sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c15, plain, X0 | barrel(sK4,sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c16, plain, X0 | down(sK4,sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c17, plain, X0 | in(sK4,sK3), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c18, plain, X0 | seat(sK9), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c19, plain, X0 | furniture(sK9), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c20, plain, X0 | front(sK9), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c21, plain, X0 | sK7 != sK8, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c22, plain, X0 | fellow(sK7), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c23, plain, X0 | man(sK7), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c24, plain, X0 | young(sK7), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c25, plain, X0 | fellow(sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c26, plain, X0 | man(sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c27, plain, X0 | young(sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c28, plain, X0 | sK7 = sK10, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c29, plain, X0 | in(sK10,sK9), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c30, plain, X0 | sK8 = sK11, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c31, plain, X0 | in(sK11,sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c32, plain, ~man(X0) | ~in(X1,X2) | ~in(X3,X4) | ~fellow(X5) | ~furniture(X2) | ~city(X4) | ~young(X0) | ~dirty(X6) | ~street(X7) | ~seat(X8) | ~car(X6) | ~way(X7) | X9 | ~man(X5) | ~furniture(X8) | ~barrel(X3,X6) | ~old(X6) | ~white(X6) | ~hollywood(X4) | ~front(X8) | X0 = X5 | X0 != X1 | ~down(X3,X7) | ~fellow(X0) | ~front(X2) | ~young(X5) | ~lonely(X7) | ~seat(X2) | ~event(X3) | X5 != X10 | ~chevy(X6) | ~in(X10,X8), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c33, plain, X0 | seat(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c34, plain, X0 | furniture(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c35, plain, X0 | front(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c36, plain, X0 | hollywood(sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c37, plain, X0 | city(sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c38, plain, X0 | event(sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c39, plain, X0 | chevy(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c40, plain, X0 | car(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c41, plain, X0 | white(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c42, plain, X0 | dirty(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c43, plain, X0 | old(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c44, plain, X0 | street(sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c45, plain, X0 | way(sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c46, plain, X0 | lonely(sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c47, plain, X0 | barrel(sK24,sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c48, plain, X0 | down(sK24,sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c49, plain, X0 | in(sK24,sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c50, plain, X0 | seat(sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c51, plain, X0 | furniture(sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c52, plain, X0 | front(sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c53, plain, X0 | sK27 != sK28, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c54, plain, X0 | fellow(sK27), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c55, plain, X0 | man(sK27), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c56, plain, X0 | young(sK27), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c57, plain, X0 | fellow(sK28), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c58, plain, X0 | man(sK28), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c59, plain, X0 | young(sK28), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c60, plain, X0 | sK27 = sK30, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c61, plain, X0 | in(sK30,sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c62, plain, X0 | sK28 = sK31, inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c63, plain, X0 | in(sK31,sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(c64, plain, ~front(X0) | ~in(X1,X0) | ~fellow(X2) | ~in(X3,X4) | ~way(X5) | ~front(X4) | ~hollywood(X6) | ~city(X6) | ~in(X7,X6) | ~fellow(X8) | ~white(X9) | ~man(X8) | ~lonely(X5) | ~seat(X4) | X8 != X3 | ~chevy(X9) | ~young(X8) | X10 | ~event(X7) | ~street(X5) | X2 != X1 | ~car(X9) | ~furniture(X4) | ~young(X2) | ~man(X2) | ~seat(X0) | X2 = X8 | ~old(X9) | ~dirty(X9) | ~barrel(X7,X9) | ~down(X7,X5) | ~furniture(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 27.50/4.06 cnf(d0, plain, in(sK8,sK2) | 'Ts0' | 'Ts0', inference(superposition, [status(thm)], [c30,c31])). % 27.50/4.06 cnf(d1, plain, X0 != X1 | X0 = X2 | 'Ts0' | ~seat(X3) | ~seat(X4) | ~furniture(X3) | ~furniture(X4) | ~front(X3) | ~front(X4) | ~hollywood(X5) | ~city(X5) | ~event(X6) | ~chevy(X7) | ~car(X7) | ~white(X7) | ~dirty(X7) | ~old(X7) | ~street(X8) | ~way(X8) | ~lonely(X8) | ~barrel(X6,X7) | ~down(X6,X8) | ~in(X1,X3) | ~in(X2,X4) | ~in(X6,X5) | ~fellow(X0) | ~fellow(X2) | ~man(X0) | ~man(X2) | ~young(X0) | ~young(X2), inference(equality_resolution, [status(thm)], [c32])). % 27.50/4.06 cnf(d2, plain, X0 = X1 | 'Ts0' | ~seat(X2) | ~seat(X3) | ~furniture(X2) | ~furniture(X3) | ~front(X2) | ~front(X3) | ~hollywood(X4) | ~city(X4) | ~event(X5) | ~chevy(X6) | ~car(X6) | ~white(X6) | ~dirty(X6) | ~old(X6) | ~street(X7) | ~way(X7) | ~lonely(X7) | ~barrel(X5,X6) | ~down(X5,X7) | ~in(X5,X4) | ~in(X1,X2) | ~in(X0,X3) | ~fellow(X1) | ~fellow(X0) | ~man(X1) | ~man(X0) | ~young(X1) | ~young(X0), inference(equality_resolution, [status(thm)], [d1])). % 27.50/4.06 cnf(d3, plain, sK8 = X0 | 'Ts0' | ~seat(sK2) | ~seat(X1) | ~furniture(sK2) | ~furniture(X1) | ~front(sK2) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~fellow(sK8) | ~man(X0) | ~man(sK8) | ~young(X0) | ~young(sK8) | 'Ts0', inference(resolution, [status(thm)], [d2,d0])). % 27.50/4.06 cnf(d4, plain, sK8 = sK10 | 'Ts0' | ~seat(sK9) | ~seat(sK2) | ~furniture(sK9) | ~furniture(sK2) | ~front(sK9) | ~front(sK2) | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~fellow(sK10) | ~fellow(sK8) | ~man(sK10) | ~man(sK8) | ~young(sK10) | ~young(sK8) | 'Ts0', inference(resolution, [status(thm)], [d3,c29])). % 27.50/4.06 cnf(d5, plain, sK8 = sK10 | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sK4,X0) | ~down(sK4,X1) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | ~young(sK10) | 'Ts0', inference(resolution, [status(thm)], [d4,c17])). % 27.50/4.06 cnf(d6, plain, sK8 = sK10 | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~barrel(sK4,X0) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | ~young(sK10) | 'Ts0', inference(resolution, [status(thm)], [d5,c16])). % 27.50/4.06 cnf(d7, plain, sK8 = sK10 | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | ~young(sK10) | 'Ts0', inference(resolution, [status(thm)], [d6,c15])). % 27.50/4.06 cnf(d8, plain, sK7 = sK8 | 'Ts0' | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | ~young(sK10), inference(superposition, [status(thm)], [d7,c28])). % 27.50/4.06 cnf(d9, plain, sK7 != sK7 | 'Ts0' | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | ~young(sK10), inference(superposition, [status(thm)], [d8,c21])). % 27.50/4.06 cnf(d10, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | ~young(sK10), inference(equality_resolution, [status(thm)], [d9])). % 27.50/4.06 cnf(d11, plain, ~young(sK7) | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK8) | 'Ts0', inference(superposition, [status(thm)], [c28,d10])). % 27.50/4.06 cnf(d12, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | ~young(sK7) | 'Ts0', inference(resolution, [status(thm)], [d11,c27])). % 27.50/4.06 cnf(d13, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | ~man(sK10) | 'Ts0', inference(resolution, [status(thm)], [d12,c24])). % 27.50/4.06 cnf(d14, plain, ~man(sK7) | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK8) | 'Ts0', inference(superposition, [status(thm)], [c28,d13])). % 27.50/4.06 cnf(d15, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | ~man(sK7) | 'Ts0', inference(resolution, [status(thm)], [d14,c26])). % 27.50/4.06 cnf(d16, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | ~fellow(sK10) | 'Ts0', inference(resolution, [status(thm)], [d15,c23])). % 27.50/4.06 cnf(d17, plain, ~fellow(sK7) | 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK8) | 'Ts0', inference(superposition, [status(thm)], [c28,d16])). % 27.50/4.06 cnf(d18, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | ~fellow(sK7) | 'Ts0', inference(resolution, [status(thm)], [d17,c25])). % 27.50/4.06 cnf(d19, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | ~lonely(sK6) | 'Ts0', inference(resolution, [status(thm)], [d18,c22])). % 27.50/4.06 cnf(d20, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | ~way(sK6) | 'Ts0', inference(resolution, [status(thm)], [d19,c14])). % 27.50/4.06 cnf(d21, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~street(sK6) | 'Ts0', inference(resolution, [status(thm)], [d20,c13])). % 27.50/4.06 cnf(d22, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | 'Ts0', inference(resolution, [status(thm)], [d21,c12])). % 27.50/4.06 cnf(d23, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | 'Ts0', inference(resolution, [status(thm)], [d22,c11])). % 27.50/4.06 cnf(d24, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | 'Ts0', inference(resolution, [status(thm)], [d23,c10])). % 27.50/4.06 cnf(d25, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | ~car(sK5) | 'Ts0', inference(resolution, [status(thm)], [d24,c9])). % 27.50/4.06 cnf(d26, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | ~chevy(sK5) | 'Ts0', inference(resolution, [status(thm)], [d25,c8])). % 27.50/4.06 cnf(d27, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | ~event(sK4) | 'Ts0', inference(resolution, [status(thm)], [d26,c7])). % 27.50/4.06 cnf(d28, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | ~city(sK3) | 'Ts0', inference(resolution, [status(thm)], [d27,c6])). % 27.50/4.06 cnf(d29, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | ~hollywood(sK3) | 'Ts0', inference(resolution, [status(thm)], [d28,c5])). % 27.50/4.06 cnf(d30, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | ~front(sK9) | 'Ts0', inference(resolution, [status(thm)], [d29,c4])). % 27.50/4.06 cnf(d31, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | ~front(sK2) | 'Ts0', inference(resolution, [status(thm)], [d30,c20])). % 27.50/4.06 cnf(d32, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | ~furniture(sK9) | 'Ts0', inference(resolution, [status(thm)], [d31,c3])). % 27.50/4.06 cnf(d33, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | ~furniture(sK2) | 'Ts0', inference(resolution, [status(thm)], [d32,c19])). % 27.50/4.06 cnf(d34, plain, 'Ts0' | ~seat(sK2) | ~seat(sK9) | 'Ts0', inference(resolution, [status(thm)], [d33,c2])). % 27.50/4.06 cnf(d35, plain, 'Ts0' | ~seat(sK2) | 'Ts0', inference(resolution, [status(thm)], [d34,c18])). % 27.50/4.06 cnf(d36, plain, 'Ts0' | 'Ts0', inference(resolution, [status(thm)], [d35,c1])). % 27.50/4.06 cnf(d37, plain, ~'Ts1', inference(resolution, [status(thm)], [d36,c0])). % 27.50/4.06 cnf(d38, plain, barrel(sK24,sK25), inference(resolution, [status(thm)], [d37,c47])). % 27.50/4.06 cnf(d39, plain, down(sK24,sK26), inference(resolution, [status(thm)], [d37,c48])). % 27.50/4.06 cnf(d40, plain, in(sK24,sK23), inference(resolution, [status(thm)], [d37,c49])). % 27.50/4.06 cnf(d41, plain, sK28 = sK31, inference(resolution, [status(thm)], [d37,c62])). % 27.50/4.06 cnf(d42, plain, in(sK31,sK29), inference(resolution, [status(thm)], [d37,c63])). % 27.50/4.06 cnf(d43, plain, in(sK28,sK29), inference(demodulation, [status(thm)], [d42,d41])). % 27.50/4.06 cnf(d44, plain, in(sK27,sK22) | 'Ts1' | 'Ts1', inference(superposition, [status(thm)], [c60,c61])). % 27.50/4.06 cnf(d45, plain, in(sK27,sK22), inference(resolution, [status(thm)], [d37,d44])). % 27.50/4.06 cnf(d46, plain, X0 != X1 | X2 = X0 | 'Ts1' | ~seat(X3) | ~seat(X4) | ~furniture(X3) | ~furniture(X4) | ~front(X3) | ~front(X4) | ~hollywood(X5) | ~city(X5) | ~event(X6) | ~chevy(X7) | ~car(X7) | ~white(X7) | ~dirty(X7) | ~old(X7) | ~street(X8) | ~way(X8) | ~lonely(X8) | ~barrel(X6,X7) | ~down(X6,X8) | ~in(X6,X5) | ~in(X1,X3) | ~in(X2,X4) | ~fellow(X0) | ~fellow(X2) | ~man(X0) | ~man(X2) | ~young(X0) | ~young(X2), inference(equality_resolution, [status(thm)], [c64])). % 27.50/4.06 cnf(d47, plain, X0 = X1 | 'Ts1' | ~seat(X2) | ~seat(X3) | ~furniture(X2) | ~furniture(X3) | ~front(X2) | ~front(X3) | ~hollywood(X4) | ~city(X4) | ~event(X5) | ~chevy(X6) | ~car(X6) | ~white(X6) | ~dirty(X6) | ~old(X6) | ~street(X7) | ~way(X7) | ~lonely(X7) | ~barrel(X5,X6) | ~down(X5,X7) | ~in(X5,X4) | ~in(X0,X2) | ~in(X1,X3) | ~fellow(X0) | ~fellow(X1) | ~man(X0) | ~man(X1) | ~young(X0) | ~young(X1), inference(equality_resolution, [status(thm)], [d46])). % 27.50/4.06 cnf(d48, plain, X0 = X1 | ~seat(X2) | ~seat(X3) | ~furniture(X2) | ~furniture(X3) | ~front(X2) | ~front(X3) | ~hollywood(X4) | ~city(X4) | ~event(X5) | ~chevy(X6) | ~car(X6) | ~white(X6) | ~dirty(X6) | ~old(X6) | ~street(X7) | ~way(X7) | ~lonely(X7) | ~barrel(X5,X6) | ~down(X5,X7) | ~in(X5,X4) | ~in(X1,X2) | ~in(X0,X3) | ~fellow(X1) | ~fellow(X0) | ~man(X1) | ~man(X0) | ~young(X1) | ~young(X0), inference(resolution, [status(thm)], [d37,d47])). % 27.50/4.06 cnf(d49, plain, sK27 = X0 | ~seat(sK22) | ~seat(X1) | ~furniture(sK22) | ~furniture(X1) | ~front(sK22) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~fellow(sK27) | ~man(X0) | ~man(sK27) | ~young(X0) | ~young(sK27), inference(resolution, [status(thm)], [d48,d45])). % 27.50/4.06 cnf(d50, plain, front(sK22), inference(resolution, [status(thm)], [d37,c35])). % 27.50/4.06 cnf(d51, plain, sK27 = X0 | ~seat(X1) | ~seat(sK22) | ~furniture(X1) | ~furniture(sK22) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~fellow(sK27) | ~man(X0) | ~man(sK27) | ~young(X0) | ~young(sK27), inference(resolution, [status(thm)], [d50,d49])). % 27.50/4.06 cnf(d52, plain, furniture(sK22), inference(resolution, [status(thm)], [d37,c34])). % 27.50/4.06 cnf(d53, plain, sK27 = X0 | ~seat(X1) | ~seat(sK22) | ~furniture(X1) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~fellow(sK27) | ~man(X0) | ~man(sK27) | ~young(X0) | ~young(sK27), inference(resolution, [status(thm)], [d52,d51])). % 27.50/4.06 cnf(d54, plain, seat(sK22), inference(resolution, [status(thm)], [d37,c33])). % 27.50/4.06 cnf(d55, plain, sK27 = X0 | ~seat(X1) | ~furniture(X1) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~fellow(sK27) | ~man(X0) | ~man(sK27) | ~young(X0) | ~young(sK27), inference(resolution, [status(thm)], [d54,d53])). % 27.50/4.06 cnf(d56, plain, fellow(sK27), inference(resolution, [status(thm)], [d37,c54])). % 27.50/4.06 cnf(d57, plain, sK27 = X0 | ~seat(X1) | ~furniture(X1) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~man(X0) | ~man(sK27) | ~young(X0) | ~young(sK27), inference(resolution, [status(thm)], [d56,d55])). % 27.50/4.06 cnf(d58, plain, young(sK27), inference(resolution, [status(thm)], [d37,c56])). % 27.50/4.06 cnf(d59, plain, sK27 = X0 | ~seat(X1) | ~furniture(X1) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~man(X0) | ~man(sK27) | ~young(X0), inference(resolution, [status(thm)], [d58,d57])). % 27.50/4.06 cnf(d60, plain, man(sK27), inference(resolution, [status(thm)], [d37,c55])). % 27.50/4.06 cnf(d61, plain, sK27 = X0 | ~seat(X1) | ~furniture(X1) | ~front(X1) | ~hollywood(X2) | ~city(X2) | ~event(X3) | ~chevy(X4) | ~car(X4) | ~white(X4) | ~dirty(X4) | ~old(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~barrel(X3,X4) | ~down(X3,X5) | ~in(X3,X2) | ~in(X0,X1) | ~fellow(X0) | ~man(X0) | ~young(X0), inference(resolution, [status(thm)], [d60,d59])). % 27.50/4.06 cnf(d62, plain, sK27 = sK28 | ~seat(sK29) | ~furniture(sK29) | ~front(sK29) | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~fellow(sK28) | ~man(sK28) | ~young(sK28), inference(resolution, [status(thm)], [d61,d43])). % 27.50/4.06 cnf(d63, plain, fellow(sK28), inference(resolution, [status(thm)], [d37,c57])). % 27.50/4.06 cnf(d64, plain, sK27 = sK28 | ~seat(sK29) | ~furniture(sK29) | ~front(sK29) | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~man(sK28) | ~young(sK28), inference(resolution, [status(thm)], [d63,d62])). % 27.50/4.06 cnf(d65, plain, man(sK28), inference(resolution, [status(thm)], [d37,c58])). % 27.50/4.06 cnf(d66, plain, sK27 = sK28 | ~seat(sK29) | ~furniture(sK29) | ~front(sK29) | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~young(sK28), inference(resolution, [status(thm)], [d65,d64])). % 27.50/4.06 cnf(d67, plain, furniture(sK29), inference(resolution, [status(thm)], [d37,c51])). % 27.50/4.06 cnf(d68, plain, sK27 = sK28 | ~seat(sK29) | ~front(sK29) | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~young(sK28), inference(resolution, [status(thm)], [d67,d66])). % 27.50/4.06 cnf(d69, plain, front(sK29), inference(resolution, [status(thm)], [d37,c52])). % 27.50/4.06 cnf(d70, plain, sK27 = sK28 | ~seat(sK29) | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~young(sK28), inference(resolution, [status(thm)], [d69,d68])). % 27.50/4.06 cnf(d71, plain, seat(sK29), inference(resolution, [status(thm)], [d37,c50])). % 27.50/4.06 cnf(d72, plain, sK27 = sK28 | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0) | ~young(sK28), inference(resolution, [status(thm)], [d71,d70])). % 27.50/4.06 cnf(d73, plain, young(sK28), inference(resolution, [status(thm)], [d37,c59])). % 27.50/4.06 cnf(d74, plain, sK27 = sK28 | ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0), inference(resolution, [status(thm)], [d73,d72])). % 27.50/4.06 cnf(d75, plain, sK27 != sK28, inference(resolution, [status(thm)], [d37,c53])). % 27.50/4.06 cnf(d76, plain, ~hollywood(X0) | ~city(X0) | ~event(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~street(X3) | ~way(X3) | ~lonely(X3) | ~barrel(X1,X2) | ~down(X1,X3) | ~in(X1,X0), inference(resolution, [status(thm)], [d75,d74])). % 27.50/4.06 cnf(d77, plain, ~hollywood(sK23) | ~city(sK23) | ~event(sK24) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sK24,X0) | ~down(sK24,X1), inference(resolution, [status(thm)], [d76,d40])). % 27.50/4.06 cnf(d78, plain, event(sK24), inference(resolution, [status(thm)], [d37,c38])). % 27.50/4.06 cnf(d79, plain, ~hollywood(sK23) | ~city(sK23) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sK24,X0) | ~down(sK24,X1), inference(resolution, [status(thm)], [d78,d77])). % 27.50/4.06 cnf(d80, plain, city(sK23), inference(resolution, [status(thm)], [d37,c37])). % 27.50/4.06 cnf(d81, plain, ~hollywood(sK23) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sK24,X0) | ~down(sK24,X1), inference(resolution, [status(thm)], [d80,d79])). % 27.50/4.06 cnf(d82, plain, hollywood(sK23), inference(resolution, [status(thm)], [d37,c36])). % 27.50/4.06 cnf(d83, plain, ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sK24,X0) | ~down(sK24,X1), inference(resolution, [status(thm)], [d82,d81])). % 27.50/4.06 cnf(d84, plain, ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(sK26) | ~way(sK26) | ~lonely(sK26) | ~barrel(sK24,X0), inference(resolution, [status(thm)], [d83,d39])). % 27.50/4.06 cnf(d85, plain, way(sK26), inference(resolution, [status(thm)], [d37,c45])). % 27.50/4.06 cnf(d86, plain, ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(sK26) | ~lonely(sK26) | ~barrel(sK24,X0), inference(resolution, [status(thm)], [d85,d84])). % 27.50/4.06 cnf(d87, plain, street(sK26), inference(resolution, [status(thm)], [d37,c44])). % 27.50/4.06 cnf(d88, plain, ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~lonely(sK26) | ~barrel(sK24,X0), inference(resolution, [status(thm)], [d87,d86])). % 27.50/4.06 cnf(d89, plain, lonely(sK26), inference(resolution, [status(thm)], [d37,c46])). % 27.50/4.06 cnf(d90, plain, ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sK24,X0), inference(resolution, [status(thm)], [d89,d88])). % 27.50/4.06 cnf(d91, plain, ~chevy(sK25) | ~car(sK25) | ~white(sK25) | ~dirty(sK25) | ~old(sK25), inference(resolution, [status(thm)], [d90,d38])). % 27.50/4.06 cnf(d92, plain, old(sK25), inference(resolution, [status(thm)], [d37,c43])). % 27.50/4.06 cnf(d93, plain, ~chevy(sK25) | ~car(sK25) | ~white(sK25) | ~dirty(sK25), inference(resolution, [status(thm)], [d92,d91])). % 27.50/4.06 cnf(d94, plain, dirty(sK25), inference(resolution, [status(thm)], [d37,c42])). % 27.50/4.06 cnf(d95, plain, ~chevy(sK25) | ~car(sK25) | ~white(sK25), inference(resolution, [status(thm)], [d94,d93])). % 27.50/4.06 cnf(d96, plain, white(sK25), inference(resolution, [status(thm)], [d37,c41])). % 27.50/4.06 cnf(d97, plain, ~chevy(sK25) | ~car(sK25), inference(resolution, [status(thm)], [d96,d95])). % 27.50/4.06 cnf(d98, plain, car(sK25), inference(resolution, [status(thm)], [d37,c40])). % 27.50/4.06 cnf(d99, plain, ~chevy(sK25), inference(resolution, [status(thm)], [d98,d97])). % 27.50/4.06 cnf(d100, plain, chevy(sK25), inference(resolution, [status(thm)], [d37,c39])). % 27.50/4.06 cnf(d101, plain, $false, inference(resolution, [status(thm)], [d100,d99])). % 27.50/4.06 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------