%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SYO881^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:44:54 AM UTC 2026
% Result : Theorem 73.51s 38.17s
% Output : CNFRefutation 73.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO881^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n002.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.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:26:52 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.20/0.27 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.QGprp28Z5m/E---3.1_1598623.p
% 73.51/38.17 % Version: 3.5.1-ho
% 73.51/38.17 % partial match(1): HSLMSMSSSSLCHSA
% 73.51/38.17 % Preprocessing class: HSLMSLSSSSLCHSA.
% 73.51/38.17 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 73.51/38.17 % Starting pre_casc_6 with 1500s (5) cores
% 73.51/38.17 % Starting ehoh_best7 with 300s (1) cores
% 73.51/38.17 % Starting new_bool_8 with 300s (1) cores
% 73.51/38.17 % Starting new_ho_11 with 300s (1) cores
% 73.51/38.17 % ehoh_best7 with pid 1598637 completed with status 0
% 73.51/38.17 % Result found by ehoh_best7
% 73.51/38.17 % partial match(1): HSLMSMSSSSLCHSA
% 73.51/38.17 % Preprocessing class: HSLMSLSSSSLCHSA.
% 73.51/38.17 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 73.51/38.17 % Starting pre_casc_6 with 1500s (5) cores
% 73.51/38.17 % Starting ehoh_best7 with 300s (1) cores
% 73.51/38.17 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 73.51/38.17 % No SInE strategy applied
% 73.51/38.17 % Search class: HGHSM-SMLM33-DHSFFSBC
% 73.51/38.17 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 73.51/38.17 % Scheduled 7 strats onto 1 cores with 274 seconds (274 total)
% 73.51/38.17 % Starting SubtermCWHack with 25s (1) cores
% 73.51/38.17 % SubtermCWHack with pid 1598649 completed with status 0
% 73.51/38.17 % Result found by SubtermCWHack
% 73.51/38.17 % partial match(1): HSLMSMSSSSLCHSA
% 73.51/38.17 % Preprocessing class: HSLMSLSSSSLCHSA.
% 73.51/38.17 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 73.51/38.17 % Starting pre_casc_6 with 1500s (5) cores
% 73.51/38.17 % Starting ehoh_best7 with 300s (1) cores
% 73.51/38.17 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 73.51/38.17 % No SInE strategy applied
% 73.51/38.17 % Search class: HGHSM-SMLM33-DHSFFSBC
% 73.51/38.17 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 73.51/38.17 % Scheduled 7 strats onto 1 cores with 274 seconds (274 total)
% 73.51/38.17 % Starting SubtermCWHack with 25s (1) cores
% 73.51/38.17 % Preprocessing time : 0.120 s
% 73.51/38.17
% 73.51/38.17 % Proof found!
% 73.51/38.17 % SZS status Theorem
% 73.51/38.17 % SZS output start CNFRefutation
% 73.51/38.17 thf(decl_24, type, c_False: $o).
% 73.51/38.17 thf(decl_26, type, c_not: $o > $o).
% 73.51/38.17 thf(decl_27, type, c_and: $o > $o > $o).
% 73.51/38.17 thf(decl_29, type, c_iff: $o > $o > $o).
% 73.51/38.17 thf(decl_30, type, c_In: $i > $i > $o).
% 73.51/38.17 thf(decl_31, type, c_Subq: $i > $i > $o).
% 73.51/38.17 thf(decl_32, type, c_Empty: $i).
% 73.51/38.17 thf(decl_33, type, c_Union: $i > $i).
% 73.51/38.17 thf(decl_34, type, c_Power: $i > $i).
% 73.51/38.17 thf(decl_48, type, c_irreflexive_i: ($i > $i > $o) > $o).
% 73.51/38.17 thf(decl_51, type, c_transitive_i: ($i > $i > $o) > $o).
% 73.51/38.17 thf(decl_127, type, epred1_2: $i > $i > $o).
% 73.51/38.17 thf(decl_165, type, epred39_1: ($i > $i > $o) > $o).
% 73.51/38.17 thf(decl_269, type, esk1_0: $i).
% 73.51/38.17 thf(decl_270, type, esk2_2: $i > $i > $i).
% 73.51/38.17 thf(decl_271, type, esk3_2: $i > $i > $i).
% 73.51/38.17 thf(decl_280, type, esk12_1: ($i > $o) > $i).
% 73.51/38.17 thf(decl_281, type, epred143_0: $o).
% 73.51/38.17 thf(decl_282, type, epred144_2: $o > $o > $o).
% 73.51/38.17 thf(decl_284, type, esk13_2: $i > $i > $i).
% 73.51/38.17 thf(decl_288, type, esk17_1: ($i > $i > $o) > $i).
% 73.51/38.17 thf(decl_289, type, esk18_1: ($i > $i > $o) > $i).
% 73.51/38.17 thf(decl_294, type, esk23_1: ($i > $i > $o) > $i).
% 73.51/38.17 thf(decl_295, type, esk24_1: ($i > $i > $o) > $i).
% 73.51/38.17 thf(decl_296, type, esk25_1: ($i > $i > $o) > $i).
% 73.51/38.17 thf(decl_327, type, esk52_0: $i > $i > $i).
% 73.51/38.17 thf(decl_328, type, esk53_0: $i > $i).
% 73.51/38.17 thf(decl_329, type, esk54_0: $i).
% 73.51/38.17 thf(decl_330, type, esk55_0: $i).
% 73.51/38.17 thf(decl_331, type, esk56_0: $i).
% 73.51/38.17 thf(decl_498, type, esk217_0: ($i > $i) > $i > $i).
% 73.51/38.17 thf(decl_505, type, esk222_1: $i > $i > $i).
% 73.51/38.17 thf(decl_513, type, epred161_1: ($i > $o) > $i > $o).
% 73.51/38.17 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax13)).
% 73.51/38.17 thf(ax6, axiom, ![X8:$i, X2:$i]:((c_iff @ ((c_In @ X2 @ (c_Union @ X8))) @ (?[X9:$i]:((c_and @ ((c_In @ X2 @ X9)) @ ((c_In @ X9 @ X8))))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax6)).
% 73.51/38.17 thf(ax14, axiom, ((c_and)=(^[X18:$o, X19:$o]:(![X20:$o]:((((((X18))=>((((X19))=>((X20))))))=>((X20))))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax14)).
% 73.51/38.17 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax5)).
% 73.51/38.17 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax11)).
% 73.51/38.17 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax3)).
% 73.51/38.17 thf(conj, conjecture, (c_not @ (![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((X205 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ X206 @ X206) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ X206 @ X207))) @ X206)) @ X207) @ (X202 @ (X205 @ X83) @ X207)) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X205 @ (X202 @ X207 @ X206))) @ (X202 @ X83 @ X83)) @ (X202 @ X83 @ (X202 @ X207 @ X206))) @ X206))) @ X207))) @ X206)) @ X83) @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X83 @ X83) @ X83)) @ X206)))) @ (X205 @ (X205 @ X83))) @ X206))=(X205 @ (X205 @ X207)))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', conj)).
% 73.51/38.17 thf(ax17, axiom, ((c_Subq)=(^[X26:$i, X2:$i]:(![X9:$i]:((((c_In @ X9 @ X26))=>((c_In @ X9 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax17)).
% 73.51/38.17 thf(ax4, axiom, ![X6:$i, X2:$i]:(((c_Subq @ X6 @ X2)=>((c_Subq @ X2 @ X6)=>((X6)=(X2))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax4)).
% 73.51/38.17 thf(ax30, axiom, ((c_irreflexive_i)=(^[X38:$i > $i > $o]:(![X2:$i]:((c_not @ ((X38 @ X2 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax30)).
% 73.51/38.17 thf(ax33, axiom, ((c_transitive_i)=(^[X41:$i > $i > $o]:(![X2:$i, X9:$i, X13:$i]:((((X41 @ X2 @ X9))=>((((X41 @ X9 @ X13))=>((X41 @ X2 @ X13))))))))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax33)).
% 73.51/38.17 thf(ax7, axiom, ![X10:$i, X2:$i]:((c_iff @ ((c_In @ X2 @ (c_Power @ X10))) @ ((c_Subq @ X2 @ X10)))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax7)).
% 73.51/38.17 thf(ax10, axiom, ![X1:$i > $o]:((![X2:$i]:((![X9:$i]:(((c_In @ X9 @ X2)=>(X1 @ X9)))=>(X1 @ X2)))=>![X2:$i]:((X1 @ X2)))), file('/export/starexec/sandbox/tmp/tmp.QGprp28Z5m/E---3.1_1598623.p', ax10)).
% 73.51/38.17 thf(c_0_13, plain, ![X2:$i, X8:$i]:(((epred1_2 @ X8 @ X2)<=>~(?[X9:$i]:(((~(c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $true @ $true))&((c_In @ X9 @ X8)|(c_and @ $true @ $false))))&((c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $false @ $true))&((c_In @ X9 @ X8)|(c_and @ $false @ $false))))))))), introduced(definition)).
% 73.51/38.17 thf(c_0_14, plain, ![X237:$o]:(((c_not @ ((X237)))<=>((X237)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 73.51/38.17 thf(c_0_15, axiom, ![X8:$i, X2:$i]:(((~(c_In @ X2 @ (c_Union @ X8))|(((epred1_2 @ X8 @ X2)|(c_iff @ $true @ $true))&(?[X9:$i]:(((~(c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $true @ $true))&((c_In @ X9 @ X8)|(c_and @ $true @ $false))))&((c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $false @ $true))&((c_In @ X9 @ X8)|(c_and @ $false @ $false))))))|(c_iff @ $true @ $false))))&((c_In @ X2 @ (c_Union @ X8))|(((epred1_2 @ X8 @ X2)|(c_iff @ $false @ $true))&(?[X9:$i]:(((~(c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $true @ $true))&((c_In @ X9 @ X8)|(c_and @ $true @ $false))))&((c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $false @ $true))&((c_In @ X9 @ X8)|(c_and @ $false @ $false))))))|(c_iff @ $false @ $false)))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[ax6]), c_0_13]), c_0_13])).
% 73.51/38.17 thf(c_0_16, plain, ![X238:$o, X239:$o]:(((c_and @ ((X238)) @ ((X239)))<=>![X20:$o]:((((X238)=>((X239)=>(X20)))=>(X20))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax14])])).
% 73.51/38.17 thf(c_0_17, axiom, ((~(?[X7:$i]:((c_In @ X7 @ c_Empty)))|(c_not @ $true))&(?[X7:$i]:((c_In @ X7 @ c_Empty))|(c_not @ $false))), inference(fool_unroll,[status(thm)],[ax5])).
% 73.51/38.17 thf(c_0_18, plain, ![X485:$o]:(((~(c_not @ ((X485)))|(~(X485)|(c_False)))&(((X485)|(c_not @ ((X485))))&(~(c_False)|(c_not @ ((X485))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])])).
% 73.51/38.17 thf(c_0_19, plain, ![X483:$o]:(((~(c_False)|(X483))&(~(epred143_0)|(c_False)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax11])])])])])).
% 73.51/38.17 thf(c_0_20, plain, ![X454:$i, X455:$i, X457:$i, X458:$i]:(((((epred1_2 @ X454 @ X455)|(c_iff @ $true @ $true)|~(c_In @ X455 @ (c_Union @ X454)))&(((~(c_In @ (esk2_2 @ X454 @ X455) @ X454)|(c_and @ $true @ $true)|~(c_In @ X455 @ (esk2_2 @ X454 @ X455))|(c_iff @ $true @ $false)|~(c_In @ X455 @ (c_Union @ X454)))&((c_In @ (esk2_2 @ X454 @ X455) @ X454)|(c_and @ $true @ $false)|~(c_In @ X455 @ (esk2_2 @ X454 @ X455))|(c_iff @ $true @ $false)|~(c_In @ X455 @ (c_Union @ X454))))&((~(c_In @ (esk2_2 @ X454 @ X455) @ X454)|(c_and @ $false @ $true)|(c_In @ X455 @ (esk2_2 @ X454 @ X455))|(c_iff @ $true @ $false)|~(c_In @ X455 @ (c_Union @ X454)))&((c_In @ (esk2_2 @ X454 @ X455) @ X454)|(c_and @ $false @ $false)|(c_In @ X455 @ (esk2_2 @ X454 @ X455))|(c_iff @ $true @ $false)|~(c_In @ X455 @ (c_Union @ X454))))))&(((epred1_2 @ X457 @ X458)|(c_iff @ $false @ $true)|(c_In @ X458 @ (c_Union @ X457)))&(((~(c_In @ (esk3_2 @ X457 @ X458) @ X457)|(c_and @ $true @ $true)|~(c_In @ X458 @ (esk3_2 @ X457 @ X458))|(c_iff @ $false @ $false)|(c_In @ X458 @ (c_Union @ X457)))&((c_In @ (esk3_2 @ X457 @ X458) @ X457)|(c_and @ $true @ $false)|~(c_In @ X458 @ (esk3_2 @ X457 @ X458))|(c_iff @ $false @ $false)|(c_In @ X458 @ (c_Union @ X457))))&((~(c_In @ (esk3_2 @ X457 @ X458) @ X457)|(c_and @ $false @ $true)|(c_In @ X458 @ (esk3_2 @ X457 @ X458))|(c_iff @ $false @ $false)|(c_In @ X458 @ (c_Union @ X457)))&((c_In @ (esk3_2 @ X457 @ X458) @ X457)|(c_and @ $false @ $false)|(c_In @ X458 @ (esk3_2 @ X457 @ X458))|(c_iff @ $false @ $false)|(c_In @ X458 @ (c_Union @ X457)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[c_0_15])])])])])])).
% 73.51/38.17 thf(c_0_21, plain, ![X448:$o, X449:$o]:(((~(X448)|(X449)|~(c_iff @ ((X448)) @ ((X449))))&(~(X449)|(X448)|~(c_iff @ ((X448)) @ ((X449)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 73.51/38.17 thf(c_0_22, plain, ![X486:$o, X487:$o, X488:$o, X489:$o, X490:$o]:(((((X486)|(X488)|~(c_and @ ((X486)) @ ((X487))))&(((X487)|(X488)|~(c_and @ ((X486)) @ ((X487))))&(~(X488)|(X488)|~(c_and @ ((X486)) @ ((X487))))))&((~(X489)|(~(X490)|(epred144_2 @ X489 @ X490))|(c_and @ ((X489)) @ ((X490))))&(~(epred144_2 @ X489 @ X490)|(c_and @ ((X489)) @ ((X490))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])])])])).
% 73.51/38.17 thf(c_0_23, negated_conjecture, ~((c_not @ (![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((X205 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ X206 @ X206) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ X206 @ X207))) @ X206)) @ X207) @ (X202 @ (X205 @ X83) @ X207)) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X205 @ (X202 @ X207 @ X206))) @ (X202 @ X83 @ X83)) @ (X202 @ X83 @ (X202 @ X207 @ X206))) @ X206))) @ X207))) @ X206)) @ X83) @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X83 @ X83) @ X83)) @ X206)))) @ (X205 @ (X205 @ X83))) @ X206))=(X205 @ (X205 @ X207))))))), inference(assume_negation,[status(cth)],[conj])).
% 73.51/38.17 thf(c_0_24, plain, ![X452:$i]:(((~(c_In @ X452 @ c_Empty)|(c_not @ $true))&((c_In @ esk1_0 @ c_Empty)|(c_not @ $false)))), 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])])])])])).
% 73.51/38.17 thf(c_0_25, plain, ((c_False)|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_18])])])).
% 73.51/38.17 thf(c_0_26, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_19])])])).
% 73.51/38.17 thf(c_0_27, plain, ![X244:$i, X245:$i]:(((c_Subq @ X244 @ X245)<=>![X9:$i]:(((c_In @ X9 @ X244)=>(c_In @ X9 @ X245))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 73.51/38.17 thf(c_0_28, plain, ![X6:$i, X2:$i]:(((c_In @ (esk2_2 @ X2 @ X6) @ X2)|(c_and @ (~($true)) @ (~($true)))|(c_In @ X6 @ (esk2_2 @ X2 @ X6))|(c_iff @ (($true)) @ (~($true)))|~((c_In @ X6 @ (c_Union @ X2))))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 73.51/38.17 thf(c_0_29, plain, ~((c_iff @ (($true)) @ (~($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_21])])])).
% 73.51/38.17 thf(c_0_30, plain, ![X5:$o]:(~((c_and @ ((X5)) @ (~($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_22])])])).
% 73.51/38.17 thf(c_0_31, negated_conjecture, ~(((~(![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((X205 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ X206 @ X206) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ X206 @ X207))) @ X206)) @ X207) @ (X202 @ (X205 @ X83) @ X207)) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X205 @ (X202 @ X207 @ X206))) @ (X202 @ X83 @ X83)) @ (X202 @ X83 @ (X202 @ X207 @ X206))) @ X206))) @ X207))) @ X206)) @ X83) @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X83 @ X83) @ X83)) @ X206)))) @ (X205 @ (X205 @ X83))) @ X206))=(X205 @ (X205 @ X207)))))|(c_not @ $true))&(![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((X205 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ X206 @ X206) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ X206 @ X207))) @ X206)) @ X207) @ (X202 @ (X205 @ X83) @ X207)) @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X205 @ (X202 @ X207 @ X206))) @ (X202 @ X83 @ X83)) @ (X202 @ X83 @ (X202 @ X207 @ X206))) @ X206))) @ X207))) @ X206)) @ X83) @ (X202 @ X83 @ (X202 @ X206 @ (X202 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X83 @ X83) @ X83)) @ X206)))) @ (X205 @ (X205 @ X83))) @ X206))=(X205 @ (X205 @ X207))))|(c_not @ $false)))), inference(fool_unroll,[status(thm)],[c_0_23])).
% 73.51/38.17 thf(c_0_32, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 73.51/38.17 thf(c_0_33, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_25, c_0_26])).
% 73.51/38.17 thf(c_0_34, plain, ![X500:$i, X501:$i, X502:$i, X503:$i, X504:$i]:(((~(c_Subq @ X500 @ X501)|(~(c_In @ X502 @ X500)|(c_In @ X502 @ X501)))&(((c_In @ (esk13_2 @ X503 @ X504) @ X503)|(c_Subq @ X503 @ X504))&(~(c_In @ (esk13_2 @ X503 @ X504) @ X504)|(c_Subq @ X503 @ X504))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])])])])])).
% 73.51/38.17 thf(c_0_35, plain, ![X6:$i, X2:$i]:(((c_In @ (esk2_2 @ X2 @ X6) @ X2)|(c_and @ (($true)) @ (~($true)))|(c_iff @ (($true)) @ (~($true)))|~((c_In @ X6 @ (esk2_2 @ X2 @ X6)))|~((c_In @ X6 @ (c_Union @ X2))))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 73.51/38.17 thf(c_0_36, plain, ![X6:$i, X2:$i]:(((c_In @ (esk2_2 @ X2 @ X6) @ X2)|(c_In @ X6 @ (esk2_2 @ X2 @ X6))|~((c_In @ X6 @ (c_Union @ X2))))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_28, c_0_29]), c_0_30])).
% 73.51/38.17 thf(c_0_37, negated_conjecture, ![X816:$i > $i > $i, X817:$i > $i, X818:$i, X819:$i, X820:$i]:((((((esk53_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk55_0 @ esk54_0) @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk55_0 @ esk54_0) @ (esk52_0 @ esk56_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk54_0 @ esk54_0) @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk54_0 @ (esk52_0 @ (esk52_0 @ esk55_0 @ (esk52_0 @ esk54_0 @ (esk52_0 @ esk54_0 @ esk56_0))) @ esk54_0)) @ esk56_0) @ (esk52_0 @ (esk53_0 @ esk55_0) @ esk56_0)) @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk54_0 @ (esk53_0 @ (esk52_0 @ esk56_0 @ esk54_0))) @ (esk52_0 @ esk55_0 @ esk55_0)) @ (esk52_0 @ esk55_0 @ (esk52_0 @ esk56_0 @ esk54_0))) @ esk54_0))) @ esk56_0))) @ esk54_0)) @ esk55_0) @ (esk52_0 @ esk55_0 @ (esk52_0 @ esk54_0 @ (esk52_0 @ (esk52_0 @ (esk53_0 @ esk54_0) @ (esk52_0 @ (esk52_0 @ esk55_0 @ esk55_0) @ esk55_0)) @ esk54_0)))) @ (esk53_0 @ (esk53_0 @ esk55_0))) @ esk54_0))!=(esk53_0 @ (esk53_0 @ esk56_0)))|((X817 @ (X816 @ (X816 @ (X816 @ (X816 @ (X816 @ (X816 @ X819 @ X818) @ (X816 @ (X816 @ (X816 @ X819 @ X818) @ (X816 @ X820 @ (X816 @ (X816 @ (X816 @ X818 @ X818) @ (X816 @ (X816 @ (X816 @ (X816 @ X818 @ (X816 @ (X816 @ X819 @ (X816 @ X818 @ (X816 @ X818 @ X820))) @ X818)) @ X820) @ (X816 @ (X817 @ X819) @ X820)) @ (X816 @ (X816 @ (X816 @ (X816 @ X818 @ (X817 @ (X816 @ X820 @ X818))) @ (X816 @ X819 @ X819)) @ (X816 @ X819 @ (X816 @ X820 @ X818))) @ X818))) @ X820))) @ X818)) @ X819) @ (X816 @ X819 @ (X816 @ X818 @ (X816 @ (X816 @ (X817 @ X818) @ (X816 @ (X816 @ X819 @ X819) @ X819)) @ X818)))) @ (X817 @ (X817 @ X819))) @ X818))=(X817 @ (X817 @ X820))))&(~(c_not @ $false)|((X817 @ (X816 @ (X816 @ (X816 @ (X816 @ (X816 @ (X816 @ X819 @ X818) @ (X816 @ (X816 @ (X816 @ X819 @ X818) @ (X816 @ X820 @ (X816 @ (X816 @ (X816 @ X818 @ X818) @ (X816 @ (X816 @ (X816 @ (X816 @ X818 @ (X816 @ (X816 @ X819 @ (X816 @ X818 @ (X816 @ X818 @ X820))) @ X818)) @ X820) @ (X816 @ (X817 @ X819) @ X820)) @ (X816 @ (X816 @ (X816 @ (X816 @ X818 @ (X817 @ (X816 @ X820 @ X818))) @ (X816 @ X819 @ X819)) @ (X816 @ X819 @ (X816 @ X820 @ X818))) @ X818))) @ X820))) @ X818)) @ X819) @ (X816 @ X819 @ (X816 @ X818 @ (X816 @ (X816 @ (X817 @ X818) @ (X816 @ (X816 @ X819 @ X819) @ X819)) @ X818)))) @ (X817 @ (X817 @ X819))) @ X818))=(X817 @ (X817 @ X820)))))&((((esk53_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk55_0 @ esk54_0) @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk55_0 @ esk54_0) @ (esk52_0 @ esk56_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk54_0 @ esk54_0) @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk54_0 @ (esk52_0 @ (esk52_0 @ esk55_0 @ (esk52_0 @ esk54_0 @ (esk52_0 @ esk54_0 @ esk56_0))) @ esk54_0)) @ esk56_0) @ (esk52_0 @ (esk53_0 @ esk55_0) @ esk56_0)) @ (esk52_0 @ (esk52_0 @ (esk52_0 @ (esk52_0 @ esk54_0 @ (esk53_0 @ (esk52_0 @ esk56_0 @ esk54_0))) @ (esk52_0 @ esk55_0 @ esk55_0)) @ (esk52_0 @ esk55_0 @ (esk52_0 @ esk56_0 @ esk54_0))) @ esk54_0))) @ esk56_0))) @ esk54_0)) @ esk55_0) @ (esk52_0 @ esk55_0 @ (esk52_0 @ esk54_0 @ (esk52_0 @ (esk52_0 @ (esk53_0 @ esk54_0) @ (esk52_0 @ (esk52_0 @ esk55_0 @ esk55_0) @ esk55_0)) @ esk54_0)))) @ (esk53_0 @ (esk53_0 @ esk55_0))) @ esk54_0))!=(esk53_0 @ (esk53_0 @ esk56_0)))|~(c_not @ $true))&(~(c_not @ $false)|~(c_not @ $true))))), 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)],[inference(fof_simplification,[status(thm)],[c_0_31])])])])])])])).
% 73.51/38.17 thf(c_0_38, plain, ![X450:$i, X451:$i]:((~(c_Subq @ X450 @ X451)|(~(c_Subq @ X451 @ X450)|((X450)=(X451))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax4])])])).
% 73.51/38.17 thf(c_0_39, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_32, c_0_33])).
% 73.51/38.17 thf(c_0_40, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_34])).
% 73.51/38.17 thf(c_0_41, plain, ![X6:$i, X2:$i]:(((c_In @ (esk2_2 @ X2 @ X6) @ X2)|~((c_In @ X6 @ (c_Union @ X2))))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_35, c_0_30]), c_0_29]), c_0_36])).
% 73.51/38.17 thf(c_0_42, negated_conjecture, ![X2:$i, X6:$i, X12:$i > $i, X89:$i > $i > $i, X7:$i]:((((X12 @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ X6) @ (X89 @ (X89 @ (X89 @ X2 @ X6) @ (X89 @ X7 @ (X89 @ (X89 @ (X89 @ X6 @ X6) @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X89 @ X2 @ (X89 @ X6 @ (X89 @ X6 @ X7))) @ X6)) @ X7) @ (X89 @ (X12 @ X2) @ X7)) @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X12 @ (X89 @ X7 @ X6))) @ (X89 @ X2 @ X2)) @ (X89 @ X2 @ (X89 @ X7 @ X6))) @ X6))) @ X7))) @ X6)) @ X2) @ (X89 @ X2 @ (X89 @ X6 @ (X89 @ (X89 @ (X12 @ X6) @ (X89 @ (X89 @ X2 @ X2) @ X2)) @ X6)))) @ (X12 @ (X12 @ X2))) @ X6))=(X12 @ (X12 @ X7)))|~((c_not @ (~($true)))))), inference(split_conjunct,[status(thm)],[c_0_37])).
% 73.51/38.17 thf(c_0_43, plain, (c_not @ (~($true))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_18])])])).
% 73.51/38.17 thf(c_0_44, plain, ![X1967:$i, X1968:$i]:(((esk222_1 @ X1968 @ X1967)=(X1968))), inference(variable_rename,[status(thm)],[])).
% 73.51/38.17 thf(c_0_45, plain, ![X6:$i, X2:$i]:((((X2)=(X6))|~((c_Subq @ X2 @ X6))|~((c_Subq @ X6 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_38])).
% 73.51/38.17 thf(c_0_46, plain, ![X2:$i]:((c_Subq @ c_Empty @ X2)), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 73.51/38.17 thf(c_0_47, plain, ![X2:$i]:(~((c_In @ X2 @ (c_Union @ c_Empty)))), inference(spm,[status(thm)],[c_0_39, c_0_41])).
% 73.51/38.17 thf(c_0_48, plain, ![X268:$i > $i > $o]:(((epred39_1 @ X268)<=>((~(c_irreflexive_i @ X268)|((~(c_transitive_i @ X268)|(c_and @ $true @ $true))&((c_transitive_i @ X268)|(c_and @ $true @ $false))))&((c_irreflexive_i @ X268)|((~(c_transitive_i @ X268)|(c_and @ $false @ $true))&((c_transitive_i @ X268)|(c_and @ $false @ $false))))))), introduced(definition)).
% 73.51/38.17 thf(c_0_49, plain, ![X2:$i, X8:$i]:(((epred1_2 @ X8 @ X2)=>~(?[X9:$i]:(((~(c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $true @ $true))&((c_In @ X9 @ X8)|(c_and @ $true @ $false))))&((c_In @ X2 @ X9)|((~(c_In @ X9 @ X8)|(c_and @ $false @ $true))&((c_In @ X9 @ X8)|(c_and @ $false @ $false))))))))), inference(split_equiv,[status(thm)],[c_0_13])).
% 73.51/38.17 thf(c_0_50, negated_conjecture, ![X2:$i, X6:$i, X12:$i > $i, X89:$i > $i > $i, X7:$i]:(((X12 @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ X6) @ (X89 @ (X89 @ (X89 @ X2 @ X6) @ (X89 @ X7 @ (X89 @ (X89 @ (X89 @ X6 @ X6) @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X89 @ X2 @ (X89 @ X6 @ (X89 @ X6 @ X7))) @ X6)) @ X7) @ (X89 @ (X12 @ X2) @ X7)) @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X12 @ (X89 @ X7 @ X6))) @ (X89 @ X2 @ X2)) @ (X89 @ X2 @ (X89 @ X7 @ X6))) @ X6))) @ X7))) @ X6)) @ X2) @ (X89 @ X2 @ (X89 @ X6 @ (X89 @ (X89 @ (X12 @ X6) @ (X89 @ (X89 @ X2 @ X2) @ X2)) @ X6)))) @ (X12 @ (X12 @ X2))) @ X6))=(X12 @ (X12 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 73.51/38.17 thf(c_0_51, plain, ![X6:$i, X2:$i]:(((esk222_1 @ X2 @ X6)=(X2))), inference(split_conjunct,[status(thm)],[c_0_44])).
% 73.51/38.17 thf(c_0_52, plain, ![X2:$i]:((((X2)=(c_Empty))|~((c_Subq @ X2 @ c_Empty)))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 73.51/38.17 thf(c_0_53, plain, ![X2:$i]:((c_Subq @ (c_Union @ c_Empty) @ X2)), inference(spm,[status(thm)],[c_0_47, c_0_40])).
% 73.51/38.17 thf(c_0_54, plain, ![X935:$i > $i > $o]:(((((~(c_transitive_i @ X935)|(c_and @ $true @ $true)|~(c_irreflexive_i @ X935)|~(epred39_1 @ X935))&((c_transitive_i @ X935)|(c_and @ $true @ $false)|~(c_irreflexive_i @ X935)|~(epred39_1 @ X935)))&((~(c_transitive_i @ X935)|(c_and @ $false @ $true)|(c_irreflexive_i @ X935)|~(epred39_1 @ X935))&((c_transitive_i @ X935)|(c_and @ $false @ $false)|(c_irreflexive_i @ X935)|~(epred39_1 @ X935))))&(((~(c_irreflexive_i @ X935)|(c_irreflexive_i @ X935)|(epred39_1 @ X935))&(((~(c_transitive_i @ X935)|(c_transitive_i @ X935)|(c_irreflexive_i @ X935)|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|(c_transitive_i @ X935)|(c_irreflexive_i @ X935)|(epred39_1 @ X935)))&((~(c_transitive_i @ X935)|~(c_and @ $false @ $true)|(c_irreflexive_i @ X935)|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(c_irreflexive_i @ X935)|(epred39_1 @ X935)))))&((((~(c_irreflexive_i @ X935)|(~(c_transitive_i @ X935)|(c_transitive_i @ X935))|(epred39_1 @ X935))&(((~(c_transitive_i @ X935)|(c_transitive_i @ X935)|(~(c_transitive_i @ X935)|(c_transitive_i @ X935))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|(c_transitive_i @ X935)|(~(c_transitive_i @ X935)|(c_transitive_i @ X935))|(epred39_1 @ X935)))&((~(c_transitive_i @ X935)|~(c_and @ $false @ $true)|(~(c_transitive_i @ X935)|(c_transitive_i @ X935))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_transitive_i @ X935)|(c_transitive_i @ X935))|(epred39_1 @ X935)))))&((~(c_irreflexive_i @ X935)|(~(c_and @ $true @ $false)|(c_transitive_i @ X935))|(epred39_1 @ X935))&(((~(c_transitive_i @ X935)|(c_transitive_i @ X935)|(~(c_and @ $true @ $false)|(c_transitive_i @ X935))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|(c_transitive_i @ X935)|(~(c_and @ $true @ $false)|(c_transitive_i @ X935))|(epred39_1 @ X935)))&((~(c_transitive_i @ X935)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(c_transitive_i @ X935))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(c_transitive_i @ X935))|(epred39_1 @ X935))))))&(((~(c_irreflexive_i @ X935)|(~(c_transitive_i @ X935)|~(c_and @ $true @ $true))|(epred39_1 @ X935))&(((~(c_transitive_i @ X935)|(c_transitive_i @ X935)|(~(c_transitive_i @ X935)|~(c_and @ $true @ $true))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|(c_transitive_i @ X935)|(~(c_transitive_i @ X935)|~(c_and @ $true @ $true))|(epred39_1 @ X935)))&((~(c_transitive_i @ X935)|~(c_and @ $false @ $true)|(~(c_transitive_i @ X935)|~(c_and @ $true @ $true))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_transitive_i @ X935)|~(c_and @ $true @ $true))|(epred39_1 @ X935)))))&((~(c_irreflexive_i @ X935)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred39_1 @ X935))&(((~(c_transitive_i @ X935)|(c_transitive_i @ X935)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|(c_transitive_i @ X935)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred39_1 @ X935)))&((~(c_transitive_i @ X935)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred39_1 @ X935))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred39_1 @ X935)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_48])])])])).
% 73.51/38.17 thf(c_0_55, plain, ![X826:$i, X827:$i, X828:$i]:((((~(c_In @ X826 @ X828)|(c_In @ X826 @ X828)|~(epred1_2 @ X827 @ X826))&(((~(c_In @ X828 @ X827)|(c_In @ X828 @ X827)|(c_In @ X826 @ X828)|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|(c_In @ X828 @ X827)|(c_In @ X826 @ X828)|~(epred1_2 @ X827 @ X826)))&((~(c_In @ X828 @ X827)|~(c_and @ $false @ $true)|(c_In @ X826 @ X828)|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(c_In @ X826 @ X828)|~(epred1_2 @ X827 @ X826)))))&((((~(c_In @ X826 @ X828)|(~(c_In @ X828 @ X827)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))&(((~(c_In @ X828 @ X827)|(c_In @ X828 @ X827)|(~(c_In @ X828 @ X827)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|(c_In @ X828 @ X827)|(~(c_In @ X828 @ X827)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826)))&((~(c_In @ X828 @ X827)|~(c_and @ $false @ $true)|(~(c_In @ X828 @ X827)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_In @ X828 @ X827)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826)))))&((~(c_In @ X826 @ X828)|(~(c_and @ $true @ $false)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))&(((~(c_In @ X828 @ X827)|(c_In @ X828 @ X827)|(~(c_and @ $true @ $false)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|(c_In @ X828 @ X827)|(~(c_and @ $true @ $false)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826)))&((~(c_In @ X828 @ X827)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(c_In @ X828 @ X827))|~(epred1_2 @ X827 @ X826))))))&(((~(c_In @ X826 @ X828)|(~(c_In @ X828 @ X827)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))&(((~(c_In @ X828 @ X827)|(c_In @ X828 @ X827)|(~(c_In @ X828 @ X827)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|(c_In @ X828 @ X827)|(~(c_In @ X828 @ X827)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826)))&((~(c_In @ X828 @ X827)|~(c_and @ $false @ $true)|(~(c_In @ X828 @ X827)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_In @ X828 @ X827)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826)))))&((~(c_In @ X826 @ X828)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))&(((~(c_In @ X828 @ X827)|(c_In @ X828 @ X827)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|(c_In @ X828 @ X827)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826)))&((~(c_In @ X828 @ X827)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|~(epred1_2 @ X827 @ X826))))))))), 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_49])])])])])).
% 73.51/38.17 thf(c_0_56, plain, ![X3:$o, X4:$o]:(((c_and @ ((X3)) @ ((X4)))|~((epred144_2 @ ((X3)) @ ((X4)))))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 73.51/38.17 thf(c_0_57, plain, ((epred144_2 @ (($true)) @ (($true)))|(c_and @ (($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_22])])])).
% 73.51/38.17 thf(c_0_58, plain, ![X6:$i, X2:$i]:(((epred1_2 @ X2 @ X6)|(c_iff @ (~($true)) @ (($true)))|(c_In @ X6 @ (c_Union @ X2)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 73.51/38.17 thf(c_0_59, plain, ~((c_iff @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_21])])])).
% 73.51/38.17 thf(c_0_60, plain, ![X2:$i, X12:$i > $i, X6:$i]:(((X12 @ X2)=(X12 @ (X12 @ X6)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51]), c_0_51])).
% 73.51/38.17 thf(c_0_61, plain, ((c_Union @ c_Empty)=(c_Empty)), inference(spm,[status(thm)],[c_0_52, c_0_53])).
% 73.51/38.17 thf(c_0_62, plain, ![X258:$i > $i > $o]:(((c_irreflexive_i @ X258)<=>![X2:$i]:(((~(X258 @ X2 @ X2)|(c_not @ $true))&((X258 @ X2 @ X2)|(c_not @ $false)))))), inference(fool_unroll,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax30])])])).
% 73.51/38.17 thf(c_0_63, plain, ![X37:$i > $i > $o]:(((c_transitive_i @ X37)|(c_and @ (~($true)) @ (~($true)))|(c_irreflexive_i @ X37)|~((epred39_1 @ X37)))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 73.51/38.17 thf(c_0_64, plain, ![X7:$i, X6:$i, X2:$i]:((~((c_In @ X2 @ X6))|~((c_In @ X6 @ X7))|~((c_and @ (($true)) @ (($true))))|~((epred1_2 @ X7 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 73.51/38.17 thf(c_0_65, plain, (c_and @ (($true)) @ (($true))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 73.51/38.17 thf(c_0_66, plain, ![X6:$i, X2:$i]:(((c_In @ X2 @ (c_Union @ X6))|(epred1_2 @ X6 @ X2))), inference(sr,[status(thm)],[c_0_58, c_0_59])).
% 73.51/38.17 thf(c_0_67, plain, ![X2:$i]:(((c_Union @ X2)=(c_Empty))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_61])).
% 73.51/38.17 thf(c_0_68, plain, ![X527:$i > $i > $o, X528:$i, X529:$i, X530:$i > $i > $o]:((((~(X527 @ X528 @ X528)|(c_not @ $true)|~(c_irreflexive_i @ X527))&((X527 @ X529 @ X529)|(c_not @ $false)|~(c_irreflexive_i @ X527)))&(((~(X530 @ (esk18_1 @ X530) @ (esk18_1 @ X530))|(X530 @ (esk17_1 @ X530) @ (esk17_1 @ X530))|(c_irreflexive_i @ X530))&(~(c_not @ $false)|(X530 @ (esk17_1 @ X530) @ (esk17_1 @ X530))|(c_irreflexive_i @ X530)))&((~(X530 @ (esk18_1 @ X530) @ (esk18_1 @ X530))|~(c_not @ $true)|(c_irreflexive_i @ X530))&(~(c_not @ $false)|~(c_not @ $true)|(c_irreflexive_i @ X530)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_62])])])])])])])).
% 73.51/38.17 thf(c_0_69, plain, ![X261:$i > $i > $o]:(((c_transitive_i @ X261)<=>![X2:$i, X9:$i, X13:$i]:(((X261 @ X2 @ X9)=>((X261 @ X9 @ X13)=>(X261 @ X2 @ X13)))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax33])])).
% 73.51/38.17 thf(c_0_70, plain, ![X37:$i > $i > $o]:(((c_transitive_i @ X37)|(c_and @ (($true)) @ (~($true)))|~((c_irreflexive_i @ X37))|~((epred39_1 @ X37)))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 73.51/38.17 thf(c_0_71, plain, ![X37:$i > $i > $o]:(((c_transitive_i @ X37)|(c_irreflexive_i @ X37)|~((epred39_1 @ X37)))), inference(sr,[status(thm)],[c_0_63, c_0_30])).
% 73.51/38.17 thf(c_0_72, axiom, ![X10:$i, X2:$i]:(((~(c_In @ X2 @ (c_Power @ X10))|((~(c_Subq @ X2 @ X10)|(c_iff @ $true @ $true))&((c_Subq @ X2 @ X10)|(c_iff @ $true @ $false))))&((c_In @ X2 @ (c_Power @ X10))|((~(c_Subq @ X2 @ X10)|(c_iff @ $false @ $true))&((c_Subq @ X2 @ X10)|(c_iff @ $false @ $false)))))), inference(fool_unroll,[status(thm)],[ax7])).
% 73.51/38.17 thf(c_0_73, plain, ![X2:$i, X6:$i, X7:$i]:((~((c_In @ X2 @ X6))|~((c_In @ X7 @ X2))|~((epred1_2 @ X6 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 73.51/38.17 thf(c_0_74, plain, ![X2:$i, X6:$i]:((epred1_2 @ X2 @ X6)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67]), c_0_39])).
% 73.51/38.17 thf(c_0_75, plain, ![X37:$i > $i > $o]:(((X37 @ (esk17_1 @ X37) @ (esk17_1 @ X37))|(c_irreflexive_i @ X37)|~((c_not @ (~($true)))))), inference(split_conjunct,[status(thm)],[c_0_68])).
% 73.51/38.17 thf(c_0_76, plain, ![X545:$i > $i > $o, X546:$i, X547:$i, X548:$i, X549:$i > $i > $o]:(((~(c_transitive_i @ X545)|(~(X545 @ X546 @ X547)|(~(X545 @ X547 @ X548)|(X545 @ X546 @ X548))))&(((X549 @ (esk23_1 @ X549) @ (esk24_1 @ X549))|(c_transitive_i @ X549))&(((X549 @ (esk24_1 @ X549) @ (esk25_1 @ X549))|(c_transitive_i @ X549))&(~(X549 @ (esk23_1 @ X549) @ (esk25_1 @ X549))|(c_transitive_i @ X549)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_69])])])])])])])).
% 73.51/38.17 thf(c_0_77, plain, ![X2:$i, X37:$i > $i > $o]:(((c_not @ (($true)))|~((X37 @ X2 @ X2))|~((c_irreflexive_i @ X37)))), inference(split_conjunct,[status(thm)],[c_0_68])).
% 73.51/38.17 thf(c_0_78, plain, ![X37:$i > $i > $o]:(((c_and @ (~($true)) @ (($true)))|(c_irreflexive_i @ X37)|~((c_transitive_i @ X37))|~((epred39_1 @ X37)))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 73.51/38.17 thf(c_0_79, plain, ![X5:$o]:(~((c_and @ (~($true)) @ ((X5))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_22])])])).
% 73.51/38.17 thf(c_0_80, plain, ![X37:$i > $i > $o]:(((c_transitive_i @ X37)|~((epred39_1 @ X37)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_70, c_0_30]), c_0_71])).
% 73.51/38.17 thf(c_0_81, plain, ![X460:$i, X461:$i]:((((~(c_Subq @ X461 @ X460)|(c_iff @ $true @ $true)|~(c_In @ X461 @ (c_Power @ X460)))&((c_Subq @ X461 @ X460)|(c_iff @ $true @ $false)|~(c_In @ X461 @ (c_Power @ X460))))&((~(c_Subq @ X461 @ X460)|(c_iff @ $false @ $true)|(c_In @ X461 @ (c_Power @ X460)))&((c_Subq @ X461 @ X460)|(c_iff @ $false @ $false)|(c_In @ X461 @ (c_Power @ X460)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_72])])])).
% 73.51/38.17 thf(c_0_82, plain, ![X7:$i, X6:$i, X2:$i]:((~((c_In @ X2 @ X6))|~((c_In @ X7 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 73.51/38.17 thf(c_0_83, plain, ![X37:$i > $i > $o]:(((X37 @ (esk17_1 @ X37) @ (esk17_1 @ X37))|(c_irreflexive_i @ X37))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_75, c_0_43])])).
% 73.51/38.17 thf(c_0_84, plain, ![X37:$i > $i > $o]:(((X37 @ (esk24_1 @ X37) @ (esk25_1 @ X37))|(c_transitive_i @ X37))), inference(split_conjunct,[status(thm)],[c_0_76])).
% 73.51/38.17 thf(c_0_85, plain, ![X2022:$i, X2023:$i > $o]:((((~(X2023 @ X2022)|(c_not @ $true)|~(epred161_1 @ X2023 @ X2022))&((X2023 @ X2022)|(c_not @ $false)|~(epred161_1 @ X2023 @ X2022)))&(((~(X2023 @ X2022)|(X2023 @ X2022)|(epred161_1 @ X2023 @ X2022))&(~(c_not @ $false)|(X2023 @ X2022)|(epred161_1 @ X2023 @ X2022)))&((~(X2023 @ X2022)|~(c_not @ $true)|(epred161_1 @ X2023 @ X2022))&(~(c_not @ $false)|~(c_not @ $true)|(epred161_1 @ X2023 @ X2022)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fool_unroll,[status(thm)],[])])])])])).
% 73.51/38.17 thf(c_0_86, plain, ![X37:$i > $i > $o, X2:$i]:((~((c_irreflexive_i @ X37))|~((X37 @ X2 @ X2)))), inference(sr,[status(thm)],[c_0_77, c_0_33])).
% 73.51/38.17 thf(c_0_87, plain, ![X37:$i > $i > $o]:(((c_irreflexive_i @ X37)|~((epred39_1 @ X37)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_78, c_0_79]), c_0_80])).
% 73.51/38.17 thf(c_0_88, plain, ![X2:$i, X6:$i]:(((c_iff @ (~($true)) @ (($true)))|(c_In @ X2 @ (c_Power @ X6))|~((c_Subq @ X2 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_81])).
% 73.51/38.17 thf(c_0_89, plain, ![X37:$i > $i > $o]:(((epred39_1 @ X37)|~((c_irreflexive_i @ X37))|~((c_transitive_i @ X37))|~((c_and @ (($true)) @ (($true)))))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 73.51/38.17 thf(c_0_90, plain, ![X2:$i]:(((c_irreflexive_i @ c_In)|~((c_In @ X2 @ (esk17_1 @ c_In))))), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 73.51/38.17 thf(c_0_91, plain, ![X2:$i]:(((c_transitive_i @ c_In)|~((c_In @ X2 @ (esk24_1 @ c_In))))), inference(spm,[status(thm)],[c_0_82, c_0_84])).
% 73.51/38.17 thf(c_0_92, plain, ![X37:$i > $i > $o]:(((X37 @ (esk23_1 @ X37) @ (esk24_1 @ X37))|(c_transitive_i @ X37))), inference(split_conjunct,[status(thm)],[c_0_76])).
% 73.51/38.17 thf(c_0_93, plain, ![X2009:$i, X2010:$i > $i]:(((esk217_0 @ X2010 @ X2009)=(c_Power @ (X2010 @ X2009)))), inference(variable_rename,[status(thm)],[])).
% 73.51/38.17 thf(c_0_94, plain, ![X479:$i > $o, X481:$i, X482:$i]:(((~(c_In @ X481 @ (esk12_1 @ X479))|(X479 @ X481)|(X479 @ X482))&(~(X479 @ (esk12_1 @ X479))|(X479 @ X482)))), 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)],[ax10])])])])])])).
% 73.51/38.17 thf(c_0_95, plain, ![X1:$i > $o, X2:$i]:(((X1 @ X2)|(epred161_1 @ X1 @ X2)|~((c_not @ (~($true)))))), inference(split_conjunct,[status(thm)],[c_0_85])).
% 73.51/38.17 thf(c_0_96, plain, ![X2:$i, X37:$i > $i > $o]:((~((X37 @ X2 @ X2))|~((epred39_1 @ X37)))), inference(spm,[status(thm)],[c_0_86, c_0_87])).
% 73.51/38.17 thf(c_0_97, plain, ![X2:$i, X6:$i]:(((c_In @ X2 @ (c_Power @ X6))|~((c_Subq @ X2 @ X6)))), inference(sr,[status(thm)],[c_0_88, c_0_59])).
% 73.51/38.17 thf(c_0_98, plain, ![X37:$i > $i > $o]:(((epred39_1 @ X37)|~((c_irreflexive_i @ X37))|~((c_transitive_i @ X37)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_89, c_0_65])])).
% 73.51/38.17 thf(c_0_99, plain, (c_irreflexive_i @ c_In), inference(spm,[status(thm)],[c_0_90, c_0_83])).
% 73.51/38.17 thf(c_0_100, plain, (c_transitive_i @ c_In), inference(spm,[status(thm)],[c_0_91, c_0_92])).
% 73.51/38.17 thf(c_0_101, plain, ![X12:$i > $i, X2:$i]:(((esk217_0 @ X12 @ X2)=(c_Power @ (X12 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_93])).
% 73.51/38.17 thf(c_0_102, plain, ![X1:$i > $o, X2:$i]:(((c_not @ (($true)))|~((X1 @ X2))|~((epred161_1 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_85])).
% 73.51/38.17 thf(c_0_103, plain, ![X2:$i, X1:$i > $o]:(((X1 @ X2)|~((X1 @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_94])).
% 73.51/38.17 thf(c_0_104, plain, ![X1:$i > $o, X2:$i]:(((epred161_1 @ X1 @ X2)|(X1 @ X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_43])])).
% 73.51/38.17 thf(c_0_105, plain, ![X2:$i]:((~((c_Subq @ (c_Power @ X2) @ X2))|~((epred39_1 @ c_In)))), inference(spm,[status(thm)],[c_0_96, c_0_97])).
% 73.51/38.17 thf(c_0_106, plain, (epred39_1 @ c_In), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_99]), c_0_100])])).
% 73.51/38.17 thf(c_0_107, plain, ![X2:$i, X6:$i]:(((c_Power @ X2)=(esk217_0 @ c_Power @ X6))), inference(spm,[status(thm)],[c_0_101, c_0_60])).
% 73.51/38.17 thf(c_0_108, plain, ![X1:$i > $o, X2:$i]:((~((epred161_1 @ X1 @ X2))|~((X1 @ X2)))), inference(sr,[status(thm)],[c_0_102, c_0_33])).
% 73.51/38.17 thf(c_0_109, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (esk12_1 @ (epred161_1 @ X1)))|(epred161_1 @ X1 @ X2))), inference(spm,[status(thm)],[c_0_103, c_0_104])).
% 73.51/38.17 thf(c_0_110, plain, ![X2:$i, X6:$i]:(((c_Subq @ X2 @ X6)|~((c_In @ (esk13_2 @ X2 @ X6) @ X6)))), inference(split_conjunct,[status(thm)],[c_0_34])).
% 73.51/38.17 thf(c_0_111, plain, ![X2:$i]:(~((c_Subq @ (c_Power @ X2) @ X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_105, c_0_106])])).
% 73.51/38.17 thf(c_0_112, plain, ![X2:$i, X6:$i]:(((c_Power @ X2)=(c_Power @ X6))), inference(spm,[status(thm)],[c_0_107, c_0_107])).
% 73.51/38.17 thf(c_0_113, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (esk12_1 @ (epred161_1 @ X1)))|~((X1 @ X2)))), inference(spm,[status(thm)],[c_0_108, c_0_109])).
% 73.51/38.17 thf(c_0_114, plain, ![X2:$i]:((c_Subq @ X2 @ X2)), inference(spm,[status(thm)],[c_0_110, c_0_40])).
% 73.51/38.17 thf(c_0_115, plain, ![X2:$i, X6:$i]:(~((c_Subq @ (c_Power @ X2) @ X6))), inference(spm,[status(thm)],[c_0_111, c_0_112])).
% 73.51/38.17 thf(c_0_116, plain, ![X2:$i]:((c_Subq @ X2 @ (esk12_1 @ (epred161_1 @ (c_Subq @ X2))))), inference(spm,[status(thm)],[c_0_113, c_0_114])).
% 73.51/38.17 thf(c_0_117, plain, ($false), inference(spm,[status(thm)],[c_0_115, c_0_116]), ['proof']).
% 73.51/38.17 % SZS output end CNFRefutation
% 73.51/38.17 % Parsed axioms : 213
% 73.51/38.17 % Removed by relevancy pruning/SinE : 0
% 73.51/38.17 % Initial clauses : 468687
% 73.51/38.17 % Removed in clause preprocessing : 463862
% 73.51/38.17 % Initial clauses in saturation : 4825
% 73.51/38.17 % Processed clauses : 48728
% 73.51/38.17 % ...of these trivial : 1126
% 73.51/38.17 % ...subsumed : 42032
% 73.51/38.17 % ...remaining for further processing : 5570
% 73.51/38.17 % Other redundant clauses eliminated : 83
% 73.51/38.17 % Clauses deleted for lack of memory : 0
% 73.51/38.17 % Backward-subsumed : 411
% 73.51/38.17 % Backward-rewritten : 340
% 73.51/38.17 % Generated clauses : 163954
% 73.51/38.17 % ...of the previous two non-redundant : 159520
% 73.51/38.17 % ...aggressively subsumed : 0
% 73.51/38.17 % Contextual simplify-reflections : 172
% 73.51/38.17 % Paramodulations : 163866
% 73.51/38.17 % Factorizations : 0
% 73.51/38.17 % NegExts : 0
% 73.51/38.17 % Equation resolutions : 83
% 73.51/38.17 % Disequality decompositions : 0
% 73.51/38.17 % Total rewrite steps : 22437
% 73.51/38.17 % ...of those cached : 20152
% 73.51/38.17 % Propositional unsat checks : 0
% 73.51/38.17 % Propositional check models : 0
% 73.51/38.17 % Propositional check unsatisfiable : 0
% 73.51/38.17 % Propositional clauses : 0
% 73.51/38.17 % Propositional clauses after purity: 0
% 73.51/38.17 % Propositional unsat core size : 0
% 73.51/38.17 % Propositional preprocessing time : 0.000
% 73.51/38.17 % Propositional encoding time : 0.000
% 73.51/38.17 % Propositional solver time : 0.000
% 73.51/38.17 % Success case prop preproc time : 0.000
% 73.51/38.17 % Success case prop encoding time : 0.000
% 73.51/38.17 % Success case prop solver time : 0.000
% 73.51/38.17 % Current number of processed clauses : 4789
% 73.51/38.17 % Positive orientable unit clauses : 370
% 73.51/38.17 % Positive unorientable unit clauses: 6
% 73.51/38.17 % Negative unit clauses : 177
% 73.51/38.17 % Non-unit-clauses : 4236
% 73.51/38.17 % Current number of unprocessed clauses: 114617
% 73.51/38.17 % ...number of literals in the above : 431507
% 73.51/38.17 % Current number of archived formulas : 0
% 73.51/38.17 % Current number of archived clauses : 751
% 73.51/38.17 % Clause-clause subsumption calls (NU) : 21954746
% 73.51/38.17 % Rec. Clause-clause subsumption calls : 9855639
% 73.51/38.17 % Non-unit clause-clause subsumptions : 39881
% 73.51/38.17 % Unit Clause-clause subsumption calls : 783648
% 73.51/38.17 % Rewrite failures with RHS unbound : 929
% 73.51/38.17 % BW rewrite match attempts : 10707
% 73.51/38.17 % BW rewrite match successes : 517
% 73.51/38.17 % Condensation attempts : 0
% 73.51/38.17 % Condensation successes : 0
% 73.51/38.17 % Termbank termtop insertions : 22415008
% 73.51/38.17 % Search garbage collected termcells : 2011263
% 73.51/38.17
% 73.51/38.17 % -------------------------------------------------
% 73.51/38.17 % User time : 34.395 s
% 73.51/38.17 % System time : 1.977 s
% 73.51/38.17 % Total time : 36.372 s
% 73.51/38.17 % Maximum resident set size: 1255864 pages
% 73.51/38.17
% 73.51/38.17 % -------------------------------------------------
% 73.51/38.17 % User time : 34.402 s
% 73.51/38.17 % System time : 2.182 s
% 73.51/38.17 % Total time : 36.584 s
% 73.51/38.17 % Maximum resident set size: 4864 pages
% 73.51/38.17 % E exiting
%------------------------------------------------------------------------------