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