%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO852^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 : n015.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:27 AM UTC 2026
% Result : Theorem 53.79s 26.63s
% Output : CNFRefutation 53.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO852^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n015.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Tue Sep 29 17:21:48 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running higher-order theorem proving
% 0.07/0.26 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.eXi7YnW5IQ/E---3.1_3838330.p
% 53.79/26.63 % Version: 3.5.1-ho
% 53.79/26.63 % partial match(2): HSLMSMSSSSLCHSA
% 53.79/26.63 % Preprocessing class: HSLMSLSSSSLCHHA.
% 53.79/26.63 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 53.79/26.63 % Starting pre_casc_6 with 1500s (5) cores
% 53.79/26.63 % Starting ehoh_best7 with 300s (1) cores
% 53.79/26.63 % Starting new_bool_8 with 300s (1) cores
% 53.79/26.63 % Starting new_ho_11 with 300s (1) cores
% 53.79/26.63 % new_bool_8 with pid 3838345 completed with status 9
% 53.79/26.63 % ehoh_best7 with pid 3838344 completed with status 0
% 53.79/26.63 % Result found by ehoh_best7
% 53.79/26.63 % partial match(2): HSLMSMSSSSLCHSA
% 53.79/26.63 % Preprocessing class: HSLMSLSSSSLCHHA.
% 53.79/26.63 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 53.79/26.63 % Starting pre_casc_6 with 1500s (5) cores
% 53.79/26.63 % Starting ehoh_best7 with 300s (1) cores
% 53.79/26.63 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 53.79/26.63 % No SInE strategy applied
% 53.79/26.63 % Search class: HGHSM-SMLM33-DHHFFSBC
% 53.79/26.63 % partial match(2): HGHSM-SMLM33-MHFFFSBC
% 53.79/26.63 % Scheduled 7 strats onto 1 cores with 275 seconds (275 total)
% 53.79/26.63 % Starting SubtermCWHack with 25s (1) cores
% 53.79/26.63 % SubtermCWHack with pid 3838516 completed with status 0
% 53.79/26.63 % Result found by SubtermCWHack
% 53.79/26.63 % partial match(2): HSLMSMSSSSLCHSA
% 53.79/26.63 % Preprocessing class: HSLMSLSSSSLCHHA.
% 53.79/26.63 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 53.79/26.63 % Starting pre_casc_6 with 1500s (5) cores
% 53.79/26.63 % Starting ehoh_best7 with 300s (1) cores
% 53.79/26.63 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 53.79/26.63 % No SInE strategy applied
% 53.79/26.63 % Search class: HGHSM-SMLM33-DHHFFSBC
% 53.79/26.63 % partial match(2): HGHSM-SMLM33-MHFFFSBC
% 53.79/26.63 % Scheduled 7 strats onto 1 cores with 275 seconds (275 total)
% 53.79/26.63 % Starting SubtermCWHack with 25s (1) cores
% 53.79/26.63 % Preprocessing time : 0.072 s
% 53.79/26.63
% 53.79/26.63 % Proof found!
% 53.79/26.63 % SZS status Theorem
% 53.79/26.63 % SZS output start CNFRefutation
% 53.79/26.63 thf(decl_24, type, c_False: $o).
% 53.79/26.63 thf(decl_26, type, c_not: $o > $o).
% 53.79/26.63 thf(decl_29, type, c_iff: $o > $o > $o).
% 53.79/26.63 thf(decl_30, type, c_In: $i > $i > $o).
% 53.79/26.63 thf(decl_31, type, c_Subq: $i > $i > $o).
% 53.79/26.63 thf(decl_32, type, c_Empty: $i).
% 53.79/26.63 thf(decl_34, type, c_Power: $i > $i).
% 53.79/26.63 thf(decl_87, type, c_Inj1: $i > $i).
% 53.79/26.63 thf(decl_88, type, c_Inj0: $i > $i).
% 53.79/26.63 thf(decl_91, type, c_setsum: $i > $i > $i).
% 53.79/26.63 thf(decl_269, type, esk1_0: $i).
% 53.79/26.63 thf(decl_281, type, epred143_0: $o).
% 53.79/26.63 thf(decl_284, type, esk13_2: $i > $i > $i).
% 53.79/26.63 thf(decl_327, type, esk52_0: (($i > $i > $i > $i) > $i) > (((($i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i).
% 53.79/26.63 thf(decl_328, type, esk53_0: ((((($i > $i) > $i > $i) > $i > $i) > $i) > $i) > $i > $i).
% 53.79/26.63 thf(decl_329, type, esk54_0: ((((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i) > $i) > ($i > ($i > $i) > ($i > $i) > $i > $i) > $i).
% 53.79/26.63 thf(decl_330, type, esk55_0: ($i > $i) > ($i > $i > ($i > $i) > $i) > $i).
% 53.79/26.63 thf(decl_504, type, esk221_1: $i > $i > $i).
% 53.79/26.63 thf(decl_535, type, esk247_0: $i > $i > ($i > $i) > $i).
% 53.79/26.63 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox/tmp/tmp.eXi7YnW5IQ/E---3.1_3838330.p', ax13)).
% 53.79/26.63 thf(conj, conjecture, ![X201:(($i > $i > $i > $i) > $i) > (((($i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i, X202:((((($i > $i) > $i > $i) > $i > $i) > $i) > $i) > $i > $i, X203:((((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i) > $i) > ($i > ($i > $i) > ($i > $i) > $i > $i) > $i, X204:($i > $i) > ($i > $i > ($i > $i) > $i) > $i]:((![X66:$i, X205:$i, X83:$i, X206:$i]:(((X204 @ (^[X207:$i]:(c_Empty)) @ (^[X208:$i, X209:$i, X210:$i > $i]:(c_Empty)))=(X83)))=>(![X211:($i > $i > $i > $i) > $i > $i, X212:$i, X213:((($i > $i) > $i > $i) > ($i > $i) > $i > $i) > $i, X214:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i]:(((X204 @ (^[X215:$i]:(c_Empty)) @ (^[X216:$i, X217:$i, X218:$i > $i]:(X202 @ (^[X219:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Inj0 @ (X219 @ (^[X220:($i > $i) > $i > $i, X221:$i]:(X219 @ (^[X222:($i > $i) > $i > $i, X173:$i]:(c_Empty))))))) @ X217)))=(X202 @ (^[X223:((($i > $i) > $i > $i) > $i > $i) > $i]:(X203 @ (^[X224:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X225:$i, X226:$i > $i, X227:$i > $i, X228:$i]:(X226 @ (X226 @ X225))))) @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty)))))=>(![X229:((($i > $i) > $i > $i) > $i) > (($i > $i) > $i) > ($i > $i) > $i > $i, X230:$i, X231:$i > $i, X232:($i > $i) > $i > $i]:(((X203 @ (^[X233:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X234:$i, X235:$i > $i, X236:$i > $i, X237:$i]:(X201 @ (^[X238:$i > $i > $i > $i]:(c_Empty)) @ (^[X239:(($i > $i) > $i > $i) > $i, X171:$i > $i > $i]:(X203 @ (^[X240:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X241:$i > $i, X242:$i > $i, X181:$i]:(c_setsum @ (X201 @ (^[X243:$i > $i > $i > $i]:(c_Empty)) @ (^[X244:(($i > $i) > $i > $i) > $i, X245:$i > $i > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))))=(X201 @ (^[X166:$i > $i > $i > $i]:(X204 @ (^[X246:$i]:(c_Empty)) @ (^[X247:$i, X248:$i, X249:$i > $i]:(c_Empty)))) @ (^[X250:(($i > $i) > $i > $i) > $i, X251:$i > $i > $i]:(X202 @ (^[X252:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty)))))=>(![X253:$i > $i > ($i > $i) > $i, X254:$i, X255:(($i > $i > $i) > $i > $i > $i) > $i > $i, X256:(($i > $i > $i) > $i) > $i]:(((X203 @ (^[X257:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (^[X258:$i, X259:$i > $i, X260:$i > $i, X261:$i]:(c_Empty)))=(c_setsum @ c_Empty @ (X253 @ (c_setsum @ (X253 @ (c_setsum @ c_Empty @ c_Empty) @ (X202 @ (^[X262:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty) @ (^[X263:$i]:(c_Empty))) @ (X204 @ (^[X264:$i]:(c_Empty)) @ (^[X265:$i, X266:$i, X267:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))) @ (X203 @ (^[X268:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X201 @ (^[X167:$i > $i > $i > $i]:(X256 @ (^[X168:$i > $i > $i]:(c_Empty)))) @ (^[X269:(($i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(X256 @ (^[X169:$i > $i > $i]:(c_Empty)))))) @ (^[X270:$i, X271:$i > $i, X272:$i > $i, X273:$i]:(c_Empty))) @ (^[X274:$i]:(X202 @ (^[X275:((($i > $i) > $i > $i) > $i > $i) > $i]:(X203 @ (^[X276:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X277:$i, X278:$i > $i, X279:$i > $i, X280:$i]:(c_Empty)))) @ (c_setsum @ c_Empty @ (X202 @ (^[X281:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))))))))=>(![X66:$i, X282:$i, X283:$i > $i, X284:$i]:(((X202 @ (^[X285:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_setsum @ (X201 @ (^[X167:$i > $i > $i > $i]:(X167 @ c_Empty @ X284 @ c_Empty)) @ (^[X286:(($i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(X204 @ (^[X287:$i]:(X286 @ (^[X288:$i > $i, X289:$i]:(c_Empty)))) @ (^[X290:$i, X291:$i, X292:$i > $i]:(c_Empty))))) @ (c_Inj0 @ c_Empty))) @ c_Empty)=(c_Inj1 @ X66)))=>(![X293:((($i > $i) > $i > $i) > $i) > $i, X294:$i, X295:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i, X296:$i > $i > ($i > $i) > $i > $i]:(((X202 @ (^[X297:((($i > $i) > $i > $i) > $i > $i) > $i]:(X294)) @ (c_Inj1 @ c_Empty))=(c_Inj0 @ (X204 @ (^[X298:$i]:(X296 @ (X203 @ (^[X299:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X295 @ (^[X300:$i > $i, X301:$i > $i]:(c_Empty)) @ (^[X302:$i]:(c_Empty)))) @ (^[X303:$i, X304:$i > $i, X305:$i > $i, X306:$i]:(c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (^[X307:$i]:(X203 @ (^[X308:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X307)) @ (^[X309:$i, X310:$i > $i, X311:$i > $i, X312:$i]:(X310 @ c_Empty)))) @ (c_Inj0 @ c_Empty))) @ (^[X313:$i, X314:$i, X315:$i > $i]:(X313))))))=>(![X66:$i, X316:$i, X83:$i, X317:($i > ($i > $i) > $i > $i) > $i > $i]:(((X201 @ (^[X166:$i > $i > $i > $i]:(X83)) @ (^[X318:(($i > $i) > $i > $i) > $i, X319:$i > $i > $i]:(X204 @ (^[X320:$i]:(c_Inj0 @ (c_setsum @ X320 @ (X317 @ (^[X321:$i, X322:$i > $i, X323:$i]:(c_Empty)) @ c_Empty)))) @ (^[X324:$i, X325:$i, X326:$i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (X326 @ c_Empty)))))))=(X83)))=>(![X66:$i, X327:(($i > $i) > $i) > ($i > $i > $i) > $i, X83:$i, X328:$i > (($i > $i) > $i) > $i]:(((X201 @ (^[X166:$i > $i > $i > $i]:(c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ (X202 @ (^[X329:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))) @ (c_Inj1 @ c_Empty))) @ (^[X330:(($i > $i) > $i > $i) > $i, X331:$i > $i > $i]:(c_setsum @ X83 @ (c_Inj0 @ (X331 @ (X203 @ (^[X332:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X333:$i, X334:$i > $i, X335:$i > $i, X336:$i]:(c_Empty))) @ (X331 @ c_Empty @ c_Empty))))))=(X328 @ c_Empty @ (^[X337:$i > $i]:(X337 @ c_Empty)))))=>(c_False)))))))))), file('/export/starexec/sandbox/tmp/tmp.eXi7YnW5IQ/E---3.1_3838330.p', conj)).
% 53.79/26.63 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox/tmp/tmp.eXi7YnW5IQ/E---3.1_3838330.p', ax5)).
% 53.79/26.63 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox/tmp/tmp.eXi7YnW5IQ/E---3.1_3838330.p', ax11)).
% 53.79/26.63 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.eXi7YnW5IQ/E---3.1_3838330.p', ax17)).
% 53.79/26.63 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.eXi7YnW5IQ/E---3.1_3838330.p', ax7)).
% 53.79/26.63 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox/tmp/tmp.eXi7YnW5IQ/E---3.1_3838330.p', ax3)).
% 53.79/26.63 thf(c_0_7, plain, ![X403:$o]:(((c_not @ ((X403)))<=>((X403)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 53.79/26.63 thf(c_0_8, negated_conjecture, ~(![X201:(($i > $i > $i > $i) > $i) > (((($i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i, X202:((((($i > $i) > $i > $i) > $i > $i) > $i) > $i) > $i > $i, X203:((((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i) > $i) > ($i > ($i > $i) > ($i > $i) > $i > $i) > $i, X204:($i > $i) > ($i > $i > ($i > $i) > $i) > $i]:((![X66:$i, X205:$i, X83:$i, X206:$i]:(((X204 @ (^[X207:$i]:(c_Empty)) @ (^[X208:$i, X209:$i, X210:$i > $i]:(c_Empty)))=(X83)))=>(![X211:($i > $i > $i > $i) > $i > $i, X212:$i, X213:((($i > $i) > $i > $i) > ($i > $i) > $i > $i) > $i, X214:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i]:(((X204 @ (^[X215:$i]:(c_Empty)) @ (^[X216:$i, X217:$i, X218:$i > $i]:(X202 @ (^[X219:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Inj0 @ (X219 @ (^[X220:($i > $i) > $i > $i, X221:$i]:(X219 @ (^[X222:($i > $i) > $i > $i, X173:$i]:(c_Empty))))))) @ X217)))=(X202 @ (^[X223:((($i > $i) > $i > $i) > $i > $i) > $i]:(X203 @ (^[X224:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X225:$i, X226:$i > $i, X227:$i > $i, X228:$i]:(X226 @ (X226 @ X225))))) @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty)))))=>(![X229:((($i > $i) > $i > $i) > $i) > (($i > $i) > $i) > ($i > $i) > $i > $i, X230:$i, X231:$i > $i, X232:($i > $i) > $i > $i]:(((X203 @ (^[X233:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X234:$i, X235:$i > $i, X236:$i > $i, X237:$i]:(X201 @ (^[X238:$i > $i > $i > $i]:(c_Empty)) @ (^[X239:(($i > $i) > $i > $i) > $i, X171:$i > $i > $i]:(X203 @ (^[X240:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X241:$i > $i, X242:$i > $i, X181:$i]:(c_setsum @ (X201 @ (^[X243:$i > $i > $i > $i]:(c_Empty)) @ (^[X244:(($i > $i) > $i > $i) > $i, X245:$i > $i > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))))=(X201 @ (^[X166:$i > $i > $i > $i]:(X204 @ (^[X246:$i]:(c_Empty)) @ (^[X247:$i, X248:$i, X249:$i > $i]:(c_Empty)))) @ (^[X250:(($i > $i) > $i > $i) > $i, X251:$i > $i > $i]:(X202 @ (^[X252:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty)))))=>(![X253:$i > $i > ($i > $i) > $i, X254:$i, X255:(($i > $i > $i) > $i > $i > $i) > $i > $i, X256:(($i > $i > $i) > $i) > $i]:(((X203 @ (^[X257:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (^[X258:$i, X259:$i > $i, X260:$i > $i, X261:$i]:(c_Empty)))=(c_setsum @ c_Empty @ (X253 @ (c_setsum @ (X253 @ (c_setsum @ c_Empty @ c_Empty) @ (X202 @ (^[X262:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty) @ (^[X263:$i]:(c_Empty))) @ (X204 @ (^[X264:$i]:(c_Empty)) @ (^[X265:$i, X266:$i, X267:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))) @ (X203 @ (^[X268:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X201 @ (^[X167:$i > $i > $i > $i]:(X256 @ (^[X168:$i > $i > $i]:(c_Empty)))) @ (^[X269:(($i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(X256 @ (^[X169:$i > $i > $i]:(c_Empty)))))) @ (^[X270:$i, X271:$i > $i, X272:$i > $i, X273:$i]:(c_Empty))) @ (^[X274:$i]:(X202 @ (^[X275:((($i > $i) > $i > $i) > $i > $i) > $i]:(X203 @ (^[X276:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X277:$i, X278:$i > $i, X279:$i > $i, X280:$i]:(c_Empty)))) @ (c_setsum @ c_Empty @ (X202 @ (^[X281:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))))))))=>(![X66:$i, X282:$i, X283:$i > $i, X284:$i]:(((X202 @ (^[X285:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_setsum @ (X201 @ (^[X167:$i > $i > $i > $i]:(X167 @ c_Empty @ X284 @ c_Empty)) @ (^[X286:(($i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(X204 @ (^[X287:$i]:(X286 @ (^[X288:$i > $i, X289:$i]:(c_Empty)))) @ (^[X290:$i, X291:$i, X292:$i > $i]:(c_Empty))))) @ (c_Inj0 @ c_Empty))) @ c_Empty)=(c_Inj1 @ X66)))=>(![X293:((($i > $i) > $i > $i) > $i) > $i, X294:$i, X295:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i, X296:$i > $i > ($i > $i) > $i > $i]:(((X202 @ (^[X297:((($i > $i) > $i > $i) > $i > $i) > $i]:(X294)) @ (c_Inj1 @ c_Empty))=(c_Inj0 @ (X204 @ (^[X298:$i]:(X296 @ (X203 @ (^[X299:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X295 @ (^[X300:$i > $i, X301:$i > $i]:(c_Empty)) @ (^[X302:$i]:(c_Empty)))) @ (^[X303:$i, X304:$i > $i, X305:$i > $i, X306:$i]:(c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (^[X307:$i]:(X203 @ (^[X308:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X307)) @ (^[X309:$i, X310:$i > $i, X311:$i > $i, X312:$i]:(X310 @ c_Empty)))) @ (c_Inj0 @ c_Empty))) @ (^[X313:$i, X314:$i, X315:$i > $i]:(X313))))))=>(![X66:$i, X316:$i, X83:$i, X317:($i > ($i > $i) > $i > $i) > $i > $i]:(((X201 @ (^[X166:$i > $i > $i > $i]:(X83)) @ (^[X318:(($i > $i) > $i > $i) > $i, X319:$i > $i > $i]:(X204 @ (^[X320:$i]:(c_Inj0 @ (c_setsum @ X320 @ (X317 @ (^[X321:$i, X322:$i > $i, X323:$i]:(c_Empty)) @ c_Empty)))) @ (^[X324:$i, X325:$i, X326:$i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (X326 @ c_Empty)))))))=(X83)))=>(![X66:$i, X327:(($i > $i) > $i) > ($i > $i > $i) > $i, X83:$i, X328:$i > (($i > $i) > $i) > $i]:(((X201 @ (^[X166:$i > $i > $i > $i]:(c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ (X202 @ (^[X329:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))) @ (c_Inj1 @ c_Empty))) @ (^[X330:(($i > $i) > $i > $i) > $i, X331:$i > $i > $i]:(c_setsum @ X83 @ (c_Inj0 @ (X331 @ (X203 @ (^[X332:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[X333:$i, X334:$i > $i, X335:$i > $i, X336:$i]:(c_Empty))) @ (X331 @ c_Empty @ c_Empty))))))=(X328 @ c_Empty @ (^[X337:$i > $i]:(X337 @ c_Empty)))))=>(c_False))))))))))), inference(assume_negation,[status(cth)],[conj])).
% 53.79/26.63 thf(c_0_9, 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])).
% 53.79/26.63 thf(c_0_10, plain, ![X651:$o]:(((~(c_not @ ((X651)))|(~(X651)|(c_False)))&(((X651)|(c_not @ ((X651))))&(~(c_False)|(c_not @ ((X651))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])).
% 53.79/26.63 thf(c_0_11, plain, ![X649:$o]:(((~(c_False)|(X649))&(~(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])])])])])).
% 53.79/26.63 thf(c_0_12, negated_conjecture, ~(![X201:(($i > $i > $i > $i) > $i) > (((($i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i, X202:((((($i > $i) > $i > $i) > $i > $i) > $i) > $i) > $i > $i, X203:((((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i) > $i) > ($i > ($i > $i) > ($i > $i) > $i > $i) > $i, X204:($i > $i) > ($i > $i > ($i > $i) > $i) > $i]:((![X66:$i, X205:$i, X83:$i, X206:$i]:(((X204 @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Empty)))=(X83)))=>(![X211:($i > $i > $i > $i) > $i > $i, X212:$i, X213:((($i > $i) > $i > $i) > ($i > $i) > $i > $i) > $i, X214:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i]:(((X204 @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(X202 @ (^[Z3:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Inj0 @ (Z3 @ (^[Z4:($i > $i) > $i > $i, Z5:$i]:(Z3 @ (^[Z6:($i > $i) > $i > $i, Z7:$i]:(c_Empty))))))) @ Z1)))=(X202 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(X203 @ (^[Z1:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:$i > $i, Z3:$i > $i, Z4:$i]:(Z2 @ (Z2 @ Z1))))) @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty)))))=>(![X229:((($i > $i) > $i > $i) > $i) > (($i > $i) > $i) > ($i > $i) > $i > $i, X230:$i, X231:$i > $i, X232:($i > $i) > $i > $i]:(((X203 @ (^[Z0:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i > $i, Z2:$i > $i, Z3:$i]:(X201 @ (^[Z4:$i > $i > $i > $i]:(c_Empty)) @ (^[Z4:(($i > $i) > $i > $i) > $i, Z5:$i > $i > $i]:(X203 @ (^[Z6:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:$i > $i, Z8:$i > $i, Z9:$i]:(c_setsum @ (X201 @ (^[Z10:$i > $i > $i > $i]:(c_Empty)) @ (^[Z10:(($i > $i) > $i > $i) > $i, Z11:$i > $i > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))))=(X201 @ (^[Z0:$i > $i > $i > $i]:(X204 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty)))) @ (^[Z0:(($i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(X202 @ (^[Z2:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty)))))=>(![X253:$i > $i > ($i > $i) > $i, X254:$i, X255:(($i > $i > $i) > $i > $i > $i) > $i > $i, X256:(($i > $i > $i) > $i) > $i]:(((X203 @ (^[Z0:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i, Z1:$i > $i, Z2:$i > $i, Z3:$i]:(c_Empty)))=(c_setsum @ c_Empty @ (X253 @ (c_setsum @ (X253 @ (c_setsum @ c_Empty @ c_Empty) @ (X202 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty) @ (^[Z0:$i]:(c_Empty))) @ (X204 @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))) @ (X203 @ (^[Z0:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X201 @ (^[Z1:$i > $i > $i > $i]:(X256 @ (^[Z2:$i > $i > $i]:(c_Empty)))) @ (^[Z1:(($i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(X256 @ (^[Z3:$i > $i > $i]:(c_Empty)))))) @ (^[Z0:$i, Z1:$i > $i, Z2:$i > $i, Z3:$i]:(c_Empty))) @ (^[Z0:$i]:(X202 @ (^[Z1:((($i > $i) > $i > $i) > $i > $i) > $i]:(X203 @ (^[Z2:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i > $i, Z4:$i > $i, Z5:$i]:(c_Empty)))) @ (c_setsum @ c_Empty @ (X202 @ (^[Z1:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))))))))=>(![X66:$i, X282:$i, X283:$i > $i, X284:$i]:(((X202 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_setsum @ (X201 @ (^[Z1:$i > $i > $i > $i]:(Z1 @ c_Empty @ X284 @ c_Empty)) @ (^[Z1:(($i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(X204 @ (^[Z3:$i]:(Z1 @ (^[Z4:$i > $i, Z5:$i]:(c_Empty)))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_Empty))))) @ (c_Inj0 @ c_Empty))) @ c_Empty)=(c_Inj1 @ X66)))=>(![X293:((($i > $i) > $i > $i) > $i) > $i, X294:$i, X295:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i, X296:$i > $i > ($i > $i) > $i > $i]:(((X202 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(X294)) @ (c_Inj1 @ c_Empty))=(c_Inj0 @ (X204 @ (^[Z0:$i]:(X296 @ (X203 @ (^[Z1:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X295 @ (^[Z2:$i > $i, Z3:$i > $i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)))) @ (^[Z1:$i, Z2:$i > $i, Z3:$i > $i, Z4:$i]:(c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (^[Z1:$i]:(X203 @ (^[Z2:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(Z1)) @ (^[Z2:$i, Z3:$i > $i, Z4:$i > $i, Z5:$i]:(Z3 @ c_Empty)))) @ (c_Inj0 @ c_Empty))) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(Z0))))))=>(![X66:$i, X316:$i, X83:$i, X317:($i > ($i > $i) > $i > $i) > $i > $i]:(((X201 @ (^[Z0:$i > $i > $i > $i]:(X83)) @ (^[Z0:(($i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(X204 @ (^[Z2:$i]:(c_Inj0 @ (c_setsum @ Z2 @ (X317 @ (^[Z3:$i, Z4:$i > $i, Z5:$i]:(c_Empty)) @ c_Empty)))) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (Z4 @ c_Empty)))))))=(X83)))=>(![X66:$i, X327:(($i > $i) > $i) > ($i > $i > $i) > $i, X83:$i, X328:$i > (($i > $i) > $i) > $i]:(((X201 @ (^[Z0:$i > $i > $i > $i]:(c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ (X202 @ (^[Z1:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))) @ (c_Inj1 @ c_Empty))) @ (^[Z0:(($i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(c_setsum @ X83 @ (c_Inj0 @ (Z1 @ (X203 @ (^[Z2:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i > $i, Z4:$i > $i, Z5:$i]:(c_Empty))) @ (Z1 @ c_Empty @ c_Empty))))))=(X328 @ c_Empty @ (^[Z0:$i > $i]:(Z0 @ c_Empty)))))=>(c_False))))))))))), inference(fof_simplification,[status(thm)],[c_0_8])).
% 53.79/26.63 thf(c_0_13, plain, ![X618:$i]:(((~(c_In @ X618 @ 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_9])])])])])).
% 53.79/26.63 thf(c_0_14, plain, ((c_False)|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_10])])])).
% 53.79/26.63 thf(c_0_15, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11])])])).
% 53.79/26.63 thf(c_0_16, negated_conjecture, ![X986:$i, X987:$i > $i > ($i > $i) > $i, X988:(($i > $i > $i) > $i) > $i, X989:$i, X990:$i, X991:$i, X992:(($i > $i) > ($i > $i) > $i) > ($i > $i) > $i, X993:$i > $i > ($i > $i) > $i > $i, X994:$i, X995:($i > ($i > $i) > $i > $i) > $i > $i, X996:$i, X997:$i > (($i > $i) > $i) > $i]:((((esk55_0 @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Empty)))=(X986))&(((esk55_0 @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(esk53_0 @ (^[Z3:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Inj0 @ (Z3 @ (^[Z4:($i > $i) > $i > $i, Z5:$i]:(Z3 @ (^[Z6:($i > $i) > $i > $i, Z7:$i]:(c_Empty))))))) @ Z1)))=(esk53_0 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(esk54_0 @ (^[Z1:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:$i > $i, Z3:$i > $i, Z4:$i]:(Z2 @ (Z2 @ Z1))))) @ (c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))))&(((esk54_0 @ (^[Z0:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i > $i, Z2:$i > $i, Z3:$i]:(esk52_0 @ (^[Z4:$i > $i > $i > $i]:(c_Empty)) @ (^[Z4:(($i > $i) > $i > $i) > $i, Z5:$i > $i > $i]:(esk54_0 @ (^[Z6:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:$i > $i, Z8:$i > $i, Z9:$i]:(c_setsum @ (esk52_0 @ (^[Z10:$i > $i > $i > $i]:(c_Empty)) @ (^[Z10:(($i > $i) > $i > $i) > $i, Z11:$i > $i > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))))=(esk52_0 @ (^[Z0:$i > $i > $i > $i]:(esk55_0 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty)))) @ (^[Z0:(($i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(esk53_0 @ (^[Z2:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))))&(((esk54_0 @ (^[Z0:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i, Z1:$i > $i, Z2:$i > $i, Z3:$i]:(c_Empty)))=(c_setsum @ c_Empty @ (X987 @ (c_setsum @ (X987 @ (c_setsum @ c_Empty @ c_Empty) @ (esk53_0 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty) @ (^[Z0:$i]:(c_Empty))) @ (esk55_0 @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))) @ (esk54_0 @ (^[Z0:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(esk52_0 @ (^[Z1:$i > $i > $i > $i]:(X988 @ (^[Z2:$i > $i > $i]:(c_Empty)))) @ (^[Z1:(($i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(X988 @ (^[Z3:$i > $i > $i]:(c_Empty)))))) @ (^[Z0:$i, Z1:$i > $i, Z2:$i > $i, Z3:$i]:(c_Empty))) @ (^[Z0:$i]:(esk53_0 @ (^[Z1:((($i > $i) > $i > $i) > $i > $i) > $i]:(esk54_0 @ (^[Z2:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i > $i, Z4:$i > $i, Z5:$i]:(c_Empty)))) @ (c_setsum @ c_Empty @ (esk53_0 @ (^[Z1:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty)))))))&(((esk53_0 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_setsum @ (esk52_0 @ (^[Z1:$i > $i > $i > $i]:(Z1 @ c_Empty @ X990 @ c_Empty)) @ (^[Z1:(($i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(esk55_0 @ (^[Z3:$i]:(Z1 @ (^[Z4:$i > $i, Z5:$i]:(c_Empty)))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_Empty))))) @ (c_Inj0 @ c_Empty))) @ c_Empty)=(c_Inj1 @ X989))&(((esk53_0 @ (^[Z0:((($i > $i) > $i > $i) > $i > $i) > $i]:(X991)) @ (c_Inj1 @ c_Empty))=(c_Inj0 @ (esk55_0 @ (^[Z0:$i]:(X993 @ (esk54_0 @ (^[Z1:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(X992 @ (^[Z2:$i > $i, Z3:$i > $i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)))) @ (^[Z1:$i, Z2:$i > $i, Z3:$i > $i, Z4:$i]:(c_setsum @ c_Empty @ c_Empty))) @ (c_Inj1 @ c_Empty) @ (^[Z1:$i]:(esk54_0 @ (^[Z2:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(Z1)) @ (^[Z2:$i, Z3:$i > $i, Z4:$i > $i, Z5:$i]:(Z3 @ c_Empty)))) @ (c_Inj0 @ c_Empty))) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(Z0)))))&(((esk52_0 @ (^[Z0:$i > $i > $i > $i]:(X994)) @ (^[Z0:(($i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(esk55_0 @ (^[Z2:$i]:(c_Inj0 @ (c_setsum @ Z2 @ (X995 @ (^[Z3:$i, Z4:$i > $i, Z5:$i]:(c_Empty)) @ c_Empty)))) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)) @ (c_Inj0 @ (Z4 @ c_Empty)))))))=(X994))&(((esk52_0 @ (^[Z0:$i > $i > $i > $i]:(c_setsum @ (c_Inj1 @ (c_setsum @ c_Empty @ (esk53_0 @ (^[Z1:((($i > $i) > $i > $i) > $i > $i) > $i]:(c_Empty)) @ c_Empty))) @ (c_Inj1 @ c_Empty))) @ (^[Z0:(($i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(c_setsum @ X996 @ (c_Inj0 @ (Z1 @ (esk54_0 @ (^[Z2:((($i > $i) > $i > $i) > ($i > $i) > $i) > $i > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i > $i, Z4:$i > $i, Z5:$i]:(c_Empty))) @ (Z1 @ c_Empty @ c_Empty))))))=(X997 @ c_Empty @ (^[Z0:$i > $i]:(Z0 @ c_Empty))))&~(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)],[inference(fof_simplification,[status(thm)],[c_0_12])])])])])])).
% 53.79/26.63 thf(c_0_17, plain, ![X2173:$i > $i, X2172:$i, X2171:$i]:(((esk247_0 @ X2171 @ X2172 @ X2173)=(c_Empty))), introduced(definition)).
% 53.79/26.63 thf(c_0_18, plain, ![X2099:$i, X6:$i]:(((esk221_1 @ X6 @ X2099)=(X6))), introduced(definition)).
% 53.79/26.63 thf(c_0_19, plain, ![X410:$i, X411:$i]:(((c_Subq @ X410 @ X411)<=>![X9:$i]:(((c_In @ X9 @ X410)=>(c_In @ X9 @ X411))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 53.79/26.63 thf(c_0_20, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 53.79/26.63 thf(c_0_21, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 53.79/26.63 thf(c_0_22, negated_conjecture, ![X2:$i]:(((esk55_0 @ (esk221_1 @ c_Empty) @ esk247_0)=(X2))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16]), c_0_17]), c_0_18])).
% 53.79/26.63 thf(c_0_23, 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])).
% 53.79/26.63 thf(c_0_24, plain, ![X666:$i, X667:$i, X668:$i, X669:$i, X670:$i]:(((~(c_Subq @ X666 @ X667)|(~(c_In @ X668 @ X666)|(c_In @ X668 @ X667)))&(((c_In @ (esk13_2 @ X669 @ X670) @ X669)|(c_Subq @ X669 @ X670))&(~(c_In @ (esk13_2 @ X669 @ X670) @ X670)|(c_Subq @ X669 @ X670))))), 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_19])])])])])])])).
% 53.79/26.63 thf(c_0_25, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_20, c_0_21])).
% 53.79/26.63 thf(c_0_26, negated_conjecture, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(spm,[status(thm)],[c_0_22, c_0_22])).
% 53.79/26.63 thf(c_0_27, plain, ![X626:$i, X627:$i]:((((~(c_Subq @ X627 @ X626)|(c_iff @ $true @ $true)|~(c_In @ X627 @ (c_Power @ X626)))&((c_Subq @ X627 @ X626)|(c_iff @ $true @ $false)|~(c_In @ X627 @ (c_Power @ X626))))&((~(c_Subq @ X627 @ X626)|(c_iff @ $false @ $true)|(c_In @ X627 @ (c_Power @ X626)))&((c_Subq @ X627 @ X626)|(c_iff @ $false @ $false)|(c_In @ X627 @ (c_Power @ X626)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_23])])])).
% 53.79/26.63 thf(c_0_28, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 53.79/26.63 thf(c_0_29, negated_conjecture, ![X2:$i, X6:$i]:(~((c_In @ X2 @ X6))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 53.79/26.63 thf(c_0_30, plain, ![X614:$o, X615:$o]:(((~(X614)|(X615)|~(c_iff @ ((X614)) @ ((X615))))&(~(X615)|(X614)|~(c_iff @ ((X614)) @ ((X615)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 53.79/26.63 thf(c_0_31, 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_27])).
% 53.79/26.63 thf(c_0_32, plain, ![X2:$i, X6:$i]:((c_Subq @ X2 @ X6)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 53.79/26.63 thf(c_0_33, plain, ~((c_iff @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_30])])])).
% 53.79/26.63 thf(c_0_34, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])]), c_0_29]), c_0_33]), ['proof']).
% 53.79/26.63 % SZS output end CNFRefutation
% 53.79/26.63 % Parsed axioms : 213
% 53.79/26.63 % Removed by relevancy pruning/SinE : 0
% 53.79/26.63 % Initial clauses : 468728
% 53.79/26.63 % Removed in clause preprocessing : 463862
% 53.79/26.63 % Initial clauses in saturation : 4866
% 53.79/26.63 % Processed clauses : 4939
% 53.79/26.63 % ...of these trivial : 269
% 53.79/26.63 % ...subsumed : 3346
% 53.79/26.63 % ...remaining for further processing : 1323
% 53.79/26.63 % Other redundant clauses eliminated : 2
% 53.79/26.63 % Clauses deleted for lack of memory : 0
% 53.79/26.63 % Backward-subsumed : 201
% 53.79/26.63 % Backward-rewritten : 86
% 53.79/26.63 % Generated clauses : 8395
% 53.79/26.63 % ...of the previous two non-redundant : 7995
% 53.79/26.63 % ...aggressively subsumed : 0
% 53.79/26.63 % Contextual simplify-reflections : 19
% 53.79/26.63 % Paramodulations : 8378
% 53.79/26.63 % Factorizations : 0
% 53.79/26.63 % NegExts : 0
% 53.79/26.63 % Equation resolutions : 2
% 53.79/26.63 % Disequality decompositions : 0
% 53.79/26.63 % Total rewrite steps : 982
% 53.79/26.63 % ...of those cached : 734
% 53.79/26.63 % Propositional unsat checks : 0
% 53.79/26.63 % Propositional check models : 0
% 53.79/26.63 % Propositional check unsatisfiable : 0
% 53.79/26.63 % Propositional clauses : 0
% 53.79/26.63 % Propositional clauses after purity: 0
% 53.79/26.63 % Propositional unsat core size : 0
% 53.79/26.63 % Propositional preprocessing time : 0.000
% 53.79/26.63 % Propositional encoding time : 0.000
% 53.79/26.63 % Propositional solver time : 0.000
% 53.79/26.63 % Success case prop preproc time : 0.000
% 53.79/26.63 % Success case prop encoding time : 0.000
% 53.79/26.63 % Success case prop solver time : 0.000
% 53.79/26.63 % Current number of processed clauses : 1028
% 53.79/26.63 % Positive orientable unit clauses : 97
% 53.79/26.63 % Positive unorientable unit clauses: 3
% 53.79/26.63 % Negative unit clauses : 95
% 53.79/26.63 % Non-unit-clauses : 833
% 53.79/26.63 % Current number of unprocessed clauses: 7284
% 53.79/26.63 % ...number of literals in the above : 31393
% 53.79/26.63 % Current number of archived formulas : 0
% 53.79/26.63 % Current number of archived clauses : 293
% 53.79/26.63 % Clause-clause subsumption calls (NU) : 191159
% 53.79/26.63 % Rec. Clause-clause subsumption calls : 163158
% 53.79/26.63 % Non-unit clause-clause subsumptions : 3254
% 53.79/26.63 % Unit Clause-clause subsumption calls : 13957
% 53.79/26.63 % Rewrite failures with RHS unbound : 584
% 53.79/26.63 % BW rewrite match attempts : 2337
% 53.79/26.63 % BW rewrite match successes : 124
% 53.79/26.63 % Condensation attempts : 0
% 53.79/26.63 % Condensation successes : 0
% 53.79/26.63 % Termbank termtop insertions : 20014568
% 53.79/26.63 % Search garbage collected termcells : 2011863
% 53.79/26.63
% 53.79/26.63 % -------------------------------------------------
% 53.79/26.63 % User time : 24.345 s
% 53.79/26.63 % System time : 1.486 s
% 53.79/26.63 % Total time : 25.832 s
% 53.79/26.63 % Maximum resident set size: 1257540 pages
% 53.79/26.63
% 53.79/26.63 % -------------------------------------------------
% 53.79/26.63 % User time : 24.421 s
% 53.79/26.63 % System time : 1.726 s
% 53.79/26.63 % Total time : 26.147 s
% 53.79/26.63 % Maximum resident set size: 5120 pages
% 53.79/26.63 % E exiting
%------------------------------------------------------------------------------