%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV666+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:49:02 AM UTC 2026
% Result : Theorem 30.85s 5.50s
% Output : CNFRefutation 30.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEV666+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sat Sep 26 11:34:20 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.85/5.50 % SZS status Theorem for theBenchmark.p
% 30.85/5.50 % SZS output start CNFRefutation for theBenchmark.p
% 30.85/5.50 fof($_def_QuicksortComplexity.monads.extMonad, axiom, ! [X0] : (('cQuicksortComplexity$u2emonads$u2eextMonad$u$u$u24a1'(X0) <=> ! [X1] : (('cType$u$u$u24t'(X1) => ! [X2] : (('cType$u$u$u24t'(X2) => ! [X3] : (('c$u24$u$utype$u$u759$u$u$u24t'(X0,X1,X2,X3) => ! [X4] : (('c$u24$u$utype$u$u759$u$u$u24t'(X0,X1,X2,X4) => ('cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(X1,'cQuicksortComplexity$u2emonads$u2emon$u$u$u24a2'(X0,X2),X3,X4) => ! [X5] : (('cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(X0,X1,X5) => 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(X0,X1,X2,X5,X3) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(X0,X1,X2,X5,X4))))))))))))))).
% 30.85/5.50 fof($_type_176660, axiom, ! [X0] : (('c$u24$u$utype$u$u176660$u$u$u24t'(X0) <=> ! [X1] : (('cA$u$u$u24t'(X1) => 'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cB,happ(X0,X1))))))).
% 30.85/5.50 fof($_type_759, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$u24$u$utype$u$u759$u$u$u24t'(X0,X1,X2,X3) <=> ! [X4] : ((t(X4,X1) => 'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(X0,X2,happ(X3,X4))))))).
% 30.85/5.50 fof($_typeof_A, axiom, 'cType$u$u$u24t'(cA)).
% 30.85/5.50 fof($_typeof_B, axiom, 'cType$u$u$u24t'(cB)).
% 30.85/5.50 fof($_typeof_f, axiom, 'c$u24$u$utype$u$u176660$u$u$u24t'(cf)).
% 30.85/5.50 fof($_typeof_g, axiom, 'c$u24$u$utype$u$u176660$u$u$u24t'(cg)).
% 30.85/5.50 fof($_typeof_m, axiom, 'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,cm)).
% 30.85/5.50 fof(e, axiom, 'cQuicksortComplexity$u2emonads$u2eextMonad$u$u$u24a1'(cM)).
% 30.85/5.50 fof($tdef_A, axiom, ! [X0] : (('cA$u$u$u24t'(X0) <=> t(X0,cA)))).
% 30.85/5.50 fof(_HAMMER_GOAL, conjecture, (cm = cn => ('cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(cA,'cQuicksortComplexity$u2emonads$u2emon$u$u$u24a2'(cM,cB),cf,cg) => 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cn,cg)))).
% 30.85/5.50 fof(negated_conjecture, negated_conjecture, ~((cm = cn => ('cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(cA,'cQuicksortComplexity$u2emonads$u2emon$u$u$u24a2'(cM,cB),cf,cg) => 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cn,cg)))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 30.85/5.50 cnf(c8, plain, ~'cQuicksortComplexity$u2emonads$u2eextMonad$u$u$u24a1'(X0) | X1(X0), inference(clausification, [status(esa)], [$_def_QuicksortComplexity.monads.extMonad])).
% 30.85/5.50 cnf(c10, plain, ~'cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(X0,'cQuicksortComplexity$u2emonads$u2emon$u$u$u24a2'(X1,X2),X3,X4) | 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(X1,X0,X2,X5,X3) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(X1,X0,X2,X5,X4) | ~'cType$u$u$u24t'(X2) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(X1,X0,X5) | ~X6(X1) | ~'c$u24$u$utype$u$u759$u$u$u24t'(X1,X0,X2,X4) | ~'cType$u$u$u24t'(X0) | ~'c$u24$u$utype$u$u759$u$u$u24t'(X1,X0,X2,X3), inference(clausification, [status(esa)], [$_def_QuicksortComplexity.monads.extMonad])).
% 30.85/5.50 cnf(c37, plain, ~'c$u24$u$utype$u$u176660$u$u$u24t'(X0) | ~'cA$u$u$u24t'(X1) | 'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cB,happ(X0,X1)), inference(clausification, [status(esa)], [$_type_176660])).
% 30.85/5.50 cnf(c44, plain, 'c$u24$u$utype$u$u759$u$u$u24t'(X0,X1,X2,X3) | t(sK64(X0,X1,X2,X3),X1), inference(clausification, [status(esa)], [$_type_759])).
% 30.85/5.50 cnf(c45, plain, 'c$u24$u$utype$u$u759$u$u$u24t'(X0,X1,X2,X3) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(X0,X2,happ(X3,sK64(X0,X1,X2,X3))), inference(clausification, [status(esa)], [$_type_759])).
% 30.85/5.50 cnf(c46, plain, 'cType$u$u$u24t'(cA), inference(clausification, [status(esa)], [$_typeof_A])).
% 30.85/5.50 cnf(c47, plain, 'cType$u$u$u24t'(cB), inference(clausification, [status(esa)], [$_typeof_B])).
% 30.85/5.50 cnf(c49, plain, 'c$u24$u$utype$u$u176660$u$u$u24t'(cf), inference(clausification, [status(esa)], [$_typeof_f])).
% 30.85/5.50 cnf(c50, plain, 'c$u24$u$utype$u$u176660$u$u$u24t'(cg), inference(clausification, [status(esa)], [$_typeof_g])).
% 30.85/5.50 cnf(c51, plain, 'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,cm), inference(clausification, [status(esa)], [$_typeof_m])).
% 30.85/5.50 cnf(c67, plain, 'cQuicksortComplexity$u2emonads$u2eextMonad$u$u$u24a1'(cM), inference(clausification, [status(esa)], [e])).
% 30.85/5.50 cnf(c73, plain, 'cA$u$u$u24t'(X0) | ~t(X0,cA), inference(clausification, [status(esa)], [$tdef_A])).
% 30.85/5.50 cnf(c74, plain, cm = cn, inference(clausification, [status(esa)], [negated_conjecture])).
% 30.85/5.50 cnf(c75, plain, 'cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(cA,'cQuicksortComplexity$u2emonads$u2emon$u$u$u24a2'(cM,cB),cf,cg), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.85/5.50 cnf(c76, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) != 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cn,cg), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.85/5.50 cnf(d0, plain, 'c$u24$u$utype$u$u759$u$u$u24t'(X0,cA,X1,X2) | 'cA$u$u$u24t'(sK64(X0,cA,X1,X2)), inference(resolution, [status(thm)], [c44,c73])).
% 30.85/5.50 cnf(d1, plain, 'c$u24$u$utype$u$u759$u$u$u24t'(cM,X0,cB,X1) | ~'cA$u$u$u24t'(sK64(cM,X0,cB,X1)) | ~'c$u24$u$utype$u$u176660$u$u$u24t'(X1), inference(resolution, [status(thm)], [c45,c37])).
% 30.85/5.50 cnf(d2, plain, 'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,X0) | ~'c$u24$u$utype$u$u176660$u$u$u24t'(X0) | 'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,X0), inference(resolution, [status(thm)], [d1,d0])).
% 30.85/5.50 cnf(d3, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'cType$u$u$u24t'(cA) | ~'cType$u$u$u24t'(cB) | ~'Ts10'(cM) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cg) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c10,c75])).
% 30.85/5.50 cnf(d4, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'cType$u$u$u24t'(cB) | ~'Ts10'(cM) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cg) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c46,d3])).
% 30.85/5.50 cnf(d5, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'Ts10'(cM) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cg) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c47,d4])).
% 30.85/5.50 cnf(d6, plain, 'Ts10'(cM), inference(resolution, [status(thm)], [c8,c67])).
% 30.85/5.50 cnf(d7, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cg) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [d6,d5])).
% 30.85/5.50 cnf(d8, plain, ~'c$u24$u$utype$u$u176660$u$u$u24t'(cg) | 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cf) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [d2,d7])).
% 30.85/5.50 cnf(d9, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'c$u24$u$utype$u$u759$u$u$u24t'(cM,cA,cB,cf) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c50,d8])).
% 30.85/5.50 cnf(d10, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0) | ~'c$u24$u$utype$u$u176660$u$u$u24t'(cf), inference(resolution, [status(thm)], [d9,d2])).
% 30.85/5.50 cnf(d11, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'cQuicksortComplexity$u2emonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c49,d10])).
% 30.85/5.50 cnf(d12, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) = 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cg), inference(resolution, [status(thm)], [d11,c51])).
% 30.85/5.50 cnf(d13, plain, 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) != 'cQuicksortComplexity$u2emonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cg), inference(demodulation, [status(thm)], [c76,c74])).
% 30.85/5.50 cnf(d14, plain, $false, inference(resolution, [status(thm)], [d13,d12])).
% 30.85/5.50 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------