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