%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : PHI043^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:20:08 AM UTC 2026
% Result : Theorem 0.20s 0.27s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PHI043^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n007.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 13:18:11 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.07/0.24 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p
% 0.20/0.27 % Version: 3.5.1-ho
% 0.20/0.27 % Preprocessing class: HSMSSMSSMLLNHHN.
% 0.20/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.27 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.20/0.27 % Starting full_lambda_5 with 300s (1) cores
% 0.20/0.27 % Starting ho_unfolding_4 with 300s (1) cores
% 0.20/0.27 % Starting sh2 with 300s (1) cores
% 0.20/0.27 % new_ho_10_cnf2 with pid 3341070 completed with status 0
% 0.20/0.27 % Result found by new_ho_10_cnf2
% 0.20/0.27 % Preprocessing class: HSMSSMSSMLLNHHN.
% 0.20/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.27 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.20/0.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/0.27 % No SInE strategy applied
% 0.20/0.27 % Search class: HGHNF-FFSF32-SHHSMSBN
% 0.20/0.27 % partial match(1): HGHNF-FFSF33-SHHSMSBN
% 0.20/0.27 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.20/0.27 % Starting SubtermCWHack with 136s (1) cores
% 0.20/0.27 % Starting new_ho_10_cnf2 with 151s (1) cores
% 0.20/0.27 % Starting sh5l with 136s (1) cores
% 0.20/0.27 % Starting new_bool_1 with 136s (1) cores
% 0.20/0.27 % Starting new_bool_2 with 136s (1) cores
% 0.20/0.27 % SubtermCWHack with pid 3341075 completed with status 0
% 0.20/0.27 % Result found by SubtermCWHack
% 0.20/0.27 % Preprocessing class: HSMSSMSSMLLNHHN.
% 0.20/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.27 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.20/0.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/0.27 % No SInE strategy applied
% 0.20/0.27 % Search class: HGHNF-FFSF32-SHHSMSBN
% 0.20/0.27 % partial match(1): HGHNF-FFSF33-SHHSMSBN
% 0.20/0.27 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.20/0.27 % Starting SubtermCWHack with 136s (1) cores
% 0.20/0.27 % Preprocessing time : 0.001 s
% 0.20/0.27
% 0.20/0.27 % Proof found!
% 0.20/0.27 % SZS status Theorem
% 0.20/0.27 % SZS output start CNFRefutation
% 0.20/0.27 thf(decl_sort1, type, mu: $tType).
% 0.20/0.27 thf(decl_26, type, mnot: ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_29, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_31, type, mequiv: ($i > $o) > ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_34, type, mforall_indset: ((mu > $i > $o) > $i > $o) > $i > $o).
% 0.20/0.27 thf(decl_39, type, mbox_generic: ($i > $i > $o) > ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_40, type, mdia_generic: ($i > $i > $o) > ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_41, type, rel: $i > $i > $o).
% 0.20/0.27 thf(decl_42, type, mbox: ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_43, type, mdia: ($i > $o) > $i > $o).
% 0.20/0.27 thf(decl_44, type, mvalid: ($i > $o) > $o).
% 0.20/0.27 thf(decl_46, type, eiw_ind: $i > mu > $o).
% 0.20/0.27 thf(decl_47, type, mforall_eiw_ind: (mu > $i > $o) > $i > $o).
% 0.20/0.27 thf(decl_48, type, mexists_eiw_ind: (mu > $i > $o) > $i > $o).
% 0.20/0.27 thf(decl_49, type, p: (mu > $i > $o) > $i > $o).
% 0.20/0.27 thf(decl_51, type, esk2_3: $i > (mu > $i > $o) > (mu > $i > $o) > $i).
% 0.20/0.27 thf(decl_52, type, esk3_3: $i > (mu > $i > $o) > (mu > $i > $o) > mu).
% 0.20/0.27 thf(decl_53, type, esk4_0: $i).
% 0.20/0.27 thf(decl_54, type, epred1_0: mu > $i > $o).
% 0.20/0.27 thf(decl_55, type, epred2_0: mu > $i > $o).
% 0.20/0.27 thf(mdia_generic, axiom, ((mdia_generic)=(^[X15:$i > $i > $o, X4:$i > $o, X3:$i]:(?[X16:$i]:((((X15 @ X3 @ X16))&((X4 @ X16))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mdia_generic)).
% 0.20/0.27 thf(mexists_eiw_ind, axiom, ((mexists_eiw_ind)=(^[X18:mu > $i > $o]:(mnot @ (mforall_eiw_ind @ (^[X1:mu]:(mnot @ (X18 @ X1))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mexists_eiw_ind)).
% 0.20/0.27 thf(mnot, axiom, ((mnot)=(^[X4:$i > $o, X3:$i]:(~((X4 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mnot)).
% 0.20/0.27 thf(mforall_eiw_ind, axiom, ((mforall_eiw_ind)=(^[X17:mu > $i > $o, X3:$i]:(![X1:mu]:((((eiw_ind @ X3 @ X1))=>((X17 @ X1 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mforall_eiw_ind)).
% 0.20/0.27 thf(mbox_generic, axiom, ((mbox_generic)=(^[X15:$i > $i > $o, X4:$i > $o, X3:$i]:(![X16:$i]:(((~((X15 @ X3 @ X16)))|((X4 @ X16))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mbox_generic)).
% 0.20/0.27 thf(possible_instantiation_of_the_positive_variable_domain, conjecture, (mvalid @ (mforall_indset @ (^[X21:mu > $i > $o]:(mimplies @ (p @ X21) @ (mdia @ (mexists_eiw_ind @ (^[X1:mu]:(X21 @ X1)))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', possible_instantiation_of_the_positive_variable_domain)).
% 0.20/0.27 thf(mimplies, axiom, ((mimplies)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))=>((X5 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mimplies)).
% 0.20/0.27 thf(mforall_indset, axiom, ((mforall_indset)=(^[X7:(mu > $i > $o) > $i > $o, X3:$i]:(![X8:mu > $i > $o]:((X7 @ X8 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mforall_indset)).
% 0.20/0.27 thf(mdia, axiom, ((mdia)=(^[Z0:$i > $o, Z1:$i]:(?[X25:$i]:((((rel @ Z1 @ X25))&((Z0 @ X25))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mdia)).
% 0.20/0.27 thf(mvalid, axiom, ((mvalid)=(^[X4:$i > $o]:(![X3:$i]:((X4 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mvalid)).
% 0.20/0.27 thf(mequiv, axiom, ((mequiv)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))<=>((X5 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mequiv)).
% 0.20/0.27 thf(mbox, axiom, ((mbox)=(^[Z0:$i > $o, Z1:$i]:(![X24:$i]:(((~((rel @ Z1 @ X24)))|((Z0 @ X24))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', mbox)).
% 0.20/0.27 thf(axii, axiom, (mvalid @ (mforall_indset @ (^[X19:mu > $i > $o]:(mforall_indset @ (^[X20:mu > $i > $o]:(mimplies @ (mbox @ (mforall_eiw_ind @ (^[X1:mu]:(mequiv @ (X19 @ X1) @ (X20 @ X1))))) @ (mequiv @ (p @ X19) @ (p @ X20)))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', axii)).
% 0.20/0.27 thf(ax16, axiom, (mvalid @ (mnot @ (p @ (^[X1:mu, X3:$i]:(((X1)!=(X1))))))), file('/export/starexec/sandbox2/tmp/tmp.hO10dc0bu1/E---3.1_3341040.p', ax16)).
% 0.20/0.27 thf(c_0_14, plain, ((mdia_generic)=(^[Z0:$i > $i > $o, Z1:$i > $o, Z2:$i]:(?[X16:$i]:((((Z0 @ Z2 @ X16))&((Z1 @ X16))))))), inference(fof_simplification,[status(thm)],[mdia_generic])).
% 0.20/0.27 thf(c_0_15, plain, ((mexists_eiw_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(~((![X26:mu]:((((eiw_ind @ Z1 @ X26))=>((~((Z0 @ X26 @ Z1))))))))))), inference(fof_simplification,[status(thm)],[mexists_eiw_ind])).
% 0.20/0.27 thf(c_0_16, plain, ((mnot)=(^[Z0:$i > $o, Z1:$i]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot])).
% 0.20/0.27 thf(c_0_17, plain, ((mforall_eiw_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(![X1:mu]:((((eiw_ind @ Z1 @ X1))=>((Z0 @ X1 @ Z1))))))), inference(fof_simplification,[status(thm)],[mforall_eiw_ind])).
% 0.20/0.27 thf(c_0_18, plain, ((mbox_generic)=(^[Z0:$i > $i > $o, Z1:$i > $o, Z2:$i]:(![X16:$i]:(((~((Z0 @ Z2 @ X16)))|((Z1 @ X16))))))), inference(fof_simplification,[status(thm)],[mbox_generic])).
% 0.20/0.27 thf(c_0_19, negated_conjecture, ~((mvalid @ (mforall_indset @ (^[X21:mu > $i > $o]:(mimplies @ (p @ X21) @ (mdia @ (mexists_eiw_ind @ (^[X1:mu]:(X21 @ X1))))))))), inference(assume_negation,[status(cth)],[possible_instantiation_of_the_positive_variable_domain])).
% 0.20/0.27 thf(c_0_20, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies])).
% 0.20/0.27 thf(c_0_21, plain, ((mforall_indset)=(^[Z0:(mu > $i > $o) > $i > $o, Z1:$i]:(![X8:mu > $i > $o]:((Z0 @ X8 @ Z1))))), inference(fof_simplification,[status(thm)],[mforall_indset])).
% 0.20/0.27 thf(c_0_22, axiom, ((mdia)=(^[Z0:$i > $o, Z1:$i]:(?[X25:$i]:((((rel @ Z1 @ X25))&((Z0 @ X25))))))), inference(apply_def,[status(thm)],[mdia, c_0_14])).
% 0.20/0.27 thf(c_0_23, plain, ((mvalid)=(^[Z0:$i > $o]:(![X3:$i]:((Z0 @ X3))))), inference(fof_simplification,[status(thm)],[mvalid])).
% 0.20/0.27 thf(c_0_24, plain, ((mexists_eiw_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(~((![X26:mu]:((((eiw_ind @ Z1 @ X26))=>((~((Z0 @ X26 @ Z1))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_15, c_0_16]), c_0_17])).
% 0.20/0.27 thf(c_0_25, plain, ((mequiv)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))<=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mequiv])).
% 0.20/0.27 thf(c_0_26, axiom, ((mbox)=(^[Z0:$i > $o, Z1:$i]:(![X24:$i]:(((~((rel @ Z1 @ X24)))|((Z0 @ X24))))))), inference(apply_def,[status(thm)],[mbox, c_0_18])).
% 0.20/0.27 thf(c_0_27, negated_conjecture, ~(![X36:$i, X35:mu > $i > $o]:(((p @ X35 @ X36)=>?[X34:$i]:(((rel @ X36 @ X34)&~(![X33:mu]:(((eiw_ind @ X34 @ X33)=>~((X35 @ X33 @ X34)))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_19]), c_0_20]), c_0_21]), c_0_22]), c_0_23]), c_0_24])).
% 0.20/0.27 thf(c_0_28, plain, ![X32:$i, X31:mu > $i > $o, X30:mu > $i > $o]:((![X29:$i]:((~(rel @ X32 @ X29)|![X28:mu]:(((eiw_ind @ X29 @ X28)=>((X31 @ X28 @ X29)<=>(X30 @ X28 @ X29))))))=>((p @ X31 @ X32)<=>(p @ X30 @ X32)))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[axii]), c_0_20]), c_0_25]), c_0_21]), c_0_26]), c_0_23]), c_0_17])])).
% 0.20/0.27 thf(c_0_29, plain, ![X27:$i]:(~(p @ (^[Z0:mu, Z1:$i]:(~((Z0)))) @ X27)), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[ax16]), c_0_16]), c_0_23])])).
% 0.20/0.27 thf(c_0_30, negated_conjecture, ![X47:$i, X48:mu]:(((p @ epred1_0 @ esk4_0)&(~(rel @ esk4_0 @ X47)|(~(eiw_ind @ X47 @ X48)|~(epred1_0 @ X48 @ X47))))), 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_27])])])])])).
% 0.20/0.27 thf(c_0_31, plain, ![X40:$i, X41:mu > $i > $o, X42:mu > $i > $o]:((((~(p @ X41 @ X40)|(p @ X42 @ X40)|(rel @ X40 @ (esk2_3 @ X40 @ X41 @ X42)))&(~(p @ X42 @ X40)|(p @ X41 @ X40)|(rel @ X40 @ (esk2_3 @ X40 @ X41 @ X42))))&(((~(p @ X41 @ X40)|(p @ X42 @ X40)|(eiw_ind @ (esk2_3 @ X40 @ X41 @ X42) @ (esk3_3 @ X40 @ X41 @ X42)))&(~(p @ X42 @ X40)|(p @ X41 @ X40)|(eiw_ind @ (esk2_3 @ X40 @ X41 @ X42) @ (esk3_3 @ X40 @ X41 @ X42))))&(((~(p @ X41 @ X40)|(p @ X42 @ X40)|(~(X41 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))|~(X42 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))))&(~(p @ X42 @ X40)|(p @ X41 @ X40)|(~(X41 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))|~(X42 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42)))))&((~(p @ X41 @ X40)|(p @ X42 @ X40)|((X41 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))|(X42 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))))&(~(p @ X42 @ X40)|(p @ X41 @ X40)|((X41 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))|(X42 @ (esk3_3 @ X40 @ X41 @ X42) @ (esk2_3 @ X40 @ X41 @ X42))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])])])])).
% 0.20/0.27 thf(c_0_32, plain, ![X51:$i, X52:mu]:(((~(epred2_0 @ X52 @ X51)|((X52)!=(X52)))&(((X52)=(X52))|(epred2_0 @ X52 @ X51)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[])])])])).
% 0.20/0.27 thf(c_0_33, plain, ![X39:$i]:(~(p @ (^[Z0:mu, Z1:$i]:(~((Z0)))) @ X39)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_29])])).
% 0.20/0.27 thf(c_0_34, plain, ![X50:$i, X49:mu]:(((epred2_0 @ X49 @ X50)<=>~(((X49)=(X49))))), introduced(definition)).
% 0.20/0.27 thf(c_0_35, negated_conjecture, ![X1:mu, X3:$i]:((~((rel @ esk4_0 @ X3))|~((eiw_ind @ X3 @ X1))|~((epred1_0 @ X1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.20/0.27 thf(c_0_36, plain, ![X8:mu > $i > $o, X6:mu > $i > $o, X3:$i]:(((p @ X8 @ X3)|(rel @ X3 @ (esk2_3 @ X3 @ X8 @ X6))|~((p @ X6 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.20/0.27 thf(c_0_37, plain, ![X3:$i, X1:mu]:((~((epred2_0 @ X1 @ X3))|((X1)!=(X1)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.20/0.27 thf(c_0_38, plain, ![X8:mu > $i > $o, X6:mu > $i > $o, X3:$i]:(((p @ X8 @ X3)|(X8 @ (esk3_3 @ X3 @ X8 @ X6) @ (esk2_3 @ X3 @ X8 @ X6))|(X6 @ (esk3_3 @ X3 @ X8 @ X6) @ (esk2_3 @ X3 @ X8 @ X6))|~((p @ X6 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.20/0.27 thf(c_0_39, negated_conjecture, (p @ epred1_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.20/0.27 thf(c_0_40, plain, ![X3:$i]:(~((((p @ epred2_0 @ X3))=(($true))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_33]), c_0_34])).
% 0.20/0.27 thf(c_0_41, negated_conjecture, ![X6:mu > $i > $o, X1:mu, X8:mu > $i > $o]:(((p @ X6 @ esk4_0)|~((eiw_ind @ (esk2_3 @ esk4_0 @ X6 @ X8) @ X1))|~((epred1_0 @ X1 @ (esk2_3 @ esk4_0 @ X6 @ X8)))|~((p @ X8 @ esk4_0)))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.20/0.27 thf(c_0_42, plain, ![X8:mu > $i > $o, X6:mu > $i > $o, X3:$i]:(((p @ X8 @ X3)|(eiw_ind @ (esk2_3 @ X3 @ X8 @ X6) @ (esk3_3 @ X3 @ X8 @ X6))|~((p @ X6 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.20/0.27 thf(c_0_43, plain, ![X1:mu, X3:$i]:(~((epred2_0 @ X1 @ X3))), inference(cn,[status(thm)],[c_0_37])).
% 0.20/0.27 thf(c_0_44, negated_conjecture, ![X6:mu > $i > $o]:(((epred1_0 @ (esk3_3 @ esk4_0 @ X6 @ epred1_0) @ (esk2_3 @ esk4_0 @ X6 @ epred1_0))|(X6 @ (esk3_3 @ esk4_0 @ X6 @ epred1_0) @ (esk2_3 @ esk4_0 @ X6 @ epred1_0))|(p @ X6 @ esk4_0))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 0.20/0.27 thf(c_0_45, plain, ![X3:$i]:(~((p @ epred2_0 @ X3))), inference(cn,[status(thm)],[c_0_40])).
% 0.20/0.27 thf(c_0_46, negated_conjecture, ![X6:mu > $i > $o, X8:mu > $i > $o]:(((p @ X6 @ esk4_0)|~((epred1_0 @ (esk3_3 @ esk4_0 @ X6 @ X8) @ (esk2_3 @ esk4_0 @ X6 @ X8)))|~((p @ X8 @ esk4_0)))), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 0.20/0.27 thf(c_0_47, plain, (epred1_0 @ (esk3_3 @ esk4_0 @ epred2_0 @ epred1_0) @ (esk2_3 @ esk4_0 @ epred2_0 @ epred1_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45])).
% 0.20/0.27 thf(c_0_48, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_47]), c_0_39])]), c_0_45]), ['proof']).
% 0.20/0.27 % SZS output end CNFRefutation
% 0.20/0.27 % Parsed axioms : 56
% 0.20/0.27 % Removed by relevancy pruning/SinE : 0
% 0.20/0.27 % Initial clauses : 42
% 0.20/0.27 % Removed in clause preprocessing : 29
% 0.20/0.27 % Initial clauses in saturation : 13
% 0.20/0.27 % Processed clauses : 18
% 0.20/0.27 % ...of these trivial : 0
% 0.20/0.27 % ...subsumed : 0
% 0.20/0.27 % ...remaining for further processing : 18
% 0.20/0.27 % Other redundant clauses eliminated : 0
% 0.20/0.27 % Clauses deleted for lack of memory : 0
% 0.20/0.27 % Backward-subsumed : 0
% 0.20/0.27 % Backward-rewritten : 0
% 0.20/0.27 % Generated clauses : 16
% 0.20/0.27 % ...of the previous two non-redundant : 9
% 0.20/0.27 % ...aggressively subsumed : 0
% 0.20/0.27 % Contextual simplify-reflections : 0
% 0.20/0.27 % Paramodulations : 14
% 0.20/0.27 % Factorizations : 2
% 0.20/0.27 % NegExts : 0
% 0.20/0.27 % Equation resolutions : 0
% 0.20/0.27 % Disequality decompositions : 0
% 0.20/0.27 % Total rewrite steps : 6
% 0.20/0.27 % ...of those cached : 5
% 0.20/0.27 % Propositional unsat checks : 0
% 0.20/0.27 % Propositional check models : 0
% 0.20/0.27 % Propositional check unsatisfiable : 0
% 0.20/0.27 % Propositional clauses : 0
% 0.20/0.27 % Propositional clauses after purity: 0
% 0.20/0.27 % Propositional unsat core size : 0
% 0.20/0.27 % Propositional preprocessing time : 0.000
% 0.20/0.27 % Propositional encoding time : 0.000
% 0.20/0.27 % Propositional solver time : 0.000
% 0.20/0.27 % Success case prop preproc time : 0.000
% 0.20/0.27 % Success case prop encoding time : 0.000
% 0.20/0.27 % Success case prop solver time : 0.000
% 0.20/0.27 % Current number of processed clauses : 18
% 0.20/0.27 % Positive orientable unit clauses : 3
% 0.20/0.27 % Positive unorientable unit clauses: 0
% 0.20/0.27 % Negative unit clauses : 2
% 0.20/0.27 % Non-unit-clauses : 13
% 0.20/0.27 % Current number of unprocessed clauses: 4
% 0.20/0.27 % ...number of literals in the above : 14
% 0.20/0.27 % Current number of archived formulas : 0
% 0.20/0.27 % Current number of archived clauses : 0
% 0.20/0.27 % Clause-clause subsumption calls (NU) : 18
% 0.20/0.27 % Rec. Clause-clause subsumption calls : 10
% 0.20/0.27 % Non-unit clause-clause subsumptions : 0
% 0.20/0.27 % Unit Clause-clause subsumption calls : 1
% 0.20/0.27 % Rewrite failures with RHS unbound : 0
% 0.20/0.27 % BW rewrite match attempts : 0
% 0.20/0.27 % BW rewrite match successes : 0
% 0.20/0.27 % Condensation attempts : 0
% 0.20/0.27 % Condensation successes : 0
% 0.20/0.27 % Termbank termtop insertions : 2953
% 0.20/0.27 % Search garbage collected termcells : 696
% 0.20/0.27
% 0.20/0.27 % -------------------------------------------------
% 0.20/0.27 % User time : 0.005 s
% 0.20/0.27 % System time : 0.004 s
% 0.20/0.27 % Total time : 0.009 s
% 0.20/0.27 % Maximum resident set size: 3688 pages
% 0.20/0.27
% 0.20/0.27 % -------------------------------------------------
% 0.20/0.27 % User time : 0.011 s
% 0.20/0.27 % System time : 0.014 s
% 0.20/0.27 % Total time : 0.024 s
% 0.20/0.27 % Maximum resident set size: 4864 pages
% 0.20/0.27 % E exiting
%------------------------------------------------------------------------------