%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM444+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 : n011.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:45 AM UTC 2026 % Result : Theorem 40.20s 20.19s % Output : CNFRefutation 40.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM444+6 : 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.09/10.43 % Computer : n011.cluster.edu % 0.09/10.43 % Model : x86_64 x86_64 % 0.09/10.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/10.43 % Memory : 8046.5625MB % 0.09/10.43 % OS : Linux 6.8.0-71-generic % 0.09/10.43 % CPULimit : 300 % 0.09/10.43 % WCLimit : 300 % 0.09/10.43 % DateTime : Sat Sep 26 02:45:54 UTC 2026 % 0.09/10.43 % CPUTime : % 0.09/10.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 40.20/20.19 % SZS status Theorem for theBenchmark.p % 40.20/20.19 % SZS output start CNFRefutation for theBenchmark.p % 40.20/20.19 fof(m__1962, hypothesis, (aInteger0(xa) & (aInteger0(xq) & xq != sz00))). % 40.20/20.19 fof(m__, conjecture, (! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => ((((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) & ! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X2,xa,xq))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X2,xa,xq)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))) => (~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) | aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))) & (? [X2] : ((aInteger0(X2) & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(X0)))) | (aDivisorOf0(xq,sdtpldt0(X1,smndt0(X0))) | sdteqdtlpzmzozddtrp0(X1,X0,xq)))) => (aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) & (! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X2,xa,xq))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X2,xa,xq)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))))) & (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) & aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))))) => (((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) & ! [X0] : (((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X0,xa,xq))))) & ((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X0,xa,xq)))) => aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))) => ((aSet0(cS1395) & ! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0)))) => (! [X0] : ((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => aElementOf0(X0,cS1395))) | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))) & (! [X0] : (((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X0,xa,xq))))) & ((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X0,xa,xq)))) => aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq))))) => (((aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) & ! [X0] : ((aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) <=> (aInteger0(X0) & ~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))) => (! [X0] : ((aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) => ? [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,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))) | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))))))) | isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))) | isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))). % 40.20/20.19 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => ((((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) & ! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X2,xa,xq))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X2,xa,xq)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))) => (~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) | aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))) & (? [X2] : ((aInteger0(X2) & sdtasdt0(xq,X2) = sdtpldt0(X1,smndt0(X0)))) | (aDivisorOf0(xq,sdtpldt0(X1,smndt0(X0))) | sdteqdtlpzmzozddtrp0(X1,X0,xq)))) => (aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) & (! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X2,xa,xq))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(xq,X3) = sdtpldt0(X2,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X2,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X2,xa,xq)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(xa,xq))))) & (~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) & aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))))) => (((aSet0(szAzrzSzezqlpdtcmdtrp0(xa,xq)) & ! [X0] : (((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X0,xa,xq))))) & ((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X0,xa,xq)))) => aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))) => ((aSet0(cS1395) & ! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0)))) => (! [X0] : ((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => aElementOf0(X0,cS1395))) | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(xa,xq),cS1395)))) & (! [X0] : (((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)) => (aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) & (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) & sdteqdtlpzmzozddtrp0(X0,xa,xq))))) & ((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xq,X1) = sdtpldt0(X0,smndt0(xa)))) | (aDivisorOf0(xq,sdtpldt0(X0,smndt0(xa))) | sdteqdtlpzmzozddtrp0(X0,xa,xq)))) => aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq))))) => (((aSet0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) & ! [X0] : ((aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) <=> (aInteger0(X0) & ~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(xa,xq)))))) => (! [X0] : ((aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) => ? [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,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))) | aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq)))))))))) | isOpen0(stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))) | isClosed0(szAzrzSzezqlpdtcmdtrp0(xa,xq))))))), inference(negate_conjecture, [status(cth)], [m__])). % 40.20/20.19 cnf(c132, plain, aInteger0(xq), inference(clausification, [status(esa)], [m__1962])). % 40.20/20.19 cnf(c133, plain, xq != sz00, inference(clausification, [status(esa)], [m__1962])). % 40.20/20.19 cnf(c136, plain, ~X0(X1) | X2(X3) | ~sdteqdtlpzmzozddtrp0(X3,X1,xq) | ~aInteger0(X3) | ~aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c137, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c149, plain, X0(X1) | ~aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c161, plain, ~X0(X1) | aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c162, plain, ~X0(X1) | aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c172, plain, ~X0(X1,X2,X3) | aInteger0(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c176, plain, ~X0(X1,X2,X3) | sdteqdtlpzmzozddtrp0(X3,X1,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c178, plain, X0(X1,X2) | ~aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X1,X2)) | X4(X1,X2,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c182, plain, X0(X1,X2) | aElementOf0(sK131(X1,X2),szAzrzSzezqlpdtcmdtrp0(X1,X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c183, plain, X0(X1,X2) | ~aElementOf0(sK131(X1,X2),stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c190, plain, X0 | ~aElementOf0(X1,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))) | aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c193, plain, X0 | aElementOf0(sK135,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c194, plain, X0 | ~aInteger0(X1) | X1 = sz00 | ~X2(sK135,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c198, plain, X0 | ~aElementOf0(X1,szAzrzSzezqlpdtcmdtrp0(xa,xq)) | X2(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c204, plain, X0 | aElementOf0(X1,cS1395) | ~aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c205, plain, X0 | aElementOf0(sK140,szAzrzSzezqlpdtcmdtrp0(xa,xq)), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(c206, plain, X0 | ~aElementOf0(sK140,cS1395), inference(clausification, [status(esa)], [negated_conjecture])). % 40.20/20.19 cnf(d0, plain, ~aInteger0(sK140) | 'Ts116' | 'Ts116', inference(resolution, [status(thm)], [c204,c206])). % 40.20/20.19 cnf(d1, plain, 'Ts116' | 'Ts111'(sK140) | 'Ts116', inference(resolution, [status(thm)], [c198,c205])). % 40.20/20.19 cnf(d2, plain, 'Ts116' | aInteger0(sK140), inference(resolution, [status(thm)], [d1,c162])). % 40.20/20.19 cnf(d3, plain, 'Ts116' | 'Ts116', inference(resolution, [status(thm)], [d2,d0])). % 40.20/20.19 cnf(d4, plain, ~'Ts115', inference(resolution, [status(thm)], [d3,c137])). % 40.20/20.19 cnf(d5, plain, X0 = sz00 | ~aInteger0(X0) | ~'Ts114'(sK135,X0), inference(resolution, [status(thm)], [d4,c194])). % 40.20/20.19 cnf(d6, plain, 'Ts114'(X0,X1) | ~'Ts110'(sK131(X0,X1)), inference(resolution, [status(thm)], [c183,c161])). % 40.20/20.19 cnf(d7, plain, 'Ts113'(X0,X1,sK131(X0,X1)) | 'Ts114'(X0,X1) | 'Ts114'(X0,X1), inference(resolution, [status(thm)], [c178,c182])). % 40.20/20.19 cnf(d8, plain, 'Ts114'(X0,X1) | aInteger0(sK131(X0,X1)), inference(resolution, [status(thm)], [d7,c172])). % 40.20/20.19 cnf(d9, plain, 'Ts114'(X0,X1) | sdteqdtlpzmzozddtrp0(sK131(X0,X1),X0,X1), inference(resolution, [status(thm)], [d7,c176])). % 40.20/20.19 cnf(d10, plain, 'Ts114'(X0,xq) | ~aInteger0(X0) | ~aInteger0(sK131(X0,xq)) | ~'Ts108'(X0) | 'Ts110'(sK131(X0,xq)), inference(resolution, [status(thm)], [d9,c136])). % 40.20/20.19 cnf(d11, plain, ~aInteger0(X0) | ~'Ts108'(X0) | 'Ts110'(sK131(X0,xq)) | 'Ts114'(X0,xq) | 'Ts114'(X0,xq), inference(resolution, [status(thm)], [d10,d8])). % 40.20/20.19 cnf(d12, plain, ~aInteger0(X0) | ~'Ts108'(X0) | 'Ts114'(X0,xq) | 'Ts114'(X0,xq), inference(resolution, [status(thm)], [d11,d6])). % 40.20/20.19 cnf(d13, plain, ~aInteger0(sK135) | ~'Ts108'(sK135) | xq = sz00 | ~aInteger0(xq), inference(resolution, [status(thm)], [d12,d5])). % 40.20/20.19 cnf(d14, plain, 'Ts108'(sK135) | 'Ts115', inference(resolution, [status(thm)], [c149,c193])). % 40.20/20.19 cnf(d15, plain, 'Ts108'(sK135), inference(resolution, [status(thm)], [d4,d14])). % 40.20/20.19 cnf(d16, plain, xq = sz00 | ~aInteger0(xq) | ~aInteger0(sK135), inference(resolution, [status(thm)], [d15,d13])). % 40.20/20.19 cnf(d17, plain, aElementOf0(sK135,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))), inference(resolution, [status(thm)], [d4,c193])). % 40.20/20.19 cnf(d18, plain, aInteger0(X0) | ~aElementOf0(X0,stldt0(szAzrzSzezqlpdtcmdtrp0(xa,xq))), inference(resolution, [status(thm)], [d4,c190])). % 40.20/20.19 cnf(d19, plain, aInteger0(sK135), inference(resolution, [status(thm)], [d18,d17])). % 40.20/20.19 cnf(d20, plain, xq = sz00 | ~aInteger0(xq), inference(resolution, [status(thm)], [d19,d16])). % 40.20/20.19 cnf(d21, plain, xq = sz00, inference(resolution, [status(thm)], [c132,d20])). % 40.20/20.19 cnf(d22, plain, $false, inference(resolution, [status(thm)], [c133,d21])). % 40.20/20.19 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------