%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : LCL960^12 : 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 : n013.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:54 AM UTC 2026
% Result : Theorem 0.11s 0.26s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL960^12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.17 % Computer : n013.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Tue Sep 29 10:56:36 UTC 2026
% 0.11/0.18 % CPUTime :
% 0.11/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.22 Running higher-order theorem proving
% 0.11/0.23 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.xghljgFBZy/E---3.1_1946964.p
% 0.11/0.26 % Version: 3.5.1-ho
% 0.11/0.26 % Preprocessing class: HSMSSMSSMLMNHSN.
% 0.11/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.11/0.26 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.11/0.26 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.11/0.26 % Starting almost_fo_3_lam with 300s (1) cores
% 0.11/0.26 % Starting post_as_ho1 with 300s (1) cores
% 0.11/0.26 % ho_unfolding_3 with pid 1946977 completed with status 0
% 0.11/0.26 % Result found by ho_unfolding_3
% 0.11/0.26 % Preprocessing class: HSMSSMSSMLMNHSN.
% 0.11/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.11/0.26 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.11/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.11/0.26 % No SInE strategy applied
% 0.11/0.26 % Search class: HGHNF-FFSF33-SHSSMFNN
% 0.11/0.26 % partial match(2): HGHNF-FFSF00-SHSSMFNN
% 0.11/0.26 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.11/0.26 % Starting SubtermCWHack with 136s (1) cores
% 0.11/0.26 % Starting ho_unfolding_3 with 151s (1) cores
% 0.11/0.26 % Starting sh5l with 136s (1) cores
% 0.11/0.26 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.11/0.26 % Starting lpo1_def_fix with 136s (1) cores
% 0.11/0.26 % SubtermCWHack with pid 1946981 completed with status 0
% 0.11/0.26 % Result found by SubtermCWHack
% 0.11/0.26 % Preprocessing class: HSMSSMSSMLMNHSN.
% 0.11/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.11/0.26 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.11/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.11/0.26 % No SInE strategy applied
% 0.11/0.26 % Search class: HGHNF-FFSF33-SHSSMFNN
% 0.11/0.26 % partial match(2): HGHNF-FFSF00-SHSSMFNN
% 0.11/0.26 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.11/0.26 % Starting SubtermCWHack with 136s (1) cores
% 0.11/0.26 % Preprocessing time : 0.002 s
% 0.11/0.26
% 0.11/0.26 % Proof found!
% 0.11/0.26 % SZS status Theorem
% 0.11/0.26 % SZS output start CNFRefutation
% 0.11/0.26 thf(decl_sort1, type, mworld: $tType).
% 0.11/0.26 thf(decl_23, type, mrel: mworld > mworld > $o).
% 0.11/0.26 thf(decl_24, type, mactual: mworld).
% 0.11/0.26 thf(decl_25, type, mlocal: (mworld > $o) > $o).
% 0.11/0.26 thf(decl_26, type, mnot: (mworld > $o) > mworld > $o).
% 0.11/0.26 thf(decl_27, type, mand: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.11/0.26 thf(decl_29, type, mimplies: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.11/0.26 thf(decl_31, type, mbox: (mworld > $o) > mworld > $o).
% 0.11/0.26 thf(decl_33, type, eiw_di: $i > mworld > $o).
% 0.11/0.26 thf(decl_34, type, mforall_di: ($i > mworld > $o) > mworld > $o).
% 0.11/0.26 thf(decl_35, type, mexists_di: ($i > mworld > $o) > mworld > $o).
% 0.11/0.26 thf(decl_36, type, f: $i > $i > mworld > $o).
% 0.11/0.26 thf(decl_37, type, epred1_4: $i > $i > mworld > $i > $o).
% 0.11/0.26 thf(decl_39, type, esk2_0: mworld).
% 0.11/0.26 thf(decl_40, type, esk3_2: mworld > $i > $i).
% 0.11/0.26 thf(decl_41, type, esk4_0: mworld).
% 0.11/0.26 thf(decl_42, type, esk5_0: $i).
% 0.11/0.26 thf(decl_43, type, esk6_5: $i > mworld > $i > $i > mworld > mworld).
% 0.11/0.26 thf(decl_44, type, esk7_6: $i > mworld > $i > $i > mworld > mworld > mworld).
% 0.11/0.26 thf(decl_45, type, esk8_5: $i > mworld > $i > $i > mworld > mworld).
% 0.11/0.26 thf(decl_46, type, esk9_5: $i > mworld > $i > $i > mworld > mworld).
% 0.11/0.26 thf(kalish256, conjecture, (mlocal @ (mbox @ (mimplies @ (mbox @ (mforall_di @ (^[X9:$i]:(mexists_di @ (^[X10:$i]:(mbox @ (mforall_di @ (^[X6:$i]:(mand @ (mbox @ (mimplies @ (mbox @ (f @ X6 @ X10)) @ (mand @ (mbox @ (f @ X6 @ X9)) @ (mbox @ (mnot @ (mbox @ (f @ X6 @ X6))))))) @ (mbox @ (mimplies @ (mand @ (mbox @ (f @ X6 @ X9)) @ (mbox @ (mnot @ (mbox @ (f @ X6 @ X6))))) @ (mbox @ (f @ X6 @ X10))))))))))))) @ (mbox @ (mnot @ (mexists_di @ (^[X11:$i]:(mbox @ (mforall_di @ (^[X12:$i]:(mbox @ (f @ X12 @ X11)))))))))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', kalish256)).
% 0.11/0.26 thf(mlocal_def, axiom, ((mlocal)=(^[X1:mworld > $o]:((X1 @ mactual)))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mlocal_def)).
% 0.11/0.26 thf(mnot_def, axiom, ((mnot)=(^[X2:mworld > $o, X3:mworld]:(~((X2 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mnot_def)).
% 0.11/0.26 thf(mand_def, axiom, ((mand)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))&((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mand_def)).
% 0.11/0.26 thf(mimplies_def, axiom, ((mimplies)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))=>((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mimplies_def)).
% 0.11/0.26 thf(mbox_def, axiom, ((mbox)=(^[X1:mworld > $o, X3:mworld]:(![X5:mworld]:((((mrel @ X3 @ X5))=>((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mbox_def)).
% 0.11/0.26 thf(mforall_di_def, axiom, ((mforall_di)=(^[X7:$i > mworld > $o, X3:mworld]:(![X6:$i]:((((eiw_di @ X6 @ X3))=>((X7 @ X6 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mforall_di_def)).
% 0.11/0.26 thf(mexists_di_def, axiom, ((mexists_di)=(^[X8:$i > mworld > $o, X3:mworld]:(?[X6:$i]:((((eiw_di @ X6 @ X3))&((X8 @ X6 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mexists_di_def)).
% 0.11/0.26 thf(mrel_universal, axiom, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), file('/export/starexec/sandbox2/tmp/tmp.xghljgFBZy/E---3.1_1946964.p', mrel_universal)).
% 0.11/0.26 thf(c_0_9, negated_conjecture, ~((mlocal @ (mbox @ (mimplies @ (mbox @ (mforall_di @ (^[X9:$i]:(mexists_di @ (^[X10:$i]:(mbox @ (mforall_di @ (^[X6:$i]:(mand @ (mbox @ (mimplies @ (mbox @ (f @ X6 @ X10)) @ (mand @ (mbox @ (f @ X6 @ X9)) @ (mbox @ (mnot @ (mbox @ (f @ X6 @ X6))))))) @ (mbox @ (mimplies @ (mand @ (mbox @ (f @ X6 @ X9)) @ (mbox @ (mnot @ (mbox @ (f @ X6 @ X6))))) @ (mbox @ (f @ X6 @ X10))))))))))))) @ (mbox @ (mnot @ (mexists_di @ (^[X11:$i]:(mbox @ (mforall_di @ (^[X12:$i]:(mbox @ (f @ X12 @ X11))))))))))))), inference(assume_negation,[status(cth)],[kalish256])).
% 0.11/0.26 thf(c_0_10, plain, ((mlocal)=(^[Z0:mworld > $o]:((Z0 @ mactual)))), inference(fof_simplification,[status(thm)],[mlocal_def])).
% 0.11/0.26 thf(c_0_11, plain, ((mnot)=(^[Z0:mworld > $o, Z1:mworld]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot_def])).
% 0.11/0.26 thf(c_0_12, plain, ((mand)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand_def])).
% 0.11/0.26 thf(c_0_13, plain, ((mimplies)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies_def])).
% 0.11/0.26 thf(c_0_14, plain, ((mbox)=(^[Z0:mworld > $o, Z1:mworld]:(![X5:mworld]:((((mrel @ Z1 @ X5))=>((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mbox_def])).
% 0.11/0.26 thf(c_0_15, plain, ((mforall_di)=(^[Z0:$i > mworld > $o, Z1:mworld]:(![X6:$i]:((((eiw_di @ X6 @ Z1))=>((Z0 @ X6 @ Z1))))))), inference(fof_simplification,[status(thm)],[mforall_di_def])).
% 0.11/0.26 thf(c_0_16, plain, ((mexists_di)=(^[Z0:$i > mworld > $o, Z1:mworld]:(?[X6:$i]:((((eiw_di @ X6 @ Z1))&((Z0 @ X6 @ Z1))))))), inference(fof_simplification,[status(thm)],[mexists_di_def])).
% 0.11/0.26 thf(c_0_17, plain, ![X27:$i, X28:mworld, X30:$i, X29:$i]:(((epred1_4 @ X29 @ X30 @ X28 @ X27)<=>(![X21:mworld]:(((mrel @ X28 @ X21)=>(![X17:mworld]:(((mrel @ X21 @ X17)=>(f @ X27 @ X29 @ X17)))=>(![X18:mworld]:(((mrel @ X21 @ X18)=>(f @ X27 @ X30 @ X18)))&![X20:mworld]:(((mrel @ X21 @ X20)=>~(![X19:mworld]:(((mrel @ X20 @ X19)=>(f @ X27 @ X27 @ X19))))))))))&![X26:mworld]:(((mrel @ X28 @ X26)=>((![X22:mworld]:(((mrel @ X26 @ X22)=>(f @ X27 @ X30 @ X22)))&![X24:mworld]:(((mrel @ X26 @ X24)=>~(![X23:mworld]:(((mrel @ X24 @ X23)=>(f @ X27 @ X27 @ X23)))))))=>![X25:mworld]:(((mrel @ X26 @ X25)=>(f @ X27 @ X29 @ X25))))))))), introduced(definition)).
% 0.11/0.26 thf(c_0_18, negated_conjecture, ~(![X37:mworld]:(((mrel @ mactual @ X37)=>(![X31:mworld]:(((mrel @ X37 @ X31)=>![X30:$i]:(((eiw_di @ X30 @ X31)=>?[X29:$i]:(((eiw_di @ X29 @ X31)&![X28:mworld]:(((mrel @ X31 @ X28)=>![X27:$i]:(((eiw_di @ X27 @ X28)=>(epred1_4 @ X29 @ X30 @ X28 @ X27)))))))))))=>![X36:mworld]:(((mrel @ X37 @ X36)=>~(?[X35:$i]:(((eiw_di @ X35 @ X36)&![X34:mworld]:(((mrel @ X36 @ X34)=>![X33:$i]:(((eiw_di @ X33 @ X34)=>![X32:mworld]:(((mrel @ X34 @ X32)=>(f @ X33 @ X35 @ X32)))))))))))))))), 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(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_9]), c_0_10]), c_0_11]), c_0_12]), c_0_13]), c_0_14]), c_0_15]), c_0_16]), c_0_17])).
% 0.11/0.26 thf(c_0_19, plain, ![X27:$i, X28:mworld, X30:$i, X29:$i]:(((epred1_4 @ X29 @ X30 @ X28 @ X27)=>(![X21:mworld]:(((mrel @ X28 @ X21)=>(![X17:mworld]:(((mrel @ X21 @ X17)=>(f @ X27 @ X29 @ X17)))=>(![X18:mworld]:(((mrel @ X21 @ X18)=>(f @ X27 @ X30 @ X18)))&![X20:mworld]:(((mrel @ X21 @ X20)=>~(![X19:mworld]:(((mrel @ X20 @ X19)=>(f @ X27 @ X27 @ X19))))))))))&![X26:mworld]:(((mrel @ X28 @ X26)=>((![X22:mworld]:(((mrel @ X26 @ X22)=>(f @ X27 @ X30 @ X22)))&![X24:mworld]:(((mrel @ X26 @ X24)=>~(![X23:mworld]:(((mrel @ X24 @ X23)=>(f @ X27 @ X27 @ X23)))))))=>![X25:mworld]:(((mrel @ X26 @ X25)=>(f @ X27 @ X29 @ X25))))))))), inference(split_equiv,[status(thm)],[c_0_17])).
% 0.11/0.26 thf(c_0_20, negated_conjecture, ![X43:mworld, X44:$i, X46:mworld, X47:$i, X50:mworld, X51:$i, X52:mworld]:(((mrel @ mactual @ esk2_0)&((((eiw_di @ (esk3_2 @ X43 @ X44) @ X43)|~(eiw_di @ X44 @ X43)|~(mrel @ esk2_0 @ X43))&(~(mrel @ X43 @ X46)|(~(eiw_di @ X47 @ X46)|(epred1_4 @ (esk3_2 @ X43 @ X44) @ X44 @ X46 @ X47))|~(eiw_di @ X44 @ X43)|~(mrel @ esk2_0 @ X43)))&((mrel @ esk2_0 @ esk4_0)&((eiw_di @ esk5_0 @ esk4_0)&(~(mrel @ esk4_0 @ X50)|(~(eiw_di @ X51 @ X50)|(~(mrel @ X50 @ X52)|(f @ X51 @ esk5_0 @ X52))))))))), 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_18])])])])])])).
% 0.11/0.26 thf(c_0_21, plain, ![X38:mworld, X39:mworld]:((mrel @ X38 @ X39)), inference(variable_rename,[status(thm)],[mrel_universal])).
% 0.11/0.26 thf(c_0_22, plain, ![X53:$i, X54:mworld, X55:$i, X56:$i, X57:mworld, X59:mworld, X60:mworld, X62:mworld, X65:mworld, X66:mworld]:(((((~(mrel @ X57 @ X59)|(f @ X53 @ X55 @ X59)|(mrel @ X57 @ (esk6_5 @ X53 @ X54 @ X55 @ X56 @ X57))|~(mrel @ X54 @ X57)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))&(((mrel @ X60 @ (esk7_6 @ X53 @ X54 @ X55 @ X56 @ X57 @ X60))|~(mrel @ X57 @ X60)|(mrel @ X57 @ (esk6_5 @ X53 @ X54 @ X55 @ X56 @ X57))|~(mrel @ X54 @ X57)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))&(~(f @ X53 @ X53 @ (esk7_6 @ X53 @ X54 @ X55 @ X56 @ X57 @ X60))|~(mrel @ X57 @ X60)|(mrel @ X57 @ (esk6_5 @ X53 @ X54 @ X55 @ X56 @ X57))|~(mrel @ X54 @ X57)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))))&((~(mrel @ X57 @ X59)|(f @ X53 @ X55 @ X59)|~(f @ X53 @ X56 @ (esk6_5 @ X53 @ X54 @ X55 @ X56 @ X57))|~(mrel @ X54 @ X57)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))&(((mrel @ X60 @ (esk7_6 @ X53 @ X54 @ X55 @ X56 @ X57 @ X60))|~(mrel @ X57 @ X60)|~(f @ X53 @ X56 @ (esk6_5 @ X53 @ X54 @ X55 @ X56 @ X57))|~(mrel @ X54 @ X57)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))&(~(f @ X53 @ X53 @ (esk7_6 @ X53 @ X54 @ X55 @ X56 @ X57 @ X60))|~(mrel @ X57 @ X60)|~(f @ X53 @ X56 @ (esk6_5 @ X53 @ X54 @ X55 @ X56 @ X57))|~(mrel @ X54 @ X57)|~(epred1_4 @ X56 @ X55 @ X54 @ X53)))))&((((mrel @ X62 @ (esk9_5 @ X53 @ X54 @ X55 @ X56 @ X62))|(mrel @ X62 @ (esk8_5 @ X53 @ X54 @ X55 @ X56 @ X62))|(~(mrel @ X62 @ X66)|(f @ X53 @ X56 @ X66))|~(mrel @ X54 @ X62)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))&(~(mrel @ (esk9_5 @ X53 @ X54 @ X55 @ X56 @ X62) @ X65)|(f @ X53 @ X53 @ X65)|(mrel @ X62 @ (esk8_5 @ X53 @ X54 @ X55 @ X56 @ X62))|(~(mrel @ X62 @ X66)|(f @ X53 @ X56 @ X66))|~(mrel @ X54 @ X62)|~(epred1_4 @ X56 @ X55 @ X54 @ X53)))&(((mrel @ X62 @ (esk9_5 @ X53 @ X54 @ X55 @ X56 @ X62))|~(f @ X53 @ X55 @ (esk8_5 @ X53 @ X54 @ X55 @ X56 @ X62))|(~(mrel @ X62 @ X66)|(f @ X53 @ X56 @ X66))|~(mrel @ X54 @ X62)|~(epred1_4 @ X56 @ X55 @ X54 @ X53))&(~(mrel @ (esk9_5 @ X53 @ X54 @ X55 @ X56 @ X62) @ X65)|(f @ X53 @ X53 @ X65)|~(f @ X53 @ X55 @ (esk8_5 @ X53 @ X54 @ X55 @ X56 @ X62))|(~(mrel @ X62 @ X66)|(f @ X53 @ X56 @ X66))|~(mrel @ X54 @ X62)|~(epred1_4 @ X56 @ X55 @ X54 @ X53)))))), 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_19])])])])])])).
% 0.11/0.26 thf(c_0_23, negated_conjecture, ![X3:mworld, X6:$i, X5:mworld]:(((f @ X6 @ esk5_0 @ X5)|~((mrel @ esk4_0 @ X3))|~((eiw_di @ X6 @ X3))|~((mrel @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.11/0.26 thf(c_0_24, plain, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.11/0.26 thf(c_0_25, negated_conjecture, ![X6:$i, X3:mworld]:(((eiw_di @ (esk3_2 @ X3 @ X6) @ X3)|~((eiw_di @ X6 @ X3))|~((mrel @ esk2_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.11/0.26 thf(c_0_26, plain, ![X3:mworld, X5:mworld, X14:mworld, X13:mworld, X10:$i, X9:$i, X6:$i]:(((f @ X6 @ X6 @ X13)|(f @ X6 @ X10 @ X14)|~((mrel @ (esk9_5 @ X6 @ X3 @ X9 @ X10 @ X5) @ X13))|~((f @ X6 @ X9 @ (esk8_5 @ X6 @ X3 @ X9 @ X10 @ X5)))|~((mrel @ X5 @ X14))|~((mrel @ X3 @ X5))|~((epred1_4 @ X10 @ X9 @ X3 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.11/0.26 thf(c_0_27, negated_conjecture, ![X6:$i, X5:mworld, X3:mworld]:(((f @ X6 @ esk5_0 @ X5)|~((eiw_di @ X6 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24]), c_0_24])])).
% 0.11/0.26 thf(c_0_28, negated_conjecture, ![X6:$i, X3:mworld]:(((eiw_di @ (esk3_2 @ X3 @ X6) @ X3)|~((eiw_di @ X6 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_24])])).
% 0.11/0.26 thf(c_0_29, plain, ![X3:mworld, X6:$i, X14:mworld, X13:mworld, X10:$i, X9:$i, X5:mworld]:(((f @ X6 @ X10 @ X14)|(f @ X6 @ X6 @ X13)|~((epred1_4 @ X10 @ X9 @ X3 @ X6))|~((f @ X6 @ X9 @ (esk8_5 @ X6 @ X3 @ X9 @ X10 @ X5))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_24]), c_0_24]), c_0_24])])).
% 0.11/0.26 thf(c_0_30, negated_conjecture, ![X6:$i, X5:mworld, X3:mworld]:(((f @ (esk3_2 @ X3 @ X6) @ esk5_0 @ X5)|~((eiw_di @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 0.11/0.26 thf(c_0_31, negated_conjecture, ![X5:mworld, X9:$i, X6:$i, X3:mworld]:(((epred1_4 @ (esk3_2 @ X3 @ X9) @ X9 @ X5 @ X6)|~((mrel @ X3 @ X5))|~((eiw_di @ X6 @ X5))|~((eiw_di @ X9 @ X3))|~((mrel @ esk2_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.11/0.26 thf(c_0_32, negated_conjecture, ![X5:mworld, X9:$i, X14:mworld, X13:mworld, X6:$i, X3:mworld]:(((f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ X3 @ X6) @ X5)|(f @ (esk3_2 @ X3 @ X6) @ X9 @ X13)|~((epred1_4 @ X9 @ esk5_0 @ X14 @ (esk3_2 @ X3 @ X6)))|~((eiw_di @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 0.11/0.26 thf(c_0_33, negated_conjecture, ![X3:mworld, X9:$i, X6:$i, X5:mworld]:(((epred1_4 @ (esk3_2 @ X3 @ X9) @ X9 @ X5 @ X6)|~((eiw_di @ X9 @ X3))|~((eiw_di @ X6 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_24]), c_0_24])])).
% 0.11/0.26 thf(c_0_34, negated_conjecture, ![X13:mworld, X15:mworld, X14:mworld, X6:$i, X5:mworld, X3:mworld]:(((f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ X5 @ esk5_0) @ X13)|(f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ X3 @ X6) @ X14)|~((eiw_di @ (esk3_2 @ X3 @ X6) @ X15))|~((eiw_di @ esk5_0 @ X5))|~((eiw_di @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 0.11/0.26 thf(c_0_35, negated_conjecture, ![X14:mworld, X13:mworld, X6:$i, X5:mworld, X3:mworld]:(((f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ X5 @ esk5_0) @ X13)|(f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ X3 @ X6) @ X14)|~((eiw_di @ esk5_0 @ X5))|~((eiw_di @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_34, c_0_28])).
% 0.11/0.26 thf(c_0_36, negated_conjecture, (eiw_di @ esk5_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.11/0.26 thf(c_0_37, negated_conjecture, ![X13:mworld, X6:$i, X5:mworld, X3:mworld]:(((f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ esk4_0 @ esk5_0) @ X5)|(f @ (esk3_2 @ X3 @ X6) @ (esk3_2 @ X3 @ X6) @ X13)|~((eiw_di @ X6 @ X3)))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.11/0.26 thf(c_0_38, plain, ![X3:mworld, X5:mworld, X13:mworld, X10:$i, X9:$i, X6:$i]:((~((f @ X6 @ X6 @ (esk7_6 @ X6 @ X3 @ X9 @ X10 @ X5 @ X13)))|~((mrel @ X5 @ X13))|~((f @ X6 @ X10 @ (esk6_5 @ X6 @ X3 @ X9 @ X10 @ X5)))|~((mrel @ X3 @ X5))|~((epred1_4 @ X10 @ X9 @ X3 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.11/0.26 thf(c_0_39, negated_conjecture, ![X3:mworld, X5:mworld]:(((f @ (esk3_2 @ esk4_0 @ esk5_0) @ (esk3_2 @ esk4_0 @ esk5_0) @ X3)|(f @ (esk3_2 @ esk4_0 @ esk5_0) @ (esk3_2 @ esk4_0 @ esk5_0) @ X5))), inference(spm,[status(thm)],[c_0_37, c_0_36])).
% 0.11/0.26 thf(c_0_40, plain, ![X3:mworld, X6:$i, X5:mworld, X9:$i, X10:$i, X13:mworld]:((~((epred1_4 @ X10 @ X9 @ X3 @ X6))|~((f @ X6 @ X10 @ (esk6_5 @ X6 @ X3 @ X9 @ X10 @ X5)))|~((f @ X6 @ X6 @ (esk7_6 @ X6 @ X3 @ X9 @ X10 @ X5 @ X13))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_24]), c_0_24])])).
% 0.11/0.26 thf(c_0_41, negated_conjecture, ![X3:mworld]:((f @ (esk3_2 @ esk4_0 @ esk5_0) @ (esk3_2 @ esk4_0 @ esk5_0) @ X3)), inference(ef,[status(thm)],[c_0_39])).
% 0.11/0.26 thf(c_0_42, plain, ![X5:mworld, X9:$i, X6:$i, X3:mworld]:((~((f @ (esk3_2 @ esk4_0 @ esk5_0) @ X6 @ (esk6_5 @ (esk3_2 @ esk4_0 @ esk5_0) @ X3 @ X9 @ X6 @ X5)))|~((epred1_4 @ X6 @ X9 @ X3 @ (esk3_2 @ esk4_0 @ esk5_0))))), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 0.11/0.26 thf(c_0_43, negated_conjecture, ![X6:$i, X3:mworld]:(~((epred1_4 @ (esk3_2 @ esk4_0 @ esk5_0) @ X6 @ X3 @ (esk3_2 @ esk4_0 @ esk5_0)))), inference(spm,[status(thm)],[c_0_42, c_0_41])).
% 0.11/0.26 thf(c_0_44, negated_conjecture, ![X3:mworld]:(~((eiw_di @ (esk3_2 @ esk4_0 @ esk5_0) @ X3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_33]), c_0_36])])).
% 0.11/0.26 thf(c_0_45, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_28]), c_0_36])]), ['proof']).
% 0.11/0.26 % SZS output end CNFRefutation
% 0.11/0.26 % Parsed axioms : 28
% 0.11/0.26 % Removed by relevancy pruning/SinE : 0
% 0.11/0.26 % Initial clauses : 33
% 0.11/0.26 % Removed in clause preprocessing : 25
% 0.11/0.26 % Initial clauses in saturation : 8
% 0.11/0.26 % Processed clauses : 42
% 0.11/0.26 % ...of these trivial : 0
% 0.11/0.26 % ...subsumed : 3
% 0.11/0.26 % ...remaining for further processing : 39
% 0.11/0.26 % Other redundant clauses eliminated : 0
% 0.11/0.26 % Clauses deleted for lack of memory : 0
% 0.11/0.26 % Backward-subsumed : 6
% 0.11/0.26 % Backward-rewritten : 0
% 0.11/0.26 % Generated clauses : 52
% 0.11/0.26 % ...of the previous two non-redundant : 48
% 0.11/0.26 % ...aggressively subsumed : 0
% 0.11/0.26 % Contextual simplify-reflections : 0
% 0.11/0.26 % Paramodulations : 50
% 0.11/0.26 % Factorizations : 2
% 0.11/0.26 % NegExts : 0
% 0.11/0.26 % Equation resolutions : 0
% 0.11/0.26 % Disequality decompositions : 0
% 0.11/0.26 % Total rewrite steps : 8
% 0.11/0.26 % ...of those cached : 3
% 0.11/0.26 % Propositional unsat checks : 0
% 0.11/0.26 % Propositional check models : 0
% 0.11/0.26 % Propositional check unsatisfiable : 0
% 0.11/0.26 % Propositional clauses : 0
% 0.11/0.26 % Propositional clauses after purity: 0
% 0.11/0.26 % Propositional unsat core size : 0
% 0.11/0.26 % Propositional preprocessing time : 0.000
% 0.11/0.26 % Propositional encoding time : 0.000
% 0.11/0.26 % Propositional solver time : 0.000
% 0.11/0.26 % Success case prop preproc time : 0.000
% 0.11/0.26 % Success case prop encoding time : 0.000
% 0.11/0.26 % Success case prop solver time : 0.000
% 0.11/0.26 % Current number of processed clauses : 33
% 0.11/0.26 % Positive orientable unit clauses : 5
% 0.11/0.26 % Positive unorientable unit clauses: 0
% 0.11/0.26 % Negative unit clauses : 4
% 0.11/0.26 % Non-unit-clauses : 24
% 0.11/0.26 % Current number of unprocessed clauses: 13
% 0.11/0.26 % ...number of literals in the above : 44
% 0.11/0.26 % Current number of archived formulas : 0
% 0.11/0.26 % Current number of archived clauses : 7
% 0.11/0.26 % Clause-clause subsumption calls (NU) : 151
% 0.11/0.26 % Rec. Clause-clause subsumption calls : 77
% 0.11/0.26 % Non-unit clause-clause subsumptions : 5
% 0.11/0.26 % Unit Clause-clause subsumption calls : 58
% 0.11/0.26 % Rewrite failures with RHS unbound : 0
% 0.11/0.26 % BW rewrite match attempts : 2
% 0.11/0.26 % BW rewrite match successes : 2
% 0.11/0.26 % Condensation attempts : 0
% 0.11/0.26 % Condensation successes : 0
% 0.11/0.26 % Termbank termtop insertions : 4879
% 0.11/0.26 % Search garbage collected termcells : 1523
% 0.11/0.26
% 0.11/0.26 % -------------------------------------------------
% 0.11/0.26 % User time : 0.009 s
% 0.11/0.26 % System time : 0.002 s
% 0.11/0.26 % Total time : 0.012 s
% 0.11/0.26 % Maximum resident set size: 3660 pages
% 0.11/0.26
% 0.11/0.26 % -------------------------------------------------
% 0.11/0.26 % User time : 0.023 s
% 0.11/0.26 % System time : 0.017 s
% 0.11/0.26 % Total time : 0.040 s
% 0.11/0.26 % Maximum resident set size: 4608 pages
% 0.11/0.26 % E exiting
%------------------------------------------------------------------------------