%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NLP009+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 : n026.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 21.97s 10.42s % Output : CNFRefutation 21.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP009+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.12/5.39 % Computer : n026.cluster.edu % 0.12/5.39 % Model : x86_64 x86_64 % 0.12/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/5.39 % Memory : 8046.5625MB % 0.12/5.39 % OS : Linux 6.8.0-71-generic % 0.12/5.39 % CPULimit : 300 % 0.12/5.39 % WCLimit : 300 % 0.12/5.39 % DateTime : Sat Sep 26 00:26:00 UTC 2026 % 0.15/5.40 % CPUTime : % 0.15/5.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 21.97/10.42 % SZS status Theorem for theBenchmark.p % 21.97/10.42 % SZS output start CNFRefutation for theBenchmark.p % 21.97/10.42 fof(co1, conjecture, ((? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ((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) & (seat(X6) & (furniture(X6) & (front(X6) & (X4 != X5 & (fellow(X4) & (man(X4) & (young(X4) & (fellow(X5) & (man(X5) & (young(X5) & (X4 = X7 & (in(X7,X6) & (X5 = X8 & in(X8,X6))))))))))))))))))))))))))))) => ? [X9] : ? [X10] : ? [X11] : ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ((hollywood(X9) & (city(X9) & (event(X10) & (chevy(X11) & (car(X11) & (white(X11) & (dirty(X11) & (old(X11) & (street(X12) & (way(X12) & (lonely(X12) & (barrel(X10,X11) & (down(X10,X12) & (in(X10,X9) & (seat(X15) & (furniture(X15) & (front(X15) & (X13 != X14 & (fellow(X13) & (man(X13) & (young(X13) & (fellow(X14) & (man(X14) & (young(X14) & (X13 = X16 & (in(X16,X15) & (X14 = X17 & in(X17,X15)))))))))))))))))))))))))))))) & (? [X18] : ? [X19] : ? [X20] : ? [X21] : ? [X22] : ? [X23] : ? [X24] : ? [X25] : ? [X26] : ((hollywood(X18) & (city(X18) & (event(X19) & (chevy(X20) & (car(X20) & (white(X20) & (dirty(X20) & (old(X20) & (street(X21) & (way(X21) & (lonely(X21) & (barrel(X19,X20) & (down(X19,X21) & (in(X19,X18) & (seat(X24) & (furniture(X24) & (front(X24) & (X22 != X23 & (fellow(X22) & (man(X22) & (young(X22) & (fellow(X23) & (man(X23) & (young(X23) & (X22 = X25 & (in(X25,X24) & (X23 = X26 & in(X26,X24))))))))))))))))))))))))))))) => ? [X27] : ? [X28] : ? [X29] : ? [X30] : ? [X31] : ? [X32] : ? [X33] : ? [X34] : ? [X35] : ((hollywood(X27) & (city(X27) & (event(X28) & (street(X29) & (way(X29) & (lonely(X29) & (chevy(X30) & (car(X30) & (white(X30) & (dirty(X30) & (old(X30) & (barrel(X28,X30) & (down(X28,X29) & (in(X28,X27) & (seat(X33) & (furniture(X33) & (front(X33) & (X31 != X32 & (fellow(X31) & (man(X31) & (young(X31) & (fellow(X32) & (man(X32) & (young(X32) & (X31 = X34 & (in(X34,X33) & (X32 = X35 & in(X35,X33)))))))))))))))))))))))))))))))). % 21.97/10.42 fof(negated_conjecture, negated_conjecture, ~(((? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ((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) & (seat(X6) & (furniture(X6) & (front(X6) & (X4 != X5 & (fellow(X4) & (man(X4) & (young(X4) & (fellow(X5) & (man(X5) & (young(X5) & (X4 = X7 & (in(X7,X6) & (X5 = X8 & in(X8,X6))))))))))))))))))))))))))))) => ? [X9] : ? [X10] : ? [X11] : ? [X12] : ? [X13] : ? [X14] : ? [X15] : ? [X16] : ? [X17] : ((hollywood(X9) & (city(X9) & (event(X10) & (chevy(X11) & (car(X11) & (white(X11) & (dirty(X11) & (old(X11) & (street(X12) & (way(X12) & (lonely(X12) & (barrel(X10,X11) & (down(X10,X12) & (in(X10,X9) & (seat(X15) & (furniture(X15) & (front(X15) & (X13 != X14 & (fellow(X13) & (man(X13) & (young(X13) & (fellow(X14) & (man(X14) & (young(X14) & (X13 = X16 & (in(X16,X15) & (X14 = X17 & in(X17,X15)))))))))))))))))))))))))))))) & (? [X18] : ? [X19] : ? [X20] : ? [X21] : ? [X22] : ? [X23] : ? [X24] : ? [X25] : ? [X26] : ((hollywood(X18) & (city(X18) & (event(X19) & (chevy(X20) & (car(X20) & (white(X20) & (dirty(X20) & (old(X20) & (street(X21) & (way(X21) & (lonely(X21) & (barrel(X19,X20) & (down(X19,X21) & (in(X19,X18) & (seat(X24) & (furniture(X24) & (front(X24) & (X22 != X23 & (fellow(X22) & (man(X22) & (young(X22) & (fellow(X23) & (man(X23) & (young(X23) & (X22 = X25 & (in(X25,X24) & (X23 = X26 & in(X26,X24))))))))))))))))))))))))))))) => ? [X27] : ? [X28] : ? [X29] : ? [X30] : ? [X31] : ? [X32] : ? [X33] : ? [X34] : ? [X35] : ((hollywood(X27) & (city(X27) & (event(X28) & (street(X29) & (way(X29) & (lonely(X29) & (chevy(X30) & (car(X30) & (white(X30) & (dirty(X30) & (old(X30) & (barrel(X28,X30) & (down(X28,X29) & (in(X28,X27) & (seat(X33) & (furniture(X33) & (front(X33) & (X31 != X32 & (fellow(X31) & (man(X31) & (young(X31) & (fellow(X32) & (man(X32) & (young(X32) & (X31 = X34 & (in(X34,X33) & (X32 = X35 & in(X35,X33)))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 21.97/10.42 cnf(c0, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c1, plain, X0 | hollywood(sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c2, plain, X0 | city(sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c3, plain, X0 | event(sK3), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c4, plain, X0 | street(sK4), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c5, plain, X0 | way(sK4), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c6, plain, X0 | lonely(sK4), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c7, plain, X0 | chevy(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c8, plain, X0 | car(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c9, plain, X0 | white(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c10, plain, X0 | dirty(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c11, plain, X0 | old(sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c12, plain, X0 | barrel(sK3,sK5), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c13, plain, X0 | down(sK3,sK4), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c14, plain, X0 | in(sK3,sK2), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c15, plain, X0 | seat(sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c16, plain, X0 | furniture(sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c17, plain, X0 | front(sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c18, plain, X0 | sK6 != sK7, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c19, plain, X0 | fellow(sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c20, plain, X0 | man(sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c21, plain, X0 | young(sK6), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c22, plain, X0 | fellow(sK7), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c23, plain, X0 | man(sK7), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c24, plain, X0 | young(sK7), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c25, plain, X0 | sK6 = sK9, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c26, plain, X0 | in(sK9,sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c27, plain, X0 | sK7 = sK10, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c28, plain, X0 | in(sK10,sK8), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c29, plain, ~street(X0) | ~car(X1) | ~way(X0) | ~fellow(X2) | ~in(X3,X4) | X2 = X5 | ~old(X1) | ~man(X2) | ~young(X5) | ~chevy(X1) | ~fellow(X5) | ~front(X6) | X7 | ~event(X3) | ~dirty(X1) | ~furniture(X6) | ~barrel(X3,X1) | X5 != X8 | X2 != X9 | ~seat(X6) | ~down(X3,X0) | ~lonely(X0) | ~in(X9,X6) | ~city(X4) | ~white(X1) | ~man(X5) | ~in(X8,X6) | ~young(X2) | ~hollywood(X4), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c30, plain, X0 | hollywood(sK20), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c31, plain, X0 | city(sK20), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c32, plain, X0 | event(sK21), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c33, plain, X0 | chevy(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c34, plain, X0 | car(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c35, plain, X0 | white(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c36, plain, X0 | dirty(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c37, plain, X0 | old(sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c38, plain, X0 | street(sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c39, plain, X0 | way(sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c40, plain, X0 | lonely(sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c41, plain, X0 | barrel(sK21,sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c42, plain, X0 | down(sK21,sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c43, plain, X0 | in(sK21,sK20), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c44, plain, X0 | seat(sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c45, plain, X0 | furniture(sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c46, plain, X0 | front(sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c47, plain, X0 | sK24 != sK25, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c48, plain, X0 | fellow(sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c49, plain, X0 | man(sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c50, plain, X0 | young(sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c51, plain, X0 | fellow(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c52, plain, X0 | man(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c53, plain, X0 | young(sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c54, plain, X0 | sK24 = sK27, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c55, plain, X0 | in(sK27,sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c56, plain, X0 | sK25 = sK28, inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c57, plain, X0 | in(sK28,sK26), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(c58, plain, ~in(X0,X1) | ~city(X2) | ~dirty(X3) | X4 | ~street(X5) | ~fellow(X6) | ~young(X6) | ~furniture(X1) | X7 != X8 | ~white(X3) | ~fellow(X7) | ~in(X8,X1) | ~event(X9) | ~man(X6) | ~in(X9,X2) | ~way(X5) | X6 != X0 | ~lonely(X5) | ~seat(X1) | ~man(X7) | ~barrel(X9,X3) | ~down(X9,X5) | X7 = X6 | ~old(X3) | ~hollywood(X2) | ~car(X3) | ~chevy(X3) | ~young(X7) | ~front(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 21.97/10.42 cnf(d0, plain, sK25 = sK28 | ~'Ts0', inference(resolution, [status(thm)], [c56,c0])). % 21.97/10.42 cnf(d1, plain, sK24 = sK27 | ~'Ts0', inference(resolution, [status(thm)], [c54,c0])). % 21.97/10.42 cnf(d2, plain, sK24 = sK27 | sK6 = sK9, inference(resolution, [status(thm)], [d1,c25])). % 21.97/10.42 cnf(d3, plain, sK25 = sK28 | sK6 = sK9, inference(resolution, [status(thm)], [d0,c25])). % 21.97/10.42 cnf(d4, plain, X0 != X1 | X0 = X2 | 'Ts1' | ~hollywood(X3) | ~city(X3) | ~event(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~chevy(X6) | ~car(X6) | ~white(X6) | ~dirty(X6) | ~old(X6) | ~barrel(X4,X6) | ~down(X4,X5) | ~in(X1,X7) | ~in(X2,X7) | ~in(X4,X3) | ~seat(X7) | ~furniture(X7) | ~front(X7) | ~fellow(X0) | ~fellow(X2) | ~man(X0) | ~man(X2) | ~young(X0) | ~young(X2), inference(equality_resolution, [status(thm)], [c58])). % 21.97/10.42 cnf(d5, plain, X0 = X1 | 'Ts1' | ~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(X1,X6) | ~in(X0,X6) | ~seat(X6) | ~furniture(X6) | ~front(X6) | ~fellow(X1) | ~fellow(X0) | ~man(X1) | ~man(X0) | ~young(X1) | ~young(X0), inference(equality_resolution, [status(thm)], [d4])). % 21.97/10.42 cnf(d6, plain, sK27 = X0 | 'Ts1' | ~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) | ~in(X0,sK26) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(X0) | ~fellow(sK27) | ~man(X0) | ~man(sK27) | ~young(X0) | ~young(sK27) | 'Ts1', inference(resolution, [status(thm)], [d5,c55])). % 21.97/10.42 cnf(d7, plain, sK27 = sK28 | 'Ts1' | ~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) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK28) | ~fellow(sK27) | ~man(sK28) | ~man(sK27) | ~young(sK28) | ~young(sK27) | 'Ts1', inference(resolution, [status(thm)], [d6,c57])). % 21.97/10.42 cnf(d8, plain, sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(X0) | ~way(X0) | ~lonely(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~barrel(sK21,X1) | ~down(sK21,X0) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28) | 'Ts1', inference(resolution, [status(thm)], [d7,c43])). % 21.97/10.42 cnf(d9, plain, sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sK21,X0) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28) | 'Ts1', inference(resolution, [status(thm)], [d8,c42])). % 21.97/10.42 cnf(d10, plain, sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28) | 'Ts1', inference(resolution, [status(thm)], [d9,c41])). % 21.97/10.42 cnf(d11, plain, ~young(sK25) | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | sK6 = sK9, inference(superposition, [status(thm)], [d3,d10])). % 21.97/10.42 cnf(d12, plain, ~young(sK24) | sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK25) | sK6 = sK9, inference(superposition, [status(thm)], [d2,d11])). % 21.97/10.42 cnf(d13, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK24) | 'Ts1', inference(resolution, [status(thm)], [d12,c53])). % 21.97/10.42 cnf(d14, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | 'Ts1', inference(resolution, [status(thm)], [d13,c50])). % 21.97/10.42 cnf(d15, plain, ~man(sK25) | sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | sK6 = sK9, inference(superposition, [status(thm)], [d3,d14])). % 21.97/10.42 cnf(d16, plain, ~man(sK24) | sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK25) | sK6 = sK9, inference(superposition, [status(thm)], [d2,d15])). % 21.97/10.42 cnf(d17, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK24) | 'Ts1', inference(resolution, [status(thm)], [d16,c52])). % 21.97/10.42 cnf(d18, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | 'Ts1', inference(resolution, [status(thm)], [d17,c49])). % 21.97/10.42 cnf(d19, plain, ~fellow(sK25) | sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | sK6 = sK9, inference(superposition, [status(thm)], [d3,d18])). % 21.97/10.42 cnf(d20, plain, ~fellow(sK24) | sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK25) | sK6 = sK9, inference(superposition, [status(thm)], [d2,d19])). % 21.97/10.42 cnf(d21, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | 'Ts1', inference(resolution, [status(thm)], [d20,c51])). % 21.97/10.42 cnf(d22, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | 'Ts1', inference(resolution, [status(thm)], [d21,c48])). % 21.97/10.42 cnf(d23, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | 'Ts1', inference(resolution, [status(thm)], [d22,c46])). % 21.97/10.42 cnf(d24, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | 'Ts1', inference(resolution, [status(thm)], [d23,c45])). % 21.97/10.42 cnf(d25, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | 'Ts1', inference(resolution, [status(thm)], [d24,c44])). % 21.97/10.42 cnf(d26, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | 'Ts1', inference(resolution, [status(thm)], [d25,c37])). % 21.97/10.42 cnf(d27, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | 'Ts1', inference(resolution, [status(thm)], [d26,c36])). % 21.97/10.42 cnf(d28, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | 'Ts1', inference(resolution, [status(thm)], [d27,c35])). % 21.97/10.42 cnf(d29, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | 'Ts1', inference(resolution, [status(thm)], [d28,c34])). % 21.97/10.42 cnf(d30, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | 'Ts1', inference(resolution, [status(thm)], [d29,c33])). % 21.97/10.42 cnf(d31, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | 'Ts1', inference(resolution, [status(thm)], [d30,c40])). % 21.97/10.42 cnf(d32, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | 'Ts1', inference(resolution, [status(thm)], [d31,c39])). % 21.97/10.42 cnf(d33, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | 'Ts1', inference(resolution, [status(thm)], [d32,c38])). % 21.97/10.42 cnf(d34, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | 'Ts1', inference(resolution, [status(thm)], [d33,c32])). % 21.97/10.42 cnf(d35, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | 'Ts1', inference(resolution, [status(thm)], [d34,c31])). % 21.97/10.42 cnf(d36, plain, sK6 = sK9 | sK27 = sK28 | 'Ts1' | 'Ts1', inference(resolution, [status(thm)], [d35,c30])). % 21.97/10.42 cnf(d37, plain, sK6 = sK9 | sK27 = sK28 | ~'Ts0', inference(resolution, [status(thm)], [d36,c0])). % 21.97/10.42 cnf(d38, plain, sK6 = sK9 | sK27 = sK28 | sK6 = sK9, inference(resolution, [status(thm)], [d37,c25])). % 21.97/10.42 cnf(d39, plain, sK25 = sK27 | sK6 = sK9 | sK6 = sK9, inference(superposition, [status(thm)], [d38,d3])). % 21.97/10.42 cnf(d40, plain, sK24 = sK25 | sK6 = sK9 | sK6 = sK9, inference(superposition, [status(thm)], [d39,d2])). % 21.97/10.42 cnf(d41, plain, sK24 = sK27 | sK7 = sK10, inference(resolution, [status(thm)], [d1,c27])). % 21.97/10.42 cnf(d42, plain, sK25 = sK28 | sK7 = sK10, inference(resolution, [status(thm)], [d0,c27])). % 21.97/10.42 cnf(d43, plain, ~young(sK25) | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | sK7 = sK10, inference(superposition, [status(thm)], [d42,d10])). % 21.97/10.42 cnf(d44, plain, ~young(sK24) | sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK25) | sK7 = sK10, inference(superposition, [status(thm)], [d41,d43])). % 21.97/10.42 cnf(d45, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK24) | 'Ts1', inference(resolution, [status(thm)], [d44,c53])). % 21.97/10.42 cnf(d46, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | 'Ts1', inference(resolution, [status(thm)], [d45,c50])). % 21.97/10.42 cnf(d47, plain, ~man(sK25) | sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | sK7 = sK10, inference(superposition, [status(thm)], [d42,d46])). % 21.97/10.42 cnf(d48, plain, ~man(sK24) | sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK25) | sK7 = sK10, inference(superposition, [status(thm)], [d41,d47])). % 21.97/10.42 cnf(d49, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK24) | 'Ts1', inference(resolution, [status(thm)], [d48,c52])). % 21.97/10.42 cnf(d50, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | 'Ts1', inference(resolution, [status(thm)], [d49,c49])). % 21.97/10.42 cnf(d51, plain, ~fellow(sK25) | sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | sK7 = sK10, inference(superposition, [status(thm)], [d42,d50])). % 21.97/10.42 cnf(d52, plain, ~fellow(sK24) | sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK25) | sK7 = sK10, inference(superposition, [status(thm)], [d41,d51])). % 21.97/10.42 cnf(d53, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | 'Ts1', inference(resolution, [status(thm)], [d52,c51])). % 21.97/10.42 cnf(d54, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | 'Ts1', inference(resolution, [status(thm)], [d53,c48])). % 21.97/10.42 cnf(d55, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | 'Ts1', inference(resolution, [status(thm)], [d54,c46])). % 21.97/10.42 cnf(d56, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | 'Ts1', inference(resolution, [status(thm)], [d55,c45])). % 21.97/10.42 cnf(d57, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | 'Ts1', inference(resolution, [status(thm)], [d56,c44])). % 21.97/10.42 cnf(d58, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | 'Ts1', inference(resolution, [status(thm)], [d57,c37])). % 21.97/10.42 cnf(d59, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | 'Ts1', inference(resolution, [status(thm)], [d58,c36])). % 21.97/10.42 cnf(d60, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | 'Ts1', inference(resolution, [status(thm)], [d59,c35])). % 21.97/10.42 cnf(d61, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | 'Ts1', inference(resolution, [status(thm)], [d60,c34])). % 21.97/10.42 cnf(d62, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | 'Ts1', inference(resolution, [status(thm)], [d61,c33])). % 21.97/10.42 cnf(d63, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | 'Ts1', inference(resolution, [status(thm)], [d62,c40])). % 21.97/10.42 cnf(d64, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | 'Ts1', inference(resolution, [status(thm)], [d63,c39])). % 21.97/10.42 cnf(d65, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | 'Ts1', inference(resolution, [status(thm)], [d64,c38])). % 21.97/10.42 cnf(d66, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | 'Ts1', inference(resolution, [status(thm)], [d65,c32])). % 21.97/10.42 cnf(d67, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | 'Ts1', inference(resolution, [status(thm)], [d66,c31])). % 21.97/10.42 cnf(d68, plain, sK7 = sK10 | sK27 = sK28 | 'Ts1' | 'Ts1', inference(resolution, [status(thm)], [d67,c30])). % 21.97/10.42 cnf(d69, plain, sK7 = sK10 | sK27 = sK28 | ~'Ts0', inference(resolution, [status(thm)], [d68,c0])). % 21.97/10.42 cnf(d70, plain, sK7 = sK10 | sK27 = sK28 | sK7 = sK10, inference(resolution, [status(thm)], [d69,c27])). % 21.97/10.42 cnf(d71, plain, sK25 = sK27 | sK7 = sK10 | sK7 = sK10, inference(superposition, [status(thm)], [d70,d42])). % 21.97/10.42 cnf(d72, plain, sK24 = sK25 | sK7 = sK10 | sK7 = sK10, inference(superposition, [status(thm)], [d71,d41])). % 21.97/10.42 cnf(d73, plain, X0 != X1 | X0 = X2 | 'Ts0' | ~hollywood(X3) | ~city(X3) | ~event(X4) | ~street(X5) | ~way(X5) | ~lonely(X5) | ~chevy(X6) | ~car(X6) | ~white(X6) | ~dirty(X6) | ~old(X6) | ~barrel(X4,X6) | ~down(X4,X5) | ~in(X4,X3) | ~in(X1,X7) | ~in(X2,X7) | ~seat(X7) | ~furniture(X7) | ~front(X7) | ~fellow(X0) | ~fellow(X2) | ~man(X0) | ~man(X2) | ~young(X0) | ~young(X2), inference(equality_resolution, [status(thm)], [c29])). % 21.97/10.42 cnf(d74, plain, X0 = X1 | 'Ts0' | ~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(X1,X6) | ~in(X0,X6) | ~seat(X6) | ~furniture(X6) | ~front(X6) | ~fellow(X1) | ~fellow(X0) | ~man(X1) | ~man(X0) | ~young(X1) | ~young(X0), inference(equality_resolution, [status(thm)], [d73])). % 21.97/10.42 cnf(d75, plain, sK9 = X0 | 'Ts0' | ~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) | ~in(X0,sK8) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(X0) | ~fellow(sK9) | ~man(X0) | ~man(sK9) | ~young(X0) | ~young(sK9) | 'Ts0', inference(resolution, [status(thm)], [d74,c26])). % 21.97/10.42 cnf(d76, plain, sK9 = sK10 | 'Ts0' | ~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) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK10) | ~fellow(sK9) | ~man(sK10) | ~man(sK9) | ~young(sK10) | ~young(sK9) | 'Ts0', inference(resolution, [status(thm)], [d75,c28])). % 21.97/10.42 cnf(d77, plain, sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(X0) | ~way(X0) | ~lonely(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~barrel(sK3,X1) | ~down(sK3,X0) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK9) | ~young(sK10) | 'Ts0', inference(resolution, [status(thm)], [d76,c14])). % 21.97/10.42 cnf(d78, plain, sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sK3,X0) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK9) | ~young(sK10) | 'Ts0', inference(resolution, [status(thm)], [d77,c13])). % 21.97/10.42 cnf(d79, plain, sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK9) | ~young(sK10) | 'Ts0', inference(resolution, [status(thm)], [d78,c12])). % 21.97/10.42 cnf(d80, plain, ~young(sK7) | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK9) | sK24 = sK25, inference(superposition, [status(thm)], [d72,d79])). % 21.97/10.42 cnf(d81, plain, ~young(sK6) | sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK7) | sK24 = sK25, inference(superposition, [status(thm)], [d40,d80])). % 21.97/10.42 cnf(d82, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK6) | 'Ts0', inference(resolution, [status(thm)], [d81,c24])). % 21.97/10.42 cnf(d83, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | 'Ts0', inference(resolution, [status(thm)], [d82,c21])). % 21.97/10.42 cnf(d84, plain, ~man(sK7) | sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | sK24 = sK25, inference(superposition, [status(thm)], [d72,d83])). % 21.97/10.42 cnf(d85, plain, ~man(sK6) | sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK7) | sK24 = sK25, inference(superposition, [status(thm)], [d40,d84])). % 21.97/10.42 cnf(d86, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK6) | 'Ts0', inference(resolution, [status(thm)], [d85,c23])). % 21.97/10.42 cnf(d87, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | 'Ts0', inference(resolution, [status(thm)], [d86,c20])). % 21.97/10.42 cnf(d88, plain, ~fellow(sK7) | sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | sK24 = sK25, inference(superposition, [status(thm)], [d72,d87])). % 21.97/10.42 cnf(d89, plain, ~fellow(sK6) | sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK7) | sK24 = sK25, inference(superposition, [status(thm)], [d40,d88])). % 21.97/10.42 cnf(d90, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK6) | 'Ts0', inference(resolution, [status(thm)], [d89,c22])). % 21.97/10.42 cnf(d91, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | 'Ts0', inference(resolution, [status(thm)], [d90,c19])). % 21.97/10.42 cnf(d92, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | 'Ts0', inference(resolution, [status(thm)], [d91,c17])). % 21.97/10.42 cnf(d93, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | 'Ts0', inference(resolution, [status(thm)], [d92,c16])). % 21.97/10.42 cnf(d94, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | 'Ts0', inference(resolution, [status(thm)], [d93,c15])). % 21.97/10.42 cnf(d95, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | 'Ts0', inference(resolution, [status(thm)], [d94,c11])). % 21.97/10.42 cnf(d96, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | 'Ts0', inference(resolution, [status(thm)], [d95,c10])). % 21.97/10.42 cnf(d97, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | 'Ts0', inference(resolution, [status(thm)], [d96,c9])). % 21.97/10.42 cnf(d98, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | 'Ts0', inference(resolution, [status(thm)], [d97,c8])). % 21.97/10.42 cnf(d99, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | 'Ts0', inference(resolution, [status(thm)], [d98,c7])). % 21.97/10.42 cnf(d100, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | 'Ts0', inference(resolution, [status(thm)], [d99,c6])). % 21.97/10.42 cnf(d101, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | 'Ts0', inference(resolution, [status(thm)], [d100,c5])). % 21.97/10.42 cnf(d102, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | 'Ts0', inference(resolution, [status(thm)], [d101,c4])). % 21.97/10.42 cnf(d103, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | 'Ts0', inference(resolution, [status(thm)], [d102,c3])). % 21.97/10.42 cnf(d104, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | ~hollywood(sK2) | 'Ts0', inference(resolution, [status(thm)], [d103,c2])). % 21.97/10.42 cnf(d105, plain, sK9 = sK10 | sK24 = sK25 | 'Ts0' | 'Ts0', inference(resolution, [status(thm)], [d104,c1])). % 21.97/10.42 cnf(d106, plain, sK9 = sK10 | sK24 = sK25 | sK24 = sK27, inference(resolution, [status(thm)], [d105,d1])). % 21.97/10.42 cnf(d107, plain, sK9 = sK10 | sK24 = sK25 | sK25 = sK28, inference(resolution, [status(thm)], [d105,d0])). % 21.97/10.42 cnf(d108, plain, ~young(sK25) | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d107,d10])). % 21.97/10.42 cnf(d109, plain, ~young(sK24) | sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK25) | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d106,d108])). % 21.97/10.42 cnf(d110, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK24) | 'Ts1', inference(resolution, [status(thm)], [d109,c53])). % 21.97/10.42 cnf(d111, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | 'Ts1', inference(resolution, [status(thm)], [d110,c50])). % 21.97/10.42 cnf(d112, plain, ~man(sK25) | sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d107,d111])). % 21.97/10.42 cnf(d113, plain, ~man(sK24) | sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK25) | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d106,d112])). % 21.97/10.42 cnf(d114, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK24) | 'Ts1', inference(resolution, [status(thm)], [d113,c52])). % 21.97/10.42 cnf(d115, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | 'Ts1', inference(resolution, [status(thm)], [d114,c49])). % 21.97/10.42 cnf(d116, plain, ~fellow(sK25) | sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d107,d115])). % 21.97/10.42 cnf(d117, plain, ~fellow(sK24) | sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK25) | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d106,d116])). % 21.97/10.42 cnf(d118, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | 'Ts1', inference(resolution, [status(thm)], [d117,c51])). % 21.97/10.42 cnf(d119, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | 'Ts1', inference(resolution, [status(thm)], [d118,c48])). % 21.97/10.42 cnf(d120, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | 'Ts1', inference(resolution, [status(thm)], [d119,c46])). % 21.97/10.42 cnf(d121, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | 'Ts1', inference(resolution, [status(thm)], [d120,c45])). % 21.97/10.42 cnf(d122, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | 'Ts1', inference(resolution, [status(thm)], [d121,c44])). % 21.97/10.42 cnf(d123, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | 'Ts1', inference(resolution, [status(thm)], [d122,c37])). % 21.97/10.42 cnf(d124, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | 'Ts1', inference(resolution, [status(thm)], [d123,c36])). % 21.97/10.42 cnf(d125, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | 'Ts1', inference(resolution, [status(thm)], [d124,c35])). % 21.97/10.42 cnf(d126, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | 'Ts1', inference(resolution, [status(thm)], [d125,c34])). % 21.97/10.42 cnf(d127, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | 'Ts1', inference(resolution, [status(thm)], [d126,c33])). % 21.97/10.42 cnf(d128, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | 'Ts1', inference(resolution, [status(thm)], [d127,c40])). % 21.97/10.42 cnf(d129, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | 'Ts1', inference(resolution, [status(thm)], [d128,c39])). % 21.97/10.42 cnf(d130, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | 'Ts1', inference(resolution, [status(thm)], [d129,c38])). % 21.97/10.42 cnf(d131, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | ~city(sK20) | 'Ts1', inference(resolution, [status(thm)], [d130,c32])). % 21.97/10.42 cnf(d132, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | ~hollywood(sK20) | 'Ts1', inference(resolution, [status(thm)], [d131,c31])). % 21.97/10.42 cnf(d133, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | 'Ts1' | 'Ts1', inference(resolution, [status(thm)], [d132,c30])). % 21.97/10.42 cnf(d134, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | ~'Ts0', inference(resolution, [status(thm)], [d133,c0])). % 21.97/10.42 cnf(d135, plain, sK9 = sK10 | sK24 = sK25 | sK27 = sK28 | sK9 = sK10 | sK24 = sK25, inference(resolution, [status(thm)], [d134,d105])). % 21.97/10.42 cnf(d136, plain, sK25 = sK27 | sK9 = sK10 | sK24 = sK25 | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d135,d107])). % 21.97/10.42 cnf(d137, plain, sK24 = sK25 | sK9 = sK10 | sK24 = sK25 | sK9 = sK10 | sK24 = sK25, inference(superposition, [status(thm)], [d136,d106])). % 21.97/10.42 cnf(d138, plain, sK7 = sK9 | sK24 = sK25 | sK24 = sK25, inference(superposition, [status(thm)], [d137,d72])). % 21.97/10.42 cnf(d139, plain, sK6 = sK7 | sK24 = sK25 | sK24 = sK25, inference(superposition, [status(thm)], [d138,d40])). % 21.97/10.42 cnf(d140, plain, sK24 != sK24 | 'Ts1' | sK6 = sK7, inference(superposition, [status(thm)], [d139,c47])). % 21.97/10.42 cnf(d141, plain, sK6 = sK7 | 'Ts1', inference(equality_resolution, [status(thm)], [d140])). % 21.97/10.42 cnf(d142, plain, sK6 = sK7 | ~'Ts0', inference(resolution, [status(thm)], [d141,c0])). % 21.97/10.42 cnf(d143, plain, sK6 = sK7 | sK6 = sK9, inference(resolution, [status(thm)], [d142,c25])). % 21.97/10.42 cnf(d144, plain, sK6 = sK7 | sK7 = sK10, inference(resolution, [status(thm)], [d142,c27])). % 21.97/10.42 cnf(d145, plain, ~young(sK7) | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK9) | sK6 = sK7, inference(superposition, [status(thm)], [d144,d79])). % 21.97/10.42 cnf(d146, plain, ~young(sK6) | sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK7) | sK6 = sK7, inference(superposition, [status(thm)], [d143,d145])). % 21.97/10.42 cnf(d147, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | ~young(sK6) | 'Ts0', inference(resolution, [status(thm)], [d146,c24])). % 21.97/10.42 cnf(d148, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | ~man(sK10) | 'Ts0', inference(resolution, [status(thm)], [d147,c21])). % 21.97/10.42 cnf(d149, plain, ~man(sK7) | sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK9) | sK6 = sK7, inference(superposition, [status(thm)], [d144,d148])). % 21.97/10.42 cnf(d150, plain, ~man(sK6) | sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK7) | sK6 = sK7, inference(superposition, [status(thm)], [d143,d149])). % 21.97/10.42 cnf(d151, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | ~man(sK6) | 'Ts0', inference(resolution, [status(thm)], [d150,c23])). % 21.97/10.42 cnf(d152, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | ~fellow(sK10) | 'Ts0', inference(resolution, [status(thm)], [d151,c20])). % 21.97/10.42 cnf(d153, plain, ~fellow(sK7) | sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK9) | sK6 = sK7, inference(superposition, [status(thm)], [d144,d152])). % 21.97/10.42 cnf(d154, plain, ~fellow(sK6) | sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK7) | sK6 = sK7, inference(superposition, [status(thm)], [d143,d153])). % 21.97/10.42 cnf(d155, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | ~fellow(sK6) | 'Ts0', inference(resolution, [status(thm)], [d154,c22])). % 21.97/10.42 cnf(d156, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | ~front(sK8) | 'Ts0', inference(resolution, [status(thm)], [d155,c19])). % 21.97/10.42 cnf(d157, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | ~furniture(sK8) | 'Ts0', inference(resolution, [status(thm)], [d156,c17])). % 21.97/10.42 cnf(d158, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | ~seat(sK8) | 'Ts0', inference(resolution, [status(thm)], [d157,c16])). % 21.97/10.42 cnf(d159, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | ~old(sK5) | 'Ts0', inference(resolution, [status(thm)], [d158,c15])). % 21.97/10.42 cnf(d160, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | ~dirty(sK5) | 'Ts0', inference(resolution, [status(thm)], [d159,c11])). % 21.97/10.42 cnf(d161, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | ~white(sK5) | 'Ts0', inference(resolution, [status(thm)], [d160,c10])). % 21.97/10.42 cnf(d162, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | ~car(sK5) | 'Ts0', inference(resolution, [status(thm)], [d161,c9])). % 21.97/10.42 cnf(d163, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | ~chevy(sK5) | 'Ts0', inference(resolution, [status(thm)], [d162,c8])). % 21.97/10.42 cnf(d164, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | ~lonely(sK4) | 'Ts0', inference(resolution, [status(thm)], [d163,c7])). % 21.97/10.42 cnf(d165, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | ~way(sK4) | 'Ts0', inference(resolution, [status(thm)], [d164,c6])). % 21.97/10.42 cnf(d166, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | ~street(sK4) | 'Ts0', inference(resolution, [status(thm)], [d165,c5])). % 21.97/10.42 cnf(d167, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | ~event(sK3) | 'Ts0', inference(resolution, [status(thm)], [d166,c4])). % 21.97/10.42 cnf(d168, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | ~city(sK2) | 'Ts0', inference(resolution, [status(thm)], [d167,c3])). % 21.97/10.42 cnf(d169, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | ~hollywood(sK2) | 'Ts0', inference(resolution, [status(thm)], [d168,c2])). % 21.97/10.42 cnf(d170, plain, sK6 = sK7 | sK9 = sK10 | 'Ts0' | 'Ts0', inference(resolution, [status(thm)], [d169,c1])). % 21.97/10.42 cnf(d171, plain, sK6 = sK7 | sK9 = sK10 | sK6 = sK7, inference(resolution, [status(thm)], [d170,d142])). % 21.97/10.42 cnf(d172, plain, sK7 = sK9 | sK6 = sK7 | sK6 = sK7, inference(superposition, [status(thm)], [d171,d144])). % 21.97/10.42 cnf(d173, plain, sK6 = sK7 | sK6 = sK7 | sK6 = sK7, inference(superposition, [status(thm)], [d172,d143])). % 21.97/10.42 cnf(d174, plain, 'Ts0', inference(resolution, [status(thm)], [d173,c18])). % 21.97/10.42 cnf(d175, plain, sK25 = sK28, inference(resolution, [status(thm)], [d174,d0])). % 21.97/10.42 cnf(d176, plain, sK24 = sK27, inference(resolution, [status(thm)], [d174,d1])). % 21.97/10.42 cnf(d177, plain, ~'Ts1', inference(resolution, [status(thm)], [d174,c0])). % 21.97/10.42 cnf(d178, plain, sK27 = sK28 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28), inference(resolution, [status(thm)], [d177,d10])). % 21.97/10.42 cnf(d179, plain, sK24 = sK28 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28), inference(demodulation, [status(thm)], [d178,d176])). % 21.97/10.42 cnf(d180, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK27) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28), inference(demodulation, [status(thm)], [d179,d175])). % 21.97/10.42 cnf(d181, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK28) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28), inference(demodulation, [status(thm)], [d180,d176])). % 21.97/10.42 cnf(d182, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK27) | ~man(sK28) | ~young(sK27) | ~young(sK28), inference(demodulation, [status(thm)], [d181,d175])). % 21.97/10.42 cnf(d183, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK24) | ~man(sK28) | ~young(sK27) | ~young(sK28), inference(demodulation, [status(thm)], [d182,d176])). % 21.97/10.42 cnf(d184, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK24) | ~man(sK25) | ~young(sK27) | ~young(sK28), inference(demodulation, [status(thm)], [d183,d175])). % 21.97/10.42 cnf(d185, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK24) | ~man(sK25) | ~young(sK24) | ~young(sK28), inference(demodulation, [status(thm)], [d184,d176])). % 21.97/10.42 cnf(d186, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK24) | ~man(sK25) | ~young(sK24) | ~young(sK25), inference(demodulation, [status(thm)], [d185,d175])). % 21.97/10.42 cnf(d187, plain, young(sK25), inference(resolution, [status(thm)], [d177,c53])). % 21.97/10.42 cnf(d188, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK24) | ~man(sK25) | ~young(sK24), inference(resolution, [status(thm)], [d187,d186])). % 21.97/10.42 cnf(d189, plain, man(sK25), inference(resolution, [status(thm)], [d177,c52])). % 21.97/10.42 cnf(d190, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~fellow(sK25) | ~man(sK24) | ~young(sK24), inference(resolution, [status(thm)], [d189,d188])). % 21.97/10.42 cnf(d191, plain, fellow(sK25), inference(resolution, [status(thm)], [d177,c51])). % 21.97/10.42 cnf(d192, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~man(sK24) | ~young(sK24), inference(resolution, [status(thm)], [d191,d190])). % 21.97/10.42 cnf(d193, plain, young(sK24), inference(resolution, [status(thm)], [d177,c50])). % 21.97/10.42 cnf(d194, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24) | ~man(sK24), inference(resolution, [status(thm)], [d193,d192])). % 21.97/10.42 cnf(d195, plain, man(sK24), inference(resolution, [status(thm)], [d177,c49])). % 21.97/10.42 cnf(d196, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26) | ~fellow(sK24), inference(resolution, [status(thm)], [d195,d194])). % 21.97/10.42 cnf(d197, plain, fellow(sK24), inference(resolution, [status(thm)], [d177,c48])). % 21.97/10.42 cnf(d198, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26) | ~front(sK26), inference(resolution, [status(thm)], [d197,d196])). % 21.97/10.42 cnf(d199, plain, front(sK26), inference(resolution, [status(thm)], [d177,c46])). % 21.97/10.42 cnf(d200, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26) | ~furniture(sK26), inference(resolution, [status(thm)], [d199,d198])). % 21.97/10.42 cnf(d201, plain, furniture(sK26), inference(resolution, [status(thm)], [d177,c45])). % 21.97/10.42 cnf(d202, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~lonely(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d201,d200])). % 21.97/10.42 cnf(d203, plain, lonely(sK23), inference(resolution, [status(thm)], [d177,c40])). % 21.97/10.42 cnf(d204, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~way(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d203,d202])). % 21.97/10.42 cnf(d205, plain, way(sK23), inference(resolution, [status(thm)], [d177,c39])). % 21.97/10.42 cnf(d206, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~street(sK23) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d205,d204])). % 21.97/10.42 cnf(d207, plain, street(sK23), inference(resolution, [status(thm)], [d177,c38])). % 21.97/10.42 cnf(d208, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~old(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d207,d206])). % 21.97/10.42 cnf(d209, plain, old(sK22), inference(resolution, [status(thm)], [d177,c37])). % 21.97/10.42 cnf(d210, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~dirty(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d209,d208])). % 21.97/10.42 cnf(d211, plain, dirty(sK22), inference(resolution, [status(thm)], [d177,c36])). % 21.97/10.42 cnf(d212, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~chevy(sK22) | ~car(sK22) | ~white(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d211,d210])). % 21.97/10.42 cnf(d213, plain, white(sK22), inference(resolution, [status(thm)], [d177,c35])). % 21.97/10.42 cnf(d214, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~chevy(sK22) | ~car(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d213,d212])). % 21.97/10.42 cnf(d215, plain, car(sK22), inference(resolution, [status(thm)], [d177,c34])). % 21.97/10.42 cnf(d216, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~chevy(sK22) | ~seat(sK26), inference(resolution, [status(thm)], [d215,d214])). % 21.97/10.42 cnf(d217, plain, chevy(sK22), inference(resolution, [status(thm)], [d177,c33])). % 21.97/10.42 cnf(d218, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~event(sK21) | ~seat(sK26), inference(resolution, [status(thm)], [d217,d216])). % 21.97/10.42 cnf(d219, plain, event(sK21), inference(resolution, [status(thm)], [d177,c32])). % 21.97/10.42 cnf(d220, plain, sK24 = sK25 | ~hollywood(sK20) | ~city(sK20) | ~seat(sK26), inference(resolution, [status(thm)], [d219,d218])). % 21.97/10.42 cnf(d221, plain, hollywood(sK20), inference(resolution, [status(thm)], [d177,c30])). % 21.97/10.42 cnf(d222, plain, sK24 = sK25 | ~city(sK20) | ~seat(sK26), inference(resolution, [status(thm)], [d221,d220])). % 21.97/10.42 cnf(d223, plain, seat(sK26), inference(resolution, [status(thm)], [d177,c44])). % 21.97/10.42 cnf(d224, plain, sK24 = sK25 | ~city(sK20), inference(resolution, [status(thm)], [d223,d222])). % 21.97/10.42 cnf(d225, plain, city(sK20), inference(resolution, [status(thm)], [d177,c31])). % 21.97/10.42 cnf(d226, plain, sK24 = sK25, inference(resolution, [status(thm)], [d225,d224])). % 21.97/10.42 cnf(d227, plain, sK24 != sK25, inference(resolution, [status(thm)], [d177,c47])). % 21.97/10.42 cnf(d228, plain, $false, inference(resolution, [status(thm)], [d227,d226])). % 21.97/10.42 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------