%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM455+6 : TPTP v9.3.1. Released v4.0.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 08:12:47 AM UTC 2026 % Result : Theorem 26.62s 4.21s % Output : CNFRefutation 26.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM455+6 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n014.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 26 02:49:16 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 26.62/4.21 % SZS status Theorem for theBenchmark.p % 26.62/4.21 % SZS output start CNFRefutation for theBenchmark.p % 26.62/4.21 fof(mIntOne, axiom, aInteger0(sz10)). % 26.62/4.21 fof(mIntPlus, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => aInteger0(sdtpldt0(X0,X1))))). % 26.62/4.21 fof(m__2171, hypothesis, (aInteger0(xp) & (xp != sz00 & (aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)) & (! [X0] : (((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) => (aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)))) & (aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))) & sdteqdtlpzmzozddtrp0(X0,sz10,xp))))) & ((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))) | sdteqdtlpzmzozddtrp0(X0,sz10,xp)))) => aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))) & (aSet0(sbsmnsldt0(xS)) & (! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) <=> (aInteger0(X0) & ? [X1] : ((aElementOf0(X1,xS) & aElementOf0(X0,X1)))))) & (! [X0] : ((aElementOf0(X0,stldt0(sbsmnsldt0(xS))) <=> (aInteger0(X0) & ~aElementOf0(X0,sbsmnsldt0(xS))))) & (! [X0] : ((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) => aElementOf0(X0,stldt0(sbsmnsldt0(xS))))) & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))))))))))). % 26.62/4.22 fof(m__2232, hypothesis, (? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))) & (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))) & (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp) & (aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) & (? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))) & (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))) & (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp) & aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)))))))))). % 26.62/4.22 fof(m__2258, hypothesis, (sdtpldt0(sz10,xp) != sz10 & sdtpldt0(sz10,smndt0(xp)) != sz10)). % 26.62/4.22 fof(m__2286, hypothesis, (sdtpldt0(sz10,xp) != smndt0(sz10) | sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10))). % 26.62/4.22 fof(m__, conjecture, ? [X0] : ((((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))) | sdteqdtlpzmzozddtrp0(X0,sz10,xp)))) | aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))) & ~(((X0 = sz10 | X0 = smndt0(sz10)) & aElementOf0(X0,cS2200)))))). % 26.62/4.22 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))) | sdteqdtlpzmzozddtrp0(X0,sz10,xp)))) | aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))) & ~(((X0 = sz10 | X0 = smndt0(sz10)) & aElementOf0(X0,cS2200))))), inference(negate_conjecture, [status(cth)], [m__])). % 26.62/4.22 cnf(c1, plain, aInteger0(sz10), inference(clausification, [status(esa)], [mIntOne])). % 26.62/4.22 cnf(c3, plain, ~aInteger0(X0) | ~aInteger0(X1) | aInteger0(sdtpldt0(X0,X1)), inference(clausification, [status(esa)], [mIntPlus])). % 26.62/4.22 cnf(c224, plain, aInteger0(xp), inference(clausification, [status(esa)], [m__2171])). % 26.62/4.22 cnf(c247, plain, sdtasdt0(xp,sK160) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)), inference(clausification, [status(esa)], [m__2232])). % 26.62/4.22 cnf(c248, plain, aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))), inference(clausification, [status(esa)], [m__2232])). % 26.62/4.22 cnf(c255, plain, aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)), inference(clausification, [status(esa)], [m__2232])). % 26.62/4.22 cnf(c256, plain, sdtpldt0(sz10,xp) != sz10, inference(clausification, [status(esa)], [m__2258])). % 26.62/4.22 cnf(c257, plain, sdtpldt0(sz10,smndt0(xp)) != sz10, inference(clausification, [status(esa)], [m__2258])). % 26.62/4.22 cnf(c258, plain, sdtpldt0(sz10,xp) != smndt0(sz10) | sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10), inference(clausification, [status(esa)], [m__2286])). % 26.62/4.22 cnf(c259, plain, ~X0(X1) | X1 = sz10 | X1 = smndt0(sz10), inference(clausification, [status(esa)], [negated_conjecture])). % 26.62/4.22 cnf(c262, plain, X0(X1) | ~aInteger0(X1) | ~aDivisorOf0(xp,sdtpldt0(X1,smndt0(sz10))), inference(clausification, [status(esa)], [negated_conjecture])). % 26.62/4.22 cnf(c264, plain, X0(X1) | ~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(sz10,xp)), inference(clausification, [status(esa)], [negated_conjecture])). % 26.62/4.22 cnf(d0, plain, ~aDivisorOf0(xp,sdtasdt0(xp,sK160)) | ~aInteger0(sdtpldt0(sz10,xp)) | 'Ts162'(sdtpldt0(sz10,xp)), inference(superposition, [status(thm)], [c247,c262])). % 26.62/4.22 cnf(d1, plain, aDivisorOf0(xp,sdtasdt0(xp,sK160)), inference(demodulation, [status(thm)], [c248,c247])). % 26.62/4.22 cnf(d2, plain, ~aInteger0(sdtpldt0(sz10,xp)) | 'Ts162'(sdtpldt0(sz10,xp)), inference(resolution, [status(thm)], [d1,d0])). % 26.62/4.22 cnf(d3, plain, 'Ts162'(sdtpldt0(sz10,xp)) | ~aInteger0(sz10) | ~aInteger0(xp), inference(resolution, [status(thm)], [d2,c3])). % 26.62/4.22 cnf(d4, plain, ~aInteger0(xp) | 'Ts162'(sdtpldt0(sz10,xp)), inference(resolution, [status(thm)], [c1,d3])). % 26.62/4.22 cnf(d5, plain, 'Ts162'(sdtpldt0(sz10,xp)), inference(resolution, [status(thm)], [c224,d4])). % 26.62/4.22 cnf(d6, plain, sdtpldt0(sz10,xp) = sz10 | sdtpldt0(sz10,xp) = smndt0(sz10), inference(resolution, [status(thm)], [d5,c259])). % 26.62/4.22 cnf(d7, plain, sdtpldt0(sz10,xp) = smndt0(sz10), inference(resolution, [status(thm)], [c256,d6])). % 26.62/4.22 cnf(d8, plain, sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) | smndt0(sz10) != smndt0(sz10), inference(demodulation, [status(thm)], [c258,d7])). % 26.62/4.22 cnf(d9, plain, 'Ts162'(sdtpldt0(sz10,smndt0(xp))), inference(resolution, [status(thm)], [c255,c264])). % 26.62/4.22 cnf(d10, plain, sdtpldt0(sz10,smndt0(xp)) = sz10 | sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10), inference(resolution, [status(thm)], [d9,c259])). % 26.62/4.22 cnf(d11, plain, sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10), inference(resolution, [status(thm)], [c257,d10])). % 26.62/4.22 cnf(d12, plain, smndt0(sz10) != smndt0(sz10), inference(resolution, [status(thm)], [d11,d8])). % 26.62/4.22 cnf(d13, plain, $false, inference(equality_resolution, [status(thm)], [d12])). % 26.62/4.22 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------