%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : GEO340+1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 07:15:07 AM UTC 2026 % Result : Theorem 103.34s 18.45s % Output : CNFRefutation 103.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : GEO340+1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/0.37 % Computer : n004.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Fri Sep 25 13:20:50 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.34/18.45 % SZS status Theorem for theBenchmark.p % 103.34/18.45 % SZS output start CNFRefutation for theBenchmark.p % 103.34/18.45 fof(and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402)))))))))))), axiom, (vd1391 = vd1392 & (ron(vd1385,vd1391) & (ron(vd1384,vd1391) & (rline(vd1392) & (vd1385 != vd1386 & (vd1384 != vd1386 & (vd1384 != vd1385 & (? [X0] : ((vd1386 = X0 & rpoint(X0))) & (? [X1] : ((vd1385 = X1 & rpoint(X1))) & ? [X2] : ((vd1384 = X2 & rpoint(X2))))))))))))). % 103.34/18.45 fof(ass(cond(proof(404), 0), 0), axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((X3 = X4 & (ron(X1,X3) & (ron(X0,X3) & (rline(X4) & (X1 != X2 & (X0 != X2 & (X0 != X1 & (? [X5] : ((X2 = X5 & rpoint(X5))) & (? [X6] : ((X1 = X6 & rpoint(X6))) & ? [X7] : ((X0 = X7 & rpoint(X7)))))))))))) => ! [X8] : (((X8 != X2 & (vf(X1,X2) = vf(X1,X8) & (vf(X0,X2) = vf(X0,X8) & (rS(X2,X8,X3) & rpoint(X8))))) => ! [X9] : ((X9 = vskolem1416(X8,X0,X1,X2,X3,X4) => ! [X10] : X10 != vskolem1419(X9,X8,X0,X1,X2,X3,X4)))))))). % 103.34/18.45 fof(ass(cond(proof(404), 0), 3), axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((X3 = X4 & (ron(X1,X3) & (ron(X0,X3) & (rline(X4) & (X1 != X2 & (X0 != X2 & (X0 != X1 & (? [X5] : ((X2 = X5 & rpoint(X5))) & (? [X6] : ((X1 = X6 & rpoint(X6))) & ? [X7] : ((X0 = X7 & rpoint(X7)))))))))))) => ! [X8] : (((X8 != X2 & (vf(X1,X2) = vf(X1,X8) & (vf(X0,X2) = vf(X0,X8) & (rS(X2,X8,X3) & rpoint(X8))))) => ! [X9] : (((ron(X0,X9) & (ron(X2,X9) & rline(X9))) => X9 = vskolem1416(X8,X0,X1,X2,X3,X4)))))))). % 103.34/18.45 fof(ass(cond(proof(404), 0), 4), axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : (((X3 = X4 & (ron(X1,X3) & (ron(X0,X3) & (rline(X4) & (X1 != X2 & (X0 != X2 & (X0 != X1 & (? [X5] : ((X2 = X5 & rpoint(X5))) & (? [X6] : ((X1 = X6 & rpoint(X6))) & ? [X7] : ((X0 = X7 & rpoint(X7)))))))))))) => ! [X8] : (((X8 != X2 & (vf(X1,X2) = vf(X1,X8) & (vf(X0,X2) = vf(X0,X8) & (rS(X2,X8,X3) & rpoint(X8))))) => (ron(X0,vskolem1416(X8,X0,X1,X2,X3,X4)) & (ron(X2,vskolem1416(X8,X0,X1,X2,X3,X4)) & rline(vskolem1416(X8,X0,X1,X2,X3,X4))))))))). % 103.34/18.45 fof(neg(neg(403)), conjecture, ~? [X0] : ((X0 != vd1386 & (vf(vd1385,vd1386) = vf(vd1385,X0) & (vf(vd1384,vd1386) = vf(vd1384,X0) & (rS(vd1386,X0,vd1391) & rpoint(X0))))))). % 103.34/18.45 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ((X0 != vd1386 & (vf(vd1385,vd1386) = vf(vd1385,X0) & (vf(vd1384,vd1386) = vf(vd1384,X0) & (rS(vd1386,X0,vd1391) & rpoint(X0)))))), inference(negate_conjecture, [status(cth)], [neg(neg(403))])). % 103.34/18.45 cnf(c0, plain, vd1391 = vd1392, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c1, plain, ron(vd1385,vd1391), inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c2, plain, ron(vd1384,vd1391), inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c3, plain, rline(vd1392), inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c4, plain, vd1385 != vd1386, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c5, plain, vd1384 != vd1386, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c6, plain, vd1384 != vd1385, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c7, plain, vd1386 = sK0, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c8, plain, rpoint(sK0), inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c9, plain, vd1385 = sK1, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c10, plain, rpoint(sK1), inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c11, plain, vd1384 = sK2, inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c12, plain, rpoint(sK2), inference(clausification, [status(esa)], [and(pred(conjunct2(402), 5), and(pred(s2(plural(conjunct2(402))), 0), and(pred(s1(plural(conjunct2(402))), 0), and(pred(conjunct2(402), 1), and(pred(conjunct1(402), 9), and(pred(conjunct1(402), 8), and(pred(conjunct1(402), 7), and(qe(s3(plural(402))), and(qe(s2(plural(402))), qe(s1(plural(402))))))))))))])). % 103.34/18.45 cnf(c13, plain, X0 = X1 | X2 = X1 | X1 != X3 | ~rpoint(X2) | X4 != X5 | ~rS(X1,X2,X4) | ~rline(X5) | X0 != X6 | vf(X0,X1) != vf(X0,X2) | X7 != vskolem1419(X8,X2,X9,X0,X1,X4,X5) | ~rpoint(X6) | ~ron(X9,X4) | X9 != X10 | X8 != vskolem1416(X2,X9,X0,X1,X4,X5) | X9 = X1 | X9 = X0 | ~rpoint(X10) | ~rpoint(X3) | ~ron(X0,X4) | vf(X9,X1) != vf(X9,X2), inference(clausification, [status(esa)], [ass(cond(proof(404), 0), 0)])). % 103.34/18.45 cnf(c18, plain, X0 = X1 | ~ron(X0,X2) | X2 != X3 | X1 != X4 | ~rpoint(X5) | ~rline(X3) | X6 != X7 | X8 = X1 | ~ron(X6,X2) | ~rline(X9) | ~rpoint(X7) | X9 = vskolem1416(X8,X0,X6,X1,X2,X3) | X0 = X6 | vf(X6,X1) != vf(X6,X8) | X6 = X1 | vf(X0,X1) != vf(X0,X8) | ~ron(X0,X9) | ~rpoint(X4) | ~rS(X1,X8,X2) | ~ron(X1,X9) | ~rpoint(X8) | X0 != X5, inference(clausification, [status(esa)], [ass(cond(proof(404), 0), 3)])). % 103.34/18.45 cnf(c19, plain, X0 != X1 | X2 = X3 | ~rpoint(X4) | ~rS(X5,X4,X0) | X5 != X6 | ~ron(X2,X0) | X3 != X7 | ron(X2,vskolem1416(X4,X2,X3,X5,X0,X1)) | ~rline(X1) | X3 = X5 | ~rpoint(X6) | vf(X2,X5) != vf(X2,X4) | ~rpoint(X7) | ~rpoint(X8) | X2 = X5 | ~ron(X3,X0) | vf(X3,X5) != vf(X3,X4) | X2 != X8 | X4 = X5, inference(clausification, [status(esa)], [ass(cond(proof(404), 0), 4)])). % 103.34/18.45 cnf(c20, plain, X0 != X1 | ron(X2,vskolem1416(X3,X4,X5,X2,X0,X1)) | X4 = X5 | ~rpoint(X3) | ~rS(X2,X3,X0) | X2 != X6 | ~ron(X4,X0) | X5 != X7 | ~rline(X1) | X5 = X2 | ~rpoint(X6) | vf(X4,X2) != vf(X4,X3) | ~rpoint(X7) | ~rpoint(X8) | X4 = X2 | ~ron(X5,X0) | vf(X5,X2) != vf(X5,X3) | X4 != X8 | X3 = X2, inference(clausification, [status(esa)], [ass(cond(proof(404), 0), 4)])). % 103.34/18.45 cnf(c21, plain, X0 != X1 | rline(vskolem1416(X2,X3,X4,X5,X0,X1)) | X3 = X4 | ~rpoint(X2) | ~rS(X5,X2,X0) | X5 != X6 | ~ron(X3,X0) | X4 != X7 | ~rline(X1) | X4 = X5 | ~rpoint(X6) | vf(X3,X5) != vf(X3,X2) | ~rpoint(X7) | ~rpoint(X8) | X3 = X5 | ~ron(X4,X0) | vf(X4,X5) != vf(X4,X2) | X3 != X8 | X2 = X5, inference(clausification, [status(esa)], [ass(cond(proof(404), 0), 4)])). % 103.34/18.45 cnf(c289, plain, sK908 != vd1386, inference(clausification, [status(esa)], [negated_conjecture])). % 103.34/18.45 cnf(c290, plain, vf(vd1385,vd1386) = vf(vd1385,sK908), inference(clausification, [status(esa)], [negated_conjecture])). % 103.34/18.45 cnf(c291, plain, vf(vd1384,vd1386) = vf(vd1384,sK908), inference(clausification, [status(esa)], [negated_conjecture])). % 103.34/18.45 cnf(c292, plain, rS(vd1386,sK908,vd1391), inference(clausification, [status(esa)], [negated_conjecture])). % 103.34/18.45 cnf(c293, plain, rpoint(sK908), inference(clausification, [status(esa)], [negated_conjecture])). % 103.34/18.45 cnf(d0, plain, vf(vd1384,X0) != vf(vd1384,vd1386) | X1 != X2 | sK908 = X0 | X0 != X3 | X4 = X0 | X4 != X5 | vd1384 = X0 | vd1384 = X4 | vd1384 != X6 | vf(X4,X0) != vf(X4,sK908) | ~ron(X4,X1) | ~ron(vd1384,X1) | ~rline(X2) | rline(vskolem1416(sK908,vd1384,X4,X0,X1,X2)) | ~rpoint(X3) | ~rpoint(sK908) | ~rpoint(X5) | ~rpoint(X6) | ~rS(X0,sK908,X1), inference(superposition, [status(thm)], [c291,c21])). % 103.34/18.45 cnf(d1, plain, X0 != X1 | X0 = X2 | X3 != X4 | X2 != X5 | vd1384 != X6 | vd1384 = X0 | vd1384 = X2 | vf(X0,X2) != vf(X0,sK908) | vf(vd1384,X2) != vf(vd1384,vd1386) | sK908 = X2 | ~ron(X0,X3) | ~ron(vd1384,X3) | ~rline(X4) | rline(vskolem1416(sK908,vd1384,X0,X2,X3,X4)) | ~rpoint(X6) | ~rpoint(X1) | ~rpoint(X5) | ~rS(X2,sK908,X3), inference(resolution, [status(thm)], [c293,d0])). % 103.34/18.45 cnf(d2, plain, X0 != X1 | vd1386 != X2 | X3 = vd1386 | X3 != X4 | vd1384 != X5 | vd1384 = vd1386 | vd1384 = X3 | vf(X3,vd1386) != vf(X3,sK908) | sK908 = vd1386 | ~ron(X3,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,X3,vd1386,X0,X1)) | ~rpoint(X5) | ~rpoint(X2) | ~rpoint(X4) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d1])). % 103.34/18.45 cnf(d3, plain, X0 != X1 | X0 = vd1386 | X2 != X3 | vd1384 != X4 | vd1384 = X0 | vd1384 = vd1386 | vd1386 != X5 | vf(X0,vd1386) != vf(X0,sK908) | ~ron(X0,X2) | ~ron(vd1384,X2) | ~rline(X3) | rline(vskolem1416(sK908,vd1384,X0,vd1386,X2,X3)) | ~rpoint(X4) | ~rpoint(X1) | ~rpoint(X5) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c289,d2])). % 103.34/18.45 cnf(d4, plain, X0 != X1 | X2 != X3 | X2 = vd1386 | vd1384 != X4 | vd1384 = X2 | vd1386 != X5 | vf(X2,vd1386) != vf(X2,sK908) | ~ron(X2,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,X2,vd1386,X0,X1)) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c5,d3])). % 103.34/18.45 cnf(d5, plain, vf(vd1385,vd1386) != vf(vd1385,vd1386) | vd1385 != X0 | vd1385 = vd1386 | X1 != X2 | vd1384 != X3 | vd1384 = vd1385 | vd1386 != X4 | ~ron(vd1385,X1) | ~ron(vd1384,X1) | ~rline(X2) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2)) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X0) | ~rS(vd1386,sK908,X1), inference(superposition, [status(thm)], [c290,d4])). % 103.34/18.45 cnf(d6, plain, X0 != X1 | vd1385 != X2 | vd1385 = vd1386 | vd1384 != X3 | vd1386 != X4 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c6,d5])). % 103.34/18.45 cnf(d7, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | vd1386 != X4 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c4,d6])). % 103.34/18.45 cnf(d8, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | vd1386 != X4 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d7])). % 103.34/18.45 cnf(d9, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(vd1386) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d8])). % 103.34/18.45 cnf(d10, plain, rpoint(vd1386), inference(demodulation, [status(thm)], [c8,c7])). % 103.34/18.45 cnf(d11, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d10,d9])). % 103.34/18.45 cnf(d12, plain, X0 != X1 | vd1385 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(vd1384) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d11])). % 103.34/18.45 cnf(d13, plain, rpoint(vd1384), inference(demodulation, [status(thm)], [c12,c11])). % 103.34/18.45 cnf(d14, plain, X0 != X1 | vd1385 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d13,d12])). % 103.34/18.45 cnf(d15, plain, X0 != X1 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rpoint(vd1385) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d14])). % 103.34/18.45 cnf(d16, plain, rpoint(vd1385), inference(demodulation, [status(thm)], [c10,c9])). % 103.34/18.45 cnf(d17, plain, X0 != X1 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X1) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d16,d15])). % 103.34/18.45 cnf(d18, plain, ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X0) | rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X0)) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d17])). % 103.34/18.45 cnf(d19, plain, vf(vd1384,X0) != vf(vd1384,vd1386) | X1 != X2 | sK908 = X0 | X0 != X3 | X4 = X0 | X4 != X5 | vd1384 = X0 | vd1384 = X4 | vd1384 != X6 | vf(X4,X0) != vf(X4,sK908) | ~ron(X4,X1) | ~ron(vd1384,X1) | ron(vd1384,vskolem1416(sK908,vd1384,X4,X0,X1,X2)) | ~rline(X2) | ~rpoint(X3) | ~rpoint(sK908) | ~rpoint(X5) | ~rpoint(X6) | ~rS(X0,sK908,X1), inference(superposition, [status(thm)], [c291,c19])). % 103.34/18.45 cnf(d20, plain, X0 != X1 | X0 = X2 | X3 != X4 | X2 != X5 | vd1384 != X6 | vd1384 = X0 | vd1384 = X2 | vf(X0,X2) != vf(X0,sK908) | vf(vd1384,X2) != vf(vd1384,vd1386) | sK908 = X2 | ~ron(X0,X3) | ~ron(vd1384,X3) | ron(vd1384,vskolem1416(sK908,vd1384,X0,X2,X3,X4)) | ~rline(X4) | ~rpoint(X6) | ~rpoint(X1) | ~rpoint(X5) | ~rS(X2,sK908,X3), inference(resolution, [status(thm)], [c293,d19])). % 103.34/18.45 cnf(d21, plain, X0 != X1 | vd1386 != X2 | X3 = vd1386 | X3 != X4 | vd1384 != X5 | vd1384 = vd1386 | vd1384 = X3 | vf(X3,vd1386) != vf(X3,sK908) | sK908 = vd1386 | ~ron(X3,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,X3,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X5) | ~rpoint(X2) | ~rpoint(X4) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d20])). % 103.34/18.45 cnf(d22, plain, X0 != X1 | X0 = vd1386 | X2 != X3 | vd1384 != X4 | vd1384 = X0 | vd1384 = vd1386 | vd1386 != X5 | vf(X0,vd1386) != vf(X0,sK908) | ~ron(X0,X2) | ~ron(vd1384,X2) | ron(vd1384,vskolem1416(sK908,vd1384,X0,vd1386,X2,X3)) | ~rline(X3) | ~rpoint(X4) | ~rpoint(X1) | ~rpoint(X5) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c289,d21])). % 103.34/18.45 cnf(d23, plain, X0 != X1 | X2 != X3 | X2 = vd1386 | vd1384 != X4 | vd1384 = X2 | vd1386 != X5 | vf(X2,vd1386) != vf(X2,sK908) | ~ron(X2,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,X2,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c5,d22])). % 103.34/18.45 cnf(d24, plain, vf(vd1385,vd1386) != vf(vd1385,vd1386) | vd1385 != X0 | vd1385 = vd1386 | X1 != X2 | vd1384 != X3 | vd1384 = vd1385 | vd1386 != X4 | ~ron(vd1385,X1) | ~ron(vd1384,X1) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2)) | ~rline(X2) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X0) | ~rS(vd1386,sK908,X1), inference(superposition, [status(thm)], [c290,d23])). % 103.34/18.45 cnf(d25, plain, X0 != X1 | vd1385 != X2 | vd1385 = vd1386 | vd1384 != X3 | vd1386 != X4 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c6,d24])). % 103.34/18.45 cnf(d26, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | vd1386 != X4 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c4,d25])). % 103.34/18.45 cnf(d27, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | vd1386 != X4 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d26])). % 103.34/18.45 cnf(d28, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(vd1386) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d27])). % 103.34/18.45 cnf(d29, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d10,d28])). % 103.34/18.45 cnf(d30, plain, X0 != X1 | vd1385 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(vd1384) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d29])). % 103.34/18.45 cnf(d31, plain, X0 != X1 | vd1385 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d13,d30])). % 103.34/18.45 cnf(d32, plain, X0 != X1 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(vd1385) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d31])). % 103.34/18.45 cnf(d33, plain, X0 != X1 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d16,d32])). % 103.34/18.45 cnf(d34, plain, ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X0)) | ~rline(X0) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d33])). % 103.34/18.45 cnf(d35, plain, vf(vd1384,X0) != vf(vd1384,vd1386) | X1 != X2 | sK908 = X0 | X0 != X3 | X4 = X0 | X4 != X5 | vd1384 = X0 | vd1384 = X4 | vd1384 != X6 | vf(X4,X0) != vf(X4,sK908) | ron(X0,vskolem1416(sK908,vd1384,X4,X0,X1,X2)) | ~ron(X4,X1) | ~ron(vd1384,X1) | ~rline(X2) | ~rpoint(X3) | ~rpoint(sK908) | ~rpoint(X5) | ~rpoint(X6) | ~rS(X0,sK908,X1), inference(superposition, [status(thm)], [c291,c20])). % 103.34/18.45 cnf(d36, plain, X0 != X1 | X0 = X2 | X3 != X4 | X2 != X5 | vd1384 != X6 | vd1384 = X0 | vd1384 = X2 | vf(X0,X2) != vf(X0,sK908) | vf(vd1384,X2) != vf(vd1384,vd1386) | sK908 = X2 | ~ron(X0,X3) | ron(X2,vskolem1416(sK908,vd1384,X0,X2,X3,X4)) | ~ron(vd1384,X3) | ~rline(X4) | ~rpoint(X6) | ~rpoint(X1) | ~rpoint(X5) | ~rS(X2,sK908,X3), inference(resolution, [status(thm)], [c293,d35])). % 103.34/18.45 cnf(d37, plain, X0 != X1 | vd1386 != X2 | X3 = vd1386 | X3 != X4 | vd1384 != X5 | vd1384 = vd1386 | vd1384 = X3 | vf(X3,vd1386) != vf(X3,sK908) | sK908 = vd1386 | ron(vd1386,vskolem1416(sK908,vd1384,X3,vd1386,X0,X1)) | ~ron(X3,X0) | ~ron(vd1384,X0) | ~rline(X1) | ~rpoint(X5) | ~rpoint(X2) | ~rpoint(X4) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d36])). % 103.34/18.45 cnf(d38, plain, X0 != X1 | X0 = vd1386 | X2 != X3 | vd1384 != X4 | vd1384 = X0 | vd1384 = vd1386 | vd1386 != X5 | vf(X0,vd1386) != vf(X0,sK908) | ~ron(X0,X2) | ~ron(vd1384,X2) | ron(vd1386,vskolem1416(sK908,vd1384,X0,vd1386,X2,X3)) | ~rline(X3) | ~rpoint(X4) | ~rpoint(X1) | ~rpoint(X5) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c289,d37])). % 103.34/18.45 cnf(d39, plain, X0 != X1 | X2 != X3 | X2 = vd1386 | vd1384 != X4 | vd1384 = X2 | vd1386 != X5 | vf(X2,vd1386) != vf(X2,sK908) | ~ron(X2,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,X2,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c5,d38])). % 103.34/18.45 cnf(d40, plain, vf(vd1385,vd1386) != vf(vd1385,vd1386) | vd1385 != X0 | vd1385 = vd1386 | X1 != X2 | vd1384 != X3 | vd1384 = vd1385 | vd1386 != X4 | ~ron(vd1385,X1) | ~ron(vd1384,X1) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2)) | ~rline(X2) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X0) | ~rS(vd1386,sK908,X1), inference(superposition, [status(thm)], [c290,d39])). % 103.34/18.45 cnf(d41, plain, X0 != X1 | vd1385 != X2 | vd1385 = vd1386 | vd1384 != X3 | vd1386 != X4 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c6,d40])). % 103.34/18.45 cnf(d42, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | vd1386 != X4 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c4,d41])). % 103.34/18.45 cnf(d43, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | vd1386 != X4 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X4) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d42])). % 103.34/18.45 cnf(d44, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(vd1386) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d43])). % 103.34/18.45 cnf(d45, plain, X0 != X1 | vd1385 != X2 | vd1384 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X3) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d10,d44])). % 103.34/18.45 cnf(d46, plain, X0 != X1 | vd1385 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(vd1384) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d45])). % 103.34/18.45 cnf(d47, plain, X0 != X1 | vd1385 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d13,d46])). % 103.34/18.45 cnf(d48, plain, X0 != X1 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rpoint(vd1385) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d47])). % 103.34/18.45 cnf(d49, plain, X0 != X1 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1)) | ~rline(X1) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d16,d48])). % 103.34/18.45 cnf(d50, plain, ~ron(vd1385,X0) | ~ron(vd1384,X0) | ron(vd1386,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X0)) | ~rline(X0) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d49])). % 103.34/18.45 cnf(d51, plain, X0 != X1 | X0 = X2 | X3 != vskolem1416(X4,X5,X0,X2,X6,X7) | X6 != X7 | X4 = X2 | X2 != X8 | X5 != X9 | X5 = X0 | X5 = X2 | vf(X0,X2) != vf(X0,X4) | vf(X5,X2) != vf(X5,X4) | ~ron(X0,X6) | ~ron(X5,X6) | ~rline(X7) | ~rpoint(X1) | ~rpoint(X9) | ~rpoint(X8) | ~rpoint(X4) | ~rS(X2,X4,X6), inference(equality_resolution, [status(thm)], [c13])). % 103.34/18.45 cnf(d52, plain, vf(vd1385,X0) != vf(vd1385,vd1386) | X1 = vskolem1416(sK908,X2,vd1385,X0,X3,X4) | X2 != X5 | X2 = X0 | X2 = vd1385 | X0 != X6 | vd1385 = X0 | vd1385 != X7 | X3 != X4 | sK908 = X0 | vf(X2,X0) != vf(X2,sK908) | ~ron(X2,X1) | ~ron(X2,X3) | ~ron(X0,X1) | ~ron(vd1385,X3) | ~rline(X1) | ~rline(X4) | ~rpoint(X5) | ~rpoint(X7) | ~rpoint(X6) | ~rpoint(sK908) | ~rS(X0,sK908,X3), inference(superposition, [status(thm)], [c290,c18])). % 103.34/18.45 cnf(d53, plain, X0 != X1 | X2 != X3 | X2 = X4 | X2 = vd1385 | X5 = vskolem1416(sK908,X2,vd1385,X4,X0,X1) | X4 != X6 | vd1385 != X7 | vd1385 = X4 | vf(X2,X4) != vf(X2,sK908) | vf(vd1385,X4) != vf(vd1385,vd1386) | sK908 = X4 | ~ron(X2,X0) | ~ron(X2,X5) | ~ron(X4,X5) | ~ron(vd1385,X0) | ~rline(X1) | ~rline(X5) | ~rpoint(X7) | ~rpoint(X6) | ~rpoint(X3) | ~rS(X4,sK908,X0), inference(resolution, [status(thm)], [c293,d52])). % 103.34/18.45 cnf(d54, plain, X0 = vskolem1416(sK908,X1,vd1385,vd1386,X2,X3) | vd1386 != X4 | X1 = vd1386 | X1 != X5 | X1 = vd1385 | X2 != X3 | vd1385 != X6 | vd1385 = vd1386 | vf(X1,vd1386) != vf(X1,sK908) | sK908 = vd1386 | ~ron(vd1386,X0) | ~ron(X1,X0) | ~ron(X1,X2) | ~ron(vd1385,X2) | ~rline(X0) | ~rline(X3) | ~rpoint(X6) | ~rpoint(X4) | ~rpoint(X5) | ~rS(vd1386,sK908,X2), inference(equality_resolution, [status(thm)], [d53])). % 103.34/18.45 cnf(d55, plain, X0 != X1 | X2 != X3 | X2 = vd1385 | X2 = vd1386 | X4 = vskolem1416(sK908,X2,vd1385,vd1386,X0,X1) | vd1385 != X5 | vd1385 = vd1386 | vd1386 != X6 | vf(X2,vd1386) != vf(X2,sK908) | ~ron(X2,X0) | ~ron(X2,X4) | ~ron(vd1385,X0) | ~ron(vd1386,X4) | ~rline(X1) | ~rline(X4) | ~rpoint(X5) | ~rpoint(X3) | ~rpoint(X6) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c289,d54])). % 103.34/18.45 cnf(d56, plain, X0 = vskolem1416(sK908,X1,vd1385,vd1386,X2,X3) | X1 != X4 | X1 = vd1385 | X1 = vd1386 | X2 != X3 | vd1385 != X5 | vd1386 != X6 | vf(X1,vd1386) != vf(X1,sK908) | ~ron(X1,X0) | ~ron(X1,X2) | ~ron(vd1385,X2) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(X3) | ~rpoint(X6) | ~rpoint(X5) | ~rpoint(X4) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c4,d55])). % 103.34/18.45 cnf(d57, plain, vf(vd1384,vd1386) != vf(vd1384,vd1386) | X0 != X1 | vd1384 != X2 | vd1384 = vd1385 | vd1384 = vd1386 | X3 = vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1) | vd1385 != X4 | vd1386 != X5 | ~ron(vd1384,X0) | ~ron(vd1384,X3) | ~ron(vd1385,X0) | ~ron(vd1386,X3) | ~rline(X1) | ~rline(X3) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X2) | ~rS(vd1386,sK908,X0), inference(superposition, [status(thm)], [c291,d56])). % 103.34/18.45 cnf(d58, plain, X0 = vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2) | X1 != X2 | vd1385 != X3 | vd1384 != X4 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1384,vd1386) != vf(vd1384,vd1386) | ~ron(vd1385,X1) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X3) | ~rpoint(X4) | ~rS(vd1386,sK908,X1), inference(resolution, [status(thm)], [c6,d57])). % 103.34/18.45 cnf(d59, plain, X0 != X1 | X2 = vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1) | vd1385 != X3 | vd1384 != X4 | vd1386 != X5 | vf(vd1384,vd1386) != vf(vd1384,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X1) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c5,d58])). % 103.34/18.45 cnf(d60, plain, X0 = vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2) | X1 != X2 | vd1385 != X3 | vd1384 != X4 | vd1386 != X5 | ~ron(vd1385,X1) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X1), inference(equality_resolution, [status(thm)], [d59])). % 103.34/18.45 cnf(d61, plain, X0 != X1 | X2 = vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1) | vd1385 != X3 | vd1384 != X4 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X1) | ~rline(X2) | ~rpoint(vd1386) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d60])). % 103.34/18.45 cnf(d62, plain, X0 = vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2) | X1 != X2 | vd1385 != X3 | vd1384 != X4 | ~ron(vd1385,X1) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(X2) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X1), inference(resolution, [status(thm)], [d10,d61])). % 103.34/18.45 cnf(d63, plain, X0 != X1 | X2 = vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1) | vd1385 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X1) | ~rline(X2) | ~rpoint(vd1384) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d62])). % 103.34/18.45 cnf(d64, plain, X0 = vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2) | X1 != X2 | vd1385 != X3 | ~ron(vd1385,X1) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(X2) | ~rpoint(X3) | ~rS(vd1386,sK908,X1), inference(resolution, [status(thm)], [d13,d63])). % 103.34/18.45 cnf(d65, plain, X0 != X1 | X2 = vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X1) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X1) | ~rline(X2) | ~rpoint(vd1385) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d64])). % 103.34/18.45 cnf(d66, plain, X0 = vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X2) | X1 != X2 | ~ron(vd1385,X1) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(X2) | ~rS(vd1386,sK908,X1), inference(resolution, [status(thm)], [d16,d65])). % 103.34/18.45 cnf(d67, plain, X0 = vskolem1416(sK908,vd1384,vd1385,vd1386,X1,X1) | ~ron(vd1385,X1) | ~ron(vd1384,X1) | ~ron(vd1384,X0) | ~ron(vd1386,X0) | ~rline(X1) | ~rline(X0) | ~rS(vd1386,sK908,X1), inference(equality_resolution, [status(thm)], [d66])). % 103.34/18.45 cnf(d68, plain, X2 != X1 | X0 != X0 | vd1384 != X3 | vd1384 = vd1386 | vd1384 = vd1385 | sK908 = vd1386 | vd1386 != X4 | vd1385 = vd1386 | vd1385 != X5 | vf(vd1384,vd1386) != vf(vd1384,sK908) | vf(vd1385,vd1386) != vf(vd1385,sK908) | ~ron(vd1384,X0) | ~ron(vd1385,X0) | ~rline(X0) | ~rpoint(X3) | ~rpoint(X4) | ~rpoint(sK908) | ~rpoint(X5) | ~rS(vd1386,sK908,X0) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X1) | ~rline(X0) | ~rline(X1) | ~rS(vd1386,sK908,X0), inference(superposition, [status(thm)], [d67,d51])). % 103.34/18.45 cnf(d69, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1385 = vd1386 | vd1384 != X4 | vd1384 = vd1385 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,sK908) | sK908 = vd1386 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X3) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(sK908) | ~rS(vd1386,sK908,X2), inference(demodulation, [status(thm)], [d68,c290])). % 103.34/18.45 cnf(d70, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1385 = vd1386 | vd1384 != X4 | vd1384 = vd1385 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,vd1386) | sK908 = vd1386 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X3) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(sK908) | ~rS(vd1386,sK908,X2), inference(demodulation, [status(thm)], [d69,c291])). % 103.34/18.45 cnf(d71, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1385 = vd1386 | vd1384 != X4 | vd1384 = vd1385 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,vd1386) | sK908 = vd1386 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X3) | ~rpoint(X5) | ~rpoint(X4) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c293,d70])). % 103.34/18.45 cnf(d72, plain, X0 != X0 | X1 != X2 | vd1385 != X3 | vd1385 = vd1386 | vd1384 != X4 | vd1384 = vd1385 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X0) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c289,d71])). % 103.34/18.45 cnf(d73, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1385 = vd1386 | vd1384 != X4 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,vd1386) | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c6,d72])). % 103.34/18.45 cnf(d74, plain, X0 != X0 | X1 != X2 | vd1385 != X3 | vd1384 != X4 | vd1384 = vd1386 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X0) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [c4,d73])). % 103.34/18.45 cnf(d75, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1384 != X4 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | vf(vd1384,vd1386) != vf(vd1384,vd1386) | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [c5,d74])). % 103.34/18.45 cnf(d76, plain, X0 != X0 | X1 != X2 | vd1385 != X3 | vd1384 != X4 | vd1386 != X5 | vf(vd1385,vd1386) != vf(vd1385,vd1386) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X0) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d75])). % 103.34/18.45 cnf(d77, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1384 != X4 | vd1386 != X5 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X5) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X2), inference(equality_resolution, [status(thm)], [d76])). % 103.34/18.45 cnf(d78, plain, X0 != X0 | X1 != X2 | vd1385 != X3 | vd1384 != X4 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X0) | ~rline(X2) | ~rpoint(vd1386) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d77])). % 103.34/18.45 cnf(d79, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | vd1384 != X4 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X4) | ~rpoint(X3) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [d10,d78])). % 103.34/18.45 cnf(d80, plain, X0 != X0 | X1 != X2 | vd1385 != X3 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X0) | ~rline(X2) | ~rpoint(vd1384) | ~rpoint(X3) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d79])). % 103.34/18.45 cnf(d81, plain, X0 != X1 | X2 != X2 | vd1385 != X3 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rpoint(X3) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [d13,d80])). % 103.34/18.45 cnf(d82, plain, X0 != X0 | X1 != X2 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X2) | ~ron(vd1386,X2) | ~rline(X0) | ~rline(X2) | ~rpoint(vd1385) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d81])). % 103.34/18.45 cnf(d83, plain, X0 != X1 | X2 != X2 | ~ron(vd1385,X2) | ~ron(vd1384,X1) | ~ron(vd1384,X2) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X2) | ~rS(vd1386,sK908,X2), inference(resolution, [status(thm)], [d16,d82])). % 103.34/18.45 cnf(d84, plain, X0 != X0 | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~ron(vd1384,X1) | ~ron(vd1386,X1) | ~rline(X0) | ~rline(X1) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d83])). % 103.34/18.45 cnf(d85, plain, ~ron(vd1385,X0) | ~ron(vd1384,X1) | ~ron(vd1384,X0) | ~ron(vd1386,X1) | ~rline(X1) | ~rline(X0) | ~rS(vd1386,sK908,X0), inference(equality_resolution, [status(thm)], [d84])). % 103.34/18.45 cnf(d86, plain, ~ron(vd1385,vd1391) | ~ron(vd1384,X0) | ~ron(vd1384,vd1391) | ~ron(vd1386,X0) | ~rline(X0) | ~rline(vd1391), inference(resolution, [status(thm)], [d85,c292])). % 103.34/18.45 cnf(d87, plain, rline(vd1391), inference(demodulation, [status(thm)], [c3,c0])). % 103.34/18.45 cnf(d88, plain, ~ron(vd1385,vd1391) | ~ron(vd1384,X0) | ~ron(vd1384,vd1391) | ~ron(vd1386,X0) | ~rline(X0), inference(resolution, [status(thm)], [d87,d86])). % 103.34/18.45 cnf(d89, plain, ~ron(vd1384,X0) | ~ron(vd1384,vd1391) | ~ron(vd1386,X0) | ~rline(X0), inference(resolution, [status(thm)], [c1,d88])). % 103.34/18.45 cnf(d90, plain, ~ron(vd1384,X0) | ~ron(vd1386,X0) | ~rline(X0), inference(resolution, [status(thm)], [c2,d89])). % 103.34/18.45 cnf(d91, plain, ~ron(vd1384,vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X0)) | ~rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X0)) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X0) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d90,d50])). % 103.34/18.45 cnf(d92, plain, ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X0) | ~rline(vskolem1416(sK908,vd1384,vd1385,vd1386,X0,X0)) | ~rS(vd1386,sK908,X0) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X0) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d91,d34])). % 103.34/18.45 cnf(d93, plain, ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X0) | ~rS(vd1386,sK908,X0) | ~ron(vd1385,X0) | ~ron(vd1384,X0) | ~rline(X0) | ~rS(vd1386,sK908,X0), inference(resolution, [status(thm)], [d92,d18])). % 103.34/18.45 cnf(d94, plain, ~ron(vd1385,vd1391) | ~ron(vd1384,vd1391) | ~rline(vd1391), inference(resolution, [status(thm)], [d93,c292])). % 103.34/18.45 cnf(d95, plain, ~ron(vd1385,vd1391) | ~ron(vd1384,vd1391), inference(resolution, [status(thm)], [d87,d94])). % 103.34/18.45 cnf(d96, plain, ~ron(vd1384,vd1391), inference(resolution, [status(thm)], [c1,d95])). % 103.34/18.45 cnf(d97, plain, $false, inference(resolution, [status(thm)], [c2,d96])). % 103.34/18.45 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------