%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : LCL950^17 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Wed Sep 30 08:12:53 AM UTC 2026
% Result : Theorem 143.05s 21.75s
% Output : CNFRefutation 143.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL950^17 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n009.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 10:50:15 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.08/0.26 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.9LSHPwuVQG/E---3.1_3847868.p
% 143.05/21.75 % Version: 3.5.1-ho
% 143.05/21.75 % Preprocessing class: HSMSSMSSMLLNHSN.
% 143.05/21.75 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 143.05/21.75 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 143.05/21.75 % Starting post_as_ho3 with 300s (1) cores
% 143.05/21.75 % Starting new_ho_12 with 300s (1) cores
% 143.05/21.75 % Starting new_bool_2 with 300s (1) cores
% 143.05/21.75 % new_ho_12 with pid 3847883 completed with status 0
% 143.05/21.75 % Result found by new_ho_12
% 143.05/21.75 % Preprocessing class: HSMSSMSSMLLNHSN.
% 143.05/21.75 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 143.05/21.75 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 143.05/21.75 % Starting post_as_ho3 with 300s (1) cores
% 143.05/21.75 % Starting new_ho_12 with 300s (1) cores
% 143.05/21.75 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 143.05/21.75 % No SInE strategy applied
% 143.05/21.75 % Search class: HGUNS-FFMM33-SHSSMFNN
% 143.05/21.75 % partial match(2): HGHNS-FFMM32-SHSSMFNN
% 143.05/21.75 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 143.05/21.75 % Starting SubtermCWHack with 28s (1) cores
% 143.05/21.75 % SubtermCWHack with pid 3847889 completed with status 0
% 143.05/21.75 % Result found by SubtermCWHack
% 143.05/21.75 % Preprocessing class: HSMSSMSSMLLNHSN.
% 143.05/21.75 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 143.05/21.75 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 143.05/21.75 % Starting post_as_ho3 with 300s (1) cores
% 143.05/21.75 % Starting new_ho_12 with 300s (1) cores
% 143.05/21.75 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 143.05/21.75 % No SInE strategy applied
% 143.05/21.75 % Search class: HGUNS-FFMM33-SHSSMFNN
% 143.05/21.75 % partial match(2): HGHNS-FFMM32-SHSSMFNN
% 143.05/21.75 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 143.05/21.75 % Starting SubtermCWHack with 28s (1) cores
% 143.05/21.75 % Preprocessing time : 0.002 s
% 143.05/21.75
% 143.05/21.75 % Proof found!
% 143.05/21.75 % SZS status Theorem
% 143.05/21.75 % SZS output start CNFRefutation
% 143.05/21.75 thf(decl_sort1, type, mworld: $tType).
% 143.05/21.75 thf(decl_23, type, mrel: mworld > mworld > $o).
% 143.05/21.75 thf(decl_24, type, mactual: mworld).
% 143.05/21.75 thf(decl_25, type, mlocal: (mworld > $o) > $o).
% 143.05/21.75 thf(decl_27, type, mand: (mworld > $o) > (mworld > $o) > mworld > $o).
% 143.05/21.75 thf(decl_29, type, mimplies: (mworld > $o) > (mworld > $o) > mworld > $o).
% 143.05/21.75 thf(decl_31, type, mbox: (mworld > $o) > mworld > $o).
% 143.05/21.75 thf(decl_33, type, eiw_di: $i > mworld > $o).
% 143.05/21.75 thf(decl_34, type, mforall_di: ($i > mworld > $o) > mworld > $o).
% 143.05/21.75 thf(decl_35, type, mexists_di: ($i > mworld > $o) > mworld > $o).
% 143.05/21.75 thf(decl_36, type, intersect: $i > $i > mworld > $o).
% 143.05/21.75 thf(decl_37, type, member: $i > $i > mworld > $o).
% 143.05/21.75 thf(decl_38, type, epred1_3: $i > mworld > $i > $o).
% 143.05/21.75 thf(decl_41, type, esk3_0: mworld).
% 143.05/21.75 thf(decl_42, type, esk4_0: $i).
% 143.05/21.75 thf(decl_43, type, esk5_0: mworld).
% 143.05/21.75 thf(decl_44, type, esk6_0: $i).
% 143.05/21.75 thf(decl_45, type, esk7_0: mworld).
% 143.05/21.75 thf(decl_46, type, esk8_0: $i).
% 143.05/21.75 thf(decl_47, type, esk9_0: mworld).
% 143.05/21.75 thf(decl_48, type, esk10_0: mworld).
% 143.05/21.75 thf(decl_49, type, esk11_4: $i > mworld > $i > mworld > mworld).
% 143.05/21.75 thf(decl_50, type, esk12_4: $i > mworld > $i > mworld > $i).
% 143.05/21.75 thf(decl_51, type, esk13_5: $i > mworld > $i > mworld > $i > mworld).
% 143.05/21.75 thf(decl_52, type, esk14_5: $i > mworld > $i > mworld > $i > mworld).
% 143.05/21.75 thf(prove_th13, conjecture, (mlocal @ (mbox @ (mforall_di @ (^[X14:$i]:(mbox @ (mforall_di @ (^[X11:$i]:(mbox @ (mforall_di @ (^[X12:$i]:(mbox @ (mimplies @ (mand @ (mbox @ (member @ X14 @ X11)) @ (mbox @ (member @ X14 @ X12))) @ (mbox @ (intersect @ X11 @ X12)))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', prove_th13)).
% 143.05/21.75 thf(mlocal_def, axiom, ((mlocal)=(^[X1:mworld > $o]:((X1 @ mactual)))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mlocal_def)).
% 143.05/21.75 thf(mand_def, axiom, ((mand)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))&((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mand_def)).
% 143.05/21.75 thf(mimplies_def, axiom, ((mimplies)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))=>((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mimplies_def)).
% 143.05/21.75 thf(mbox_def, axiom, ((mbox)=(^[X1:mworld > $o, X3:mworld]:(![X5:mworld]:((((mrel @ X3 @ X5))=>((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mbox_def)).
% 143.05/21.75 thf(mforall_di_def, axiom, ((mforall_di)=(^[X8:$i > mworld > $o, X3:mworld]:(![X7:$i]:((((eiw_di @ X7 @ X3))=>((X8 @ X7 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mforall_di_def)).
% 143.05/21.75 thf(mrel_euclidean, axiom, ![X3:mworld, X5:mworld, X6:mworld]:((((mrel @ X3 @ X6)&(mrel @ X3 @ X5))=>(mrel @ X6 @ X5))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mrel_euclidean)).
% 143.05/21.75 thf(mrel_reflexive, axiom, ![X3:mworld]:((mrel @ X3 @ X3)), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mrel_reflexive)).
% 143.05/21.75 thf(eiw_di_cumul, axiom, ![X3:mworld, X5:mworld, X7:$i]:((((eiw_di @ X7 @ X3)&(mrel @ X3 @ X5))=>(eiw_di @ X7 @ X5))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', eiw_di_cumul)).
% 143.05/21.75 thf(mexists_di_def, axiom, ((mexists_di)=(^[X9:$i > mworld > $o, X3:mworld]:(?[X7:$i]:((((eiw_di @ X7 @ X3))&((X9 @ X7 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', mexists_di_def)).
% 143.05/21.75 thf(intersect_defn, axiom, (mlocal @ (mbox @ (mforall_di @ (^[X10:$i]:(mbox @ (mforall_di @ (^[X11:$i]:(mand @ (mbox @ (mimplies @ (mbox @ (intersect @ X10 @ X11)) @ (mexists_di @ (^[X12:$i]:(mand @ (mbox @ (member @ X12 @ X10)) @ (mbox @ (member @ X12 @ X11))))))) @ (mbox @ (mimplies @ (mexists_di @ (^[X12:$i]:(mand @ (mbox @ (member @ X12 @ X10)) @ (mbox @ (member @ X12 @ X11))))) @ (mbox @ (intersect @ X10 @ X11)))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9LSHPwuVQG/E---3.1_3847868.p', intersect_defn)).
% 143.05/21.75 thf(c_0_11, negated_conjecture, ~((mlocal @ (mbox @ (mforall_di @ (^[X14:$i]:(mbox @ (mforall_di @ (^[X11:$i]:(mbox @ (mforall_di @ (^[X12:$i]:(mbox @ (mimplies @ (mand @ (mbox @ (member @ X14 @ X11)) @ (mbox @ (member @ X14 @ X12))) @ (mbox @ (intersect @ X11 @ X12))))))))))))))), inference(assume_negation,[status(cth)],[prove_th13])).
% 143.05/21.75 thf(c_0_12, plain, ((mlocal)=(^[Z0:mworld > $o]:((Z0 @ mactual)))), inference(fof_simplification,[status(thm)],[mlocal_def])).
% 143.05/21.75 thf(c_0_13, plain, ((mand)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand_def])).
% 143.05/21.75 thf(c_0_14, plain, ((mimplies)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies_def])).
% 143.05/21.75 thf(c_0_15, plain, ((mbox)=(^[Z0:mworld > $o, Z1:mworld]:(![X5:mworld]:((((mrel @ Z1 @ X5))=>((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mbox_def])).
% 143.05/21.75 thf(c_0_16, plain, ((mforall_di)=(^[Z0:$i > mworld > $o, Z1:mworld]:(![X7:$i]:((((eiw_di @ X7 @ Z1))=>((Z0 @ X7 @ Z1))))))), inference(fof_simplification,[status(thm)],[mforall_di_def])).
% 143.05/21.75 thf(c_0_17, negated_conjecture, ~(![X54:mworld]:(((mrel @ mactual @ X54)=>![X53:$i]:(((eiw_di @ X53 @ X54)=>![X52:mworld]:(((mrel @ X54 @ X52)=>![X51:$i]:(((eiw_di @ X51 @ X52)=>![X50:mworld]:(((mrel @ X52 @ X50)=>![X49:$i]:(((eiw_di @ X49 @ X50)=>![X48:mworld]:(((mrel @ X50 @ X48)=>((![X45:mworld]:(((mrel @ X48 @ X45)=>(member @ X53 @ X51 @ X45)))&![X46:mworld]:(((mrel @ X48 @ X46)=>(member @ X53 @ X49 @ X46))))=>![X47:mworld]:(((mrel @ X48 @ X47)=>(intersect @ X51 @ X49 @ X47))))))))))))))))))), 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_11]), c_0_12]), c_0_13]), c_0_14]), c_0_15]), c_0_16])).
% 143.05/21.75 thf(c_0_18, plain, ![X56:mworld, X57:mworld, X58:mworld]:((~(mrel @ X56 @ X58)|~(mrel @ X56 @ X57)|(mrel @ X58 @ X57))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mrel_euclidean])])])).
% 143.05/21.75 thf(c_0_19, plain, ![X55:mworld]:((mrel @ X55 @ X55)), inference(variable_rename,[status(thm)],[mrel_reflexive])).
% 143.05/21.75 thf(c_0_20, negated_conjecture, ![X82:mworld, X83:mworld]:(((mrel @ mactual @ esk3_0)&((eiw_di @ esk4_0 @ esk3_0)&((mrel @ esk3_0 @ esk5_0)&((eiw_di @ esk6_0 @ esk5_0)&((mrel @ esk5_0 @ esk7_0)&((eiw_di @ esk8_0 @ esk7_0)&((mrel @ esk7_0 @ esk9_0)&(((~(mrel @ esk9_0 @ X82)|(member @ esk4_0 @ esk6_0 @ X82))&(~(mrel @ esk9_0 @ X83)|(member @ esk4_0 @ esk8_0 @ X83)))&((mrel @ esk9_0 @ esk10_0)&~(intersect @ esk6_0 @ esk8_0 @ esk10_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_17])])])])])).
% 143.05/21.75 thf(c_0_21, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((mrel @ X5 @ X6)|~((mrel @ X3 @ X5))|~((mrel @ X3 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 143.05/21.75 thf(c_0_22, plain, ![X3:mworld]:((mrel @ X3 @ X3)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 143.05/21.75 thf(c_0_23, negated_conjecture, (mrel @ esk3_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_24, plain, ![X5:mworld, X3:mworld]:(((mrel @ X3 @ X5)|~((mrel @ X5 @ X3)))), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 143.05/21.75 thf(c_0_25, negated_conjecture, (mrel @ mactual @ esk3_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_26, plain, ![X61:mworld, X62:mworld, X63:$i]:((~(eiw_di @ X63 @ X61)|~(mrel @ X61 @ X62)|(eiw_di @ X63 @ X62))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[eiw_di_cumul])])])).
% 143.05/21.75 thf(c_0_27, negated_conjecture, ![X3:mworld]:(((mrel @ X3 @ esk5_0)|~((mrel @ esk3_0 @ X3)))), inference(spm,[status(thm)],[c_0_21, c_0_23])).
% 143.05/21.75 thf(c_0_28, negated_conjecture, (mrel @ esk3_0 @ mactual), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 143.05/21.75 thf(c_0_29, negated_conjecture, (mrel @ esk5_0 @ esk7_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_30, plain, ![X36:$i, X35:mworld, X34:$i]:(((epred1_3 @ X34 @ X35 @ X36)<=>(![X28:mworld]:(((mrel @ X35 @ X28)=>(![X24:mworld]:(((mrel @ X28 @ X24)=>(intersect @ X36 @ X34 @ X24)))=>?[X27:$i]:(((eiw_di @ X27 @ X28)&(![X25:mworld]:(((mrel @ X28 @ X25)=>(member @ X27 @ X36 @ X25)))&![X26:mworld]:(((mrel @ X28 @ X26)=>(member @ X27 @ X34 @ X26)))))))))&![X33:mworld]:(((mrel @ X35 @ X33)=>(?[X31:$i]:(((eiw_di @ X31 @ X33)&(![X29:mworld]:(((mrel @ X33 @ X29)=>(member @ X31 @ X36 @ X29)))&![X30:mworld]:(((mrel @ X33 @ X30)=>(member @ X31 @ X34 @ X30))))))=>![X32:mworld]:(((mrel @ X33 @ X32)=>(intersect @ X36 @ X34 @ X32))))))))), introduced(definition)).
% 143.05/21.75 thf(c_0_31, plain, ![X3:mworld, X7:$i, X5:mworld]:(((eiw_di @ X7 @ X5)|~((eiw_di @ X7 @ X3))|~((mrel @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 143.05/21.75 thf(c_0_32, negated_conjecture, (mrel @ esk7_0 @ esk9_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_33, negated_conjecture, (mrel @ mactual @ esk5_0), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 143.05/21.75 thf(c_0_34, negated_conjecture, ![X3:mworld]:(((mrel @ X3 @ esk7_0)|~((mrel @ esk5_0 @ X3)))), inference(spm,[status(thm)],[c_0_21, c_0_29])).
% 143.05/21.75 thf(c_0_35, negated_conjecture, (mrel @ esk5_0 @ esk3_0), inference(spm,[status(thm)],[c_0_24, c_0_23])).
% 143.05/21.75 thf(c_0_36, plain, ![X36:$i, X35:mworld, X34:$i]:(((epred1_3 @ X34 @ X35 @ X36)=>(![X28:mworld]:(((mrel @ X35 @ X28)=>(![X24:mworld]:(((mrel @ X28 @ X24)=>(intersect @ X36 @ X34 @ X24)))=>?[X27:$i]:(((eiw_di @ X27 @ X28)&(![X25:mworld]:(((mrel @ X28 @ X25)=>(member @ X27 @ X36 @ X25)))&![X26:mworld]:(((mrel @ X28 @ X26)=>(member @ X27 @ X34 @ X26)))))))))&![X33:mworld]:(((mrel @ X35 @ X33)=>(?[X31:$i]:(((eiw_di @ X31 @ X33)&(![X29:mworld]:(((mrel @ X33 @ X29)=>(member @ X31 @ X36 @ X29)))&![X30:mworld]:(((mrel @ X33 @ X30)=>(member @ X31 @ X34 @ X30))))))=>![X32:mworld]:(((mrel @ X33 @ X32)=>(intersect @ X36 @ X34 @ X32))))))))), inference(split_equiv,[status(thm)],[c_0_30])).
% 143.05/21.75 thf(c_0_37, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk9_0)|~((eiw_di @ X7 @ esk7_0)))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 143.05/21.75 thf(c_0_38, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk7_0)|~((eiw_di @ X7 @ esk5_0)))), inference(spm,[status(thm)],[c_0_31, c_0_29])).
% 143.05/21.75 thf(c_0_39, plain, ((mexists_di)=(^[Z0:$i > mworld > $o, Z1:mworld]:(?[X7:$i]:((((eiw_di @ X7 @ Z1))&((Z0 @ X7 @ Z1))))))), inference(fof_simplification,[status(thm)],[mexists_di_def])).
% 143.05/21.75 thf(c_0_40, negated_conjecture, (mrel @ esk5_0 @ mactual), inference(spm,[status(thm)],[c_0_24, c_0_33])).
% 143.05/21.75 thf(c_0_41, negated_conjecture, (mrel @ esk3_0 @ esk7_0), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 143.05/21.75 thf(c_0_42, plain, ![X85:$i, X86:mworld, X87:$i, X88:mworld, X91:mworld, X92:mworld, X93:mworld, X94:$i, X97:mworld]:((((((eiw_di @ (esk12_4 @ X85 @ X86 @ X87 @ X88) @ X88)|(mrel @ X88 @ (esk11_4 @ X85 @ X86 @ X87 @ X88))|~(mrel @ X86 @ X88)|~(epred1_3 @ X87 @ X86 @ X85))&((~(mrel @ X88 @ X91)|(member @ (esk12_4 @ X85 @ X86 @ X87 @ X88) @ X85 @ X91)|(mrel @ X88 @ (esk11_4 @ X85 @ X86 @ X87 @ X88))|~(mrel @ X86 @ X88)|~(epred1_3 @ X87 @ X86 @ X85))&(~(mrel @ X88 @ X92)|(member @ (esk12_4 @ X85 @ X86 @ X87 @ X88) @ X87 @ X92)|(mrel @ X88 @ (esk11_4 @ X85 @ X86 @ X87 @ X88))|~(mrel @ X86 @ X88)|~(epred1_3 @ X87 @ X86 @ X85))))&(((eiw_di @ (esk12_4 @ X85 @ X86 @ X87 @ X88) @ X88)|~(intersect @ X85 @ X87 @ (esk11_4 @ X85 @ X86 @ X87 @ X88))|~(mrel @ X86 @ X88)|~(epred1_3 @ X87 @ X86 @ X85))&((~(mrel @ X88 @ X91)|(member @ (esk12_4 @ X85 @ X86 @ X87 @ X88) @ X85 @ X91)|~(intersect @ X85 @ X87 @ (esk11_4 @ X85 @ X86 @ X87 @ X88))|~(mrel @ X86 @ X88)|~(epred1_3 @ X87 @ X86 @ X85))&(~(mrel @ X88 @ X92)|(member @ (esk12_4 @ X85 @ X86 @ X87 @ X88) @ X87 @ X92)|~(intersect @ X85 @ X87 @ (esk11_4 @ X85 @ X86 @ X87 @ X88))|~(mrel @ X86 @ X88)|~(epred1_3 @ X87 @ X86 @ X85)))))&((((mrel @ X93 @ (esk14_5 @ X85 @ X86 @ X87 @ X93 @ X94))|(mrel @ X93 @ (esk13_5 @ X85 @ X86 @ X87 @ X93 @ X94))|~(eiw_di @ X94 @ X93)|(~(mrel @ X93 @ X97)|(intersect @ X85 @ X87 @ X97))|~(mrel @ X86 @ X93)|~(epred1_3 @ X87 @ X86 @ X85))&(~(member @ X94 @ X87 @ (esk14_5 @ X85 @ X86 @ X87 @ X93 @ X94))|(mrel @ X93 @ (esk13_5 @ X85 @ X86 @ X87 @ X93 @ X94))|~(eiw_di @ X94 @ X93)|(~(mrel @ X93 @ X97)|(intersect @ X85 @ X87 @ X97))|~(mrel @ X86 @ X93)|~(epred1_3 @ X87 @ X86 @ X85)))&(((mrel @ X93 @ (esk14_5 @ X85 @ X86 @ X87 @ X93 @ X94))|~(member @ X94 @ X85 @ (esk13_5 @ X85 @ X86 @ X87 @ X93 @ X94))|~(eiw_di @ X94 @ X93)|(~(mrel @ X93 @ X97)|(intersect @ X85 @ X87 @ X97))|~(mrel @ X86 @ X93)|~(epred1_3 @ X87 @ X86 @ X85))&(~(member @ X94 @ X87 @ (esk14_5 @ X85 @ X86 @ X87 @ X93 @ X94))|~(member @ X94 @ X85 @ (esk13_5 @ X85 @ X86 @ X87 @ X93 @ X94))|~(eiw_di @ X94 @ X93)|(~(mrel @ X93 @ X97)|(intersect @ X85 @ X87 @ X97))|~(mrel @ X86 @ X93)|~(epred1_3 @ X87 @ X86 @ X85)))))), 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_36])])])])])])).
% 143.05/21.75 thf(c_0_43, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk9_0)|~((eiw_di @ X7 @ esk5_0)))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 143.05/21.75 thf(c_0_44, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk5_0)|~((eiw_di @ X7 @ esk3_0)))), inference(spm,[status(thm)],[c_0_31, c_0_23])).
% 143.05/21.75 thf(c_0_45, plain, ![X37:mworld]:(((mrel @ mactual @ X37)=>![X36:$i]:(((eiw_di @ X36 @ X37)=>![X35:mworld]:(((mrel @ X37 @ X35)=>![X34:$i]:(((eiw_di @ X34 @ X35)=>(epred1_3 @ X34 @ X35 @ X36))))))))), 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(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[intersect_defn]), c_0_12]), c_0_13]), c_0_14]), c_0_15]), c_0_16]), c_0_39]), c_0_30])).
% 143.05/21.75 thf(c_0_46, negated_conjecture, (mrel @ mactual @ esk7_0), inference(spm,[status(thm)],[c_0_34, c_0_40])).
% 143.05/21.75 thf(c_0_47, negated_conjecture, ![X3:mworld]:(((mrel @ X3 @ esk9_0)|~((mrel @ esk7_0 @ X3)))), inference(spm,[status(thm)],[c_0_21, c_0_32])).
% 143.05/21.75 thf(c_0_48, negated_conjecture, (mrel @ esk7_0 @ esk3_0), inference(spm,[status(thm)],[c_0_24, c_0_41])).
% 143.05/21.75 thf(c_0_49, plain, ![X5:mworld, X3:mworld, X7:$i, X10:$i, X6:mworld, X11:$i]:(((mrel @ X5 @ (esk13_5 @ X11 @ X3 @ X10 @ X5 @ X7))|(intersect @ X11 @ X10 @ X6)|~((member @ X7 @ X10 @ (esk14_5 @ X11 @ X3 @ X10 @ X5 @ X7)))|~((eiw_di @ X7 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((epred1_3 @ X10 @ X3 @ X11)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 143.05/21.75 thf(c_0_50, negated_conjecture, ![X3:mworld]:(((member @ esk4_0 @ esk8_0 @ X3)|~((mrel @ esk9_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_51, plain, ![X3:mworld, X6:mworld, X5:mworld, X11:$i, X10:$i, X7:$i]:(((mrel @ X3 @ (esk14_5 @ X7 @ X5 @ X10 @ X3 @ X11))|(mrel @ X3 @ (esk13_5 @ X7 @ X5 @ X10 @ X3 @ X11))|(intersect @ X7 @ X10 @ X6)|~((eiw_di @ X11 @ X3))|~((mrel @ X3 @ X6))|~((mrel @ X5 @ X3))|~((epred1_3 @ X10 @ X5 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 143.05/21.75 thf(c_0_52, negated_conjecture, (mrel @ esk9_0 @ esk10_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_53, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk9_0)|~((eiw_di @ X7 @ esk3_0)))), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 143.05/21.75 thf(c_0_54, negated_conjecture, (eiw_di @ esk4_0 @ esk3_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_55, plain, ![X64:mworld, X65:$i, X66:mworld, X67:$i]:((~(mrel @ mactual @ X64)|(~(eiw_di @ X65 @ X64)|(~(mrel @ X64 @ X66)|(~(eiw_di @ X67 @ X66)|(epred1_3 @ X67 @ X66 @ X65)))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_45])])])])).
% 143.05/21.75 thf(c_0_56, negated_conjecture, (eiw_di @ esk6_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_57, negated_conjecture, (mrel @ esk7_0 @ mactual), inference(spm,[status(thm)],[c_0_24, c_0_46])).
% 143.05/21.75 thf(c_0_58, negated_conjecture, (mrel @ esk3_0 @ esk9_0), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 143.05/21.75 thf(c_0_59, negated_conjecture, (mrel @ esk7_0 @ esk5_0), inference(spm,[status(thm)],[c_0_24, c_0_29])).
% 143.05/21.75 thf(c_0_60, negated_conjecture, ![X7:$i, X6:mworld, X5:mworld, X3:mworld]:(((mrel @ X3 @ (esk13_5 @ X7 @ X5 @ esk8_0 @ X3 @ esk4_0))|(intersect @ X7 @ esk8_0 @ X6)|~((mrel @ esk9_0 @ (esk14_5 @ X7 @ X5 @ esk8_0 @ X3 @ esk4_0)))|~((epred1_3 @ esk8_0 @ X5 @ X7))|~((eiw_di @ esk4_0 @ X3))|~((mrel @ X3 @ X6))|~((mrel @ X5 @ X3)))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 143.05/21.75 thf(c_0_61, negated_conjecture, ![X7:$i, X11:$i, X10:$i, X3:mworld]:(((mrel @ esk9_0 @ (esk13_5 @ X7 @ X3 @ X10 @ esk9_0 @ X11))|(mrel @ esk9_0 @ (esk14_5 @ X7 @ X3 @ X10 @ esk9_0 @ X11))|(intersect @ X7 @ X10 @ esk10_0)|~((epred1_3 @ X10 @ X3 @ X7))|~((eiw_di @ X11 @ esk9_0))|~((mrel @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_51, c_0_52])).
% 143.05/21.75 thf(c_0_62, negated_conjecture, (eiw_di @ esk4_0 @ esk9_0), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 143.05/21.75 thf(c_0_63, plain, ![X3:mworld, X10:$i, X7:$i, X5:mworld]:(((epred1_3 @ X10 @ X5 @ X7)|~((mrel @ mactual @ X3))|~((eiw_di @ X7 @ X3))|~((mrel @ X3 @ X5))|~((eiw_di @ X10 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 143.05/21.75 thf(c_0_64, negated_conjecture, (eiw_di @ esk6_0 @ esk9_0), inference(spm,[status(thm)],[c_0_43, c_0_56])).
% 143.05/21.75 thf(c_0_65, negated_conjecture, (mrel @ mactual @ esk9_0), inference(spm,[status(thm)],[c_0_47, c_0_57])).
% 143.05/21.75 thf(c_0_66, negated_conjecture, ![X3:mworld]:(((mrel @ X3 @ esk10_0)|~((mrel @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_21, c_0_52])).
% 143.05/21.75 thf(c_0_67, negated_conjecture, (mrel @ esk9_0 @ esk3_0), inference(spm,[status(thm)],[c_0_24, c_0_58])).
% 143.05/21.75 thf(c_0_68, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk5_0)|~((eiw_di @ X7 @ esk7_0)))), inference(spm,[status(thm)],[c_0_31, c_0_59])).
% 143.05/21.75 thf(c_0_69, negated_conjecture, (eiw_di @ esk8_0 @ esk7_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_70, negated_conjecture, ![X7:$i, X5:mworld, X3:mworld]:(((mrel @ esk9_0 @ (esk13_5 @ X7 @ X3 @ esk8_0 @ esk9_0 @ esk4_0))|(intersect @ X7 @ esk8_0 @ esk10_0)|(intersect @ X7 @ esk8_0 @ X5)|~((epred1_3 @ esk8_0 @ X3 @ X7))|~((mrel @ esk9_0 @ X5))|~((mrel @ X3 @ esk9_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_62])])).
% 143.05/21.75 thf(c_0_71, negated_conjecture, ![X7:$i, X3:mworld]:(((epred1_3 @ X7 @ X3 @ esk6_0)|~((mrel @ esk9_0 @ X3))|~((eiw_di @ X7 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_65])])).
% 143.05/21.75 thf(c_0_72, negated_conjecture, ~((intersect @ esk6_0 @ esk8_0 @ esk10_0)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_73, negated_conjecture, (mrel @ esk3_0 @ esk10_0), inference(spm,[status(thm)],[c_0_66, c_0_67])).
% 143.05/21.75 thf(c_0_74, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk3_0)|~((eiw_di @ X7 @ esk5_0)))), inference(spm,[status(thm)],[c_0_31, c_0_35])).
% 143.05/21.75 thf(c_0_75, negated_conjecture, (eiw_di @ esk8_0 @ esk5_0), inference(spm,[status(thm)],[c_0_68, c_0_69])).
% 143.05/21.75 thf(c_0_76, negated_conjecture, ![X5:mworld, X3:mworld]:(((mrel @ esk9_0 @ (esk13_5 @ esk6_0 @ X3 @ esk8_0 @ esk9_0 @ esk4_0))|(intersect @ esk6_0 @ esk8_0 @ X5)|~((mrel @ esk9_0 @ X5))|~((mrel @ X3 @ esk9_0))|~((eiw_di @ esk8_0 @ X3)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_72]), c_0_24])).
% 143.05/21.75 thf(c_0_77, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk10_0)|~((eiw_di @ X7 @ esk3_0)))), inference(spm,[status(thm)],[c_0_31, c_0_73])).
% 143.05/21.75 thf(c_0_78, negated_conjecture, (mrel @ esk10_0 @ esk9_0), inference(spm,[status(thm)],[c_0_24, c_0_52])).
% 143.05/21.75 thf(c_0_79, negated_conjecture, (eiw_di @ esk8_0 @ esk3_0), inference(spm,[status(thm)],[c_0_74, c_0_75])).
% 143.05/21.75 thf(c_0_80, negated_conjecture, ![X3:mworld]:(((mrel @ esk9_0 @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0))|(intersect @ esk6_0 @ esk8_0 @ X3)|~((mrel @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_77]), c_0_78]), c_0_79])])).
% 143.05/21.75 thf(c_0_81, negated_conjecture, (mrel @ esk9_0 @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_52]), c_0_72])).
% 143.05/21.75 thf(c_0_82, negated_conjecture, ![X3:mworld]:(((mrel @ X3 @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0))|~((mrel @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_21, c_0_81])).
% 143.05/21.75 thf(c_0_83, plain, ![X3:mworld, X6:mworld, X5:mworld, X11:$i, X10:$i, X7:$i]:(((mrel @ X3 @ (esk14_5 @ X7 @ X5 @ X10 @ X3 @ X11))|(intersect @ X7 @ X10 @ X6)|~((member @ X11 @ X7 @ (esk13_5 @ X7 @ X5 @ X10 @ X3 @ X11)))|~((eiw_di @ X11 @ X3))|~((mrel @ X3 @ X6))|~((mrel @ X5 @ X3))|~((epred1_3 @ X10 @ X5 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 143.05/21.75 thf(c_0_84, negated_conjecture, ![X3:mworld]:(((member @ esk4_0 @ esk6_0 @ X3)|~((mrel @ esk9_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 143.05/21.75 thf(c_0_85, negated_conjecture, (mrel @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0) @ esk10_0), inference(spm,[status(thm)],[c_0_66, c_0_81])).
% 143.05/21.75 thf(c_0_86, negated_conjecture, ![X7:$i, X3:mworld]:(((eiw_di @ X7 @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0))|~((mrel @ esk9_0 @ X3))|~((eiw_di @ X7 @ X3)))), inference(spm,[status(thm)],[c_0_31, c_0_82])).
% 143.05/21.75 thf(c_0_87, negated_conjecture, (eiw_di @ esk8_0 @ esk9_0), inference(spm,[status(thm)],[c_0_37, c_0_69])).
% 143.05/21.75 thf(c_0_88, negated_conjecture, ![X3:mworld, X5:mworld, X7:$i, X6:mworld]:(((mrel @ X3 @ (esk14_5 @ esk6_0 @ X5 @ X7 @ X3 @ esk4_0))|(intersect @ esk6_0 @ X7 @ X6)|~((mrel @ esk9_0 @ (esk13_5 @ esk6_0 @ X5 @ X7 @ X3 @ esk4_0)))|~((epred1_3 @ X7 @ X5 @ esk6_0))|~((eiw_di @ esk4_0 @ X3))|~((mrel @ X5 @ X3))|~((mrel @ X3 @ X6)))), inference(spm,[status(thm)],[c_0_83, c_0_84])).
% 143.05/21.75 thf(c_0_89, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk7_0)|~((eiw_di @ X7 @ esk3_0)))), inference(spm,[status(thm)],[c_0_31, c_0_41])).
% 143.05/21.75 thf(c_0_90, negated_conjecture, (mrel @ esk9_0 @ esk7_0), inference(spm,[status(thm)],[c_0_24, c_0_32])).
% 143.05/21.75 thf(c_0_91, negated_conjecture, ![X7:$i]:(((eiw_di @ X7 @ esk10_0)|~((eiw_di @ X7 @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0))))), inference(spm,[status(thm)],[c_0_31, c_0_85])).
% 143.05/21.75 thf(c_0_92, negated_conjecture, (eiw_di @ esk8_0 @ (esk13_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_87]), c_0_22])])).
% 143.05/21.75 thf(c_0_93, plain, ![X5:mworld, X3:mworld, X7:$i, X10:$i, X6:mworld, X11:$i]:(((intersect @ X11 @ X10 @ X6)|~((member @ X7 @ X10 @ (esk14_5 @ X11 @ X3 @ X10 @ X5 @ X7)))|~((member @ X7 @ X11 @ (esk13_5 @ X11 @ X3 @ X10 @ X5 @ X7)))|~((eiw_di @ X7 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((epred1_3 @ X10 @ X3 @ X11)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 143.05/21.75 thf(c_0_94, negated_conjecture, ![X3:mworld]:(((mrel @ esk9_0 @ (esk14_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0))|(intersect @ esk6_0 @ esk8_0 @ X3)|~((epred1_3 @ esk8_0 @ esk10_0 @ esk6_0))|~((mrel @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_81]), c_0_62]), c_0_78])])).
% 143.05/21.75 thf(c_0_95, negated_conjecture, ![X10:$i, X7:$i, X3:mworld]:(((epred1_3 @ X7 @ X3 @ X10)|~((mrel @ esk7_0 @ X3))|~((eiw_di @ X10 @ esk3_0))|~((eiw_di @ X7 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_89]), c_0_46])])).
% 143.05/21.75 thf(c_0_96, negated_conjecture, (mrel @ esk7_0 @ esk10_0), inference(spm,[status(thm)],[c_0_66, c_0_90])).
% 143.05/21.75 thf(c_0_97, negated_conjecture, (eiw_di @ esk6_0 @ esk3_0), inference(spm,[status(thm)],[c_0_74, c_0_56])).
% 143.05/21.75 thf(c_0_98, negated_conjecture, (eiw_di @ esk8_0 @ esk10_0), inference(spm,[status(thm)],[c_0_91, c_0_92])).
% 143.05/21.75 thf(c_0_99, negated_conjecture, ![X3:mworld, X5:mworld, X7:$i, X6:mworld]:(((intersect @ esk6_0 @ X7 @ X3)|~((member @ esk4_0 @ X7 @ (esk14_5 @ esk6_0 @ X5 @ X7 @ X6 @ esk4_0)))|~((mrel @ esk9_0 @ (esk13_5 @ esk6_0 @ X5 @ X7 @ X6 @ esk4_0)))|~((epred1_3 @ X7 @ X5 @ esk6_0))|~((eiw_di @ esk4_0 @ X6))|~((mrel @ X6 @ X3))|~((mrel @ X5 @ X6)))), inference(spm,[status(thm)],[c_0_93, c_0_84])).
% 143.05/21.75 thf(c_0_100, negated_conjecture, ![X3:mworld]:(((mrel @ esk9_0 @ (esk14_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0))|(intersect @ esk6_0 @ esk8_0 @ X3)|~((mrel @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_96]), c_0_97]), c_0_98])])).
% 143.05/21.75 thf(c_0_101, negated_conjecture, ![X3:mworld, X5:mworld, X6:mworld]:(((intersect @ esk6_0 @ esk8_0 @ X3)|~((mrel @ esk9_0 @ (esk13_5 @ esk6_0 @ X5 @ esk8_0 @ X6 @ esk4_0)))|~((mrel @ esk9_0 @ (esk14_5 @ esk6_0 @ X5 @ esk8_0 @ X6 @ esk4_0)))|~((epred1_3 @ esk8_0 @ X5 @ esk6_0))|~((eiw_di @ esk4_0 @ X6))|~((mrel @ X6 @ X3))|~((mrel @ X5 @ X6)))), inference(spm,[status(thm)],[c_0_99, c_0_50])).
% 143.05/21.75 thf(c_0_102, negated_conjecture, (mrel @ esk9_0 @ (esk14_5 @ esk6_0 @ esk10_0 @ esk8_0 @ esk9_0 @ esk4_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_52]), c_0_72])).
% 143.05/21.75 thf(c_0_103, negated_conjecture, ![X3:mworld]:(((intersect @ esk6_0 @ esk8_0 @ X3)|~((epred1_3 @ esk8_0 @ esk10_0 @ esk6_0))|~((mrel @ esk9_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_102]), c_0_81]), c_0_62]), c_0_78])])).
% 143.05/21.75 thf(c_0_104, negated_conjecture, ~((epred1_3 @ esk8_0 @ esk10_0 @ esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_103]), c_0_52])])).
% 143.05/21.75 thf(c_0_105, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_95]), c_0_96]), c_0_97]), c_0_98])]), ['proof']).
% 143.05/21.75 % SZS output end CNFRefutation
% 143.05/21.75 % Parsed axioms : 33
% 143.05/21.75 % Removed by relevancy pruning/SinE : 0
% 143.05/21.75 % Initial clauses : 44
% 143.05/21.75 % Removed in clause preprocessing : 16
% 143.05/21.75 % Initial clauses in saturation : 28
% 143.05/21.75 % Processed clauses : 37149
% 143.05/21.75 % ...of these trivial : 2380
% 143.05/21.75 % ...subsumed : 27735
% 143.05/21.75 % ...remaining for further processing : 7034
% 143.05/21.75 % Other redundant clauses eliminated : 0
% 143.05/21.75 % Clauses deleted for lack of memory : 0
% 143.05/21.75 % Backward-subsumed : 2
% 143.05/21.75 % Backward-rewritten : 7
% 143.05/21.75 % Generated clauses : 345253
% 143.05/21.75 % ...of the previous two non-redundant : 325789
% 143.05/21.75 % ...aggressively subsumed : 0
% 143.05/21.75 % Contextual simplify-reflections : 1
% 143.05/21.75 % Paramodulations : 345253
% 143.05/21.75 % Factorizations : 0
% 143.05/21.75 % NegExts : 0
% 143.05/21.75 % Equation resolutions : 0
% 143.05/21.75 % Disequality decompositions : 0
% 143.05/21.75 % Total rewrite steps : 139915
% 143.05/21.75 % ...of those cached : 139578
% 143.05/21.75 % Propositional unsat checks : 0
% 143.05/21.75 % Propositional check models : 0
% 143.05/21.75 % Propositional check unsatisfiable : 0
% 143.05/21.75 % Propositional clauses : 0
% 143.05/21.75 % Propositional clauses after purity: 0
% 143.05/21.75 % Propositional unsat core size : 0
% 143.05/21.75 % Propositional preprocessing time : 0.000
% 143.05/21.75 % Propositional encoding time : 0.000
% 143.05/21.75 % Propositional solver time : 0.000
% 143.05/21.75 % Success case prop preproc time : 0.000
% 143.05/21.75 % Success case prop encoding time : 0.000
% 143.05/21.75 % Success case prop solver time : 0.000
% 143.05/21.75 % Current number of processed clauses : 7025
% 143.05/21.75 % Positive orientable unit clauses : 314
% 143.05/21.75 % Positive unorientable unit clauses: 0
% 143.05/21.75 % Negative unit clauses : 2
% 143.05/21.75 % Non-unit-clauses : 6709
% 143.05/21.75 % Current number of unprocessed clauses: 288528
% 143.05/21.75 % ...number of literals in the above : 2591100
% 143.05/21.75 % Current number of archived formulas : 0
% 143.05/21.75 % Current number of archived clauses : 9
% 143.05/21.75 % Clause-clause subsumption calls (NU) : 18530750
% 143.05/21.75 % Rec. Clause-clause subsumption calls : 2543856
% 143.05/21.75 % Non-unit clause-clause subsumptions : 27737
% 143.05/21.75 % Unit Clause-clause subsumption calls : 134992
% 143.05/21.75 % Rewrite failures with RHS unbound : 0
% 143.05/21.75 % BW rewrite match attempts : 162
% 143.05/21.75 % BW rewrite match successes : 7
% 143.05/21.75 % Condensation attempts : 0
% 143.05/21.75 % Condensation successes : 0
% 143.05/21.75 % Termbank termtop insertions : 12742746
% 143.05/21.75 % Search garbage collected termcells : 2117
% 143.05/21.75
% 143.05/21.75 % -------------------------------------------------
% 143.05/21.75 % User time : 20.068 s
% 143.05/21.75 % System time : 0.294 s
% 143.05/21.75 % Total time : 20.362 s
% 143.05/21.75 % Maximum resident set size: 4176 pages
% 143.05/21.75
% 143.05/21.75 % -------------------------------------------------
% 143.05/21.75 % User time : 20.071 s
% 143.05/21.75 % System time : 0.300 s
% 143.05/21.75 % Total time : 20.371 s
% 143.05/21.75 % Maximum resident set size: 4864 pages
% 143.05/21.75 % E exiting
%------------------------------------------------------------------------------