%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO879^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : 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:43:29 AM UTC 2026
% Result : Theorem 91.70s 46.89s
% Output : CNFRefutation 91.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO879^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 % Computer : n002.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Tue Sep 29 17:25:07 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.28 Running higher-order theorem proving
% 0.23/0.31 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p
% 91.70/46.89 % Version: 3.5.1-ho
% 91.70/46.89 % partial match(1): HSLMSMSSSSLCHSA
% 91.70/46.89 % Preprocessing class: HSLMSLSSSSLCHSA.
% 91.70/46.89 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 91.70/46.89 % Starting pre_casc_6 with 1500s (5) cores
% 91.70/46.89 % Starting ehoh_best7 with 300s (1) cores
% 91.70/46.89 % Starting new_bool_8 with 300s (1) cores
% 91.70/46.89 % Starting new_ho_11 with 300s (1) cores
% 91.70/46.89 % new_bool_8 with pid 1596530 completed with status 9
% 91.70/46.89 % new_ho_11 with pid 1596531 completed with status 0
% 91.70/46.89 % Result found by new_ho_11
% 91.70/46.89 % partial match(1): HSLMSMSSSSLCHSA
% 91.70/46.89 % Preprocessing class: HSLMSLSSSSLCHSA.
% 91.70/46.89 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 91.70/46.89 % Starting pre_casc_6 with 1500s (5) cores
% 91.70/46.89 % Starting ehoh_best7 with 300s (1) cores
% 91.70/46.89 % Starting new_bool_8 with 300s (1) cores
% 91.70/46.89 % Starting new_ho_11 with 300s (1) cores
% 91.70/46.89 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 91.70/46.89 % No SInE strategy applied
% 91.70/46.89 % Search class: HGHSM-SMLM33-DHSFFSBC
% 91.70/46.89 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 91.70/46.89 % Scheduled 7 strats onto 1 cores with 284 seconds (284 total)
% 91.70/46.89 % Starting SubtermCWHack with 26s (1) cores
% 91.70/46.89 % SubtermCWHack with pid 1596612 completed with status 8
% 91.70/46.89 % Starting new_ho_11 with 29s (1) cores
% 91.70/46.89 % new_ho_11 with pid 1596829 completed with status 0
% 91.70/46.89 % Result found by new_ho_11
% 91.70/46.89 % partial match(1): HSLMSMSSSSLCHSA
% 91.70/46.89 % Preprocessing class: HSLMSLSSSSLCHSA.
% 91.70/46.89 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 91.70/46.89 % Starting pre_casc_6 with 1500s (5) cores
% 91.70/46.89 % Starting ehoh_best7 with 300s (1) cores
% 91.70/46.89 % Starting new_bool_8 with 300s (1) cores
% 91.70/46.89 % Starting new_ho_11 with 300s (1) cores
% 91.70/46.89 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 91.70/46.89 % No SInE strategy applied
% 91.70/46.89 % Search class: HGHSM-SMLM33-DHSFFSBC
% 91.70/46.89 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 91.70/46.89 % Scheduled 7 strats onto 1 cores with 284 seconds (284 total)
% 91.70/46.89 % Starting SubtermCWHack with 26s (1) cores
% 91.70/46.89 % SubtermCWHack with pid 1596612 completed with status 8
% 91.70/46.89 % Starting new_ho_11 with 29s (1) cores
% 91.70/46.89 % Preprocessing time : 0.159 s
% 91.70/46.89 % Presaturation interreduction done
% 91.70/46.89
% 91.70/46.89 % Proof found!
% 91.70/46.89 % SZS status Theorem
% 91.70/46.89 % SZS output start CNFRefutation
% 91.70/46.89 thf(decl_24, type, c_False: $o).
% 91.70/46.89 thf(decl_26, type, c_not: $o > $o).
% 91.70/46.89 thf(decl_27, type, c_and: $o > $o > $o).
% 91.70/46.89 thf(decl_29, type, c_iff: $o > $o > $o).
% 91.70/46.89 thf(decl_30, type, c_In: $i > $i > $o).
% 91.70/46.89 thf(decl_31, type, c_Subq: $i > $i > $o).
% 91.70/46.89 thf(decl_32, type, c_Empty: $i).
% 91.70/46.89 thf(decl_34, type, c_Power: $i > $i).
% 91.70/46.89 thf(decl_80, type, c_ordsucc: $i > $i).
% 91.70/46.89 thf(decl_97, type, c_ap: $i > $i > $i).
% 91.70/46.89 thf(decl_254, type, epred128_10: $i > ($i > $i > $i > $i) > ($i > $i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i) > $i > $i > $i > $i > $o).
% 91.70/46.89 thf(decl_270, type, epred144_8: $i > $i > $i > $i > ($i > $o) > ($i > $i) > ($i > $i > $i) > ($i > $o) > $o).
% 91.70/46.89 thf(decl_271, type, epred145_7: $i > $i > $i > $i > ($i > $o) > $i > ($i > $o) > $o).
% 91.70/46.89 thf(decl_272, type, epred146_8: $i > $i > $i > $i > ($i > $o) > ($i > $i) > ($i > $i > $i) > ($i > $o) > $o).
% 91.70/46.89 thf(decl_273, type, esk1_0: $i).
% 91.70/46.89 thf(decl_286, type, epred148_2: $o > $o > $o).
% 91.70/46.89 thf(decl_288, type, esk13_2: $i > $i > $i).
% 91.70/46.89 thf(decl_331, type, esk52_0: $i > $i > $i).
% 91.70/46.89 thf(decl_332, type, epred154_0: $i > $o).
% 91.70/46.89 thf(decl_333, type, epred155_0: $i > $o).
% 91.70/46.89 thf(decl_334, type, esk53_0: $i > $i).
% 91.70/46.89 thf(decl_335, type, esk54_0: $i).
% 91.70/46.89 thf(decl_336, type, esk55_0: $i).
% 91.70/46.89 thf(decl_337, type, esk56_0: $i).
% 91.70/46.89 thf(decl_338, type, esk57_0: $i).
% 91.70/46.89 thf(decl_339, type, esk58_0: $i).
% 91.70/46.89 thf(decl_497, type, esk214_8: ($i > $i > $i) > ($i > $o) > ($i > $o) > ($i > $i) > $i > $i > $i > $i > $i).
% 91.70/46.89 thf(decl_498, type, esk215_8: ($i > $i > $i) > ($i > $o) > ($i > $o) > ($i > $i) > $i > $i > $i > $i > $i).
% 91.70/46.89 thf(decl_506, type, esk219_0: $i > $i > $i).
% 91.70/46.89 thf(decl_519, type, epred166_1: ($i > $i > $o) > $i > $o).
% 91.70/46.89 thf(ax2, axiom, ![X3:$o]:(((c_not @ ((c_not @ ((X3)))))=>(X3))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax2)).
% 91.70/46.89 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax13)).
% 91.70/46.89 thf(ax14, axiom, ((c_and)=(^[X18:$o, X19:$o]:(![X20:$o]:((((((X18))=>((((X19))=>((X20))))))=>((X20))))))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax14)).
% 91.70/46.89 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, X208:$i, X209:$i]:((((c_and @ (![X210:$i]:(((((X205 @ X209)=(X210)))=>((((c_and @ ((X203 @ X210)) @ (((((X207)=(X206)))=>((c_and @ (![X211:$i]:(((X209)=(X208)))) @ (?[X212:$i]:((X204 @ X210)))))))))=>(?[X213:$i]:(((X207)=(X207))))))))) @ ((c_not @ ((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206)))))))))=>(((X83)=(X209))))))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', conj)).
% 91.70/46.89 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax5)).
% 91.70/46.89 thf(ax7, axiom, ![X10:$i, X2:$i]:((c_iff @ ((c_In @ X2 @ (c_Power @ X10))) @ ((c_Subq @ X2 @ X10)))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax7)).
% 91.70/46.89 thf(ax17, axiom, ((c_Subq)=(^[X26:$i, X2:$i]:(![X9:$i]:((((c_In @ X9 @ X26))=>((c_In @ X9 @ X2))))))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax17)).
% 91.70/46.89 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox2/tmp/tmp.LDNFiBt0UO/E---3.1_1596515.p', ax3)).
% 91.70/46.89 thf(c_0_8, axiom, ![X3:$o]:((((~(c_not @ ((X3)))|(c_not @ $true))&((c_not @ ((X3)))|(c_not @ $false)))=>(X3))), inference(fool_unroll,[status(thm)],[ax2])).
% 91.70/46.89 thf(c_0_9, plain, ![X243:$o]:(((c_not @ ((X243)))<=>((X243)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 91.70/46.89 thf(c_0_10, plain, ![X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X209:$i, X208:$i, X207:$i, X206:$i]:(((epred146_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203)<=>(![X210:$i]:((((X205 @ X209)=(X210))=>(((~(X203 @ X210)|((~((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $true))&((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false))))))|(c_and @ $true @ $false))))&((X203 @ X210)|((~((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $true))&((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false))))))|(c_and @ $false @ $false)))))=>?[X213:$i]:(((X207)=(X207))))))|((((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $false)))|(c_and @ $false @ $false)))))), introduced(definition)).
% 91.70/46.89 thf(c_0_11, plain, ![X203:$i > $o, X204:$i > $o, X206:$i, X207:$i, X208:$i, X209:$i, X210:$i]:(((epred145_7 @ X210 @ X207 @ X209 @ X208 @ X204 @ X206 @ X203)<=>((~(X203 @ X210)|((~((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $true))&((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false))))))|(c_and @ $true @ $false))))&((X203 @ X210)|((~((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $true))&((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false))))))|(c_and @ $false @ $false))))))), introduced(definition)).
% 91.70/46.89 thf(c_0_12, plain, ![X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X209:$i, X208:$i, X207:$i, X206:$i]:(((epred144_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203)<=>(~(![X210:$i]:((((X205 @ X209)=(X210))=>(((~(X203 @ X210)|((~((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $true))&((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false))))))|(c_and @ $true @ $false))))&((X203 @ X210)|((~((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $true))&((((X207)=(X206))=>((~(![X211:$i]:(((X209)=(X208))))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $true @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $true @ $false))))&(![X211:$i]:(((X209)=(X208)))|((~(?[X212:$i]:((X204 @ X210)))|(c_and @ $false @ $true))&(?[X212:$i]:((X204 @ X210))|(c_and @ $false @ $false))))))|(c_and @ $false @ $false)))))=>?[X213:$i]:(((X207)=(X207)))))))|((((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $false)))|(c_and @ $true @ $false)))))), introduced(definition)).
% 91.70/46.89 thf(c_0_13, plain, ![X172:$i, X173:$i, X174:$i, X181:$i, X188:$i, X432:$i > $i > $i, X434:$i > $i > $i, X440:$i > $i > $i > $i, X437:$i > $i > $i > $i, X435:$i]:(((epred128_10 @ X435 @ X437 @ X440 @ X188 @ X434 @ X432 @ X181 @ X173 @ X174 @ X172)<=>((((((X437 @ X188 @ (X432 @ (X434 @ X435 @ X172) @ (X440 @ X173 @ X174 @ X172)) @ X181)!=(X435))|~(c_not @ $true))&(((X437 @ X188 @ (X432 @ (X434 @ X435 @ X172) @ (X440 @ X173 @ X174 @ X172)) @ X181)=(X435))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((((X437 @ X188 @ (X432 @ (X434 @ X435 @ X172) @ (X440 @ X173 @ X174 @ X172)) @ X181)!=(X435))|(c_not @ $true))&(((X437 @ X188 @ (X432 @ (X434 @ X435 @ X172) @ (X440 @ X173 @ X174 @ X172)) @ X181)=(X435))|(c_not @ $false)))|(c_and @ $false @ $false))))), introduced(definition)).
% 91.70/46.89 thf(c_0_14, plain, ![X453:$o]:((((~(c_not @ ((X453)))|(c_not @ ((X453)))|(X453))&(~(c_not @ $false)|(c_not @ ((X453)))|(X453)))&((~(c_not @ ((X453)))|~(c_not @ $true)|(X453))&(~(c_not @ $false)|~(c_not @ $true)|(X453))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])).
% 91.70/46.89 thf(c_0_15, plain, ![X491:$o]:(((~(c_not @ ((X491)))|(~(X491)|(c_False)))&(((X491)|(c_not @ ((X491))))&(~(c_False)|(c_not @ ((X491))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])).
% 91.70/46.89 thf(c_0_16, plain, ![X244:$o, X245:$o]:(((c_and @ ((X244)) @ ((X245)))<=>![X20:$o]:((((X244)=>((X245)=>(X20)))=>(X20))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax14])])).
% 91.70/46.89 thf(c_0_17, 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, X208:$i, X209:$i]:((((c_and @ (![X210:$i]:(((((X205 @ X209)=(X210)))=>((((c_and @ ((X203 @ X210)) @ (((((X207)=(X206)))=>((c_and @ (![X211:$i]:(((X209)=(X208)))) @ (?[X212:$i]:((X204 @ X210)))))))))=>(?[X213:$i]:(((X207)=(X207))))))))) @ ((c_not @ ((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206)))))))))=>(((X83)=(X209)))))))), inference(assume_negation,[status(cth)],[conj])).
% 91.70/46.89 thf(c_0_18, plain, ![X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X209:$i, X208:$i, X207:$i, X206:$i]:(((epred146_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203)<=>(![X210:$i]:((((X205 @ X209)=(X210))=>((epred145_7 @ X210 @ X207 @ X209 @ X208 @ X204 @ X206 @ X203)=>?[X213:$i]:(((X207)=(X207))))))|((((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $false)))|(c_and @ $false @ $false)))))), inference(apply_def,[status(thm)],[c_0_10, c_0_11])).
% 91.70/46.89 thf(c_0_19, plain, ![X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X209:$i, X208:$i, X207:$i, X206:$i]:(((epred144_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203)<=>(~(![X210:$i]:((((X205 @ X209)=(X210))=>((epred145_7 @ X210 @ X207 @ X209 @ X208 @ X204 @ X206 @ X203)=>?[X213:$i]:(((X207)=(X207)))))))|((((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $true))&((X204 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))|(c_not @ $false)))|(c_and @ $true @ $false)))))), inference(apply_def,[status(thm)],[c_0_12, c_0_11])).
% 91.70/46.89 thf(c_0_20, plain, ![X1751:$i, X1752:$i, X1753:$i, X1754:$i, X1755:$i, X1756:$i > $i > $i, X1757:$i > $i > $i, X1758:$i > $i > $i > $i, X1759:$i > $i > $i > $i, X1760:$i]:(((((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|~(c_not @ $true)|(c_and @ $false @ $true)|~(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|~(c_not @ $false)|(c_and @ $false @ $true)|~(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|(c_not @ $true)|(c_and @ $false @ $false)|~(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|(c_not @ $false)|(c_and @ $false @ $false)|~(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(((((((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|~(c_not @ $true)|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|~(c_not @ $true)|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(~(c_and @ $false @ $false)|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|((c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|((c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|~(c_not @ $true)|((c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(~(c_and @ $false @ $false)|((c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760)))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(((((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|~(c_not @ $true)|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|~(c_not @ $true)|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(~(c_and @ $false @ $false)|(((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|((c_not @ $false)|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|((c_not @ $false)|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(~(c_and @ $false @ $false)|((c_not @ $false)|(c_not @ $true))|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))))&((((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|~(c_and @ $false @ $true)|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)=(X1760))|~(c_and @ $false @ $true)|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))&((((X1759 @ X1755 @ (X1756 @ (X1757 @ X1760 @ X1751) @ (X1758 @ X1752 @ X1753 @ X1751)) @ X1754)!=(X1760))|~(c_not @ $true)|~(c_and @ $false @ $true)|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))&(~(c_not @ $false)|~(c_not @ $true)|~(c_and @ $false @ $true)|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(epred128_10 @ X1760 @ X1759 @ X1758 @ X1755 @ X1757 @ X1756 @ X1754 @ X1752 @ X1753 @ X1751)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])])).
% 91.70/46.89 thf(c_0_21, plain, (~((c_not @ (~($true))))|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_14])])])).
% 91.70/46.89 thf(c_0_22, plain, (c_not @ (~($true))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_15])])])).
% 91.70/46.89 thf(c_0_23, plain, ![X492:$o, X493:$o, X494:$o, X495:$o, X496:$o]:(((((X492)|(X494)|~(c_and @ ((X492)) @ ((X493))))&(((X493)|(X494)|~(c_and @ ((X492)) @ ((X493))))&(~(X494)|(X494)|~(c_and @ ((X492)) @ ((X493))))))&((~(X495)|(~(X496)|(epred148_2 @ X495 @ X496))|(c_and @ ((X495)) @ ((X496))))&(~(epred148_2 @ X495 @ X496)|(c_and @ ((X495)) @ ((X496))))))), 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])])])])])])])).
% 91.70/46.89 thf(c_0_24, plain, ![X2036:$i]:(((esk219_0 @ X2036)=(c_ordsucc))), inference(variable_rename,[status(thm)],[])).
% 91.70/46.89 thf(c_0_25, 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, X208:$i, X209:$i]:((((epred144_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203)&(epred146_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203))=>((X83)=(X209)))))|(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, X208:$i, X209:$i]:((((epred144_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203)&(epred146_8 @ X206 @ X207 @ X208 @ X209 @ X204 @ X205 @ X202 @ X203))=>((X83)=(X209))))|(c_not @ $false)))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_17]), c_0_12]), c_0_10]), c_0_12]), c_0_10])).
% 91.70/46.89 thf(c_0_26, plain, ![X1940:$i > $i > $i, X1941:$i > $o, X1942:$i > $o, X1943:$i > $i, X1944:$i, X1945:$i, X1946:$i, X1947:$i, X1948:$i, X1949:$i > $i > $i, X1950:$i > $o, X1951:$i > $o, X1952:$i > $i, X1953:$i, X1954:$i, X1955:$i, X1956:$i]:(((((~(X1942 @ (X1943 @ (X1943 @ (X1940 @ X1946 @ X1947))))|~(c_not @ $true)|(c_and @ $false @ $true)|(((X1943 @ X1944)!=(X1948))|(~(epred145_7 @ X1948 @ X1946 @ X1944 @ X1945 @ X1942 @ X1947 @ X1941)|((X1946)=(X1946))))|~(epred146_8 @ X1947 @ X1946 @ X1945 @ X1944 @ X1942 @ X1943 @ X1940 @ X1941))&((X1942 @ (X1943 @ (X1943 @ (X1940 @ X1946 @ X1947))))|~(c_not @ $false)|(c_and @ $false @ $true)|(((X1943 @ X1944)!=(X1948))|(~(epred145_7 @ X1948 @ X1946 @ X1944 @ X1945 @ X1942 @ X1947 @ X1941)|((X1946)=(X1946))))|~(epred146_8 @ X1947 @ X1946 @ X1945 @ X1944 @ X1942 @ X1943 @ X1940 @ X1941)))&((~(X1942 @ (X1943 @ (X1943 @ (X1940 @ X1946 @ X1947))))|(c_not @ $true)|(c_and @ $false @ $false)|(((X1943 @ X1944)!=(X1948))|(~(epred145_7 @ X1948 @ X1946 @ X1944 @ X1945 @ X1942 @ X1947 @ X1941)|((X1946)=(X1946))))|~(epred146_8 @ X1947 @ X1946 @ X1945 @ X1944 @ X1942 @ X1943 @ X1940 @ X1941))&((X1942 @ (X1943 @ (X1943 @ (X1940 @ X1946 @ X1947))))|(c_not @ $false)|(c_and @ $false @ $false)|(((X1943 @ X1944)!=(X1948))|(~(epred145_7 @ X1948 @ X1946 @ X1944 @ X1945 @ X1942 @ X1947 @ X1941)|((X1946)=(X1946))))|~(epred146_8 @ X1947 @ X1946 @ X1945 @ X1944 @ X1942 @ X1943 @ X1940 @ X1941))))&(((((X1952 @ X1953)=(esk215_8 @ X1949 @ X1950 @ X1951 @ X1952 @ X1953 @ X1954 @ X1955 @ X1956))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(((epred145_7 @ (esk215_8 @ X1949 @ X1950 @ X1951 @ X1952 @ X1953 @ X1954 @ X1955 @ X1956) @ X1955 @ X1953 @ X1954 @ X1951 @ X1956 @ X1950)|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(((X1955)!=(X1955))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(((((((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_not @ $true)|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(~(c_and @ $false @ $false)|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|((c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|((c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_not @ $true)|((c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(~(c_and @ $false @ $false)|((c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956)))))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(((((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_not @ $true)|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(~(c_and @ $false @ $false)|(~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|((c_not @ $false)|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|((c_not @ $false)|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(~(c_and @ $false @ $false)|((c_not @ $false)|(c_not @ $true))|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))))&((((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_and @ $false @ $true)|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_and @ $false @ $true)|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950)))&((~(X1951 @ (X1952 @ (X1952 @ (X1949 @ X1955 @ X1956))))|~(c_not @ $true)|~(c_and @ $false @ $true)|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))&(~(c_not @ $false)|~(c_not @ $true)|~(c_and @ $false @ $true)|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(epred146_8 @ X1956 @ X1955 @ X1954 @ X1953 @ X1951 @ X1952 @ X1949 @ X1950))))))), 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)],[inference(fof_simplification,[status(thm)],[c_0_18])])])])])])])])).
% 91.70/46.89 thf(c_0_27, plain, ![X1915:$i > $i > $i, X1916:$i > $o, X1917:$i > $o, X1918:$i > $i, X1919:$i, X1920:$i, X1921:$i, X1922:$i, X1924:$i > $i > $i, X1925:$i > $o, X1926:$i > $o, X1927:$i > $i, X1928:$i, X1929:$i, X1930:$i, X1931:$i, X1932:$i]:((((((~(X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|~(c_not @ $true)|(c_and @ $true @ $true)|((X1918 @ X1919)=(esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))&((X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|~(c_not @ $false)|(c_and @ $true @ $true)|((X1918 @ X1919)=(esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916)))&((~(X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|(c_not @ $true)|(c_and @ $true @ $false)|((X1918 @ X1919)=(esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))&((X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|(c_not @ $false)|(c_and @ $true @ $false)|((X1918 @ X1919)=(esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))))&((((~(X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|~(c_not @ $true)|(c_and @ $true @ $true)|(epred145_7 @ (esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922) @ X1921 @ X1919 @ X1920 @ X1917 @ X1922 @ X1916)|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))&((X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|~(c_not @ $false)|(c_and @ $true @ $true)|(epred145_7 @ (esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922) @ X1921 @ X1919 @ X1920 @ X1917 @ X1922 @ X1916)|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916)))&((~(X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|(c_not @ $true)|(c_and @ $true @ $false)|(epred145_7 @ (esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922) @ X1921 @ X1919 @ X1920 @ X1917 @ X1922 @ X1916)|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))&((X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|(c_not @ $false)|(c_and @ $true @ $false)|(epred145_7 @ (esk214_8 @ X1915 @ X1916 @ X1917 @ X1918 @ X1919 @ X1920 @ X1921 @ X1922) @ X1921 @ X1919 @ X1920 @ X1917 @ X1922 @ X1916)|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))))&(((~(X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|~(c_not @ $true)|(c_and @ $true @ $true)|((X1921)!=(X1921))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))&((X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|~(c_not @ $false)|(c_and @ $true @ $true)|((X1921)!=(X1921))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916)))&((~(X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|(c_not @ $true)|(c_and @ $true @ $false)|((X1921)!=(X1921))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))&((X1917 @ (X1918 @ (X1918 @ (X1915 @ X1921 @ X1922))))|(c_not @ $false)|(c_and @ $true @ $false)|((X1921)!=(X1921))|~(epred144_8 @ X1922 @ X1921 @ X1920 @ X1919 @ X1917 @ X1918 @ X1915 @ X1916))))))&((((X1927 @ X1928)!=(X1932))|(~(epred145_7 @ X1932 @ X1930 @ X1928 @ X1929 @ X1926 @ X1931 @ X1925)|((X1930)=(X1930)))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(((((((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_not @ $true)|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))&(~(c_and @ $true @ $false)|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|((c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|((c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_not @ $true)|((c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))&(~(c_and @ $true @ $false)|((c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931)))))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))&(((((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_not @ $true)|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))&(~(c_and @ $true @ $false)|(~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|((c_not @ $false)|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|((c_not @ $false)|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))&(~(c_and @ $true @ $false)|((c_not @ $false)|(c_not @ $true))|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))))&((((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_and @ $true @ $true)|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_and @ $true @ $true)|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925)))&((~(X1926 @ (X1927 @ (X1927 @ (X1924 @ X1930 @ X1931))))|~(c_not @ $true)|~(c_and @ $true @ $true)|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))&(~(c_not @ $false)|~(c_not @ $true)|~(c_and @ $true @ $true)|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))&(~(c_and @ $true @ $false)|~(c_and @ $true @ $true)|(epred144_8 @ X1931 @ X1930 @ X1929 @ X1928 @ X1926 @ X1927 @ X1924 @ X1925))))))), 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)],[inference(fof_simplification,[status(thm)],[c_0_19])])])])])])])])).
% 91.70/46.89 thf(c_0_28, plain, ![X2:$i, X6:$i, X166:$i > $i > $i > $i, X164:$i > $i > $i > $i, X123:$i > $i > $i, X89:$i > $i > $i, X10:$i, X9:$i, X8:$i, X7:$i]:(((c_not @ (($true)))|(c_and @ (~($true)) @ (~($true)))|((X164 @ X2 @ (X89 @ (X123 @ X6 @ X7) @ (X166 @ X8 @ X9 @ X7)) @ X10)!=(X6))|~((epred128_10 @ X6 @ X164 @ X166 @ X2 @ X123 @ X89 @ X10 @ X8 @ X9 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 91.70/46.89 thf(c_0_29, plain, ~((c_not @ (($true)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 91.70/46.89 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_23])])])).
% 91.70/46.89 thf(c_0_31, plain, ![X2074:$i, X2075:$i > $i > $o]:(((~(epred166_1 @ X2075 @ X2074)|(X2075 @ (c_ap @ X2074 @ c_Empty) @ (c_ap @ X2074 @ (c_ordsucc @ c_Empty))))&(~(X2075 @ (c_ap @ X2074 @ c_Empty) @ (c_ap @ X2074 @ (c_ordsucc @ c_Empty)))|(epred166_1 @ X2075 @ X2074)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 91.70/46.89 thf(c_0_32, plain, ![X2:$i]:(((esk219_0 @ X2)=(c_ordsucc))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 91.70/46.89 thf(c_0_33, negated_conjecture, ![X822:$i > $i > $i, X823:$i > $o, X824:$i > $o, X825:$i > $i, X826:$i, X827:$i, X828:$i, X829:$i, X830:$i]:(((((((epred144_8 @ esk54_0 @ esk56_0 @ esk57_0 @ esk58_0 @ epred155_0 @ esk53_0 @ esk52_0 @ epred154_0)|(~(epred144_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|~(epred146_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|((X827)=(X830))))&((epred146_8 @ esk54_0 @ esk56_0 @ esk57_0 @ esk58_0 @ epred155_0 @ esk53_0 @ esk52_0 @ epred154_0)|(~(epred144_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|~(epred146_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|((X827)=(X830)))))&(((esk55_0)!=(esk58_0))|(~(epred144_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|~(epred146_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|((X827)=(X830)))))&(~(c_not @ $false)|(~(epred144_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|~(epred146_8 @ X826 @ X828 @ X829 @ X830 @ X824 @ X825 @ X822 @ X823)|((X827)=(X830)))))&(((((epred144_8 @ esk54_0 @ esk56_0 @ esk57_0 @ esk58_0 @ epred155_0 @ esk53_0 @ esk52_0 @ epred154_0)|~(c_not @ $true))&((epred146_8 @ esk54_0 @ esk56_0 @ esk57_0 @ esk58_0 @ epred155_0 @ esk53_0 @ esk52_0 @ epred154_0)|~(c_not @ $true)))&(((esk55_0)!=(esk58_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_25])])])])])])])).
% 91.70/46.89 thf(c_0_34, plain, ![X1:$i > $o, X6:$i, X7:$i, X89:$i > $i > $i, X8:$i, X65:$i > $o, X12:$i > $i, X2:$i]:(((epred146_8 @ X6 @ X2 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65)|((X2)!=(X2)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 91.70/46.89 thf(c_0_35, plain, ![X6:$i, X2:$i, X1:$i > $o, X8:$i, X7:$i, X89:$i > $i > $i, X12:$i > $i, X65:$i > $o]:(((X1 @ (X12 @ (X12 @ (X89 @ X2 @ X6))))|(epred144_8 @ X6 @ X2 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65)|~((c_not @ (~($true))))|~((c_and @ (($true)) @ (($true)))))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 91.70/46.89 thf(c_0_36, plain, ![X3:$o, X4:$o]:(((c_and @ ((X3)) @ ((X4)))|~((epred148_2 @ ((X3)) @ ((X4)))))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 91.70/46.89 thf(c_0_37, plain, ((epred148_2 @ (($true)) @ (($true)))|(c_and @ (($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23])])])).
% 91.70/46.89 thf(c_0_38, 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])).
% 91.70/46.89 thf(c_0_39, 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])).
% 91.70/46.89 thf(c_0_40, plain, ![X2:$i, X6:$i, X166:$i > $i > $i > $i, X164:$i > $i > $i > $i, X123:$i > $i > $i, X89:$i > $i > $i, X10:$i, X9:$i, X8:$i, X7:$i]:((((X164 @ X2 @ (X89 @ (X123 @ X6 @ X7) @ (X166 @ X8 @ X9 @ X7)) @ X10)=(X6))|(c_and @ (~($true)) @ (($true)))|~((c_not @ (~($true))))|~((epred128_10 @ X6 @ X164 @ X166 @ X2 @ X123 @ X89 @ X10 @ X8 @ X9 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 91.70/46.89 thf(c_0_41, plain, ![X5:$o]:(~((c_and @ (~($true)) @ ((X5))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23])])])).
% 91.70/46.89 thf(c_0_42, plain, ![X2:$i, X6:$i, X166:$i > $i > $i > $i, X164:$i > $i > $i > $i, X123:$i > $i > $i, X89:$i > $i > $i, X10:$i, X9:$i, X8:$i, X7:$i]:((((X164 @ X2 @ (X89 @ (X123 @ X6 @ X7) @ (X166 @ X8 @ X9 @ X7)) @ X10)!=(X6))|~((epred128_10 @ X6 @ X164 @ X166 @ X2 @ X123 @ X89 @ X10 @ X8 @ X9 @ X7)))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_28, c_0_29]), c_0_30])).
% 91.70/46.89 thf(c_0_43, plain, ![X37:$i > $i > $o, X2:$i]:(((X37 @ (c_ap @ X2 @ c_Empty) @ (c_ap @ X2 @ (c_ordsucc @ c_Empty)))|~((epred166_1 @ X37 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 91.70/46.89 thf(c_0_44, plain, ![X2:$i, X6:$i]:(((esk219_0 @ X2 @ X6)=(c_ordsucc @ X6))), inference(arg_cong,[status(thm)],[c_0_32])).
% 91.70/46.89 thf(c_0_45, negated_conjecture, ![X6:$i, X2:$i, X1:$i > $o, X8:$i, X7:$i, X9:$i, X89:$i > $i > $i, X12:$i > $i, X65:$i > $o]:((((X9)=(X8))|~((c_not @ (~($true))))|~((epred144_8 @ X2 @ X6 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65))|~((epred146_8 @ X2 @ X6 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 91.70/46.89 thf(c_0_46, plain, ![X1:$i > $o, X6:$i, X7:$i, X2:$i, X8:$i, X89:$i > $i > $i, X12:$i > $i, X65:$i > $o]:((epred146_8 @ X6 @ X2 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65)), inference(cn,[status(thm)],[c_0_34])).
% 91.70/46.89 thf(c_0_47, plain, ![X1:$i > $o, X7:$i, X65:$i > $o, X12:$i > $i, X89:$i > $i > $i, X8:$i, X6:$i, X2:$i]:(((epred144_8 @ X2 @ X6 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65)|(X1 @ (X12 @ (X12 @ (X89 @ X6 @ X2))))|~((c_and @ (($true)) @ (($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_22])])).
% 91.70/46.89 thf(c_0_48, plain, (c_and @ (($true)) @ (($true))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 91.70/46.89 thf(c_0_49, plain, ![X458:$i]:(((~(c_In @ X458 @ 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_38])])])])])).
% 91.70/46.89 thf(c_0_50, plain, ![X250:$i, X251:$i]:(((c_Subq @ X250 @ X251)<=>![X9:$i]:(((c_In @ X9 @ X250)=>(c_In @ X9 @ X251))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 91.70/46.89 thf(c_0_51, plain, ![X466:$i, X467:$i]:((((~(c_Subq @ X467 @ X466)|(c_iff @ $true @ $true)|~(c_In @ X467 @ (c_Power @ X466)))&((c_Subq @ X467 @ X466)|(c_iff @ $true @ $false)|~(c_In @ X467 @ (c_Power @ X466))))&((~(c_Subq @ X467 @ X466)|(c_iff @ $false @ $true)|(c_In @ X467 @ (c_Power @ X466)))&((c_Subq @ X467 @ X466)|(c_iff @ $false @ $false)|(c_In @ X467 @ (c_Power @ X466)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_39])])])).
% 91.70/46.89 thf(c_0_52, plain, ![X454:$o, X455:$o]:(((~(X454)|(X455)|~(c_iff @ ((X454)) @ ((X455))))&(~(X455)|(X454)|~(c_iff @ ((X454)) @ ((X455)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 91.70/46.89 thf(c_0_53, plain, ![X2:$i, X6:$i, X7:$i, X8:$i, X9:$i, X166:$i > $i > $i > $i, X164:$i > $i > $i > $i, X123:$i > $i > $i, X89:$i > $i > $i, X10:$i]:(~((epred128_10 @ X2 @ X164 @ X166 @ X6 @ X89 @ X123 @ X7 @ X8 @ X9 @ X10))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_22])]), c_0_41]), c_0_42])).
% 91.70/46.89 thf(c_0_54, plain, ![X37:$i > $i > $o, X2:$i]:(((X37 @ (c_ap @ X2 @ c_Empty) @ (c_ap @ X2 @ (esk219_0 @ c_Empty @ c_Empty)))|~((epred166_1 @ X37 @ X2)))), inference(rw,[status(thm)],[c_0_43, c_0_44])).
% 91.70/46.89 thf(c_0_55, negated_conjecture, ![X1:$i > $o, X7:$i, X6:$i, X8:$i, X2:$i, X9:$i, X89:$i > $i > $i, X12:$i > $i, X65:$i > $o]:((((X2)=(X6))|~((epred144_8 @ X7 @ X8 @ X9 @ X2 @ X1 @ X12 @ X89 @ X65)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_22]), c_0_46])])).
% 91.70/46.89 thf(c_0_56, plain, ![X1:$i > $o, X7:$i, X65:$i > $o, X12:$i > $i, X89:$i > $i > $i, X8:$i, X6:$i, X2:$i]:(((epred144_8 @ X2 @ X6 @ X7 @ X8 @ X1 @ X12 @ X89 @ X65)|(X1 @ (X12 @ (X12 @ (X89 @ X6 @ X2)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48])])).
% 91.70/46.89 thf(c_0_57, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_49])).
% 91.70/46.89 thf(c_0_58, plain, ![X506:$i, X507:$i, X508:$i, X509:$i, X510:$i]:(((~(c_Subq @ X506 @ X507)|(~(c_In @ X508 @ X506)|(c_In @ X508 @ X507)))&(((c_In @ (esk13_2 @ X509 @ X510) @ X509)|(c_Subq @ X509 @ X510))&(~(c_In @ (esk13_2 @ X509 @ X510) @ X510)|(c_Subq @ X509 @ X510))))), 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_50])])])])])])])).
% 91.70/46.89 thf(c_0_59, 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_51])).
% 91.70/46.89 thf(c_0_60, plain, ~((c_iff @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_52])])])).
% 91.70/46.89 thf(c_0_61, plain, ![X2:$i, X6:$i, X7:$i, X8:$i, X166:$i > $i > $i > $i, X164:$i > $i > $i > $i, X123:$i > $i > $i, X89:$i > $i > $i, X9:$i]:(~((epred166_1 @ (epred128_10 @ X2 @ X164 @ X166 @ X6 @ X89 @ X123 @ X7 @ X8) @ X9))), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 91.70/46.89 thf(c_0_62, negated_conjecture, ![X1:$i > $o, X2:$i, X6:$i, X7:$i, X12:$i > $i, X89:$i > $i > $i, X8:$i]:((((X2)=(X6))|(X1 @ (X12 @ (X12 @ (X89 @ X7 @ X8)))))), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 91.70/46.89 thf(c_0_63, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_57, c_0_29])).
% 91.70/46.89 thf(c_0_64, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 91.70/46.89 thf(c_0_65, plain, ![X2:$i, X6:$i]:(((c_In @ X2 @ (c_Power @ X6))|~((c_Subq @ X2 @ X6)))), inference(sr,[status(thm)],[c_0_59, c_0_60])).
% 91.70/46.89 thf(c_0_66, plain, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 91.70/46.89 thf(c_0_67, plain, ![X2:$i]:((c_Subq @ c_Empty @ X2)), inference(spm,[status(thm)],[c_0_63, c_0_64])).
% 91.70/46.89 thf(c_0_68, plain, ![X2:$i, X6:$i]:(~((c_Subq @ X2 @ X6))), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66]), c_0_63])).
% 91.70/46.89 thf(c_0_69, plain, ($false), inference(sr,[status(thm)],[c_0_67, c_0_68]), ['proof']).
% 91.70/46.89 % SZS output end CNFRefutation
% 91.70/46.89 % Parsed axioms : 213
% 91.70/46.89 % Removed by relevancy pruning/SinE : 0
% 91.70/46.89 % Initial clauses : 468845
% 91.70/46.89 % Removed in clause preprocessing : 463944
% 91.70/46.89 % Initial clauses in saturation : 4901
% 91.70/46.89 % Processed clauses : 8450
% 91.70/46.89 % ...of these trivial : 462
% 91.70/46.89 % ...subsumed : 4240
% 91.70/46.89 % ...remaining for further processing : 3748
% 91.70/46.89 % Other redundant clauses eliminated : 197
% 91.70/46.89 % Clauses deleted for lack of memory : 0
% 91.70/46.89 % Backward-subsumed : 195
% 91.70/46.89 % Backward-rewritten : 1695
% 91.70/46.89 % Generated clauses : 50461
% 91.70/46.89 % ...of the previous two non-redundant : 50206
% 91.70/46.89 % ...aggressively subsumed : 0
% 91.70/46.89 % Contextual simplify-reflections : 278
% 91.70/46.89 % Paramodulations : 50176
% 91.70/46.89 % Factorizations : 62
% 91.70/46.89 % NegExts : 0
% 91.70/46.89 % Equation resolutions : 197
% 91.70/46.89 % Disequality decompositions : 0
% 91.70/46.89 % Total rewrite steps : 15018
% 91.70/46.89 % ...of those cached : 11413
% 91.70/46.89 % Propositional unsat checks : 0
% 91.70/46.89 % Propositional check models : 0
% 91.70/46.89 % Propositional check unsatisfiable : 0
% 91.70/46.89 % Propositional clauses : 0
% 91.70/46.89 % Propositional clauses after purity: 0
% 91.70/46.89 % Propositional unsat core size : 0
% 91.70/46.89 % Propositional preprocessing time : 0.000
% 91.70/46.89 % Propositional encoding time : 0.000
% 91.70/46.89 % Propositional solver time : 0.000
% 91.70/46.89 % Success case prop preproc time : 0.000
% 91.70/46.89 % Success case prop encoding time : 0.000
% 91.70/46.89 % Success case prop solver time : 0.000
% 91.70/46.89 % Current number of processed clauses : 613
% 91.70/46.89 % Positive orientable unit clauses : 100
% 91.70/46.89 % Positive unorientable unit clauses: 2
% 91.70/46.89 % Negative unit clauses : 71
% 91.70/46.89 % Non-unit-clauses : 440
% 91.70/46.89 % Current number of unprocessed clauses: 47727
% 91.70/46.89 % ...number of literals in the above : 207442
% 91.70/46.89 % Current number of archived formulas : 0
% 91.70/46.89 % Current number of archived clauses : 3084
% 91.70/46.89 % Clause-clause subsumption calls (NU) : 2005508
% 91.70/46.89 % Rec. Clause-clause subsumption calls : 587299
% 91.70/46.89 % Non-unit clause-clause subsumptions : 1594
% 91.70/46.89 % Unit Clause-clause subsumption calls : 122841
% 91.70/46.89 % Rewrite failures with RHS unbound : 0
% 91.70/46.89 % BW rewrite match attempts : 7356
% 91.70/46.89 % BW rewrite match successes : 2364
% 91.70/46.89 % Condensation attempts : 0
% 91.70/46.89 % Condensation successes : 0
% 91.70/46.89 % Termbank termtop insertions : 21178789
% 91.70/46.89 % Search garbage collected termcells : 2012572
% 91.70/46.89
% 91.70/46.89 % -------------------------------------------------
% 91.70/46.89 % User time : 42.795 s
% 91.70/46.89 % System time : 2.569 s
% 91.70/46.89 % Total time : 45.364 s
% 91.70/46.89 % Maximum resident set size: 1257140 pages
% 91.70/46.89
% 91.70/46.89 % -------------------------------------------------
% 91.70/46.89 % User time : 42.941 s
% 91.70/46.89 % System time : 2.786 s
% 91.70/46.89 % Total time : 45.728 s
% 91.70/46.89 % Maximum resident set size: 5120 pages
% 91.70/46.89 % E exiting
%------------------------------------------------------------------------------