%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM437+5 : 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 : 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 08:12:44 AM UTC 2026 % Result : Theorem 36.43s 5.14s % Output : CNFRefutation 36.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM437+5 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.42 % Computer : n004.cluster.edu % 0.08/0.42 % Model : x86_64 x86_64 % 0.08/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.42 % Memory : 8046.5625MB % 0.08/0.42 % OS : Linux 6.8.0-71-generic % 0.08/0.42 % CPULimit : 300 % 0.08/0.42 % WCLimit : 300 % 0.08/0.42 % DateTime : Sat Sep 26 02:43:22 UTC 2026 % 0.08/0.43 % CPUTime : % 0.08/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 36.43/5.14 % SZS status Theorem for theBenchmark.p % 36.43/5.14 % SZS output start CNFRefutation for theBenchmark.p % 36.43/5.14 fof(m__1750, hypothesis, (aSet0(xS) & ! [X0] : ((aElementOf0(X0,xS) => (aSet0(cS1395) & (! [X1] : ((aElementOf0(X1,cS1395) <=> aInteger0(X1))) & (aSet0(X0) & (! [X1] : ((aElementOf0(X1,X0) => aElementOf0(X1,cS1395))) & (aSubsetOf0(X0,cS1395) & (! [X1] : ((aElementOf0(X1,X0) => ? [X2] : ((aInteger0(X2) & (X2 != sz00 & (aSet0(szAzrzSzezqlpdtcmdtrp0(X1,X2)) & (! [X3] : (((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) => (aInteger0(X3) & (? [X4] : ((aInteger0(X4) & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)))) & (aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1))) & sdteqdtlpzmzozddtrp0(X3,X1,X2))))) & ((aInteger0(X3) & (? [X4] : ((aInteger0(X4) & sdtasdt0(X2,X4) = sdtpldt0(X3,smndt0(X1)))) | (aDivisorOf0(X2,sdtpldt0(X3,smndt0(X1))) | sdteqdtlpzmzozddtrp0(X3,X1,X2)))) => aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2))))) & (! [X3] : ((aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) => aElementOf0(X3,X0))) & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X2),X0))))))))) & isOpen0(X0))))))))))). % 36.43/5.14 fof(m__, conjecture, ((aSet0(sbsmnsldt0(xS)) & ! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) <=> (aInteger0(X0) & ? [X1] : ((aElementOf0(X1,xS) & aElementOf0(X0,X1))))))) => (! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) => ? [X1] : ((aInteger0(X1) & (X1 != sz00 & ((aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) & ! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) & (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) & sdteqdtlpzmzozddtrp0(X2,X0,X1))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) | (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) | sdteqdtlpzmzozddtrp0(X2,X0,X1)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)))))) => (! [X2] : ((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => aElementOf0(X2,sbsmnsldt0(xS)))) | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),sbsmnsldt0(xS))))))))) | isOpen0(sbsmnsldt0(xS))))). % 36.43/5.14 fof(negated_conjecture, negated_conjecture, ~(((aSet0(sbsmnsldt0(xS)) & ! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) <=> (aInteger0(X0) & ? [X1] : ((aElementOf0(X1,xS) & aElementOf0(X0,X1))))))) => (! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) => ? [X1] : ((aInteger0(X1) & (X1 != sz00 & ((aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) & ! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) & (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) & sdteqdtlpzmzozddtrp0(X2,X0,X1))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) | (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) | sdteqdtlpzmzozddtrp0(X2,X0,X1)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)))))) => (! [X2] : ((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => aElementOf0(X2,sbsmnsldt0(xS)))) | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),sbsmnsldt0(xS))))))))) | isOpen0(sbsmnsldt0(xS))))), inference(negate_conjecture, [status(cth)], [m__])). % 36.43/5.14 cnf(c126, plain, ~aElementOf0(X0,xS) | X1(X0), inference(clausification, [status(esa)], [m__1750])). % 36.43/5.14 cnf(c132, plain, ~X0(X1,X2) | aInteger0(sK104(X1,X2)), inference(clausification, [status(esa)], [m__1750])). % 36.43/5.14 cnf(c133, plain, ~X0(X1,X2) | sK104(X1,X2) != sz00, inference(clausification, [status(esa)], [m__1750])). % 36.43/5.14 cnf(c139, plain, ~X0(X1,X2) | ~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X2,sK104(X1,X2))) | aElementOf0(X3,X1), inference(clausification, [status(esa)], [m__1750])). % 36.43/5.14 cnf(c147, plain, ~X0(X1) | ~aElementOf0(X2,X1) | X3(X1,X2), inference(clausification, [status(esa)], [m__1750])). % 36.43/5.14 cnf(c151, plain, ~aElementOf0(X0,sbsmnsldt0(xS)) | aElementOf0(sK114(X0),xS), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c152, plain, ~aElementOf0(X0,sbsmnsldt0(xS)) | aElementOf0(X0,sK114(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c153, plain, aElementOf0(X0,sbsmnsldt0(xS)) | ~aInteger0(X0) | ~aElementOf0(X1,xS) | ~aElementOf0(X0,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c154, plain, aElementOf0(sK116,sbsmnsldt0(xS)), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c155, plain, ~aInteger0(X0) | X0 = sz00 | ~X1(sK116,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c157, plain, ~X0(X1,X2,X3) | aInteger0(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c163, plain, X0(X1,X2) | ~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) | X4(X1,X2,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c167, plain, X0(X1,X2) | aElementOf0(sK121(X1,X2),szAzrzSzezqlpdtcmdtrp0(X1,X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(c168, plain, X0(X1,X2) | ~aElementOf0(sK121(X1,X2),sbsmnsldt0(xS)), inference(clausification, [status(esa)], [negated_conjecture])). % 36.43/5.14 cnf(d0, plain, aElementOf0(sK116,sK114(sK116)), inference(resolution, [status(thm)], [c152,c154])). % 36.43/5.14 cnf(d1, plain, ~'Ts101'(sK114(sK116)) | 'Ts100'(sK114(sK116),sK116), inference(resolution, [status(thm)], [c147,d0])). % 36.43/5.14 cnf(d2, plain, aElementOf0(sK114(sK116),xS), inference(resolution, [status(thm)], [c151,c154])). % 36.43/5.14 cnf(d3, plain, 'Ts101'(sK114(sK116)), inference(resolution, [status(thm)], [c126,d2])). % 36.43/5.14 cnf(d4, plain, 'Ts100'(sK114(sK116),sK116), inference(resolution, [status(thm)], [d3,d1])). % 36.43/5.14 cnf(d5, plain, 'Ts112'(X0,X1) | 'Ts111'(X0,X1,sK121(X0,X1)) | 'Ts112'(X0,X1), inference(resolution, [status(thm)], [c163,c167])). % 36.43/5.14 cnf(d6, plain, 'Ts112'(X0,X1) | aInteger0(sK121(X0,X1)), inference(resolution, [status(thm)], [d5,c157])). % 36.43/5.14 cnf(d7, plain, ~aInteger0(sK121(X0,X1)) | ~aElementOf0(X2,xS) | ~aElementOf0(sK121(X0,X1),X2) | 'Ts112'(X0,X1), inference(resolution, [status(thm)], [c153,c168])). % 36.43/5.14 cnf(d8, plain, aElementOf0(sK121(X0,sK104(X1,X0)),X1) | ~'Ts100'(X1,X0) | 'Ts112'(X0,sK104(X1,X0)), inference(resolution, [status(thm)], [c139,c167])). % 36.43/5.14 cnf(d9, plain, ~'Ts100'(X0,X1) | 'Ts112'(X1,sK104(X0,X1)) | ~aInteger0(sK121(X1,sK104(X0,X1))) | ~aElementOf0(X0,xS) | 'Ts112'(X1,sK104(X0,X1)), inference(resolution, [status(thm)], [d8,d7])). % 36.43/5.14 cnf(d10, plain, ~aElementOf0(X0,xS) | ~'Ts100'(X0,X1) | 'Ts112'(X1,sK104(X0,X1)) | 'Ts112'(X1,sK104(X0,X1)), inference(resolution, [status(thm)], [d9,d6])). % 36.43/5.14 cnf(d11, plain, ~aElementOf0(X0,xS) | ~'Ts100'(X0,sK116) | sK104(X0,sK116) = sz00 | ~aInteger0(sK104(X0,sK116)), inference(resolution, [status(thm)], [d10,c155])). % 36.43/5.14 cnf(d12, plain, sz00 != sz00 | ~'Ts100'(X0,sK116) | ~aInteger0(sK104(X0,sK116)) | ~aElementOf0(X0,xS) | ~'Ts100'(X0,sK116), inference(superposition, [status(thm)], [d11,c133])). % 36.43/5.14 cnf(d13, plain, ~aInteger0(sK104(X0,sK116)) | ~aElementOf0(X0,xS) | ~'Ts100'(X0,sK116), inference(equality_resolution, [status(thm)], [d12])). % 36.43/5.14 cnf(d14, plain, ~aElementOf0(X0,xS) | ~'Ts100'(X0,sK116) | ~'Ts100'(X0,sK116), inference(resolution, [status(thm)], [d13,c132])). % 36.43/5.14 cnf(d15, plain, ~aElementOf0(sK114(sK116),xS), inference(resolution, [status(thm)], [d14,d4])). % 36.43/5.14 cnf(d16, plain, $false, inference(resolution, [status(thm)], [d2,d15])). % 36.43/5.14 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------