%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : ITP006+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 07:37:56 AM UTC 2026
% Result : Theorem 36.67s 10.17s
% Output : CNFRefutation 36.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n009.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Fri Sep 25 17:05:19 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.67/10.17 % SZS status Theorem for theBenchmark.p
% 36.67/10.17 % SZS output start CNFRefutation for theBenchmark.p
% 36.67/10.17 fof(conj_thm_2EquantHeuristics_2EGUESS__REWRITES, axiom, ! [X0] : ((ne(X0) => ! [X1] : ((ne(X1) => ! [X2] : ((mem(X2,arr(X0,X1)) => ! [X3] : ((mem(X3,arr(X1,bool)) => ((p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uEXISTS'(X0,X1),X2),X3)) <=> ! [X4] : ((mem(X4,X1) => (p(ap(X3,X4)) => ? [X5] : ((mem(X5,X0) & p(ap(X3,ap(X2,X5))))))))) & ((p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL'(X0,X1),X2),X3)) <=> ! [X6] : ((mem(X6,X1) => (~p(ap(X3,X6)) => ? [X7] : ((mem(X7,X0) & ~p(ap(X3,ap(X2,X7))))))))) & (! [X8] : ((mem(X8,arr(X0,X1)) => ! [X9] : ((mem(X9,arr(X1,bool)) => (p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uEXISTS$u$uPOINT'(X0,X1),X8),X9)) <=> ! [X10] : ((mem(X10,X0) => p(ap(X9,ap(X8,X10)))))))))) & (! [X11] : ((mem(X11,arr(X0,X1)) => ! [X12] : ((mem(X12,arr(X1,bool)) => (p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X0,X1),X11),X12)) <=> ! [X13] : ((mem(X13,X0) => ~p(ap(X12,ap(X11,X13)))))))))) & (! [X14] : ((mem(X14,arr(X0,X1)) => ! [X15] : ((mem(X15,arr(X1,bool)) => (p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uEXISTS$u$uGAP'(X0,X1),X14),X15)) <=> ! [X16] : ((mem(X16,X1) => (p(ap(X15,X16)) => ? [X17] : ((mem(X17,X0) & X16 = ap(X14,X17))))))))))) & ! [X18] : ((mem(X18,arr(X0,X1)) => ! [X19] : ((mem(X19,arr(X1,bool)) => (p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uGAP'(X0,X1),X18),X19)) <=> ! [X20] : ((mem(X20,X1) => (~p(ap(X19,X20)) => ? [X21] : ((mem(X21,X0) & X20 = ap(X18,X21))))))))))))))))))))))))).
% 36.67/10.17 fof(ap_tp, axiom, ! [X0] : ! [X1] : ! [X2] : ((mem(X2,arr(X0,X1)) => ! [X3] : ((mem(X3,X0) => mem(ap(X2,X3),X1)))))).
% 36.67/10.17 fof(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT, conjecture, ! [X0] : ((ne(X0) => ! [X1] : ((ne(X1) => ! [X2] : ((mem(X2,arr(X1,X0)) => ! [X3] : ((mem(X3,arr(X0,bool)) => ! [X4] : ((mem(X4,arr(X0,bool)) => (! [X5] : ((mem(X5,X0) => (p(ap(X4,X5)) => p(ap(X3,X5))))) => (p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X1,X0),X2),X3)) => p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X1,X0),X2),X4))))))))))))))).
% 36.67/10.17 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((ne(X0) => ! [X1] : ((ne(X1) => ! [X2] : ((mem(X2,arr(X1,X0)) => ! [X3] : ((mem(X3,arr(X0,bool)) => ! [X4] : ((mem(X4,arr(X0,bool)) => (! [X5] : ((mem(X5,X0) => (p(ap(X4,X5)) => p(ap(X3,X5))))) => (p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X1,X0),X2),X3)) => p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X1,X0),X2),X4)))))))))))))), inference(negate_conjecture, [status(cth)], [conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT])).
% 36.67/10.17 cnf(c76, plain, X0(X1,X2,X3,X4) | ~mem(X3,arr(X1,X2)) | ~ne(X2) | ~mem(X4,arr(X2,bool)) | ~ne(X1), inference(clausification, [status(esa)], [conj_thm_2EquantHeuristics_2EGUESS__REWRITES])).
% 36.67/10.17 cnf(c104, plain, ~mem(X0,arr(X1,bool)) | ~X2(X3,X1,X4,X5) | ~p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X3,X1),X6),X0)) | ~mem(X7,X3) | ~p(ap(X0,ap(X6,X7))) | ~mem(X6,arr(X3,X1)), inference(clausification, [status(esa)], [conj_thm_2EquantHeuristics_2EGUESS__REWRITES])).
% 36.67/10.17 cnf(c105, plain, ~mem(X0,arr(X1,bool)) | mem(sK83(X2,X3,X0),X2) | ~X4(X2,X1,X5,X6) | p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X2,X1),X3),X0)) | ~mem(X3,arr(X2,X1)), inference(clausification, [status(esa)], [conj_thm_2EquantHeuristics_2EGUESS__REWRITES])).
% 36.67/10.17 cnf(c106, plain, ~mem(X0,arr(X1,bool)) | ~X2(X3,X1,X4,X5) | p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X3,X1),X6),X0)) | p(ap(X0,ap(X6,sK83(X3,X6,X0)))) | ~mem(X6,arr(X3,X1)), inference(clausification, [status(esa)], [conj_thm_2EquantHeuristics_2EGUESS__REWRITES])).
% 36.67/10.17 cnf(c226, plain, ~mem(X0,arr(X1,X2)) | ~mem(X3,X1) | mem(ap(X0,X3),X2), inference(clausification, [status(esa)], [ap_tp])).
% 36.67/10.17 cnf(c235, plain, ne(sK140), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c236, plain, ne(sK141), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c237, plain, mem(sK142,arr(sK141,sK140)), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c238, plain, mem(sK143,arr(sK140,bool)), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c239, plain, mem(sK144,arr(sK140,bool)), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c240, plain, ~mem(X0,sK140) | ~p(ap(sK144,X0)) | p(ap(sK143,X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c241, plain, p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(sK141,sK140),sK142),sK143)), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(c242, plain, ~p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(sK141,sK140),sK142),sK144)), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.67/10.17 cnf(d0, plain, ~mem(X0,arr(sK140,bool)) | ~ne(sK141) | ~ne(sK140) | 'Ts55'(sK141,sK140,sK142,X0), inference(resolution, [status(thm)], [c76,c237])).
% 36.67/10.17 cnf(d1, plain, ~mem(X0,arr(sK140,bool)) | ~ne(sK141) | 'Ts55'(sK141,sK140,sK142,X0), inference(resolution, [status(thm)], [c235,d0])).
% 36.67/10.17 cnf(d2, plain, ~mem(X0,arr(sK140,bool)) | 'Ts55'(sK141,sK140,sK142,X0), inference(resolution, [status(thm)], [c236,d1])).
% 36.67/10.17 cnf(d3, plain, 'Ts55'(sK141,sK140,sK142,sK143), inference(resolution, [status(thm)], [d2,c238])).
% 36.67/10.17 cnf(d4, plain, 'Ts55'(sK141,sK140,sK142,sK144), inference(resolution, [status(thm)], [d2,c239])).
% 36.67/10.17 cnf(d5, plain, ~mem(sK144,arr(sK140,bool)) | ~mem(sK142,arr(sK141,sK140)) | mem(sK83(sK141,sK142,sK144),sK141) | ~'Ts55'(sK141,sK140,X0,X1), inference(resolution, [status(thm)], [c105,c242])).
% 36.67/10.17 cnf(d6, plain, mem(sK83(sK141,sK142,sK144),sK141) | ~mem(sK144,arr(sK140,bool)) | ~'Ts55'(sK141,sK140,X0,X1), inference(resolution, [status(thm)], [c237,d5])).
% 36.67/10.17 cnf(d7, plain, mem(sK83(sK141,sK142,sK144),sK141) | ~'Ts55'(sK141,sK140,X0,X1), inference(resolution, [status(thm)], [c239,d6])).
% 36.67/10.17 cnf(d8, plain, ~mem(X0,sK141) | mem(ap(sK142,X0),sK140), inference(resolution, [status(thm)], [c226,c237])).
% 36.67/10.17 cnf(d9, plain, ~mem(X0,sK141) | ~mem(sK142,arr(sK141,sK140)) | ~mem(sK143,arr(sK140,bool)) | ~p(ap(sK143,ap(sK142,X0))) | ~'Ts55'(sK141,sK140,X1,X2), inference(resolution, [status(thm)], [c104,c241])).
% 36.67/10.17 cnf(d10, plain, ~mem(X0,sK141) | ~mem(sK143,arr(sK140,bool)) | ~p(ap(sK143,ap(sK142,X0))) | ~'Ts55'(sK141,sK140,X1,X2), inference(resolution, [status(thm)], [c237,d9])).
% 36.67/10.17 cnf(d11, plain, ~mem(X0,sK141) | ~p(ap(sK143,ap(sK142,X0))) | ~'Ts55'(sK141,sK140,X1,X2), inference(resolution, [status(thm)], [c238,d10])).
% 36.67/10.17 cnf(d12, plain, ~mem(sK144,arr(X0,bool)) | ~mem(X1,arr(X2,X0)) | p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X2,X0),X1),sK144)) | ~'Ts55'(X2,X0,X3,X4) | ~mem(ap(X1,sK83(X2,X1,sK144)),sK140) | p(ap(sK143,ap(X1,sK83(X2,X1,sK144)))), inference(resolution, [status(thm)], [c106,c240])).
% 36.67/10.17 cnf(d13, plain, ~mem(sK142,arr(X0,X1)) | ~mem(ap(sK142,sK83(X0,sK142,sK144)),sK140) | ~mem(sK144,arr(X1,bool)) | p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X0,X1),sK142),sK144)) | ~'Ts55'(X0,X1,X2,X3) | ~mem(sK83(X0,sK142,sK144),sK141) | ~'Ts55'(sK141,sK140,X4,X5), inference(resolution, [status(thm)], [d12,d11])).
% 36.67/10.17 cnf(d14, plain, ~mem(sK83(X0,sK142,sK144),sK141) | ~mem(sK142,arr(X0,X1)) | ~mem(sK144,arr(X1,bool)) | p(ap(ap('c$u2EquantHeuristics$u2EGUESS$u$uFORALL$u$uPOINT'(X0,X1),sK142),sK144)) | ~'Ts55'(X0,X1,X2,X3) | ~'Ts55'(sK141,sK140,X4,X5) | ~mem(sK83(X0,sK142,sK144),sK141), inference(resolution, [status(thm)], [d13,d8])).
% 36.67/10.17 cnf(d15, plain, ~mem(sK83(sK141,sK142,sK144),sK141) | ~mem(sK142,arr(sK141,sK140)) | ~mem(sK144,arr(sK140,bool)) | ~'Ts55'(sK141,sK140,X0,X1) | ~'Ts55'(sK141,sK140,X2,X3), inference(resolution, [status(thm)], [d14,c242])).
% 36.67/10.17 cnf(d16, plain, ~mem(sK83(sK141,sK142,sK144),sK141) | ~mem(sK144,arr(sK140,bool)) | ~'Ts55'(sK141,sK140,X0,X1) | ~'Ts55'(sK141,sK140,X2,X3), inference(resolution, [status(thm)], [c237,d15])).
% 36.67/10.17 cnf(d17, plain, ~mem(sK83(sK141,sK142,sK144),sK141) | ~'Ts55'(sK141,sK140,X0,X1) | ~'Ts55'(sK141,sK140,X2,X3), inference(resolution, [status(thm)], [c239,d16])).
% 36.67/10.17 cnf(d18, plain, ~'Ts55'(sK141,sK140,X0,X1) | ~'Ts55'(sK141,sK140,X2,X3) | ~'Ts55'(sK141,sK140,X4,X5), inference(resolution, [status(thm)], [d17,d7])).
% 36.67/10.17 cnf(d19, plain, ~'Ts55'(sK141,sK140,X0,X1) | ~'Ts55'(sK141,sK140,X2,X3), inference(resolution, [status(thm)], [d18,d4])).
% 36.67/10.17 cnf(d20, plain, ~'Ts55'(sK141,sK140,X0,X1), inference(resolution, [status(thm)], [d19,d4])).
% 36.67/10.17 cnf(d21, plain, $false, inference(resolution, [status(thm)], [d20,d3])).
% 36.67/10.17 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------