%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : MED006+1 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n017.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:00:28 AM UTC 2026 % Result : Theorem 13.80s 3.11s % Output : CNFRefutation 13.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MED006+1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n017.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 : Fri Sep 25 23:57:02 UTC 2026 % 0.08/0.35 % CPUTime : % 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 13.80/3.11 % SZS status Theorem for theBenchmark.p % 13.80/3.11 % SZS output start CNFRefutation for theBenchmark.p % 13.80/3.11 fof(irreflexivity_gt, axiom, ! [X0] : ~gt(X0,X0)). % 13.80/3.11 fof(xorcondition3, axiom, ! [X0] : ((~conditionhyper(X0) | ~conditionnormo(X0)))). % 13.80/3.11 fof(liver_glucose, axiom, ! [X0] : ! [X1] : ((~gt(X0,X1) => (uptakelg(X1) => ~releaselg(X1))))). % 13.80/3.11 fof(xorstep6, axiom, ! [X0] : ((~s1(X0) | ~s3(X0)))). % 13.80/3.11 fof(normo, axiom, ! [X0] : ((! [X1] : ((~gt(X0,X1) => conditionnormo(X1))) => ((! [X1] : ((~gt(X0,X1) => bsecretioni(X1))) & (bcapacitysn(X0) & (qilt27(X0) & ! [X1] : ((gt(X0,X1) => conditionhyper(X1)))))) | ((! [X1] : ((~gt(X0,X1) => ~releaselg(X1))) & (bcapacitysn(X0) & (~qilt27(X0) & ! [X1] : ((gt(X0,X1) => conditionhyper(X1)))))) | (((! [X1] : ((~gt(X0,X1) => ~releaselg(X1))) | ! [X1] : ((~gt(X0,X1) => uptakepg(X1)))) & (bcapacityne(X0) & (! [X1] : ((~gt(X0,X1) => bsecretioni(X1))) & ! [X1] : ((gt(X0,X1) => conditionhyper(X1)))))) | (! [X1] : ((~gt(X0,X1) => uptakelg(X1))) & (! [X1] : ((~gt(X0,X1) => uptakepg(X1))) & (bcapacityex(X0) & ! [X1] : ((gt(X0,X1) => conditionhyper(X1)))))))))))). % 13.80/3.11 fof(insulincomp, axiom, ! [X0] : ((drugi(X0) => s3(X0)))). % 13.80/3.11 fof(insulin_completion, axiom, ! [X0] : (((! [X1] : ((~gt(X0,X1) => uptakelg(X1))) | ! [X1] : ((~gt(X0,X1) => uptakepg(X1)))) => ! [X1] : ((~gt(X0,X1) => drugi(X1)))))). % 13.80/3.11 fof(uptake_completion, axiom, ! [X0] : ! [X1] : ((~gt(X0,X1) => (~releaselg(X1) => uptakelg(X1))))). % 13.80/3.11 fof(unsuccessfuls1_qilt27, conjecture, ((s1(n0) & (! [X0] : ((gt(n0,X0) => conditionhyper(X0))) & (~bcapacitysn(n0) & qilt27(n0)))) => ~! [X0] : ((~gt(n0,X0) => conditionnormo(X0))))). % 13.80/3.11 fof(negated_conjecture, negated_conjecture, ~(((s1(n0) & (! [X0] : ((gt(n0,X0) => conditionhyper(X0))) & (~bcapacitysn(n0) & qilt27(n0)))) => ~! [X0] : ((~gt(n0,X0) => conditionnormo(X0))))), inference(negate_conjecture, [status(cth)], [unsuccessfuls1_qilt27])). % 13.80/3.11 cnf(c0, plain, ~gt(X0,X0), inference(clausification, [status(esa)], [irreflexivity_gt])). % 13.80/3.11 cnf(c8, plain, ~conditionhyper(X0) | ~conditionnormo(X0), inference(clausification, [status(esa)], [xorcondition3])). % 13.80/3.11 cnf(c14, plain, gt(X0,X1) | ~uptakelg(X1) | ~releaselg(X1), inference(clausification, [status(esa)], [liver_glucose])). % 13.80/3.11 cnf(c46, plain, ~s1(X0) | ~s3(X0), inference(clausification, [status(esa)], [xorstep6])). % 13.80/3.11 cnf(c48, plain, ~gt(X0,sK56(X0)) | X1(X0), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c49, plain, ~conditionnormo(sK56(X0)) | X1(X0), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c50, plain, gt(X0,X1) | uptakepg(X2) | ~releaselg(X1) | gt(X0,X2) | ~X3(X0), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c53, plain, ~X0(X1) | ~gt(X1,X2) | conditionhyper(X2), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c55, plain, ~X0(X1) | bcapacitysn(X1), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c59, plain, ~X0(X1) | bcapacitysn(X1), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c62, plain, X0(X1) | gt(X1,X2) | X3(X1) | uptakelg(X2) | ~X4(X1) | X5(X1), inference(clausification, [status(esa)], [normo])). % 13.80/3.11 cnf(c76, plain, ~drugi(X0) | s3(X0), inference(clausification, [status(esa)], [insulincomp])). % 13.80/3.11 cnf(c77, plain, ~gt(X0,sK76(X0)) | gt(X0,X1) | drugi(X1), inference(clausification, [status(esa)], [insulin_completion])). % 13.80/3.11 cnf(c78, plain, ~uptakelg(sK76(X0)) | gt(X0,X1) | drugi(X1), inference(clausification, [status(esa)], [insulin_completion])). % 13.80/3.11 cnf(c79, plain, ~gt(X0,sK77(X0)) | gt(X0,X1) | drugi(X1), inference(clausification, [status(esa)], [insulin_completion])). % 13.80/3.11 cnf(c80, plain, ~uptakepg(sK77(X0)) | gt(X0,X1) | drugi(X1), inference(clausification, [status(esa)], [insulin_completion])). % 13.80/3.11 cnf(c81, plain, gt(X0,X1) | releaselg(X1) | uptakelg(X1), inference(clausification, [status(esa)], [uptake_completion])). % 13.80/3.11 cnf(c99, plain, s1(n0), inference(clausification, [status(esa)], [negated_conjecture])). % 13.80/3.11 cnf(c100, plain, ~gt(n0,X0) | conditionhyper(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 13.80/3.11 cnf(c101, plain, ~bcapacitysn(n0), inference(clausification, [status(esa)], [negated_conjecture])). % 13.80/3.11 cnf(c103, plain, gt(n0,X0) | conditionnormo(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 13.80/3.11 cnf(d0, plain, uptakelg(X0) | releaselg(X0) | conditionhyper(X0), inference(resolution, [status(thm)], [c81,c100])). % 13.80/3.11 cnf(d1, plain, conditionhyper(sK76(X0)) | releaselg(sK76(X0)) | gt(X0,X1) | drugi(X1), inference(resolution, [status(thm)], [d0,c78])). % 13.80/3.11 cnf(d2, plain, conditionhyper(sK76(n0)) | drugi(X0) | releaselg(sK76(n0)) | conditionhyper(X0), inference(resolution, [status(thm)], [d1,c100])). % 13.80/3.11 cnf(d3, plain, gt(n0,X0) | drugi(X0) | conditionnormo(sK76(n0)), inference(resolution, [status(thm)], [c77,c103])). % 13.80/3.11 cnf(d4, plain, conditionnormo(sK76(n0)) | drugi(X0) | conditionhyper(X0), inference(resolution, [status(thm)], [d3,c100])). % 13.80/3.11 cnf(d5, plain, conditionhyper(X0) | conditionnormo(sK76(n0)) | s3(X0), inference(resolution, [status(thm)], [d4,c76])). % 13.80/3.11 cnf(d6, plain, conditionhyper(X0) | conditionnormo(sK76(n0)) | ~s1(X0), inference(resolution, [status(thm)], [d5,c46])). % 13.80/3.11 cnf(d7, plain, conditionhyper(n0) | conditionnormo(sK76(n0)), inference(resolution, [status(thm)], [d6,c99])). % 13.80/3.11 cnf(d8, plain, conditionnormo(n0), inference(resolution, [status(thm)], [c103,c0])). % 13.80/3.11 cnf(d9, plain, ~conditionhyper(n0), inference(resolution, [status(thm)], [c8,d8])). % 13.80/3.11 cnf(d10, plain, conditionnormo(sK76(n0)), inference(resolution, [status(thm)], [d9,d7])). % 13.80/3.11 cnf(d11, plain, ~conditionhyper(sK76(n0)), inference(resolution, [status(thm)], [d10,c8])). % 13.80/3.11 cnf(d12, plain, conditionhyper(X0) | drugi(X0) | releaselg(sK76(n0)), inference(resolution, [status(thm)], [d11,d2])). % 13.80/3.11 cnf(d13, plain, conditionhyper(X0) | releaselg(sK76(n0)) | s3(X0), inference(resolution, [status(thm)], [d12,c76])). % 13.80/3.11 cnf(d14, plain, conditionhyper(X0) | releaselg(sK76(n0)) | ~s1(X0), inference(resolution, [status(thm)], [d13,c46])). % 13.80/3.11 cnf(d15, plain, conditionhyper(n0) | releaselg(sK76(n0)), inference(resolution, [status(thm)], [d14,c99])). % 13.80/3.11 cnf(d16, plain, releaselg(sK76(n0)), inference(resolution, [status(thm)], [d9,d15])). % 13.80/3.11 cnf(d17, plain, conditionhyper(X0) | ~'Ts51'(X1) | gt(X1,X2) | uptakepg(X2) | ~releaselg(X0) | ~'Ts51'(X1), inference(resolution, [status(thm)], [c53,c50])). % 13.80/3.11 cnf(d18, plain, uptakelg(X0) | ~'Ts54'(n0) | 'Ts51'(n0) | 'Ts52'(n0) | 'Ts53'(n0) | conditionhyper(X0), inference(resolution, [status(thm)], [c62,c100])). % 13.80/3.11 cnf(d19, plain, 'Ts54'(n0) | conditionnormo(sK56(n0)), inference(resolution, [status(thm)], [c48,c103])). % 13.80/3.11 cnf(d20, plain, 'Ts54'(n0) | 'Ts54'(n0), inference(resolution, [status(thm)], [c49,d19])). % 13.80/3.11 cnf(d21, plain, conditionhyper(X0) | uptakelg(X0) | 'Ts51'(n0) | 'Ts52'(n0) | 'Ts53'(n0), inference(resolution, [status(thm)], [d20,d18])). % 13.80/3.11 cnf(d22, plain, ~uptakelg(X0) | ~releaselg(X0), inference(resolution, [status(thm)], [c14,c0])). % 13.80/3.11 cnf(d23, plain, ~uptakelg(sK76(n0)), inference(resolution, [status(thm)], [d16,d22])). % 13.80/3.11 cnf(d24, plain, conditionhyper(sK76(n0)) | 'Ts51'(n0) | 'Ts52'(n0) | 'Ts53'(n0), inference(resolution, [status(thm)], [d23,d21])). % 13.80/3.11 cnf(d25, plain, 'Ts51'(n0) | 'Ts52'(n0) | 'Ts53'(n0), inference(resolution, [status(thm)], [d11,d24])). % 13.80/3.11 cnf(d26, plain, 'Ts51'(n0) | 'Ts52'(n0) | bcapacitysn(n0), inference(resolution, [status(thm)], [d25,c59])). % 13.80/3.11 cnf(d27, plain, 'Ts51'(n0) | 'Ts52'(n0), inference(resolution, [status(thm)], [c101,d26])). % 13.80/3.11 cnf(d28, plain, 'Ts51'(n0) | bcapacitysn(n0), inference(resolution, [status(thm)], [d27,c55])). % 13.80/3.11 cnf(d29, plain, 'Ts51'(n0), inference(resolution, [status(thm)], [c101,d28])). % 13.80/3.11 cnf(d30, plain, gt(n0,X0) | conditionhyper(X1) | uptakepg(X0) | ~releaselg(X1), inference(resolution, [status(thm)], [d29,d17])). % 13.80/3.11 cnf(d31, plain, gt(n0,X0) | conditionhyper(sK76(n0)) | uptakepg(X0), inference(resolution, [status(thm)], [d30,d16])). % 13.80/3.11 cnf(d32, plain, gt(n0,X0) | uptakepg(X0), inference(resolution, [status(thm)], [d11,d31])). % 13.80/3.11 cnf(d33, plain, uptakepg(sK77(n0)) | gt(n0,X0) | drugi(X0), inference(resolution, [status(thm)], [d32,c79])). % 13.80/3.11 cnf(d34, plain, uptakepg(sK77(n0)) | drugi(n0), inference(resolution, [status(thm)], [d33,c0])). % 13.80/3.11 cnf(d35, plain, drugi(n0) | gt(n0,X0) | drugi(X0), inference(resolution, [status(thm)], [d34,c80])). % 13.80/3.11 cnf(d36, plain, drugi(n0) | drugi(n0), inference(resolution, [status(thm)], [d35,c0])). % 13.80/3.11 cnf(d37, plain, s3(n0), inference(resolution, [status(thm)], [d36,c76])). % 13.80/3.11 cnf(d38, plain, ~s1(n0), inference(resolution, [status(thm)], [d37,c46])). % 13.80/3.11 cnf(d39, plain, $false, inference(resolution, [status(thm)], [c99,d38])). % 13.80/3.11 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------