%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SET914^7 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/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:22:19 AM UTC 2026
% Result : Theorem 1.05s 0.50s
% Output : CNFRefutation 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET914^7 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/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:39:10 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.07/0.25 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.VzmI1SJd6n/E---3.1_3373847.p
% 1.05/0.50 % Version: 3.5.1-ho
% 1.05/0.50 % Preprocessing class: HSMSSMSSMLLNHSN.
% 1.05/0.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.05/0.50 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 1.05/0.50 % Starting post_as_ho3 with 300s (1) cores
% 1.05/0.50 % Starting new_ho_12 with 300s (1) cores
% 1.05/0.50 % Starting new_bool_2 with 300s (1) cores
% 1.05/0.50 % new_ho_10_cnf2 with pid 3373884 completed with status 0
% 1.05/0.50 % Result found by new_ho_10_cnf2
% 1.05/0.50 % Preprocessing class: HSMSSMSSMLLNHSN.
% 1.05/0.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.05/0.50 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 1.05/0.50 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.05/0.50 % No SInE strategy applied
% 1.05/0.50 % Search class: HGHNM-FFMS32-SHSSMFNN
% 1.05/0.50 % partial match(2): HGUNM-FFMF32-SHSSMFNN
% 1.05/0.50 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 1.05/0.50 % Starting SubtermCWHack with 136s (1) cores
% 1.05/0.50 % Starting new_ho_10_cnf2 with 151s (1) cores
% 1.05/0.50 % Starting sh5l with 136s (1) cores
% 1.05/0.50 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 1.05/0.50 % Starting lpo1_def_fix with 136s (1) cores
% 1.05/0.50 % new_ho_10_cnf2 with pid 3373897 completed with status 0
% 1.05/0.50 % Result found by new_ho_10_cnf2
% 1.05/0.50 % Preprocessing class: HSMSSMSSMLLNHSN.
% 1.05/0.50 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.05/0.50 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 1.05/0.50 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.05/0.50 % No SInE strategy applied
% 1.05/0.50 % Search class: HGHNM-FFMS32-SHSSMFNN
% 1.05/0.50 % partial match(2): HGUNM-FFMF32-SHSSMFNN
% 1.05/0.50 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 1.05/0.50 % Starting SubtermCWHack with 136s (1) cores
% 1.05/0.50 % Starting new_ho_10_cnf2 with 151s (1) cores
% 1.05/0.50 % Preprocessing time : 0.003 s
% 1.05/0.50 % Presaturation interreduction done
% 1.05/0.50
% 1.05/0.50 % Proof found!
% 1.05/0.50 % SZS status Theorem
% 1.05/0.50 % SZS output start CNFRefutation
% 1.05/0.50 thf(decl_sort1, type, mu: $tType).
% 1.05/0.50 thf(decl_23, type, qmltpeq: mu > mu > $i > $o).
% 1.05/0.50 thf(decl_25, type, mnot: ($i > $o) > $i > $o).
% 1.05/0.50 thf(decl_26, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 1.05/0.50 thf(decl_31, type, mand: ($i > $o) > ($i > $o) > $i > $o).
% 1.05/0.50 thf(decl_32, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 1.05/0.50 thf(decl_34, type, mequiv: ($i > $o) > ($i > $o) > $i > $o).
% 1.05/0.50 thf(decl_37, type, exists_in_world: mu > $i > $o).
% 1.05/0.50 thf(decl_38, type, mforall_ind: (mu > $i > $o) > $i > $o).
% 1.05/0.50 thf(decl_51, type, mvalid: ($i > $o) > $o).
% 1.05/0.50 thf(decl_59, type, in: mu > mu > $i > $o).
% 1.05/0.50 thf(decl_60, type, disjoint: mu > mu > $i > $o).
% 1.05/0.50 thf(decl_61, type, empty_set: mu).
% 1.05/0.50 thf(decl_62, type, set_intersection2: mu > mu > mu).
% 1.05/0.50 thf(decl_63, type, unordered_pair: mu > mu > mu).
% 1.05/0.50 thf(decl_64, type, epred1_4: $i > mu > mu > mu > $o).
% 1.05/0.50 thf(decl_65, type, epred2_4: $i > mu > mu > mu > $o).
% 1.05/0.50 thf(decl_67, type, esk2_2: $i > mu > mu).
% 1.05/0.50 thf(decl_70, type, esk5_0: $i).
% 1.05/0.50 thf(decl_71, type, esk6_0: mu).
% 1.05/0.50 thf(decl_72, type, esk7_0: mu).
% 1.05/0.50 thf(decl_73, type, esk8_0: mu).
% 1.05/0.50 thf(decl_74, type, esk9_4: mu > mu > mu > $i > mu).
% 1.05/0.50 thf(decl_75, type, esk10_4: mu > mu > mu > $i > mu).
% 1.05/0.50 thf(mimplies, axiom, ((mimplies)=(^[X4:$i > $o, X5:$i > $o]:(mor @ (mnot @ X4) @ X5))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mimplies)).
% 1.05/0.50 thf(mnot, axiom, ((mnot)=(^[X4:$i > $o, X3:$i]:(~((X4 @ X3))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mnot)).
% 1.05/0.50 thf(mor, axiom, ((mor)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))|((X5 @ X3)))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mor)).
% 1.05/0.50 thf(mforall_ind, axiom, ((mforall_ind)=(^[X11:mu > $i > $o, X3:$i]:(![X12:mu]:((((exists_in_world @ X12 @ X3))=>((X11 @ X12 @ X3))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mforall_ind)).
% 1.05/0.50 thf(mvalid, axiom, ((mvalid)=(^[X4:$i > $o]:(![X3:$i]:((X4 @ X3))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mvalid)).
% 1.05/0.50 thf(mand, axiom, ((mand)=(^[X4:$i > $o, X5:$i > $o]:(mnot @ (mor @ (mnot @ X4) @ (mnot @ X5))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mand)).
% 1.05/0.50 thf(idempotence_k3_xboole_0, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(qmltpeq @ (set_intersection2 @ X28 @ X28) @ X28)))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', idempotence_k3_xboole_0)).
% 1.05/0.50 thf(mequiv, axiom, ((mequiv)=(^[X4:$i > $o, X5:$i > $o]:(mand @ (mimplies @ X4 @ X5) @ (mimplies @ X5 @ X4)))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', mequiv)).
% 1.05/0.50 thf(symmetry, axiom, (mvalid @ (mforall_ind @ (^[X23:mu]:(mforall_ind @ (^[X24:mu]:(mimplies @ (qmltpeq @ X23 @ X24) @ (qmltpeq @ X24 @ X23))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', symmetry)).
% 1.05/0.50 thf(in_substitution_2, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mforall_ind @ (^[X30:mu]:(mimplies @ (mand @ (qmltpeq @ X28 @ X29) @ (in @ X30 @ X28)) @ (in @ X30 @ X29))))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', in_substitution_2)).
% 1.05/0.50 thf(existence_of_set_intersection2_ax, axiom, ![X7:$i, X20:mu, X21:mu]:((exists_in_world @ (set_intersection2 @ X20 @ X21) @ X7)), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', existence_of_set_intersection2_ax)).
% 1.05/0.50 thf(d1_xboole_0, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mequiv @ (qmltpeq @ X28 @ empty_set) @ (mforall_ind @ (^[X29:mu]:(mnot @ (in @ X29 @ X28)))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', d1_xboole_0)).
% 1.05/0.50 thf(d7_xboole_0, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mequiv @ (disjoint @ X28 @ X29) @ (qmltpeq @ (set_intersection2 @ X28 @ X29) @ empty_set))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', d7_xboole_0)).
% 1.05/0.50 thf(existence_of_empty_set_ax, axiom, ![X7:$i]:((exists_in_world @ empty_set @ X7)), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', existence_of_empty_set_ax)).
% 1.05/0.50 thf(d3_xboole_0, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mforall_ind @ (^[X30:mu]:(mequiv @ (qmltpeq @ X30 @ (set_intersection2 @ X28 @ X29)) @ (mforall_ind @ (^[X31:mu]:(mequiv @ (in @ X31 @ X30) @ (mand @ (in @ X31 @ X28) @ (in @ X31 @ X29))))))))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', d3_xboole_0)).
% 1.05/0.50 thf(t55_zfmisc_1, conjecture, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mforall_ind @ (^[X30:mu]:(mnot @ (mand @ (disjoint @ (unordered_pair @ X28 @ X29) @ X30) @ (in @ X28 @ X30)))))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', t55_zfmisc_1)).
% 1.05/0.50 thf(disjoint_substitution_1, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mforall_ind @ (^[X30:mu]:(mimplies @ (mand @ (qmltpeq @ X28 @ X29) @ (disjoint @ X28 @ X30)) @ (disjoint @ X29 @ X30))))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', disjoint_substitution_1)).
% 1.05/0.50 thf(commutativity_k2_tarski, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(qmltpeq @ (unordered_pair @ X28 @ X29) @ (unordered_pair @ X29 @ X28))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', commutativity_k2_tarski)).
% 1.05/0.50 thf(existence_of_unordered_pair_ax, axiom, ![X7:$i, X20:mu, X21:mu]:((exists_in_world @ (unordered_pair @ X20 @ X21) @ X7)), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', existence_of_unordered_pair_ax)).
% 1.05/0.50 thf(d2_tarski, axiom, (mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mforall_ind @ (^[X30:mu]:(mequiv @ (qmltpeq @ X30 @ (unordered_pair @ X28 @ X29)) @ (mforall_ind @ (^[X31:mu]:(mequiv @ (in @ X31 @ X30) @ (mor @ (qmltpeq @ X31 @ X28) @ (qmltpeq @ X31 @ X29))))))))))))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', d2_tarski)).
% 1.05/0.50 thf(reflexivity, axiom, (mvalid @ (mforall_ind @ (^[X22:mu]:(qmltpeq @ X22 @ X22)))), file('/export/starexec/sandbox/tmp/tmp.VzmI1SJd6n/E---3.1_3373847.p', reflexivity)).
% 1.05/0.50 thf(c_0_21, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((Z0 @ Z2))))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies])).
% 1.05/0.50 thf(c_0_22, plain, ((mnot)=(^[Z0:$i > $o, Z1:$i]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot])).
% 1.05/0.50 thf(c_0_23, plain, ((mor)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor])).
% 1.05/0.50 thf(c_0_24, plain, ((mforall_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(![X12:mu]:((((exists_in_world @ X12 @ Z1))=>((Z0 @ X12 @ Z1))))))), inference(fof_simplification,[status(thm)],[mforall_ind])).
% 1.05/0.50 thf(c_0_25, plain, ((mvalid)=(^[Z0:$i > $o]:(![X3:$i]:((Z0 @ X3))))), inference(fof_simplification,[status(thm)],[mvalid])).
% 1.05/0.50 thf(c_0_26, plain, ((mand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~((Z0 @ Z2))))|((~((Z1 @ Z2)))))))))), inference(fof_simplification,[status(thm)],[mand])).
% 1.05/0.50 thf(c_0_27, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((Z0 @ Z2))))|((Z1 @ Z2)))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_21, c_0_22]), c_0_23])).
% 1.05/0.50 thf(c_0_28, plain, ![X124:$i, X123:mu]:(((exists_in_world @ X123 @ X124)=>![X122:mu]:(((exists_in_world @ X122 @ X124)=>(qmltpeq @ (set_intersection2 @ X123 @ X123) @ X123 @ X124))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[idempotence_k3_xboole_0]), c_0_24]), c_0_25])).
% 1.05/0.50 thf(c_0_29, plain, ((mequiv)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~(((((~((Z0 @ Z2))))|((Z1 @ Z2)))))))|((~(((((~((Z1 @ Z2))))|((Z0 @ Z2))))))))))))), inference(fof_simplification,[status(thm)],[mequiv])).
% 1.05/0.50 thf(c_0_30, plain, ((mand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~((Z0 @ Z2))))|((~((Z1 @ Z2)))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_26, c_0_22]), c_0_23])).
% 1.05/0.50 thf(c_0_31, plain, ![X56:$i, X55:mu]:(((exists_in_world @ X55 @ X56)=>![X54:mu]:(((exists_in_world @ X54 @ X56)=>(~(qmltpeq @ X55 @ X54 @ X56)|(qmltpeq @ X54 @ X55 @ X56)))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[symmetry]), c_0_27]), c_0_24]), c_0_25])])).
% 1.05/0.50 thf(c_0_32, plain, ![X221:$i, X222:mu, X223:mu]:((~(exists_in_world @ X222 @ X221)|(~(exists_in_world @ X223 @ X221)|(qmltpeq @ (set_intersection2 @ X222 @ X222) @ X222 @ X221)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])])])).
% 1.05/0.50 thf(c_0_33, plain, ((mequiv)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~(((((~((Z0 @ Z2))))|((Z1 @ Z2)))))))|((~(((((~((Z1 @ Z2))))|((Z0 @ Z2))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_29, c_0_30]), c_0_27])).
% 1.05/0.50 thf(c_0_34, plain, ![X95:$i, X94:mu]:(((exists_in_world @ X94 @ X95)=>![X93:mu]:(((exists_in_world @ X93 @ X95)=>![X92:mu]:(((exists_in_world @ X92 @ X95)=>(~(~((~(qmltpeq @ X94 @ X93 @ X95)|~(in @ X92 @ X94 @ X95))))|(in @ X92 @ X93 @ X95)))))))), 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(fof_simplification,[status(thm)],[in_substitution_2]), c_0_30]), c_0_27]), c_0_24]), c_0_25])])).
% 1.05/0.50 thf(c_0_35, plain, ![X154:$i, X155:mu, X156:mu]:((~(exists_in_world @ X155 @ X154)|(~(exists_in_world @ X156 @ X154)|(~(qmltpeq @ X155 @ X156 @ X154)|(qmltpeq @ X156 @ X155 @ X154))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_31])])])])).
% 1.05/0.50 thf(c_0_36, plain, ![X12:mu, X10:mu, X3:$i]:(((qmltpeq @ (set_intersection2 @ X10 @ X10) @ X10 @ X3)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 1.05/0.50 thf(c_0_37, plain, ![X146:$i, X147:mu, X148:mu]:((exists_in_world @ (set_intersection2 @ X147 @ X148) @ X146)), inference(variable_rename,[status(thm)],[existence_of_set_intersection2_ax])).
% 1.05/0.50 thf(c_0_38, plain, ![X107:$i, X106:mu]:(((exists_in_world @ X106 @ X107)=>~((~((~(qmltpeq @ X106 @ empty_set @ X107)|![X105:mu]:(((exists_in_world @ X105 @ X107)=>~(in @ X105 @ X106 @ X107)))))|~((~(![X105:mu]:(((exists_in_world @ X105 @ X107)=>~(in @ X105 @ X106 @ X107))))|(qmltpeq @ X106 @ empty_set @ X107))))))), 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(fof_simplification,[status(thm)],[d1_xboole_0]), c_0_22]), c_0_33]), c_0_24]), c_0_25])])).
% 1.05/0.50 thf(c_0_39, plain, ![X192:$i, X193:mu, X194:mu, X195:mu]:((~(exists_in_world @ X193 @ X192)|(~(exists_in_world @ X194 @ X192)|(~(exists_in_world @ X195 @ X192)|(~(qmltpeq @ X193 @ X194 @ X192)|~(in @ X195 @ X193 @ X192)|(in @ X195 @ X194 @ X192)))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_34])])])])).
% 1.05/0.50 thf(c_0_40, plain, ![X12:mu, X10:mu, X3:$i]:(((qmltpeq @ X12 @ X10 @ X3)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((qmltpeq @ X10 @ X12 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.05/0.50 thf(c_0_41, plain, ![X10:mu, X3:$i]:(((qmltpeq @ (set_intersection2 @ X10 @ X10) @ X10 @ X3)|~((exists_in_world @ X10 @ X3)))), inference(condense,[status(thm)],[c_0_36])).
% 1.05/0.50 thf(c_0_42, plain, ![X12:mu, X10:mu, X3:$i]:((exists_in_world @ (set_intersection2 @ X10 @ X12) @ X3)), inference(split_conjunct,[status(thm)],[c_0_37])).
% 1.05/0.50 thf(c_0_43, plain, ![X114:mu, X115:mu, X116:mu, X117:$i]:(((epred2_4 @ X117 @ X116 @ X115 @ X114)<=>~((~((~(qmltpeq @ X114 @ (set_intersection2 @ X116 @ X115) @ X117)|![X113:mu]:(((exists_in_world @ X113 @ X117)=>~((~((~(in @ X113 @ X114 @ X117)|~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117)))))|~((~(~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117))))|(in @ X113 @ X114 @ X117)))))))))|~((~(![X113:mu]:(((exists_in_world @ X113 @ X117)=>~((~((~(in @ X113 @ X114 @ X117)|~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117)))))|~((~(~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117))))|(in @ X113 @ X114 @ X117))))))))|(qmltpeq @ X114 @ (set_intersection2 @ X116 @ X115) @ X117))))))), introduced(definition)).
% 1.05/0.50 thf(c_0_44, plain, ![X120:$i, X119:mu]:(((exists_in_world @ X119 @ X120)=>![X118:mu]:(((exists_in_world @ X118 @ X120)=>~((~((~(disjoint @ X119 @ X118 @ X120)|(qmltpeq @ (set_intersection2 @ X119 @ X118) @ empty_set @ X120)))|~((~(qmltpeq @ (set_intersection2 @ X119 @ X118) @ empty_set @ X120)|(disjoint @ X119 @ X118 @ X120))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[d7_xboole_0]), c_0_33]), c_0_24]), c_0_25])])).
% 1.05/0.50 thf(c_0_45, plain, ![X205:$i, X206:mu, X207:mu]:(((~(qmltpeq @ X206 @ empty_set @ X205)|(~(exists_in_world @ X207 @ X205)|~(in @ X207 @ X206 @ X205))|~(exists_in_world @ X206 @ X205))&(((exists_in_world @ (esk2_2 @ X205 @ X206) @ X205)|(qmltpeq @ X206 @ empty_set @ X205)|~(exists_in_world @ X206 @ X205))&((in @ (esk2_2 @ X205 @ X206) @ X206 @ X205)|(qmltpeq @ X206 @ empty_set @ X205)|~(exists_in_world @ X206 @ X205))))), 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_38])])])])])])).
% 1.05/0.50 thf(c_0_46, plain, ![X12:mu, X14:mu, X10:mu, X3:$i]:(((in @ X14 @ X12 @ X3)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3))|~((qmltpeq @ X10 @ X12 @ X3))|~((in @ X14 @ X10 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 1.05/0.50 thf(c_0_47, plain, ![X10:mu, X3:$i]:(((qmltpeq @ X10 @ (set_intersection2 @ X10 @ X10) @ X3)|~((exists_in_world @ X10 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42])])).
% 1.05/0.50 thf(c_0_48, plain, ![X114:mu, X115:mu, X116:mu, X117:$i]:(((epred2_4 @ X117 @ X116 @ X115 @ X114)=>~((~((~(qmltpeq @ X114 @ (set_intersection2 @ X116 @ X115) @ X117)|![X113:mu]:(((exists_in_world @ X113 @ X117)=>~((~((~(in @ X113 @ X114 @ X117)|~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117)))))|~((~(~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117))))|(in @ X113 @ X114 @ X117)))))))))|~((~(![X113:mu]:(((exists_in_world @ X113 @ X117)=>~((~((~(in @ X113 @ X114 @ X117)|~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117)))))|~((~(~((~(in @ X113 @ X116 @ X117)|~(in @ X113 @ X115 @ X117))))|(in @ X113 @ X114 @ X117))))))))|(qmltpeq @ X114 @ (set_intersection2 @ X116 @ X115) @ X117))))))), inference(split_equiv,[status(thm)],[c_0_43])).
% 1.05/0.50 thf(c_0_49, plain, ![X217:$i, X218:mu, X219:mu]:(((~(disjoint @ X218 @ X219 @ X217)|(qmltpeq @ (set_intersection2 @ X218 @ X219) @ empty_set @ X217)|~(exists_in_world @ X219 @ X217)|~(exists_in_world @ X218 @ X217))&(~(qmltpeq @ (set_intersection2 @ X218 @ X219) @ empty_set @ X217)|(disjoint @ X218 @ X219 @ X217)|~(exists_in_world @ X219 @ X217)|~(exists_in_world @ X218 @ X217)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_44])])])])])).
% 1.05/0.50 thf(c_0_50, plain, ![X145:$i]:((exists_in_world @ empty_set @ X145)), inference(variable_rename,[status(thm)],[existence_of_empty_set_ax])).
% 1.05/0.50 thf(c_0_51, plain, ![X12:mu, X10:mu, X3:$i]:((~((qmltpeq @ X10 @ empty_set @ X3))|~((exists_in_world @ X12 @ X3))|~((in @ X12 @ X10 @ X3))|~((exists_in_world @ X10 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 1.05/0.50 thf(c_0_52, plain, ![X12:mu, X10:mu, X3:$i]:(((in @ X10 @ (set_intersection2 @ X12 @ X12) @ X3)|~((in @ X10 @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_47]), c_0_42])])).
% 1.05/0.50 thf(c_0_53, plain, ![X241:mu, X242:mu, X243:mu, X244:$i, X245:mu]:((((((in @ X245 @ X243 @ X244)|~(in @ X245 @ X241 @ X244)|~(exists_in_world @ X245 @ X244)|~(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241))&((in @ X245 @ X242 @ X244)|~(in @ X245 @ X241 @ X244)|~(exists_in_world @ X245 @ X244)|~(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241)))&(~(in @ X245 @ X243 @ X244)|~(in @ X245 @ X242 @ X244)|(in @ X245 @ X241 @ X244)|~(exists_in_world @ X245 @ X244)|~(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241)))&(((exists_in_world @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X244)|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241))&(((((in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X243 @ X244)|(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X241 @ X244)|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241))&((in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X242 @ X244)|(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X241 @ X244)|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241)))&(~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X241 @ X244)|(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X241 @ X244)|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241)))&((((in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X243 @ X244)|(~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X243 @ X244)|~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X242 @ X244))|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241))&((in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X242 @ X244)|(~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X243 @ X244)|~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X242 @ X244))|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241)))&(~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X241 @ X244)|(~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X243 @ X244)|~(in @ (esk10_4 @ X241 @ X242 @ X243 @ X244) @ X242 @ X244))|(qmltpeq @ X241 @ (set_intersection2 @ X243 @ X242) @ X244)|~(epred2_4 @ X244 @ X243 @ X242 @ X241))))))), 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_48])])])])])])).
% 1.05/0.50 thf(c_0_54, plain, ![X12:mu, X10:mu, X3:$i]:(((qmltpeq @ (set_intersection2 @ X10 @ X12) @ empty_set @ X3)|~((disjoint @ X10 @ X12 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_49])).
% 1.05/0.50 thf(c_0_55, plain, ![X3:$i]:((exists_in_world @ empty_set @ X3)), inference(split_conjunct,[status(thm)],[c_0_50])).
% 1.05/0.50 thf(c_0_56, plain, ![X12:mu, X10:mu, X3:$i]:((~((qmltpeq @ (set_intersection2 @ X10 @ X10) @ empty_set @ X3))|~((in @ X12 @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_42])])).
% 1.05/0.50 thf(c_0_57, plain, ![X117:$i, X116:mu]:(((exists_in_world @ X116 @ X117)=>![X115:mu]:(((exists_in_world @ X115 @ X117)=>![X114:mu]:(((exists_in_world @ X114 @ X117)=>(epred2_4 @ X117 @ X116 @ X115 @ X114))))))), inference(apply_def,[status(thm)],[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(fof_simplification,[status(thm)],[d3_xboole_0]), c_0_30]), c_0_33]), c_0_24]), c_0_25])]), c_0_43])).
% 1.05/0.50 thf(c_0_58, negated_conjecture, ~((mvalid @ (mforall_ind @ (^[X28:mu]:(mforall_ind @ (^[X29:mu]:(mforall_ind @ (^[X30:mu]:(mnot @ (mand @ (disjoint @ (unordered_pair @ X28 @ X29) @ X30) @ (in @ X28 @ X30))))))))))), inference(assume_negation,[status(cth)],[t55_zfmisc_1])).
% 1.05/0.50 thf(c_0_59, plain, ![X80:$i, X79:mu]:(((exists_in_world @ X79 @ X80)=>![X78:mu]:(((exists_in_world @ X78 @ X80)=>![X77:mu]:(((exists_in_world @ X77 @ X80)=>(~(~((~(qmltpeq @ X79 @ X78 @ X80)|~(disjoint @ X79 @ X77 @ X80))))|(disjoint @ X78 @ X77 @ X80)))))))), 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(fof_simplification,[status(thm)],[disjoint_substitution_1]), c_0_30]), c_0_27]), c_0_24]), c_0_25])])).
% 1.05/0.50 thf(c_0_60, plain, ![X101:$i, X100:mu]:(((exists_in_world @ X100 @ X101)=>![X99:mu]:(((exists_in_world @ X99 @ X101)=>(qmltpeq @ (unordered_pair @ X100 @ X99) @ (unordered_pair @ X99 @ X100) @ X101))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[commutativity_k2_tarski]), c_0_24]), c_0_25])).
% 1.05/0.50 thf(c_0_61, plain, ![X109:mu, X110:mu, X111:mu, X112:$i]:(((epred1_4 @ X112 @ X111 @ X110 @ X109)<=>~((~((~(qmltpeq @ X109 @ (unordered_pair @ X111 @ X110) @ X112)|![X108:mu]:(((exists_in_world @ X108 @ X112)=>~((~((~(in @ X108 @ X109 @ X112)|((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112))))|~((~(((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112)))|(in @ X108 @ X109 @ X112)))))))))|~((~(![X108:mu]:(((exists_in_world @ X108 @ X112)=>~((~((~(in @ X108 @ X109 @ X112)|((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112))))|~((~(((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112)))|(in @ X108 @ X109 @ X112))))))))|(qmltpeq @ X109 @ (unordered_pair @ X111 @ X110) @ X112))))))), introduced(definition)).
% 1.05/0.50 thf(c_0_62, plain, ![X10:mu, X3:$i, X12:mu, X14:mu, X19:mu]:(((in @ X10 @ X19 @ X3)|~((in @ X10 @ X12 @ X3))|~((in @ X10 @ X14 @ X3))|~((exists_in_world @ X10 @ X3))|~((qmltpeq @ X19 @ (set_intersection2 @ X12 @ X14) @ X3))|~((epred2_4 @ X3 @ X12 @ X14 @ X19)))), inference(split_conjunct,[status(thm)],[c_0_53])).
% 1.05/0.50 thf(c_0_63, plain, ![X12:mu, X10:mu, X3:$i]:(((qmltpeq @ empty_set @ (set_intersection2 @ X10 @ X12) @ X3)|~((disjoint @ X10 @ X12 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_54]), c_0_55]), c_0_42])])).
% 1.05/0.50 thf(c_0_64, plain, ![X10:mu, X3:$i]:((~((in @ X10 @ empty_set @ X3))|~((exists_in_world @ X10 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_41]), c_0_55])])).
% 1.05/0.50 thf(c_0_65, plain, ![X213:$i, X214:mu, X215:mu, X216:mu]:((~(exists_in_world @ X214 @ X213)|(~(exists_in_world @ X215 @ X213)|(~(exists_in_world @ X216 @ X213)|(epred2_4 @ X213 @ X214 @ X215 @ X216))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_57])])])])).
% 1.05/0.50 thf(c_0_66, negated_conjecture, ~(![X135:$i, X134:mu]:(((exists_in_world @ X134 @ X135)=>![X133:mu]:(((exists_in_world @ X133 @ X135)=>![X132:mu]:(((exists_in_world @ X132 @ X135)=>~(~((~(disjoint @ (unordered_pair @ X134 @ X133) @ X132 @ X135)|~(in @ X134 @ X132 @ X135))))))))))), 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(fof_simplification,[status(thm)],[c_0_58]), c_0_22]), c_0_30]), c_0_24]), c_0_25])])).
% 1.05/0.50 thf(c_0_67, plain, ![X177:$i, X178:mu, X179:mu, X180:mu]:((~(exists_in_world @ X178 @ X177)|(~(exists_in_world @ X179 @ X177)|(~(exists_in_world @ X180 @ X177)|(~(qmltpeq @ X178 @ X179 @ X177)|~(disjoint @ X178 @ X180 @ X177)|(disjoint @ X179 @ X180 @ X177)))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_59])])])])).
% 1.05/0.50 thf(c_0_68, plain, ![X199:$i, X200:mu, X201:mu]:((~(exists_in_world @ X200 @ X199)|(~(exists_in_world @ X201 @ X199)|(qmltpeq @ (unordered_pair @ X200 @ X201) @ (unordered_pair @ X201 @ X200) @ X199)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_60])])])])).
% 1.05/0.50 thf(c_0_69, plain, ![X149:$i, X150:mu, X151:mu]:((exists_in_world @ (unordered_pair @ X150 @ X151) @ X149)), inference(variable_rename,[status(thm)],[existence_of_unordered_pair_ax])).
% 1.05/0.50 thf(c_0_70, plain, ![X109:mu, X110:mu, X111:mu, X112:$i]:(((epred1_4 @ X112 @ X111 @ X110 @ X109)=>~((~((~(qmltpeq @ X109 @ (unordered_pair @ X111 @ X110) @ X112)|![X108:mu]:(((exists_in_world @ X108 @ X112)=>~((~((~(in @ X108 @ X109 @ X112)|((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112))))|~((~(((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112)))|(in @ X108 @ X109 @ X112)))))))))|~((~(![X108:mu]:(((exists_in_world @ X108 @ X112)=>~((~((~(in @ X108 @ X109 @ X112)|((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112))))|~((~(((qmltpeq @ X108 @ X111 @ X112)|(qmltpeq @ X108 @ X110 @ X112)))|(in @ X108 @ X109 @ X112))))))))|(qmltpeq @ X109 @ (unordered_pair @ X111 @ X110) @ X112))))))), inference(split_equiv,[status(thm)],[c_0_61])).
% 1.05/0.50 thf(c_0_71, plain, ![X112:$i, X111:mu]:(((exists_in_world @ X111 @ X112)=>![X110:mu]:(((exists_in_world @ X110 @ X112)=>![X109:mu]:(((exists_in_world @ X109 @ X112)=>(epred1_4 @ X112 @ X111 @ X110 @ X109))))))), inference(apply_def,[status(thm)],[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(fof_simplification,[status(thm)],[d2_tarski]), c_0_23]), c_0_33]), c_0_24]), c_0_25])]), c_0_61])).
% 1.05/0.50 thf(c_0_72, plain, ![X14:mu, X12:mu, X10:mu, X3:$i]:((~((epred2_4 @ X3 @ X10 @ X12 @ empty_set))|~((in @ X14 @ X12 @ X3))|~((in @ X14 @ X10 @ X3))|~((disjoint @ X10 @ X12 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_64])).
% 1.05/0.50 thf(c_0_73, plain, ![X12:mu, X14:mu, X10:mu, X3:$i]:(((epred2_4 @ X3 @ X10 @ X12 @ X14)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_65])).
% 1.05/0.50 thf(c_0_74, negated_conjecture, ((exists_in_world @ esk6_0 @ esk5_0)&((exists_in_world @ esk7_0 @ esk5_0)&((exists_in_world @ esk8_0 @ esk5_0)&((disjoint @ (unordered_pair @ esk6_0 @ esk7_0) @ esk8_0 @ esk5_0)&(in @ esk6_0 @ esk8_0 @ esk5_0))))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_66])])])).
% 1.05/0.50 thf(c_0_75, plain, ![X10:mu, X14:mu, X12:mu, X3:$i]:(((disjoint @ X12 @ X14 @ X3)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3))|~((qmltpeq @ X10 @ X12 @ X3))|~((disjoint @ X10 @ X14 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_67])).
% 1.05/0.50 thf(c_0_76, plain, ![X12:mu, X10:mu, X3:$i]:(((qmltpeq @ (unordered_pair @ X10 @ X12) @ (unordered_pair @ X12 @ X10) @ X3)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_68])).
% 1.05/0.50 thf(c_0_77, plain, ![X12:mu, X10:mu, X3:$i]:((exists_in_world @ (unordered_pair @ X10 @ X12) @ X3)), inference(split_conjunct,[status(thm)],[c_0_69])).
% 1.05/0.50 thf(c_0_78, plain, ![X235:mu, X236:mu, X237:mu, X238:$i, X239:mu]:((((~(in @ X239 @ X235 @ X238)|((qmltpeq @ X239 @ X237 @ X238)|(qmltpeq @ X239 @ X236 @ X238))|~(exists_in_world @ X239 @ X238)|~(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))&((~(qmltpeq @ X239 @ X237 @ X238)|(in @ X239 @ X235 @ X238)|~(exists_in_world @ X239 @ X238)|~(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))&(~(qmltpeq @ X239 @ X236 @ X238)|(in @ X239 @ X235 @ X238)|~(exists_in_world @ X239 @ X238)|~(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))))&(((exists_in_world @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))&((((qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X237 @ X238)|(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X236 @ X238)|(in @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X235 @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))&(~(in @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X235 @ X238)|(in @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X235 @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235)))&((((qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X237 @ X238)|(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X236 @ X238)|~(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X237 @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))&(~(in @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X235 @ X238)|~(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X237 @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235)))&(((qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X237 @ X238)|(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X236 @ X238)|~(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X236 @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235))&(~(in @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X235 @ X238)|~(qmltpeq @ (esk9_4 @ X235 @ X236 @ X237 @ X238) @ X236 @ X238)|(qmltpeq @ X235 @ (unordered_pair @ X237 @ X236) @ X238)|~(epred1_4 @ X238 @ X237 @ X236 @ X235)))))))), 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_70])])])])])])).
% 1.05/0.50 thf(c_0_79, plain, ![X209:$i, X210:mu, X211:mu, X212:mu]:((~(exists_in_world @ X210 @ X209)|(~(exists_in_world @ X211 @ X209)|(~(exists_in_world @ X212 @ X209)|(epred1_4 @ X209 @ X210 @ X211 @ X212))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_71])])])])).
% 1.05/0.50 thf(c_0_80, plain, ![X53:$i, X52:mu]:(((exists_in_world @ X52 @ X53)=>(qmltpeq @ X52 @ X52 @ X53))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity]), c_0_24]), c_0_25])).
% 1.05/0.50 thf(c_0_81, plain, ![X12:mu, X14:mu, X10:mu, X3:$i]:((~((in @ X10 @ X12 @ X3))|~((in @ X10 @ X14 @ X3))|~((disjoint @ X14 @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_73]), c_0_55])])).
% 1.05/0.50 thf(c_0_82, negated_conjecture, (in @ esk6_0 @ esk8_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.05/0.50 thf(c_0_83, negated_conjecture, (exists_in_world @ esk6_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.05/0.50 thf(c_0_84, negated_conjecture, (exists_in_world @ esk8_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.05/0.50 thf(c_0_85, plain, ![X14:mu, X12:mu, X10:mu, X3:$i]:(((disjoint @ (unordered_pair @ X10 @ X12) @ X14 @ X3)|~((disjoint @ (unordered_pair @ X12 @ X10) @ X14 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_77]), c_0_77])])).
% 1.05/0.50 thf(c_0_86, negated_conjecture, (disjoint @ (unordered_pair @ esk6_0 @ esk7_0) @ esk8_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.05/0.50 thf(c_0_87, negated_conjecture, (exists_in_world @ esk7_0 @ esk5_0), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.05/0.50 thf(c_0_88, plain, ![X3:$i, X10:mu, X12:mu, X19:mu, X14:mu]:(((in @ X10 @ X14 @ X3)|~((qmltpeq @ X10 @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((qmltpeq @ X14 @ (unordered_pair @ X19 @ X12) @ X3))|~((epred1_4 @ X3 @ X19 @ X12 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_78])).
% 1.05/0.50 thf(c_0_89, plain, ![X12:mu, X14:mu, X10:mu, X3:$i]:(((epred1_4 @ X3 @ X10 @ X12 @ X14)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_79])).
% 1.05/0.50 thf(c_0_90, plain, ![X152:$i, X153:mu]:((~(exists_in_world @ X153 @ X152)|(qmltpeq @ X153 @ X153 @ X152))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_80])])])).
% 1.05/0.50 thf(c_0_91, negated_conjecture, ![X10:mu]:((~((in @ esk6_0 @ X10 @ esk5_0))|~((disjoint @ X10 @ esk8_0 @ esk5_0))|~((exists_in_world @ X10 @ esk5_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_82]), c_0_83]), c_0_84])])).
% 1.05/0.50 thf(c_0_92, negated_conjecture, (disjoint @ (unordered_pair @ esk7_0 @ esk6_0) @ esk8_0 @ esk5_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_86]), c_0_84]), c_0_87]), c_0_83])])).
% 1.05/0.50 thf(c_0_93, plain, ![X12:mu, X19:mu, X14:mu, X10:mu, X3:$i]:(((in @ X10 @ X12 @ X3)|~((qmltpeq @ X12 @ (unordered_pair @ X14 @ X19) @ X3))|~((qmltpeq @ X10 @ X19 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X14 @ X3)))), inference(spm,[status(thm)],[c_0_88, c_0_89])).
% 1.05/0.50 thf(c_0_94, plain, ![X10:mu, X3:$i]:(((qmltpeq @ X10 @ X10 @ X3)|~((exists_in_world @ X10 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_90])).
% 1.05/0.50 thf(c_0_95, negated_conjecture, ~((in @ esk6_0 @ (unordered_pair @ esk7_0 @ esk6_0) @ esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_92]), c_0_77])])).
% 1.05/0.50 thf(c_0_96, plain, ![X14:mu, X12:mu, X10:mu, X3:$i]:(((in @ X10 @ (unordered_pair @ X12 @ X14) @ X3)|~((qmltpeq @ X10 @ X14 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_94]), c_0_77])])).
% 1.05/0.50 thf(c_0_97, plain, ~((qmltpeq @ esk6_0 @ esk6_0 @ esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95, c_0_96]), c_0_83]), c_0_87])])).
% 1.05/0.50 thf(c_0_98, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_94]), c_0_83])]), ['proof']).
% 1.05/0.50 % SZS output end CNFRefutation
% 1.05/0.50 % Parsed axioms : 106
% 1.05/0.50 % Removed by relevancy pruning/SinE : 0
% 1.05/0.50 % Initial clauses : 103
% 1.05/0.50 % Removed in clause preprocessing : 48
% 1.05/0.50 % Initial clauses in saturation : 55
% 1.05/0.50 % Processed clauses : 602
% 1.05/0.50 % ...of these trivial : 5
% 1.05/0.50 % ...subsumed : 140
% 1.05/0.50 % ...remaining for further processing : 457
% 1.05/0.50 % Other redundant clauses eliminated : 0
% 1.05/0.50 % Clauses deleted for lack of memory : 0
% 1.05/0.50 % Backward-subsumed : 12
% 1.05/0.50 % Backward-rewritten : 1
% 1.05/0.50 % Generated clauses : 4019
% 1.05/0.50 % ...of the previous two non-redundant : 3855
% 1.05/0.50 % ...aggressively subsumed : 0
% 1.05/0.50 % Contextual simplify-reflections : 5
% 1.05/0.50 % Paramodulations : 4019
% 1.05/0.50 % Factorizations : 0
% 1.05/0.50 % NegExts : 0
% 1.05/0.50 % Equation resolutions : 0
% 1.05/0.50 % Disequality decompositions : 0
% 1.05/0.50 % Total rewrite steps : 5459
% 1.05/0.50 % ...of those cached : 5309
% 1.05/0.50 % Propositional unsat checks : 0
% 1.05/0.50 % Propositional check models : 0
% 1.05/0.50 % Propositional check unsatisfiable : 0
% 1.05/0.50 % Propositional clauses : 0
% 1.05/0.50 % Propositional clauses after purity: 0
% 1.05/0.50 % Propositional unsat core size : 0
% 1.05/0.50 % Propositional preprocessing time : 0.000
% 1.05/0.50 % Propositional encoding time : 0.000
% 1.05/0.50 % Propositional solver time : 0.000
% 1.05/0.50 % Success case prop preproc time : 0.000
% 1.05/0.50 % Success case prop encoding time : 0.000
% 1.05/0.50 % Success case prop solver time : 0.000
% 1.05/0.50 % Current number of processed clauses : 389
% 1.05/0.50 % Positive orientable unit clauses : 45
% 1.05/0.50 % Positive unorientable unit clauses: 0
% 1.05/0.50 % Negative unit clauses : 7
% 1.05/0.50 % Non-unit-clauses : 337
% 1.05/0.50 % Current number of unprocessed clauses: 3336
% 1.05/0.50 % ...number of literals in the above : 20116
% 1.05/0.50 % Current number of archived formulas : 0
% 1.05/0.50 % Current number of archived clauses : 68
% 1.05/0.50 % Clause-clause subsumption calls (NU) : 45313
% 1.05/0.50 % Rec. Clause-clause subsumption calls : 3896
% 1.05/0.50 % Non-unit clause-clause subsumptions : 149
% 1.05/0.50 % Unit Clause-clause subsumption calls : 352
% 1.05/0.50 % Rewrite failures with RHS unbound : 0
% 1.05/0.50 % BW rewrite match attempts : 9
% 1.05/0.50 % BW rewrite match successes : 1
% 1.05/0.50 % Condensation attempts : 602
% 1.05/0.50 % Condensation successes : 1
% 1.05/0.50 % Termbank termtop insertions : 130785
% 1.05/0.50 % Search garbage collected termcells : 5889
% 1.05/0.50
% 1.05/0.50 % -------------------------------------------------
% 1.05/0.50 % User time : 0.214 s
% 1.05/0.50 % System time : 0.016 s
% 1.05/0.50 % Total time : 0.230 s
% 1.05/0.50 % Maximum resident set size: 4468 pages
% 1.05/0.50
% 1.05/0.50 % -------------------------------------------------
% 1.05/0.50 % User time : 1.055 s
% 1.05/0.50 % System time : 0.049 s
% 1.05/0.50 % Total time : 1.105 s
% 1.05/0.50 % Maximum resident set size: 4864 pages
% 1.05/0.50 % E exiting
%------------------------------------------------------------------------------