%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG106+2 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n002.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:25:54 AM UTC 2026 % Result : Theorem 26.56s 19.13s % Output : CNFRefutation 26.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : RNG106+2 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.10/15.40 % Computer : n002.cluster.edu % 0.10/15.40 % Model : x86_64 x86_64 % 0.10/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/15.40 % Memory : 8046.5625MB % 0.10/15.40 % OS : Linux 6.8.0-71-generic % 0.10/15.40 % CPULimit : 300 % 0.10/15.40 % WCLimit : 300 % 0.10/15.40 % DateTime : Sat Sep 26 06:09:44 UTC 2026 % 0.10/15.40 % CPUTime : % 0.10/15.41 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.56/19.13 % SZS status Theorem for theBenchmark.p % 26.56/19.13 % SZS output start CNFRefutation for theBenchmark.p % 26.56/19.13 fof(mSortsC, axiom, aElement0(sz00)). % 26.56/19.13 fof(m__, conjecture, (! [X0] : ! [X1] : ! [X2] : ((((? [X3] : ((aElement0(X3) & sdtasdt0(xc,X3) = X0)) | aElementOf0(X0,slsdtgt0(xc))) & ((? [X3] : ((aElement0(X3) & sdtasdt0(xc,X3) = X1)) | aElementOf0(X1,slsdtgt0(xc))) & aElement0(X2))) => ? [X3] : ((aElement0(X3) & (sdtasdt0(xc,X3) = X0 & ? [X4] : ((aElement0(X4) & (sdtasdt0(xc,X4) = X1 & (sdtpldt0(X0,X1) = sdtasdt0(xc,sdtpldt0(X3,X4)) & (sdtasdt0(X2,X0) = sdtasdt0(xc,sdtasdt0(X3,X2)) & (? [X5] : ((aElement0(X5) & sdtasdt0(xc,X5) = sdtpldt0(X0,X1))) & (aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc)) & (? [X5] : ((aElement0(X5) & sdtasdt0(xc,X5) = sdtasdt0(X2,X0))) & aElementOf0(sdtasdt0(X2,X0),slsdtgt0(xc))))))))))))))) => ((aSet0(slsdtgt0(xc)) & ! [X0] : ((aElementOf0(X0,slsdtgt0(xc)) <=> ? [X1] : ((aElement0(X1) & sdtasdt0(xc,X1) = X0))))) => (! [X0] : ((aElementOf0(X0,slsdtgt0(xc)) => (! [X1] : ((aElementOf0(X1,slsdtgt0(xc)) => aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc)))) & ! [X1] : ((aElement0(X1) => aElementOf0(sdtasdt0(X1,X0),slsdtgt0(xc))))))) | aIdeal0(slsdtgt0(xc)))))). % 26.56/19.13 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ! [X1] : ! [X2] : ((((? [X3] : ((aElement0(X3) & sdtasdt0(xc,X3) = X0)) | aElementOf0(X0,slsdtgt0(xc))) & ((? [X3] : ((aElement0(X3) & sdtasdt0(xc,X3) = X1)) | aElementOf0(X1,slsdtgt0(xc))) & aElement0(X2))) => ? [X3] : ((aElement0(X3) & (sdtasdt0(xc,X3) = X0 & ? [X4] : ((aElement0(X4) & (sdtasdt0(xc,X4) = X1 & (sdtpldt0(X0,X1) = sdtasdt0(xc,sdtpldt0(X3,X4)) & (sdtasdt0(X2,X0) = sdtasdt0(xc,sdtasdt0(X3,X2)) & (? [X5] : ((aElement0(X5) & sdtasdt0(xc,X5) = sdtpldt0(X0,X1))) & (aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc)) & (? [X5] : ((aElement0(X5) & sdtasdt0(xc,X5) = sdtasdt0(X2,X0))) & aElementOf0(sdtasdt0(X2,X0),slsdtgt0(xc))))))))))))))) => ((aSet0(slsdtgt0(xc)) & ! [X0] : ((aElementOf0(X0,slsdtgt0(xc)) <=> ? [X1] : ((aElement0(X1) & sdtasdt0(xc,X1) = X0))))) => (! [X0] : ((aElementOf0(X0,slsdtgt0(xc)) => (! [X1] : ((aElementOf0(X1,slsdtgt0(xc)) => aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc)))) & ! [X1] : ((aElement0(X1) => aElementOf0(sdtasdt0(X1,X0),slsdtgt0(xc))))))) | aIdeal0(slsdtgt0(xc)))))), inference(negate_conjecture, [status(cth)], [m__])). % 26.56/19.13 cnf(c0, plain, aElement0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 26.56/19.13 cnf(c111, plain, ~aElementOf0(X0,slsdtgt0(xc)) | ~aElementOf0(X1,slsdtgt0(xc)) | ~aElement0(X2) | X3(X0,X1,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c116, plain, aElementOf0(sK115,slsdtgt0(xc)), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c117, plain, aElementOf0(sK116,slsdtgt0(xc)) | aElement0(sK117), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c118, plain, aElementOf0(sK116,slsdtgt0(xc)) | ~aElementOf0(sdtasdt0(sK117,sK115),slsdtgt0(xc)), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c119, plain, ~aElementOf0(sdtpldt0(sK115,sK116),slsdtgt0(xc)) | aElement0(sK117), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c120, plain, ~aElementOf0(sdtpldt0(sK115,sK116),slsdtgt0(xc)) | ~aElementOf0(sdtasdt0(sK117,sK115),slsdtgt0(xc)), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c130, plain, ~X0(X1,X2,X3) | aElementOf0(sdtpldt0(X1,X2),slsdtgt0(xc)), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(c133, plain, ~X0(X1,X2,X3) | aElementOf0(sdtasdt0(X3,X1),slsdtgt0(xc)), inference(clausification, [status(esa)], [negated_conjecture])). % 26.56/19.13 cnf(d0, plain, ~aElement0(X0) | ~aElementOf0(X1,slsdtgt0(xc)) | 'Ts106'(sK115,X1,X0), inference(resolution, [status(thm)], [c111,c116])). % 26.56/19.13 cnf(d1, plain, ~aElement0(X0) | 'Ts106'(sK115,sK115,X0), inference(resolution, [status(thm)], [d0,c116])). % 26.56/19.13 cnf(d2, plain, ~aElementOf0(sdtpldt0(sK115,sK116),slsdtgt0(xc)) | ~'Ts106'(sK115,X0,sK117), inference(resolution, [status(thm)], [c120,c133])). % 26.56/19.13 cnf(d3, plain, ~'Ts106'(sK115,X0,sK117) | ~'Ts106'(sK115,sK116,X1), inference(resolution, [status(thm)], [d2,c130])). % 26.56/19.13 cnf(d4, plain, ~'Ts106'(sK115,X0,sK117) | aElementOf0(sK116,slsdtgt0(xc)), inference(resolution, [status(thm)], [c133,c118])). % 26.56/19.13 cnf(d5, plain, ~aElement0(sK117) | aElementOf0(sK116,slsdtgt0(xc)), inference(resolution, [status(thm)], [d1,d4])). % 26.56/19.13 cnf(d6, plain, ~'Ts106'(sK115,sK116,X0) | aElement0(sK117), inference(resolution, [status(thm)], [c130,c119])). % 26.56/19.13 cnf(d7, plain, ~aElement0(X0) | 'Ts106'(sK115,sK116,X0) | aElement0(sK117), inference(resolution, [status(thm)], [d0,c117])). % 26.56/19.13 cnf(d8, plain, ~aElement0(X0) | aElement0(sK117) | aElement0(sK117), inference(resolution, [status(thm)], [d7,d6])). % 26.56/19.13 cnf(d9, plain, aElement0(sK117), inference(resolution, [status(thm)], [d8,c0])). % 26.56/19.13 cnf(d10, plain, aElementOf0(sK116,slsdtgt0(xc)), inference(resolution, [status(thm)], [d9,d5])). % 26.56/19.13 cnf(d11, plain, ~aElement0(X0) | 'Ts106'(sK115,sK116,X0), inference(resolution, [status(thm)], [d10,d0])). % 26.56/19.13 cnf(d12, plain, ~aElement0(X0) | ~'Ts106'(sK115,X1,sK117), inference(resolution, [status(thm)], [d11,d3])). % 26.56/19.13 cnf(d13, plain, ~aElement0(X0) | ~aElement0(sK117), inference(resolution, [status(thm)], [d12,d1])). % 26.56/19.13 cnf(d14, plain, ~aElement0(X0), inference(resolution, [status(thm)], [d9,d13])). % 26.56/19.13 cnf(d15, plain, $false, inference(resolution, [status(thm)], [d14,c0])). % 26.56/19.13 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------