%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : GEO331+1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n014.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:06 AM UTC 2026 % Result : Theorem 40.49s 5.66s % Output : CNFRefutation 40.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : GEO331+1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.42 % Computer : n014.cluster.edu % 0.16/0.42 % Model : x86_64 x86_64 % 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.42 % Memory : 8046.5625MB % 0.16/0.42 % OS : Linux 6.8.0-71-generic % 0.16/0.42 % CPULimit : 300 % 0.16/0.42 % WCLimit : 300 % 0.16/0.42 % DateTime : Fri Sep 25 13:19:47 UTC 2026 % 0.16/0.42 % CPUTime : % 0.16/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 40.49/5.66 % SZS status Theorem for theBenchmark.p % 40.49/5.66 % SZS output start CNFRefutation for theBenchmark.p % 40.49/5.66 fof(holds(383, 1356, 0), axiom, vangle(vd1352,vd1353,vd1354) = vangle(vd1352,vd1354,vd1353)). % 40.49/5.66 fof(pred(383, 9), axiom, vd1353 != vd1354). % 40.49/5.66 fof(pred(383, 8), axiom, vd1352 != vd1354). % 40.49/5.66 fof(pred(383, 7), axiom, vd1352 != vd1353). % 40.49/5.66 fof(qe(s3(plural(383))), axiom, ? [X0] : ((vd1354 = X0 & rpoint(X0)))). % 40.49/5.66 fof(qe(s2(plural(383))), axiom, ? [X0] : ((vd1353 = X0 & rpoint(X0)))). % 40.49/5.66 fof(qe(s1(plural(383))), axiom, ? [X0] : ((vd1352 = X0 & rpoint(X0)))). % 40.49/5.66 fof(ass(cond(proof(385), 0), 0), axiom, ! [X0] : ! [X1] : ! [X2] : (((vangle(X0,X1,X2) = vangle(X0,X2,X1) & (X1 != X2 & (X0 != X2 & (X0 != X1 & (? [X3] : ((X2 = X3 & rpoint(X3))) & (? [X4] : ((X1 = X4 & rpoint(X4))) & ? [X5] : ((X0 = X5 & rpoint(X5))))))))) => (vf(X0,X1) != vf(X0,X2) => (rless(vf(X0,X1),vf(X0,X2)) | rless(vf(X0,X2),vf(X0,X1))))))). % 40.49/5.66 fof(ass(cond(proof(385), 0), 1), axiom, ! [X0] : ! [X1] : ! [X2] : (((vangle(X0,X1,X2) = vangle(X0,X2,X1) & (X1 != X2 & (X0 != X2 & (X0 != X1 & (? [X3] : ((X2 = X3 & rpoint(X3))) & (? [X4] : ((X1 = X4 & rpoint(X4))) & ? [X5] : ((X0 = X5 & rpoint(X5))))))))) => (vf(X0,X1) != vf(X0,X2) => ~rless(vf(X0,X1),vf(X0,X2)))))). % 40.49/5.66 fof(ass(cond(proof(385), 0), 2), axiom, ! [X0] : ! [X1] : ! [X2] : (((vangle(X0,X1,X2) = vangle(X0,X2,X1) & (X1 != X2 & (X0 != X2 & (X0 != X1 & (? [X3] : ((X2 = X3 & rpoint(X3))) & (? [X4] : ((X1 = X4 & rpoint(X4))) & ? [X5] : ((X0 = X5 & rpoint(X5))))))))) => (vf(X0,X1) != vf(X0,X2) => ~rless(vf(X0,X2),vf(X0,X1)))))). % 40.49/5.66 fof(holds(384, 1360, 0), conjecture, vf(vd1352,vd1353) = vf(vd1352,vd1354)). % 40.49/5.66 fof(negated_conjecture, negated_conjecture, vf(vd1352,vd1353) != vf(vd1352,vd1354), inference(negate_conjecture, [status(cth)], [holds(384, 1360, 0)])). % 40.49/5.66 cnf(c0, plain, vangle(vd1352,vd1353,vd1354) = vangle(vd1352,vd1354,vd1353), inference(clausification, [status(esa)], [holds(383, 1356, 0)])). % 40.49/5.66 cnf(c1, plain, vd1353 != vd1354, inference(clausification, [status(esa)], [pred(383, 9)])). % 40.49/5.66 cnf(c2, plain, vd1352 != vd1354, inference(clausification, [status(esa)], [pred(383, 8)])). % 40.49/5.66 cnf(c3, plain, vd1352 != vd1353, inference(clausification, [status(esa)], [pred(383, 7)])). % 40.49/5.66 cnf(c4, plain, vd1354 = sK0, inference(clausification, [status(esa)], [qe(s3(plural(383)))])). % 40.49/5.66 cnf(c5, plain, rpoint(sK0), inference(clausification, [status(esa)], [qe(s3(plural(383)))])). % 40.49/5.66 cnf(c6, plain, vd1353 = sK1, inference(clausification, [status(esa)], [qe(s2(plural(383)))])). % 40.49/5.66 cnf(c7, plain, rpoint(sK1), inference(clausification, [status(esa)], [qe(s2(plural(383)))])). % 40.49/5.66 cnf(c8, plain, vd1352 = sK2, inference(clausification, [status(esa)], [qe(s1(plural(383)))])). % 40.49/5.66 cnf(c9, plain, rpoint(sK2), inference(clausification, [status(esa)], [qe(s1(plural(383)))])). % 40.49/5.66 cnf(c10, plain, X0 != X1 | X2 = X0 | vangle(X3,X2,X0) != vangle(X3,X0,X2) | X3 != X4 | ~rpoint(X5) | X3 = X0 | X3 = X2 | vf(X3,X2) = vf(X3,X0) | ~rpoint(X4) | rless(vf(X3,X2),vf(X3,X0)) | X2 != X5 | ~rpoint(X1) | rless(vf(X3,X0),vf(X3,X2)), inference(clausification, [status(esa)], [ass(cond(proof(385), 0), 0)])). % 40.49/5.66 cnf(c11, plain, vangle(X0,X1,X2) != vangle(X0,X2,X1) | ~rpoint(X3) | X1 = X2 | ~rless(vf(X0,X1),vf(X0,X2)) | X0 != X4 | vf(X0,X1) = vf(X0,X2) | X2 != X5 | X0 = X2 | ~rpoint(X4) | X1 != X3 | X0 = X1 | ~rpoint(X5), inference(clausification, [status(esa)], [ass(cond(proof(385), 0), 1)])). % 40.49/5.66 cnf(c12, plain, ~rpoint(X0) | X1 != X2 | X1 = X3 | ~rpoint(X4) | ~rless(vf(X1,X3),vf(X1,X5)) | X5 != X4 | X1 = X5 | X5 = X3 | ~rpoint(X2) | X3 != X0 | vangle(X1,X5,X3) != vangle(X1,X3,X5) | vf(X1,X5) = vf(X1,X3), inference(clausification, [status(esa)], [ass(cond(proof(385), 0), 2)])). % 40.49/5.66 cnf(c278, plain, vf(vd1352,vd1353) != vf(vd1352,vd1354), inference(clausification, [status(esa)], [negated_conjecture])). % 40.49/5.66 cnf(d0, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1354 != X0 | vd1353 = vd1354 | vd1353 != X1 | vd1352 = vd1354 | vd1352 = vd1353 | vd1352 != X2 | vf(vd1352,vd1353) = vf(vd1352,vd1354) | ~rpoint(X2) | ~rpoint(X0) | ~rpoint(X1) | ~rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(superposition, [status(thm)], [c0,c12])). % 40.49/5.66 cnf(d1, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1352 = vd1354 | vd1353 != X1 | vd1353 = vd1354 | vd1354 != X2 | ~rpoint(X0) | ~rpoint(X1) | ~rpoint(X2) | ~rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c278,d0])). % 40.49/5.66 cnf(d2, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1352 = vd1354 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c1,d1])). % 40.49/5.66 cnf(d3, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c2,d2])). % 40.49/5.66 cnf(d4, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c3,d3])). % 40.49/5.66 cnf(d5, plain, vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(equality_resolution, [status(thm)], [d4])). % 40.49/5.66 cnf(d6, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1354 != X0 | vd1353 != X1 | vd1353 = vd1354 | vd1352 != X2 | vd1352 = vd1354 | vd1352 = vd1353 | vf(vd1352,vd1353) = vf(vd1352,vd1354) | ~rpoint(X1) | ~rpoint(X2) | ~rpoint(X0) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(superposition, [status(thm)], [c0,c10])). % 40.49/5.66 cnf(d7, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1352 = vd1354 | vd1353 != X1 | vd1353 = vd1354 | vd1354 != X2 | ~rpoint(X0) | ~rpoint(X1) | ~rpoint(X2) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c278,d6])). % 40.49/5.66 cnf(d8, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1352 = vd1354 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c1,d7])). % 40.49/5.66 cnf(d9, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c2,d8])). % 40.49/5.66 cnf(d10, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [c3,d9])). % 40.49/5.66 cnf(d11, plain, vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(equality_resolution, [status(thm)], [d10])). % 40.49/5.66 cnf(d12, plain, vd1352 != X0 | vd1353 != X1 | ~rpoint(vd1354) | ~rpoint(X1) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(equality_resolution, [status(thm)], [d11])). % 40.49/5.66 cnf(d13, plain, rpoint(vd1354), inference(demodulation, [status(thm)], [c5,c4])). % 40.49/5.66 cnf(d14, plain, vd1352 != X0 | vd1353 != X1 | ~rpoint(X1) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [d13,d12])). % 40.49/5.66 cnf(d15, plain, vd1352 != X0 | ~rpoint(vd1353) | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(equality_resolution, [status(thm)], [d14])). % 40.49/5.66 cnf(d16, plain, rpoint(vd1353), inference(demodulation, [status(thm)], [c7,c6])). % 40.49/5.66 cnf(d17, plain, vd1352 != X0 | ~rpoint(X0) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [d16,d15])). % 40.49/5.66 cnf(d18, plain, ~rpoint(vd1352) | rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(equality_resolution, [status(thm)], [d17])). % 40.49/5.66 cnf(d19, plain, rpoint(vd1352), inference(demodulation, [status(thm)], [c9,c8])). % 40.49/5.66 cnf(d20, plain, rless(vf(vd1352,vd1353),vf(vd1352,vd1354)) | rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [d19,d18])). % 40.49/5.66 cnf(d21, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 = vd1354 | vd1352 = vd1353 | vd1352 != X0 | vd1354 != X1 | vd1353 = vd1354 | vd1353 != X2 | vf(vd1352,vd1353) = vf(vd1352,vd1354) | ~rpoint(X1) | ~rpoint(X0) | ~rpoint(X2) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(superposition, [status(thm)], [c0,c11])). % 40.49/5.66 cnf(d22, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1352 = vd1354 | vd1353 != X1 | vd1353 = vd1354 | vd1354 != X2 | ~rpoint(X1) | ~rpoint(X2) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [c278,d21])). % 40.49/5.66 cnf(d23, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1352 = vd1354 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [c1,d22])). % 40.49/5.66 cnf(d24, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1352 = vd1353 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [c2,d23])). % 40.49/5.66 cnf(d25, plain, vangle(vd1352,vd1353,vd1354) != vangle(vd1352,vd1353,vd1354) | vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [c3,d24])). % 40.49/5.66 cnf(d26, plain, vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(equality_resolution, [status(thm)], [d25])). % 40.49/5.66 cnf(d27, plain, vd1352 != X0 | vd1353 != X1 | ~rpoint(vd1354) | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(equality_resolution, [status(thm)], [d26])). % 40.49/5.66 cnf(d28, plain, vd1352 != X0 | vd1353 != X1 | ~rpoint(X1) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [d13,d27])). % 40.49/5.66 cnf(d29, plain, vd1352 != X0 | ~rpoint(vd1353) | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(equality_resolution, [status(thm)], [d28])). % 40.49/5.66 cnf(d30, plain, vd1352 != X0 | ~rpoint(X0) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [d16,d29])). % 40.49/5.66 cnf(d31, plain, ~rpoint(vd1352) | ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(equality_resolution, [status(thm)], [d30])). % 40.49/5.66 cnf(d32, plain, ~rless(vf(vd1352,vd1353),vf(vd1352,vd1354)), inference(resolution, [status(thm)], [d19,d31])). % 40.49/5.66 cnf(d33, plain, rless(vf(vd1352,vd1354),vf(vd1352,vd1353)), inference(resolution, [status(thm)], [d32,d20])). % 40.49/5.66 cnf(d34, plain, vd1352 != X0 | vd1353 != X1 | vd1354 != X2 | ~rpoint(X2) | ~rpoint(X1) | ~rpoint(X0), inference(resolution, [status(thm)], [d33,d5])). % 40.49/5.66 cnf(d35, plain, vd1352 != X0 | vd1353 != X1 | ~rpoint(vd1354) | ~rpoint(X1) | ~rpoint(X0), inference(equality_resolution, [status(thm)], [d34])). % 40.49/5.66 cnf(d36, plain, vd1352 != X0 | vd1353 != X1 | ~rpoint(X1) | ~rpoint(X0), inference(resolution, [status(thm)], [d13,d35])). % 40.49/5.66 cnf(d37, plain, vd1352 != X0 | ~rpoint(vd1353) | ~rpoint(X0), inference(equality_resolution, [status(thm)], [d36])). % 40.49/5.66 cnf(d38, plain, vd1352 != X0 | ~rpoint(X0), inference(resolution, [status(thm)], [d16,d37])). % 40.49/5.66 cnf(d39, plain, ~rpoint(vd1352), inference(equality_resolution, [status(thm)], [d38])). % 40.49/5.66 cnf(d40, plain, $false, inference(resolution, [status(thm)], [d19,d39])). % 40.49/5.66 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------