%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP006^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 : Wed Sep 30 08:03:58 AM UTC 2026
% Result : Theorem 10.75s 1.68s
% Output : CNFRefutation 10.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP006^2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n003.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Tue Sep 29 19:24:33 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running higher-order theorem proving
% 0.06/0.24 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.VJ4gIfEJ4i/E---3.1_2942171.p
% 10.75/1.68 % Version: 3.5.1-ho
% 10.75/1.68 % Preprocessing class: HSLSSMSMSSSNSFA.
% 10.75/1.68 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 10.75/1.68 % Starting new_ho_10 with 900s (3) cores
% 10.75/1.68 % Starting sh2lt with 300s (1) cores
% 10.75/1.68 % Starting new_ho_5 with 300s (1) cores
% 10.75/1.68 % Starting full_lambda_5 with 300s (1) cores
% 10.75/1.68 % Starting sh9 with 300s (1) cores
% 10.75/1.68 % Starting ehoh_best8_lambda with 300s (1) cores
% 10.75/1.68 % sh2lt with pid 2942185 completed with status 0
% 10.75/1.68 % Result found by sh2lt
% 10.75/1.68 % Preprocessing class: HSLSSMSMSSSNSFA.
% 10.75/1.68 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 10.75/1.68 % Starting new_ho_10 with 900s (3) cores
% 10.75/1.68 % Starting sh2lt with 300s (1) cores
% 10.75/1.68 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 10.75/1.68 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 10.75/1.68 % Search class: HGHSM-FFMS33-MSFFFFNN
% 10.75/1.68 % partial match(3): FGHSM-FFMS31-MFFFFFNN
% 10.75/1.68 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 10.75/1.68 % Starting SubtermCWHack with 28s (1) cores
% 10.75/1.68 % SubtermCWHack with pid 2942193 completed with status 0
% 10.75/1.68 % Result found by SubtermCWHack
% 10.75/1.68 % Preprocessing class: HSLSSMSMSSSNSFA.
% 10.75/1.68 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 10.75/1.68 % Starting new_ho_10 with 900s (3) cores
% 10.75/1.68 % Starting sh2lt with 300s (1) cores
% 10.75/1.68 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,5,,4,20000,1.0,true))
% 10.75/1.68 % SinE strategy is GSinE(CountFormulas,hypos,5,,4,20000,1.0,true)
% 10.75/1.68 % Search class: HGHSM-FFMS33-MSFFFFNN
% 10.75/1.68 % partial match(3): FGHSM-FFMS31-MFFFFFNN
% 10.75/1.68 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 10.75/1.68 % Starting SubtermCWHack with 28s (1) cores
% 10.75/1.68 % Preprocessing time : 0.003 s
% 10.75/1.68
% 10.75/1.68 % Proof found!
% 10.75/1.68 % SZS status Theorem
% 10.75/1.68 % SZS output start CNFRefutation
% 10.75/1.68 thf(decl_sort1, type, del: $tType).
% 10.75/1.68 thf(decl_23, type, bool: del).
% 10.75/1.68 thf(decl_25, type, arr: del > del > del).
% 10.75/1.68 thf(decl_26, type, mem: $i > del > $o).
% 10.75/1.68 thf(decl_27, type, ap: $i > $i > $i).
% 10.75/1.68 thf(decl_29, type, p: $i > $o).
% 10.75/1.68 thf(decl_32, type, c_2EquantHeuristics_2EGUESS__FORALL__GAP: del > del > $i).
% 10.75/1.68 thf(decl_33, type, c_2EquantHeuristics_2EGUESS__EXISTS__GAP: del > del > $i).
% 10.75/1.68 thf(decl_34, type, c_2EquantHeuristics_2EGUESS__FORALL__POINT: del > del > $i).
% 10.75/1.68 thf(decl_35, type, c_2EquantHeuristics_2EGUESS__EXISTS__POINT: del > del > $i).
% 10.75/1.68 thf(decl_36, type, c_2EquantHeuristics_2EGUESS__FORALL: del > del > $i).
% 10.75/1.68 thf(decl_38, type, c_2EquantHeuristics_2EGUESS__EXISTS: del > del > $i).
% 10.75/1.68 thf(decl_49, type, epred4_4: del > del > $i > $i > $o).
% 10.75/1.68 thf(decl_50, type, esk1_0: del).
% 10.75/1.68 thf(decl_51, type, esk2_0: del).
% 10.75/1.68 thf(decl_52, type, esk3_0: $i).
% 10.75/1.68 thf(decl_53, type, esk4_0: $i).
% 10.75/1.68 thf(decl_54, type, esk5_0: $i).
% 10.75/1.68 thf(decl_56, type, esk7_5: $i > $i > del > del > $i > $i).
% 10.75/1.68 thf(decl_57, type, esk8_4: $i > $i > del > del > $i).
% 10.75/1.68 thf(decl_58, type, esk9_5: $i > $i > del > del > $i > $i).
% 10.75/1.68 thf(decl_59, type, esk10_4: $i > $i > del > del > $i).
% 10.75/1.68 thf(decl_60, type, esk11_6: $i > $i > del > del > $i > $i > $i).
% 10.75/1.68 thf(decl_61, type, esk12_6: $i > $i > del > del > $i > $i > $i).
% 10.75/1.68 thf(decl_62, type, esk13_7: $i > $i > del > del > $i > $i > $i > $i).
% 10.75/1.68 thf(decl_63, type, esk14_6: $i > $i > del > del > $i > $i > $i).
% 10.75/1.68 thf(decl_64, type, esk15_7: $i > $i > del > del > $i > $i > $i > $i).
% 10.75/1.68 thf(decl_65, type, esk16_6: $i > $i > del > del > $i > $i > $i).
% 10.75/1.68 thf(conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT, conjecture, ![X13:del, X14:del, X30:$i]:(((mem @ X30 @ (arr @ X14 @ X13))=>![X31:$i]:(((mem @ X31 @ (arr @ X13 @ bool))=>![X55:$i]:(((mem @ X55 @ (arr @ X13 @ bool))=>(![X56:$i]:(((mem @ X56 @ X13)=>((p @ (ap @ X55 @ X56))=>(p @ (ap @ X31 @ X56)))))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X14 @ X13) @ X30) @ X31))=>(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X14 @ X13) @ X30) @ X55)))))))))), file('/export/starexec/sandbox/tmp/tmp.VJ4gIfEJ4i/E---3.1_2942171.p', conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 10.75/1.68 thf(conj_thm_2EquantHeuristics_2EGUESS__REWRITES, axiom, ![X13:del, X14:del, X30:$i]:(((mem @ X30 @ (arr @ X13 @ X14))=>![X31:$i]:(((mem @ X31 @ (arr @ X14 @ bool))=>(((((((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X13 @ X14) @ X30) @ X31))<=>![X32:$i]:(((mem @ X32 @ X14)=>((p @ (ap @ X31 @ X32))=>?[X33:$i]:(((mem @ X33 @ X13)&(p @ (ap @ X31 @ (ap @ X30 @ X33)))))))))&((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X13 @ X14) @ X30) @ X31))<=>![X34:$i]:(((mem @ X34 @ X14)=>(~((p @ (ap @ X31 @ X34)))=>?[X35:$i]:(((mem @ X35 @ X13)&~((p @ (ap @ X31 @ (ap @ X30 @ X35)))))))))))&![X36:$i]:(((mem @ X36 @ (arr @ X13 @ X14))=>![X37:$i]:(((mem @ X37 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X13 @ X14) @ X36) @ X37))<=>![X38:$i]:(((mem @ X38 @ X13)=>(p @ (ap @ X37 @ (ap @ X36 @ X38)))))))))))&![X39:$i]:(((mem @ X39 @ (arr @ X13 @ X14))=>![X40:$i]:(((mem @ X40 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X13 @ X14) @ X39) @ X40))<=>![X41:$i]:(((mem @ X41 @ X13)=>~((p @ (ap @ X40 @ (ap @ X39 @ X41))))))))))))&![X42:$i]:(((mem @ X42 @ (arr @ X13 @ X14))=>![X43:$i]:(((mem @ X43 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X13 @ X14) @ X42) @ X43))<=>![X44:$i]:(((mem @ X44 @ X14)=>((p @ (ap @ X43 @ X44))=>?[X45:$i]:(((mem @ X45 @ X13)&((X44)=(ap @ X42 @ X45)))))))))))))&![X46:$i]:(((mem @ X46 @ (arr @ X13 @ X14))=>![X47:$i]:(((mem @ X47 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X13 @ X14) @ X46) @ X47))<=>![X48:$i]:(((mem @ X48 @ X14)=>(~((p @ (ap @ X47 @ X48)))=>?[X49:$i]:(((mem @ X49 @ X13)&((X48)=(ap @ X46 @ X49))))))))))))))))), file('/export/starexec/sandbox/tmp/tmp.VJ4gIfEJ4i/E---3.1_2942171.p', conj_thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 10.75/1.68 thf(ap_tp, axiom, ![X3:del, X4:del, X5:$i]:(((mem @ X5 @ (arr @ X3 @ X4))=>![X6:$i]:(((mem @ X6 @ X3)=>(mem @ (ap @ X5 @ X6) @ X4))))), file('/export/starexec/sandbox/tmp/tmp.VJ4gIfEJ4i/E---3.1_2942171.p', ap_tp)).
% 10.75/1.68 thf(c_0_3, plain, ![X31:$i, X30:$i, X14:del, X13:del]:(((epred4_4 @ X13 @ X14 @ X30 @ X31)<=>(((((((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X13 @ X14) @ X30) @ X31))<=>![X32:$i]:(((mem @ X32 @ X14)=>((p @ (ap @ X31 @ X32))=>?[X33:$i]:(((mem @ X33 @ X13)&(p @ (ap @ X31 @ (ap @ X30 @ X33)))))))))&((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X13 @ X14) @ X30) @ X31))<=>![X34:$i]:(((mem @ X34 @ X14)=>(~(p @ (ap @ X31 @ X34))=>?[X35:$i]:(((mem @ X35 @ X13)&~(p @ (ap @ X31 @ (ap @ X30 @ X35))))))))))&![X36:$i]:(((mem @ X36 @ (arr @ X13 @ X14))=>![X37:$i]:(((mem @ X37 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X13 @ X14) @ X36) @ X37))<=>![X38:$i]:(((mem @ X38 @ X13)=>(p @ (ap @ X37 @ (ap @ X36 @ X38)))))))))))&![X39:$i]:(((mem @ X39 @ (arr @ X13 @ X14))=>![X40:$i]:(((mem @ X40 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X13 @ X14) @ X39) @ X40))<=>![X41:$i]:(((mem @ X41 @ X13)=>~(p @ (ap @ X40 @ (ap @ X39 @ X41)))))))))))&![X42:$i]:(((mem @ X42 @ (arr @ X13 @ X14))=>![X43:$i]:(((mem @ X43 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X13 @ X14) @ X42) @ X43))<=>![X44:$i]:(((mem @ X44 @ X14)=>((p @ (ap @ X43 @ X44))=>?[X45:$i]:(((mem @ X45 @ X13)&((X44)=(ap @ X42 @ X45)))))))))))))&![X46:$i]:(((mem @ X46 @ (arr @ X13 @ X14))=>![X47:$i]:(((mem @ X47 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X13 @ X14) @ X46) @ X47))<=>![X48:$i]:(((mem @ X48 @ X14)=>(~(p @ (ap @ X47 @ X48))=>?[X49:$i]:(((mem @ X49 @ X13)&((X48)=(ap @ X46 @ X49))))))))))))))), introduced(definition)).
% 10.75/1.68 thf(c_0_4, plain, ![X31:$i, X30:$i, X14:del, X13:del]:(((epred4_4 @ X13 @ X14 @ X30 @ X31)=>(((((((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X13 @ X14) @ X30) @ X31))<=>![X32:$i]:(((mem @ X32 @ X14)=>((p @ (ap @ X31 @ X32))=>?[X33:$i]:(((mem @ X33 @ X13)&(p @ (ap @ X31 @ (ap @ X30 @ X33)))))))))&((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X13 @ X14) @ X30) @ X31))<=>![X34:$i]:(((mem @ X34 @ X14)=>(~(p @ (ap @ X31 @ X34))=>?[X35:$i]:(((mem @ X35 @ X13)&~(p @ (ap @ X31 @ (ap @ X30 @ X35))))))))))&![X36:$i]:(((mem @ X36 @ (arr @ X13 @ X14))=>![X37:$i]:(((mem @ X37 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X13 @ X14) @ X36) @ X37))<=>![X38:$i]:(((mem @ X38 @ X13)=>(p @ (ap @ X37 @ (ap @ X36 @ X38)))))))))))&![X39:$i]:(((mem @ X39 @ (arr @ X13 @ X14))=>![X40:$i]:(((mem @ X40 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X13 @ X14) @ X39) @ X40))<=>![X41:$i]:(((mem @ X41 @ X13)=>~(p @ (ap @ X40 @ (ap @ X39 @ X41)))))))))))&![X42:$i]:(((mem @ X42 @ (arr @ X13 @ X14))=>![X43:$i]:(((mem @ X43 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X13 @ X14) @ X42) @ X43))<=>![X44:$i]:(((mem @ X44 @ X14)=>((p @ (ap @ X43 @ X44))=>?[X45:$i]:(((mem @ X45 @ X13)&((X44)=(ap @ X42 @ X45)))))))))))))&![X46:$i]:(((mem @ X46 @ (arr @ X13 @ X14))=>![X47:$i]:(((mem @ X47 @ (arr @ X14 @ bool))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X13 @ X14) @ X46) @ X47))<=>![X48:$i]:(((mem @ X48 @ X14)=>(~(p @ (ap @ X47 @ X48))=>?[X49:$i]:(((mem @ X49 @ X13)&((X48)=(ap @ X46 @ X49))))))))))))))), inference(split_equiv,[status(thm)],[c_0_3])).
% 10.75/1.68 thf(c_0_5, plain, ![X214:$i, X215:$i, X216:del, X217:del, X218:$i, X221:$i, X222:$i, X225:$i, X226:$i, X227:$i, X228:$i, X230:$i, X231:$i, X232:$i, X234:$i, X235:$i, X236:$i, X239:$i, X240:$i, X241:$i, X242:$i, X245:$i]:((((((((((mem @ (esk7_5 @ X214 @ X215 @ X216 @ X217 @ X218) @ X217)|~(p @ (ap @ X214 @ X218))|~(mem @ X218 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&((p @ (ap @ X214 @ (ap @ X215 @ (esk7_5 @ X214 @ X215 @ X216 @ X217 @ X218))))|~(p @ (ap @ X214 @ X218))|~(mem @ X218 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))&(((mem @ (esk8_4 @ X214 @ X215 @ X216 @ X217) @ X216)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(((p @ (ap @ X214 @ (esk8_4 @ X214 @ X215 @ X216 @ X217)))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(~(mem @ X221 @ X217)|~(p @ (ap @ X214 @ (ap @ X215 @ X221)))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))))&((((mem @ (esk9_5 @ X214 @ X215 @ X216 @ X217 @ X222) @ X217)|(p @ (ap @ X214 @ X222))|~(mem @ X222 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(~(p @ (ap @ X214 @ (ap @ X215 @ (esk9_5 @ X214 @ X215 @ X216 @ X217 @ X222))))|(p @ (ap @ X214 @ X222))|~(mem @ X222 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))&(((mem @ (esk10_4 @ X214 @ X215 @ X216 @ X217) @ X216)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&((~(p @ (ap @ X214 @ (esk10_4 @ X214 @ X215 @ X216 @ X217)))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(~(mem @ X225 @ X217)|(p @ (ap @ X214 @ (ap @ X215 @ X225)))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL @ X217 @ X216) @ X215) @ X214))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))))))&((~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X217 @ X216) @ X226) @ X227))|(~(mem @ X228 @ X217)|(p @ (ap @ X227 @ (ap @ X226 @ X228))))|~(mem @ X227 @ (arr @ X216 @ bool))|~(mem @ X226 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(((mem @ (esk11_6 @ X214 @ X215 @ X216 @ X217 @ X226 @ X227) @ X217)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X217 @ X216) @ X226) @ X227))|~(mem @ X227 @ (arr @ X216 @ bool))|~(mem @ X226 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(~(p @ (ap @ X227 @ (ap @ X226 @ (esk11_6 @ X214 @ X215 @ X216 @ X217 @ X226 @ X227))))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X217 @ X216) @ X226) @ X227))|~(mem @ X227 @ (arr @ X216 @ bool))|~(mem @ X226 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))))&((~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X217 @ X216) @ X230) @ X231))|(~(mem @ X232 @ X217)|~(p @ (ap @ X231 @ (ap @ X230 @ X232))))|~(mem @ X231 @ (arr @ X216 @ bool))|~(mem @ X230 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(((mem @ (esk12_6 @ X214 @ X215 @ X216 @ X217 @ X230 @ X231) @ X217)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X217 @ X216) @ X230) @ X231))|~(mem @ X231 @ (arr @ X216 @ bool))|~(mem @ X230 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&((p @ (ap @ X231 @ (ap @ X230 @ (esk12_6 @ X214 @ X215 @ X216 @ X217 @ X230 @ X231))))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X217 @ X216) @ X230) @ X231))|~(mem @ X231 @ (arr @ X216 @ bool))|~(mem @ X230 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))))&((((mem @ (esk13_7 @ X214 @ X215 @ X216 @ X217 @ X234 @ X235 @ X236) @ X217)|~(p @ (ap @ X235 @ X236))|~(mem @ X236 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X217 @ X216) @ X234) @ X235))|~(mem @ X235 @ (arr @ X216 @ bool))|~(mem @ X234 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(((X236)=(ap @ X234 @ (esk13_7 @ X214 @ X215 @ X216 @ X217 @ X234 @ X235 @ X236)))|~(p @ (ap @ X235 @ X236))|~(mem @ X236 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X217 @ X216) @ X234) @ X235))|~(mem @ X235 @ (arr @ X216 @ bool))|~(mem @ X234 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))&(((mem @ (esk14_6 @ X214 @ X215 @ X216 @ X217 @ X234 @ X235) @ X216)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X217 @ X216) @ X234) @ X235))|~(mem @ X235 @ (arr @ X216 @ bool))|~(mem @ X234 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(((p @ (ap @ X235 @ (esk14_6 @ X214 @ X215 @ X216 @ X217 @ X234 @ X235)))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X217 @ X216) @ X234) @ X235))|~(mem @ X235 @ (arr @ X216 @ bool))|~(mem @ X234 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(~(mem @ X239 @ X217)|((esk14_6 @ X214 @ X215 @ X216 @ X217 @ X234 @ X235)!=(ap @ X234 @ X239))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X217 @ X216) @ X234) @ X235))|~(mem @ X235 @ (arr @ X216 @ bool))|~(mem @ X234 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))))))&((((mem @ (esk15_7 @ X214 @ X215 @ X216 @ X217 @ X240 @ X241 @ X242) @ X217)|(p @ (ap @ X241 @ X242))|~(mem @ X242 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X217 @ X216) @ X240) @ X241))|~(mem @ X241 @ (arr @ X216 @ bool))|~(mem @ X240 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(((X242)=(ap @ X240 @ (esk15_7 @ X214 @ X215 @ X216 @ X217 @ X240 @ X241 @ X242)))|(p @ (ap @ X241 @ X242))|~(mem @ X242 @ X216)|~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X217 @ X216) @ X240) @ X241))|~(mem @ X241 @ (arr @ X216 @ bool))|~(mem @ X240 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214)))&(((mem @ (esk16_6 @ X214 @ X215 @ X216 @ X217 @ X240 @ X241) @ X216)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X217 @ X216) @ X240) @ X241))|~(mem @ X241 @ (arr @ X216 @ bool))|~(mem @ X240 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&((~(p @ (ap @ X241 @ (esk16_6 @ X214 @ X215 @ X216 @ X217 @ X240 @ X241)))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X217 @ X216) @ X240) @ X241))|~(mem @ X241 @ (arr @ X216 @ bool))|~(mem @ X240 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))&(~(mem @ X245 @ X217)|((esk16_6 @ X214 @ X215 @ X216 @ X217 @ X240 @ X241)!=(ap @ X240 @ X245))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X217 @ X216) @ X240) @ X241))|~(mem @ X241 @ (arr @ X216 @ bool))|~(mem @ X240 @ (arr @ X217 @ X216))|~(epred4_4 @ X217 @ X216 @ X215 @ X214))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])])])).
% 10.75/1.68 thf(c_0_6, negated_conjecture, ~(![X13:del, X14:del, X30:$i]:(((mem @ X30 @ (arr @ X14 @ X13))=>![X31:$i]:(((mem @ X31 @ (arr @ X13 @ bool))=>![X55:$i]:(((mem @ X55 @ (arr @ X13 @ bool))=>(![X56:$i]:(((mem @ X56 @ X13)=>((p @ (ap @ X55 @ X56))=>(p @ (ap @ X31 @ X56)))))=>((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X14 @ X13) @ X30) @ X31))=>(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X14 @ X13) @ X30) @ X55))))))))))), inference(assume_negation,[status(cth)],[conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT])).
% 10.75/1.68 thf(c_0_7, plain, ![X2:$i, X3:del, X4:del, X6:$i, X5:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X3 @ X4) @ X6) @ X5))|~((mem @ X2 @ X3))|~((p @ (ap @ X5 @ (ap @ X6 @ X2))))|~((epred4_4 @ X3 @ X4 @ X6 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 10.75/1.68 thf(c_0_8, plain, ![X2:$i, X8:$i, X4:del, X5:$i, X3:del, X6:$i]:(((p @ (ap @ X2 @ (ap @ X5 @ (esk12_6 @ X6 @ X8 @ X3 @ X4 @ X5 @ X2))))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X4 @ X3) @ X5) @ X2))|~((mem @ X2 @ (arr @ X3 @ bool)))|~((mem @ X5 @ (arr @ X4 @ X3)))|~((epred4_4 @ X4 @ X3 @ X8 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 10.75/1.68 thf(c_0_9, plain, ![X13:del, X14:del, X30:$i]:(((mem @ X30 @ (arr @ X13 @ X14))=>![X31:$i]:(((mem @ X31 @ (arr @ X14 @ bool))=>(epred4_4 @ X13 @ X14 @ X30 @ X31))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[conj_thm_2EquantHeuristics_2EGUESS__REWRITES]), c_0_3])).
% 10.75/1.68 thf(c_0_10, negated_conjecture, ![X146:$i]:(((mem @ esk3_0 @ (arr @ esk2_0 @ esk1_0))&((mem @ esk4_0 @ (arr @ esk1_0 @ bool))&((mem @ esk5_0 @ (arr @ esk1_0 @ bool))&((~(mem @ X146 @ esk1_0)|(~(p @ (ap @ esk5_0 @ X146))|(p @ (ap @ esk4_0 @ X146))))&((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ esk1_0) @ esk3_0) @ esk4_0))&~(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ esk1_0) @ esk3_0) @ esk5_0)))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])])])])).
% 10.75/1.68 thf(c_0_11, plain, ![X177:del, X178:del, X179:$i, X180:$i]:((~(mem @ X179 @ (arr @ X177 @ X178))|(~(mem @ X180 @ X177)|(mem @ (ap @ X179 @ X180) @ X178)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ap_tp])])])])).
% 10.75/1.68 thf(c_0_12, plain, ![X2:$i, X8:$i, X4:del, X5:$i, X3:del, X14:del, X13:del, X6:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ X4) @ X2) @ X5))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X13 @ X14) @ X2) @ X5))|~((mem @ (esk12_6 @ X6 @ X8 @ X4 @ X3 @ X2 @ X5) @ X13))|~((mem @ X5 @ (arr @ X4 @ bool)))|~((mem @ X2 @ (arr @ X3 @ X4)))|~((epred4_4 @ X13 @ X14 @ X2 @ X5))|~((epred4_4 @ X3 @ X4 @ X8 @ X6)))), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 10.75/1.68 thf(c_0_13, plain, ![X3:del, X8:$i, X6:$i, X5:$i, X4:del, X2:$i]:(((mem @ (esk12_6 @ X2 @ X5 @ X3 @ X4 @ X6 @ X8) @ X4)|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X4 @ X3) @ X6) @ X8))|~((mem @ X8 @ (arr @ X3 @ bool)))|~((mem @ X6 @ (arr @ X4 @ X3)))|~((epred4_4 @ X4 @ X3 @ X5 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 10.75/1.68 thf(c_0_14, plain, ![X188:del, X189:del, X190:$i, X191:$i]:((~(mem @ X190 @ (arr @ X188 @ X189))|(~(mem @ X191 @ (arr @ X189 @ bool))|(epred4_4 @ X188 @ X189 @ X190 @ X191)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])).
% 10.75/1.68 thf(c_0_15, plain, ![X2:$i, X8:$i, X4:del, X5:$i, X3:del, X6:$i, X9:$i]:((~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ X4) @ X2) @ X5)))|~((mem @ X6 @ X3))|~((p @ (ap @ X5 @ (ap @ X2 @ X6))))|~((mem @ X5 @ (arr @ X4 @ bool)))|~((mem @ X2 @ (arr @ X3 @ X4)))|~((epred4_4 @ X3 @ X4 @ X8 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 10.75/1.68 thf(c_0_16, negated_conjecture, (p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ esk1_0) @ esk3_0) @ esk4_0)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.75/1.68 thf(c_0_17, negated_conjecture, (mem @ esk4_0 @ (arr @ esk1_0 @ bool)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.75/1.68 thf(c_0_18, negated_conjecture, (mem @ esk3_0 @ (arr @ esk2_0 @ esk1_0)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.75/1.68 thf(c_0_19, negated_conjecture, ![X2:$i]:(((p @ (ap @ esk4_0 @ X2))|~((mem @ X2 @ esk1_0))|~((p @ (ap @ esk5_0 @ X2))))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.75/1.68 thf(c_0_20, plain, ![X3:del, X6:$i, X5:$i, X4:del, X2:$i]:(((p @ (ap @ X2 @ (ap @ X5 @ (esk7_5 @ X2 @ X5 @ X3 @ X4 @ X6))))|~((p @ (ap @ X2 @ X6)))|~((mem @ X6 @ X3))|~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X4 @ X3) @ X5) @ X2)))|~((epred4_4 @ X4 @ X3 @ X5 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 10.75/1.68 thf(c_0_21, plain, ![X2:$i, X5:$i, X4:del, X3:del]:(((mem @ (ap @ X2 @ X5) @ X4)|~((mem @ X2 @ (arr @ X3 @ X4)))|~((mem @ X5 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 10.75/1.68 thf(c_0_22, plain, ![X2:$i, X4:del, X3:del, X13:del, X6:$i, X5:$i, X8:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X3 @ X4) @ X2) @ X5))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ X13) @ X2) @ X5))|~((mem @ X5 @ (arr @ X13 @ bool)))|~((mem @ X2 @ (arr @ X3 @ X13)))|~((epred4_4 @ X3 @ X4 @ X2 @ X5))|~((epred4_4 @ X3 @ X13 @ X6 @ X8)))), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 10.75/1.68 thf(c_0_23, plain, ![X2:$i, X3:del, X5:$i, X4:del]:(((epred4_4 @ X3 @ X4 @ X2 @ X5)|~((mem @ X2 @ (arr @ X3 @ X4)))|~((mem @ X5 @ (arr @ X4 @ bool))))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 10.75/1.68 thf(c_0_24, negated_conjecture, ![X6:$i, X5:$i, X2:$i]:((~((p @ (ap @ esk4_0 @ (ap @ esk3_0 @ X2))))|~((epred4_4 @ esk2_0 @ esk1_0 @ X5 @ X6))|~((mem @ X2 @ esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_16]), c_0_17]), c_0_18])])).
% 10.75/1.68 thf(c_0_25, negated_conjecture, ![X2:$i, X4:del, X5:$i, X3:del]:(((p @ (ap @ esk4_0 @ (ap @ X2 @ (esk7_5 @ esk5_0 @ X2 @ X3 @ X4 @ X5))))|~((mem @ (ap @ X2 @ (esk7_5 @ esk5_0 @ X2 @ X3 @ X4 @ X5)) @ esk1_0))|~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X4 @ X3) @ X2) @ esk5_0)))|~((p @ (ap @ esk5_0 @ X5)))|~((epred4_4 @ X4 @ X3 @ X2 @ esk5_0))|~((mem @ X5 @ X3)))), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 10.75/1.68 thf(c_0_26, negated_conjecture, ![X2:$i]:(((mem @ (ap @ esk3_0 @ X2) @ esk1_0)|~((mem @ X2 @ esk2_0)))), inference(spm,[status(thm)],[c_0_21, c_0_18])).
% 10.75/1.68 thf(c_0_27, plain, ![X3:del, X8:$i, X2:$i, X4:del, X13:del, X6:$i, X5:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ X4) @ X2) @ X5))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X3 @ X13) @ X2) @ X5))|~((mem @ X5 @ (arr @ X4 @ bool)))|~((mem @ X6 @ (arr @ X4 @ bool)))|~((mem @ X2 @ (arr @ X3 @ X4)))|~((mem @ X8 @ (arr @ X3 @ X4)))|~((epred4_4 @ X3 @ X13 @ X2 @ X5)))), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 10.75/1.68 thf(c_0_28, negated_conjecture, (mem @ esk5_0 @ (arr @ esk1_0 @ bool)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.75/1.68 thf(c_0_29, negated_conjecture, ![X2:$i, X3:del, X6:$i, X5:$i, X4:del]:((~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X3 @ X4) @ esk3_0) @ esk5_0)))|~((mem @ (esk7_5 @ esk5_0 @ esk3_0 @ X4 @ X3 @ X2) @ esk2_0))|~((epred4_4 @ esk2_0 @ esk1_0 @ X5 @ X6))|~((epred4_4 @ X3 @ X4 @ esk3_0 @ esk5_0))|~((p @ (ap @ esk5_0 @ X2)))|~((mem @ X2 @ X4)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26])).
% 10.75/1.68 thf(c_0_30, plain, ![X3:del, X6:$i, X5:$i, X4:del, X2:$i]:(((mem @ (esk7_5 @ X2 @ X5 @ X3 @ X4 @ X6) @ X4)|~((p @ (ap @ X2 @ X6)))|~((mem @ X6 @ X3))|~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X4 @ X3) @ X5) @ X2)))|~((epred4_4 @ X4 @ X3 @ X5 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 10.75/1.68 thf(c_0_31, negated_conjecture, ![X2:$i, X4:del, X3:del, X6:$i, X5:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ esk1_0) @ X2) @ X5))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ X3 @ X4) @ X2) @ X5))|~((mem @ X5 @ (arr @ esk1_0 @ bool)))|~((mem @ X2 @ (arr @ X3 @ esk1_0)))|~((mem @ X6 @ (arr @ X3 @ esk1_0)))|~((epred4_4 @ X3 @ X4 @ X2 @ X5)))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 10.75/1.68 thf(c_0_32, plain, ![X2:$i, X6:$i, X5:$i, X3:del]:((~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ esk2_0 @ X3) @ esk3_0) @ esk5_0)))|~((epred4_4 @ esk2_0 @ X3 @ esk3_0 @ esk5_0))|~((epred4_4 @ esk2_0 @ esk1_0 @ X2 @ X5))|~((p @ (ap @ esk5_0 @ X6)))|~((mem @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 10.75/1.68 thf(c_0_33, negated_conjecture, ![X2:$i, X3:del, X5:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ esk1_0) @ X2) @ X5))|(p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__EXISTS @ esk2_0 @ X3) @ X2) @ X5))|~((mem @ X5 @ (arr @ esk1_0 @ bool)))|~((mem @ X2 @ (arr @ esk2_0 @ esk1_0)))|~((epred4_4 @ esk2_0 @ X3 @ X2 @ X5)))), inference(spm,[status(thm)],[c_0_31, c_0_18])).
% 10.75/1.68 thf(c_0_34, negated_conjecture, ~((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ esk1_0) @ esk3_0) @ esk5_0))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.75/1.68 thf(c_0_35, plain, ![X2:$i, X6:$i, X5:$i, X3:del]:((~((epred4_4 @ esk2_0 @ X3 @ esk3_0 @ esk5_0))|~((epred4_4 @ esk2_0 @ esk1_0 @ X2 @ X5))|~((p @ (ap @ esk5_0 @ X6)))|~((mem @ X6 @ X3)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_28]), c_0_18])]), c_0_34])).
% 10.75/1.68 thf(c_0_36, plain, ![X2:$i, X6:$i, X5:$i, X3:del]:((~((mem @ esk5_0 @ (arr @ X3 @ bool)))|~((mem @ esk3_0 @ (arr @ esk2_0 @ X3)))|~((epred4_4 @ esk2_0 @ esk1_0 @ X2 @ X5))|~((p @ (ap @ esk5_0 @ X6)))|~((mem @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_35, c_0_23])).
% 10.75/1.68 thf(c_0_37, negated_conjecture, ![X2:$i, X5:$i, X6:$i]:((~((epred4_4 @ esk2_0 @ esk1_0 @ X2 @ X5))|~((p @ (ap @ esk5_0 @ X6)))|~((mem @ X6 @ esk1_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_18]), c_0_28])])).
% 10.75/1.68 thf(c_0_38, negated_conjecture, ![X2:$i, X5:$i, X6:$i]:((~((mem @ X2 @ (arr @ esk1_0 @ bool)))|~((mem @ X5 @ (arr @ esk2_0 @ esk1_0)))|~((p @ (ap @ esk5_0 @ X6)))|~((mem @ X6 @ esk1_0)))), inference(spm,[status(thm)],[c_0_37, c_0_23])).
% 10.75/1.68 thf(c_0_39, negated_conjecture, ![X2:$i, X5:$i]:((~((mem @ X2 @ (arr @ esk2_0 @ esk1_0)))|~((p @ (ap @ esk5_0 @ X5)))|~((mem @ X5 @ esk1_0)))), inference(spm,[status(thm)],[c_0_38, c_0_28])).
% 10.75/1.68 thf(c_0_40, negated_conjecture, ![X2:$i]:((~((p @ (ap @ esk5_0 @ X2)))|~((mem @ X2 @ esk1_0)))), inference(spm,[status(thm)],[c_0_39, c_0_18])).
% 10.75/1.68 thf(c_0_41, plain, ![X2:$i, X3:del, X4:del, X6:$i, X5:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ X4) @ X2) @ esk5_0))|~((mem @ (ap @ X2 @ (esk12_6 @ X5 @ X6 @ X4 @ X3 @ X2 @ esk5_0)) @ esk1_0))|~((mem @ esk5_0 @ (arr @ X4 @ bool)))|~((mem @ X2 @ (arr @ X3 @ X4)))|~((epred4_4 @ X3 @ X4 @ X6 @ X5)))), inference(spm,[status(thm)],[c_0_40, c_0_8])).
% 10.75/1.68 thf(c_0_42, negated_conjecture, ![X3:del, X5:$i, X4:del, X2:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X3 @ X4) @ esk3_0) @ esk5_0))|~((mem @ (esk12_6 @ X2 @ X5 @ X4 @ X3 @ esk3_0 @ esk5_0) @ esk2_0))|~((mem @ esk5_0 @ (arr @ X4 @ bool)))|~((mem @ esk3_0 @ (arr @ X3 @ X4)))|~((epred4_4 @ X3 @ X4 @ X5 @ X2)))), inference(spm,[status(thm)],[c_0_41, c_0_26])).
% 10.75/1.68 thf(c_0_43, plain, ![X2:$i, X3:del, X5:$i]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ X3) @ esk3_0) @ esk5_0))|~((mem @ esk5_0 @ (arr @ X3 @ bool)))|~((mem @ esk3_0 @ (arr @ esk2_0 @ X3)))|~((epred4_4 @ esk2_0 @ X3 @ X2 @ X5)))), inference(spm,[status(thm)],[c_0_42, c_0_13])).
% 10.75/1.68 thf(c_0_44, plain, ![X2:$i, X5:$i, X3:del]:(((p @ (ap @ (ap @ (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ esk2_0 @ X3) @ esk3_0) @ esk5_0))|~((mem @ esk5_0 @ (arr @ X3 @ bool)))|~((mem @ esk3_0 @ (arr @ esk2_0 @ X3)))|~((mem @ X2 @ (arr @ X3 @ bool)))|~((mem @ X5 @ (arr @ esk2_0 @ X3))))), inference(spm,[status(thm)],[c_0_43, c_0_23])).
% 10.75/1.68 thf(c_0_45, negated_conjecture, ![X2:$i]:(~((mem @ X2 @ (arr @ esk2_0 @ esk1_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_28]), c_0_28]), c_0_18])]), c_0_34])).
% 10.75/1.68 thf(c_0_46, negated_conjecture, ($false), inference(sr,[status(thm)],[c_0_18, c_0_45]), ['proof']).
% 10.75/1.68 % SZS output end CNFRefutation
% 10.75/1.68 % Parsed axioms : 75
% 10.75/1.68 % Removed by relevancy pruning/SinE : 48
% 10.75/1.68 % Initial clauses : 282
% 10.75/1.68 % Removed in clause preprocessing : 213
% 10.75/1.68 % Initial clauses in saturation : 69
% 10.75/1.68 % Processed clauses : 1899
% 10.75/1.68 % ...of these trivial : 0
% 10.75/1.68 % ...subsumed : 435
% 10.75/1.68 % ...remaining for further processing : 1464
% 10.75/1.68 % Other redundant clauses eliminated : 4
% 10.75/1.68 % Clauses deleted for lack of memory : 0
% 10.75/1.68 % Backward-subsumed : 192
% 10.75/1.68 % Backward-rewritten : 0
% 10.75/1.68 % Generated clauses : 24026
% 10.75/1.68 % ...of the previous two non-redundant : 23936
% 10.75/1.68 % ...aggressively subsumed : 0
% 10.75/1.68 % Contextual simplify-reflections : 22
% 10.75/1.68 % Paramodulations : 24020
% 10.75/1.68 % Factorizations : 0
% 10.75/1.68 % NegExts : 0
% 10.75/1.68 % Equation resolutions : 5
% 10.75/1.68 % Disequality decompositions : 0
% 10.75/1.68 % Total rewrite steps : 2101
% 10.75/1.68 % ...of those cached : 2097
% 10.75/1.68 % Propositional unsat checks : 0
% 10.75/1.68 % Propositional check models : 0
% 10.75/1.68 % Propositional check unsatisfiable : 0
% 10.75/1.68 % Propositional clauses : 0
% 10.75/1.68 % Propositional clauses after purity: 0
% 10.75/1.68 % Propositional unsat core size : 0
% 10.75/1.68 % Propositional preprocessing time : 0.000
% 10.75/1.68 % Propositional encoding time : 0.000
% 10.75/1.68 % Propositional solver time : 0.000
% 10.75/1.68 % Success case prop preproc time : 0.000
% 10.75/1.68 % Success case prop encoding time : 0.000
% 10.75/1.68 % Success case prop solver time : 0.000
% 10.75/1.68 % Current number of processed clauses : 1271
% 10.75/1.68 % Positive orientable unit clauses : 9
% 10.75/1.68 % Positive unorientable unit clauses: 0
% 10.75/1.68 % Negative unit clauses : 2
% 10.75/1.68 % Non-unit-clauses : 1260
% 10.75/1.68 % Current number of unprocessed clauses: 21980
% 10.75/1.68 % ...number of literals in the above : 194279
% 10.75/1.68 % Current number of archived formulas : 0
% 10.75/1.68 % Current number of archived clauses : 193
% 10.75/1.68 % Clause-clause subsumption calls (NU) : 217591
% 10.75/1.68 % Rec. Clause-clause subsumption calls : 14455
% 10.75/1.68 % Non-unit clause-clause subsumptions : 614
% 10.75/1.68 % Unit Clause-clause subsumption calls : 1208
% 10.75/1.68 % Rewrite failures with RHS unbound : 0
% 10.75/1.68 % BW rewrite match attempts : 0
% 10.75/1.68 % BW rewrite match successes : 0
% 10.75/1.68 % Condensation attempts : 0
% 10.75/1.68 % Condensation successes : 0
% 10.75/1.68 % Termbank termtop insertions : 1176861
% 10.75/1.68 % Search garbage collected termcells : 4710
% 10.75/1.68
% 10.75/1.68 % -------------------------------------------------
% 10.75/1.68 % User time : 1.201 s
% 10.75/1.68 % System time : 0.039 s
% 10.75/1.68 % Total time : 1.240 s
% 10.75/1.68 % Maximum resident set size: 4536 pages
% 10.75/1.68
% 10.75/1.68 % -------------------------------------------------
% 10.75/1.68 % User time : 1.204 s
% 10.75/1.68 % System time : 0.045 s
% 10.75/1.68 % Total time : 1.248 s
% 10.75/1.68 % Maximum resident set size: 4608 pages
% 10.75/1.68 % E exiting
%------------------------------------------------------------------------------