%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV660+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:01 AM UTC 2026
% Result : Theorem 67.93s 12.84s
% Output : CNFRefutation 67.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV660+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n016.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 11:37:47 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.93/12.84 % SZS status Theorem for theBenchmark.p
% 67.93/12.84 % SZS output start CNFRefutation for theBenchmark.p
% 67.93/12.84 fof($_def_monads.extMonad, axiom, ! [X0] : (('cmonads$u2eextMonad$u$u$u24a1'(X0) <=> ! [X1] : (('cType$u$u$u24t'(X1) => ! [X2] : (('cType$u$u$u24t'(X2) => ! [X3] : (('c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X3) => ! [X4] : (('c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X4) => ('cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(X1,'cmonads$u2emon$u$u$u24a2'(X0,X2),X3,X4) => ! [X5] : (('cmonads$u2emon$u$u$u24t'(X0,X1,X5) => 'cmonads$u2ebind$u$u$u24a5'(X0,X1,X2,X5,X3) = 'cmonads$u2ebind$u$u$u24a5'(X0,X1,X2,X5,X4))))))))))))))).
% 67.93/12.84 fof($_type_1, axiom, ! [X0] : (('c$u24$u$utype$u$u1$u$u$u24t'(X0) <=> ! [X1] : (('cA$u$u$u24t'(X1) => 'cmonads$u2emon$u$u$u24t'(cM,cB,happ(X0,X1))))))).
% 67.93/12.84 fof($_type_172, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X3) <=> ! [X4] : ((t(X4,X1) => 'cmonads$u2emon$u$u$u24t'(X0,X2,happ(X3,X4))))))).
% 67.93/12.84 fof($_typeof_A, axiom, 'cType$u$u$u24t'(cA)).
% 67.93/12.84 fof($_typeof_B, axiom, 'cType$u$u$u24t'(cB)).
% 67.93/12.84 fof($_typeof_f, axiom, 'c$u24$u$utype$u$u1$u$u$u24t'(cf)).
% 67.93/12.84 fof($_typeof_g, axiom, 'c$u24$u$utype$u$u1$u$u$u24t'(cg)).
% 67.93/12.84 fof($_typeof_m, axiom, 'cmonads$u2emon$u$u$u24t'(cM,cA,cm)).
% 67.93/12.84 fof(e, axiom, 'cmonads$u2eextMonad$u$u$u24a1'(cM)).
% 67.93/12.84 fof($tdef_A, axiom, ! [X0] : (('cA$u$u$u24t'(X0) <=> t(X0,cA)))).
% 67.93/12.84 fof(_HAMMER_GOAL, conjecture, (cm = cn => ('cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(cA,'cmonads$u2emon$u$u$u24a2'(cM,cB),cf,cg) => 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cn,cg)))).
% 67.93/12.84 fof(negated_conjecture, negated_conjecture, ~((cm = cn => ('cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(cA,'cmonads$u2emon$u$u$u24a2'(cM,cB),cf,cg) => 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cn,cg)))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 67.93/12.84 cnf(c3, plain, ~'cmonads$u2eextMonad$u$u$u24a1'(X0) | X1(X0), inference(clausification, [status(esa)], [$_def_monads.extMonad])).
% 67.93/12.84 cnf(c5, plain, ~'c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X3) | ~'cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(X1,'cmonads$u2emon$u$u$u24a2'(X0,X2),X3,X4) | ~'cType$u$u$u24t'(X1) | ~'cType$u$u$u24t'(X2) | ~'cmonads$u2emon$u$u$u24t'(X0,X1,X5) | ~'c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X4) | 'cmonads$u2ebind$u$u$u24a5'(X0,X1,X2,X5,X3) = 'cmonads$u2ebind$u$u$u24a5'(X0,X1,X2,X5,X4) | ~X6(X0), inference(clausification, [status(esa)], [$_def_monads.extMonad])).
% 67.93/12.84 cnf(c22, plain, ~'c$u24$u$utype$u$u1$u$u$u24t'(X0) | ~'cA$u$u$u24t'(X1) | 'cmonads$u2emon$u$u$u24t'(cM,cB,happ(X0,X1)), inference(clausification, [status(esa)], [$_type_1])).
% 67.93/12.84 cnf(c36, plain, 'c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X3) | t(sK60(X0,X1,X2,X3),X1), inference(clausification, [status(esa)], [$_type_172])).
% 67.93/12.84 cnf(c37, plain, 'c$u24$u$utype$u$u172$u$u$u24t'(X0,X1,X2,X3) | ~'cmonads$u2emon$u$u$u24t'(X0,X2,happ(X3,sK60(X0,X1,X2,X3))), inference(clausification, [status(esa)], [$_type_172])).
% 67.93/12.84 cnf(c54, plain, 'cType$u$u$u24t'(cA), inference(clausification, [status(esa)], [$_typeof_A])).
% 67.93/12.84 cnf(c55, plain, 'cType$u$u$u24t'(cB), inference(clausification, [status(esa)], [$_typeof_B])).
% 67.93/12.84 cnf(c57, plain, 'c$u24$u$utype$u$u1$u$u$u24t'(cf), inference(clausification, [status(esa)], [$_typeof_f])).
% 67.93/12.84 cnf(c58, plain, 'c$u24$u$utype$u$u1$u$u$u24t'(cg), inference(clausification, [status(esa)], [$_typeof_g])).
% 67.93/12.84 cnf(c59, plain, 'cmonads$u2emon$u$u$u24t'(cM,cA,cm), inference(clausification, [status(esa)], [$_typeof_m])).
% 67.93/12.84 cnf(c73, plain, 'cmonads$u2eextMonad$u$u$u24a1'(cM), inference(clausification, [status(esa)], [e])).
% 67.93/12.84 cnf(c82, plain, 'cA$u$u$u24t'(X0) | ~t(X0,cA), inference(clausification, [status(esa)], [$tdef_A])).
% 67.93/12.84 cnf(c87, plain, cm = cn, inference(clausification, [status(esa)], [negated_conjecture])).
% 67.93/12.84 cnf(c88, plain, 'cQuicksortComplexity$u2eutil$u2eext$u$ueq$u$u$u24a4'(cA,'cmonads$u2emon$u$u$u24a2'(cM,cB),cf,cg), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.93/12.84 cnf(c89, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) != 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cn,cg), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.93/12.84 cnf(d0, plain, 'c$u24$u$utype$u$u172$u$u$u24t'(X0,cA,X1,X2) | 'cA$u$u$u24t'(sK60(X0,cA,X1,X2)), inference(resolution, [status(thm)], [c36,c82])).
% 67.93/12.84 cnf(d1, plain, 'c$u24$u$utype$u$u172$u$u$u24t'(cM,X0,cB,X1) | ~'c$u24$u$utype$u$u1$u$u$u24t'(X1) | ~'cA$u$u$u24t'(sK60(cM,X0,cB,X1)), inference(resolution, [status(thm)], [c37,c22])).
% 67.93/12.84 cnf(d2, plain, 'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,X0) | ~'c$u24$u$utype$u$u1$u$u$u24t'(X0) | 'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,X0), inference(resolution, [status(thm)], [d1,d0])).
% 67.93/12.84 cnf(d3, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'Ts6'(cM) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cg) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cf) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0) | ~'cType$u$u$u24t'(cB) | ~'cType$u$u$u24t'(cA), inference(resolution, [status(thm)], [c88,c5])).
% 67.93/12.84 cnf(d4, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'Ts6'(cM) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cg) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0) | ~'cType$u$u$u24t'(cB), inference(resolution, [status(thm)], [c54,d3])).
% 67.93/12.84 cnf(d5, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'Ts6'(cM) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cg) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c55,d4])).
% 67.93/12.84 cnf(d6, plain, 'Ts6'(cM), inference(resolution, [status(thm)], [c73,c3])).
% 67.93/12.84 cnf(d7, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cf) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cg) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [d6,d5])).
% 67.93/12.84 cnf(d8, plain, ~'c$u24$u$utype$u$u1$u$u$u24t'(cg) | 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cf) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [d2,d7])).
% 67.93/12.84 cnf(d9, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'c$u24$u$utype$u$u172$u$u$u24t'(cM,cA,cB,cf) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c58,d8])).
% 67.93/12.84 cnf(d10, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0) | ~'c$u24$u$utype$u$u1$u$u$u24t'(cf), inference(resolution, [status(thm)], [d9,d2])).
% 67.93/12.84 cnf(d11, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,X0,cg) | ~'cmonads$u2emon$u$u$u24t'(cM,cA,X0), inference(resolution, [status(thm)], [c57,d10])).
% 67.93/12.84 cnf(d12, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) = 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cg), inference(resolution, [status(thm)], [d11,c59])).
% 67.93/12.84 cnf(d13, plain, 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cf) != 'cmonads$u2ebind$u$u$u24a5'(cM,cA,cB,cm,cg), inference(demodulation, [status(thm)], [c89,c87])).
% 67.93/12.84 cnf(d14, plain, $false, inference(resolution, [status(thm)], [d13,d12])).
% 67.93/12.84 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------