%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SYO856^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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:44:52 AM UTC 2026
% Result : Theorem 56.96s 28.71s
% Output : CNFRefutation 56.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYO856^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 % Computer : n014.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Tue Sep 29 17:18:45 UTC 2026
% 0.10/0.24 % CPUTime :
% 0.10/0.24 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.30 Running higher-order theorem proving
% 0.24/0.35 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.g4zQzYSncN/E---3.1_2955748.p
% 56.96/28.71 % Version: 3.5.1-ho
% 56.96/28.71 % partial match(2): HSLMSMSSSSLCHSA
% 56.96/28.71 % Preprocessing class: HSLMSLSSSSLCHHA.
% 56.96/28.71 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 56.96/28.71 % Starting pre_casc_6 with 1500s (5) cores
% 56.96/28.71 % Starting ehoh_best7 with 300s (1) cores
% 56.96/28.71 % Starting new_bool_8 with 300s (1) cores
% 56.96/28.71 % Starting new_ho_11 with 300s (1) cores
% 56.96/28.71 % new_bool_8 with pid 2955763 completed with status 9
% 56.96/28.71 % ehoh_best7 with pid 2955762 completed with status 0
% 56.96/28.71 % Result found by ehoh_best7
% 56.96/28.71 % partial match(2): HSLMSMSSSSLCHSA
% 56.96/28.71 % Preprocessing class: HSLMSLSSSSLCHHA.
% 56.96/28.71 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 56.96/28.71 % Starting pre_casc_6 with 1500s (5) cores
% 56.96/28.71 % Starting ehoh_best7 with 300s (1) cores
% 56.96/28.71 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 56.96/28.71 % No SInE strategy applied
% 56.96/28.71 % Search class: HGHSM-SMLM33-DHHFFSBC
% 56.96/28.71 % partial match(2): HGHSM-SMLM33-MHFFFSBC
% 56.96/28.71 % Scheduled 7 strats onto 1 cores with 273 seconds (273 total)
% 56.96/28.71 % Starting SubtermCWHack with 25s (1) cores
% 56.96/28.71 % SubtermCWHack with pid 2955951 completed with status 0
% 56.96/28.71 % Result found by SubtermCWHack
% 56.96/28.71 % partial match(2): HSLMSMSSSSLCHSA
% 56.96/28.71 % Preprocessing class: HSLMSLSSSSLCHHA.
% 56.96/28.71 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 56.96/28.71 % Starting pre_casc_6 with 1500s (5) cores
% 56.96/28.71 % Starting ehoh_best7 with 300s (1) cores
% 56.96/28.71 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 56.96/28.71 % No SInE strategy applied
% 56.96/28.71 % Search class: HGHSM-SMLM33-DHHFFSBC
% 56.96/28.71 % partial match(2): HGHSM-SMLM33-MHFFFSBC
% 56.96/28.71 % Scheduled 7 strats onto 1 cores with 273 seconds (273 total)
% 56.96/28.71 % Starting SubtermCWHack with 25s (1) cores
% 56.96/28.71 % Preprocessing time : 0.129 s
% 56.96/28.71
% 56.96/28.71 % Proof found!
% 56.96/28.71 % SZS status Theorem
% 56.96/28.71 % SZS output start CNFRefutation
% 56.96/28.71 thf(decl_24, type, c_False: $o).
% 56.96/28.71 thf(decl_26, type, c_not: $o > $o).
% 56.96/28.71 thf(decl_29, type, c_iff: $o > $o > $o).
% 56.96/28.71 thf(decl_30, type, c_In: $i > $i > $o).
% 56.96/28.71 thf(decl_31, type, c_Subq: $i > $i > $o).
% 56.96/28.71 thf(decl_32, type, c_Empty: $i).
% 56.96/28.71 thf(decl_34, type, c_Power: $i > $i).
% 56.96/28.71 thf(decl_87, type, c_Inj1: $i > $i).
% 56.96/28.71 thf(decl_88, type, c_Inj0: $i > $i).
% 56.96/28.71 thf(decl_91, type, c_setsum: $i > $i > $i).
% 56.96/28.71 thf(decl_269, type, esk1_0: $i).
% 56.96/28.71 thf(decl_281, type, epred143_0: $o).
% 56.96/28.71 thf(decl_284, type, esk13_2: $i > $i > $i).
% 56.96/28.71 thf(decl_327, type, esk52_0: (($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i).
% 56.96/28.71 thf(decl_328, type, esk53_0: ($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i).
% 56.96/28.71 thf(decl_329, type, esk54_0: ($i > $i > $i) > ($i > $i) > $i > $i > $i > $i).
% 56.96/28.71 thf(decl_330, type, esk55_0: (((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i).
% 56.96/28.71 thf(decl_514, type, esk226_0: ($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i).
% 56.96/28.71 thf(decl_515, type, esk227_0: $i > $i > ($i > $i) > $i).
% 56.96/28.71 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox2/tmp/tmp.g4zQzYSncN/E---3.1_2955748.p', ax13)).
% 56.96/28.71 thf(conj, conjecture, ![X201:(($i > $i) > (($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 > $i, X203:($i > $i > $i) > ($i > $i) > $i > $i > $i > $i, X204:(((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i]:((![X205:($i > $i > $i) > $i, X206:$i, X207:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i, X208:(($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i]:(((X204 @ (^[X209:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (X201 @ (^[X210:$i > $i, X211:($i > $i > $i) > $i > $i, X212:$i, X213:$i > $i]:(X202 @ (^[X214:$i, X215:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty))) @ (^[X216:$i, X217:$i, X218:$i > $i]:(c_Empty))) @ (X202 @ (^[X219:$i, X220:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (X203 @ (^[X221:$i, X222:$i]:(X208 @ (^[X169:$i > $i > $i]:(c_Empty)) @ (^[X223:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[X224:$i]:(c_Empty)) @ (X207 @ (^[X225:($i > $i) > $i, X226:$i > $i, X227:$i]:(c_Empty)) @ c_Empty) @ (X202 @ (^[X228:$i, X229:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[X230:$i]:(X230)))=(c_Inj1 @ c_Empty)))=>(![X66:$i, X231:$i, X232:$i > $i, X233:$i]:(((X204 @ (^[X234:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X235:$i]:(X232 @ X235)))=(X232 @ (c_setsum @ (X203 @ (^[X236:$i, X237:$i]:(X202 @ (^[X238:$i, X239:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[X240:$i]:(X240)) @ X231 @ c_Empty @ c_Empty) @ (X202 @ (^[X241:$i, X242:(($i > $i) > $i > $i) > $i > $i > $i]:(X242 @ (^[X243:$i > $i, X244:$i]:(c_Empty)) @ X241 @ (X203 @ (^[X245:$i, X246:$i]:(c_Empty)) @ (^[X247:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty)))))=>(![X66:$i, X248:($i > ($i > $i) > $i) > $i, X83:$i, X249:$i > $i]:(((X203 @ (^[X250:$i, X251:$i]:(c_Empty)) @ (^[X252:$i]:(X203 @ (^[X253:$i, X254:$i]:(X203 @ (^[X255:$i, X256:$i]:(c_Empty)) @ (^[X257:$i]:(c_Empty)) @ (X201 @ (^[X258:$i > $i, X259:($i > $i > $i) > $i > $i, X260:$i, X261:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[X262:$i, X263:$i, X264:$i > $i]:(X201 @ (^[X265:$i > $i, X266:($i > $i > $i) > $i > $i, X174:$i, X267:$i > $i]:(c_Empty)) @ (^[X172:$i, X173:$i, X268:$i > $i]:(c_Empty))))) @ (X249 @ X254) @ X254)) @ (^[X269:$i]:(X252)) @ (X202 @ (^[X270:$i, X271:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (X203 @ (^[X272:$i, X273:$i]:(c_Inj1 @ c_Empty)) @ (^[X274:$i]:(X202 @ (^[X275:$i, X276:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty)) @ (X204 @ (^[X277:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X278:$i]:(c_Empty))) @ (c_Inj1 @ c_Empty) @ (X201 @ (^[X279:$i > $i, X280:($i > $i > $i) > $i > $i, X281:$i, X282:$i > $i]:(c_Empty)) @ (^[X283:$i, X284:$i, X285:$i > $i]:(c_Empty))))) @ (X249 @ c_Empty) @ c_Empty)) @ X66 @ (X201 @ (^[X286:$i > $i, X287:($i > $i > $i) > $i > $i, X288:$i, X289:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[X290:$i, X291:$i, X292:$i > $i]:(c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X202 @ (^[X293:$i, X294:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (c_setsum @ c_Empty @ (X249 @ c_Empty)))=(X66)))=>(![X295:$i > $i > $i, X296:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i, X297:(($i > $i > $i) > $i > $i) > $i, X298:$i > $i]:(((X203 @ (^[X299:$i, X300:$i]:(X203 @ (^[X301:$i, X302:$i]:(c_Empty)) @ (^[X303:$i]:(X299)) @ (X298 @ c_Empty) @ (X297 @ (^[X168:$i > $i > $i, X304:$i]:(c_setsum @ c_Empty @ (X201 @ (^[X305:$i > $i, X306:($i > $i > $i) > $i > $i, X172:$i, X307:$i > $i]:(c_Empty)) @ (^[X308:$i, X309:$i, X310:$i > $i]:(c_Empty)))))) @ c_Empty)) @ (^[X311:$i]:(c_Empty)) @ (X296 @ (^[X312:($i > $i) > $i, X313:$i > $i, X314:$i]:(c_Empty)) @ c_Empty @ (X203 @ (^[X315:$i, X316:$i]:(X204 @ (^[X317:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X316)) @ (^[X318:$i]:(c_Inj0 @ c_Empty)))) @ (^[X319:$i]:(X204 @ (^[X320:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X297 @ (^[X168:$i > $i > $i, X321:$i]:(c_Empty)))) @ (^[X322:$i]:(c_Inj0 @ c_Empty)))) @ (X298 @ c_Empty) @ c_Empty @ (X296 @ (^[X323:($i > $i) > $i, X324:$i > $i, X325:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X298 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X296 @ (^[X326:($i > $i) > $i, X327:$i > $i, X328:$i]:(c_setsum @ c_Empty @ c_Empty)) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X298 @ (c_Inj1 @ c_Empty)))=(X298 @ (c_Inj0 @ c_Empty))))=>(![X66:$i, X329:$i > $i > ($i > $i) > $i > $i, X330:(($i > $i) > $i > $i) > $i, X331:$i]:(((X202 @ (^[X332:$i, X333:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X203 @ (^[X334:$i, X335:$i]:(c_Empty)) @ (^[X336:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X204 @ (^[X337:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X338:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ (X201 @ (^[X339:$i > $i, X340:($i > $i > $i) > $i > $i, X341:$i, X342:$i > $i]:(c_Empty)) @ (^[X343:$i, X344:$i, X345:$i > $i]:(c_Empty))) @ c_Empty) @ (X333 @ (^[X346:$i > $i, X347:$i]:(c_Inj0 @ c_Empty)) @ (X333 @ (^[X348:$i > $i, X349:$i]:(c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))) @ (X203 @ (^[X350:$i, X351:$i]:(c_Empty)) @ (^[X352:$i]:(X330 @ (^[X353:$i > $i, X354:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X203 @ (^[X355:$i, X356:$i]:(c_Empty)) @ (^[X357:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ X66 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))=(X203 @ (^[X358:$i, X359:$i]:(c_setsum @ X331 @ (c_Inj1 @ X331))) @ (^[X360:$i]:(X201 @ (^[X361:$i > $i, X362:($i > $i > $i) > $i > $i, X363:$i, X364:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[X365:$i, X366:$i, X367:$i > $i]:(c_Empty)))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X201 @ (^[X368:$i > $i, X369:($i > $i > $i) > $i > $i, X370:$i, X371:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[X372:$i, X373:$i, X374:$i > $i]:(c_Inj0 @ (X203 @ (^[X375:$i, X376:$i]:(c_Empty)) @ (^[X377:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ (c_Inj1 @ (X330 @ (^[X378:$i > $i, X379:$i]:(c_Inj1 @ c_Empty)))) @ (c_setsum @ (X204 @ (^[X380:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X380 @ (^[X381:$i > $i > $i, X382:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[X383:$i]:(c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))=>(![X384:$i > ($i > $i > $i) > $i > $i, X385:$i, X83:$i, X386:(($i > $i > $i) > $i > $i) > $i]:(((X202 @ (^[X387:$i, X388:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X202 @ (^[X389:$i, X390:(($i > $i) > $i > $i) > $i > $i > $i]:(X387)) @ (c_setsum @ (X203 @ (^[X391:$i, X392:$i]:(c_Empty)) @ (^[X393:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X202 @ (^[X394:$i, X395:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))) @ c_Empty)) @ (X203 @ (^[X396:$i, X397:$i]:(X397)) @ (^[X398:$i]:(X201 @ (^[X399:$i > $i, X400:($i > $i > $i) > $i > $i, X401:$i, X402:$i > $i]:(X401)) @ (^[X403:$i, X404:$i, X405:$i > $i]:(X204 @ (^[X406:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X406 @ (^[X171:$i > $i > $i, X407:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[X408:$i]:(c_Empty)))))) @ X385 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X203 @ (^[X409:$i, X410:$i]:(c_Empty)) @ (^[X411:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))=(X203 @ (^[X412:$i, X413:$i]:(c_Inj0 @ c_Empty)) @ (^[X414:$i]:(X202 @ (^[X415:$i, X416:(($i > $i) > $i > $i) > $i > $i > $i]:(X386 @ (^[X169:$i > $i > $i, X417:$i]:(X416 @ (^[X418:$i > $i, X172:$i]:(X203 @ (^[X173:$i, X174:$i]:(c_Empty)) @ (^[X173:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)) @ c_Empty @ (X202 @ (^[X419:$i, X420:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ c_Empty)) @ (c_Inj0 @ (X204 @ (^[X421:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[X422:$i]:(X204 @ (^[X423:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[X424:$i]:(X203 @ (^[X425:$i, X426:$i]:(c_Empty)) @ (^[X427:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X385 @ (X202 @ (^[X428:$i, X429:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (X203 @ (^[X430:$i, X431:$i]:(c_Empty)) @ (^[X432:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X202 @ (^[X433:$i, X434:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ (X201 @ (^[X435:$i > $i, X436:($i > $i > $i) > $i > $i, X437:$i, X438:$i > $i]:(c_Empty)) @ (^[X439:$i, X440:$i, X441:$i > $i]:(c_Empty))))) @ X385)) @ (c_setsum @ (c_setsum @ X83 @ (X203 @ (^[X442:$i, X443:$i]:(X443)) @ (^[X444:$i]:(X386 @ (^[X445:$i > $i > $i, X446:$i]:(c_Empty)))) @ (X384 @ c_Empty @ (^[X447:$i, X448:$i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X204 @ (^[X449:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X450:$i]:(c_Empty))))) @ (X384 @ (X204 @ (^[X451:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X452:$i]:(X201 @ (^[X453:$i > $i, X454:($i > $i > $i) > $i > $i, X455:$i, X456:$i > $i]:(c_Empty)) @ (^[X457:$i, X458:$i, X459:$i > $i]:(c_Empty))))) @ (^[X460:$i, X461:$i]:(X202 @ (^[X462:$i, X463:(($i > $i) > $i > $i) > $i > $i > $i]:(X463 @ (^[X464:$i > $i, X465:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ X461)) @ X385)))))=>(![X466:($i > $i) > $i, X82:$i > $i, X83:$i, X467:$i]:(((X201 @ (^[X468:$i > $i, X469:($i > $i > $i) > $i > $i, X470:$i, X471:$i > $i]:(c_Empty)) @ (^[X472:$i, X473:$i, X474:$i > $i]:(X201 @ (^[X475:$i > $i, X476:($i > $i > $i) > $i > $i, X477:$i, X478:$i > $i]:(X203 @ (^[X173:$i, X174:$i]:(X478 @ X477)) @ (^[X173:$i]:(X173)) @ c_Empty @ (X478 @ (X204 @ (^[X479:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X173:$i]:(c_Empty)))) @ (X201 @ (^[X480:$i > $i, X481:($i > $i > $i) > $i > $i, X181:$i, X482:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[X173:$i, X174:$i, X483:$i > $i]:(X202 @ (^[X188:$i, X484:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (^[X485:$i, X486:$i, X487:$i > $i]:(c_Inj1 @ (X201 @ (^[X488:$i > $i, X489:($i > $i > $i) > $i > $i, X174:$i, X490:$i > $i]:(c_Empty)) @ (^[X172:$i, X173:$i, X491:$i > $i]:(X487 @ c_Empty))))))))=(X201 @ (^[X492:$i > $i, X493:($i > $i > $i) > $i > $i, X494:$i, X495:$i > $i]:(c_setsum @ (X201 @ (^[X496:$i > $i, X497:($i > $i > $i) > $i > $i, X172:$i, X498:$i > $i]:(c_Empty)) @ (^[X499:$i, X500:$i, X501:$i > $i]:(c_Empty))) @ c_Empty)) @ (^[X502:$i, X503:$i, X504:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))=>(![X66:$i, X505:$i, X83:$i, X506:$i]:(((X201 @ (^[X507:$i > $i, X508:($i > $i > $i) > $i > $i, X509:$i, X510:$i > $i]:(c_Empty)) @ (^[X511:$i, X512:$i, X513:$i > $i]:(c_Empty)))=(X66)))=>(c_False)))))))))), file('/export/starexec/sandbox2/tmp/tmp.g4zQzYSncN/E---3.1_2955748.p', conj)).
% 56.96/28.71 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox2/tmp/tmp.g4zQzYSncN/E---3.1_2955748.p', ax5)).
% 56.96/28.71 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox2/tmp/tmp.g4zQzYSncN/E---3.1_2955748.p', ax11)).
% 56.96/28.71 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.g4zQzYSncN/E---3.1_2955748.p', ax17)).
% 56.96/28.71 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.g4zQzYSncN/E---3.1_2955748.p', ax7)).
% 56.96/28.71 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox2/tmp/tmp.g4zQzYSncN/E---3.1_2955748.p', ax3)).
% 56.96/28.71 thf(c_0_7, plain, ![X579:$o]:(((c_not @ ((X579)))<=>((X579)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 56.96/28.71 thf(c_0_8, negated_conjecture, ~(![X201:(($i > $i) > (($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 > $i, X203:($i > $i > $i) > ($i > $i) > $i > $i > $i > $i, X204:(((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i]:((![X205:($i > $i > $i) > $i, X206:$i, X207:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i, X208:(($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i]:(((X204 @ (^[X209:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (X201 @ (^[X210:$i > $i, X211:($i > $i > $i) > $i > $i, X212:$i, X213:$i > $i]:(X202 @ (^[X214:$i, X215:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty))) @ (^[X216:$i, X217:$i, X218:$i > $i]:(c_Empty))) @ (X202 @ (^[X219:$i, X220:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (X203 @ (^[X221:$i, X222:$i]:(X208 @ (^[X169:$i > $i > $i]:(c_Empty)) @ (^[X223:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[X224:$i]:(c_Empty)) @ (X207 @ (^[X225:($i > $i) > $i, X226:$i > $i, X227:$i]:(c_Empty)) @ c_Empty) @ (X202 @ (^[X228:$i, X229:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[X230:$i]:(X230)))=(c_Inj1 @ c_Empty)))=>(![X66:$i, X231:$i, X232:$i > $i, X233:$i]:(((X204 @ (^[X234:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X235:$i]:(X232 @ X235)))=(X232 @ (c_setsum @ (X203 @ (^[X236:$i, X237:$i]:(X202 @ (^[X238:$i, X239:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[X240:$i]:(X240)) @ X231 @ c_Empty @ c_Empty) @ (X202 @ (^[X241:$i, X242:(($i > $i) > $i > $i) > $i > $i > $i]:(X242 @ (^[X243:$i > $i, X244:$i]:(c_Empty)) @ X241 @ (X203 @ (^[X245:$i, X246:$i]:(c_Empty)) @ (^[X247:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty)))))=>(![X66:$i, X248:($i > ($i > $i) > $i) > $i, X83:$i, X249:$i > $i]:(((X203 @ (^[X250:$i, X251:$i]:(c_Empty)) @ (^[X252:$i]:(X203 @ (^[X253:$i, X254:$i]:(X203 @ (^[X255:$i, X256:$i]:(c_Empty)) @ (^[X257:$i]:(c_Empty)) @ (X201 @ (^[X258:$i > $i, X259:($i > $i > $i) > $i > $i, X260:$i, X261:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[X262:$i, X263:$i, X264:$i > $i]:(X201 @ (^[X265:$i > $i, X266:($i > $i > $i) > $i > $i, X174:$i, X267:$i > $i]:(c_Empty)) @ (^[X172:$i, X173:$i, X268:$i > $i]:(c_Empty))))) @ (X249 @ X254) @ X254)) @ (^[X269:$i]:(X252)) @ (X202 @ (^[X270:$i, X271:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (X203 @ (^[X272:$i, X273:$i]:(c_Inj1 @ c_Empty)) @ (^[X274:$i]:(X202 @ (^[X275:$i, X276:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty)) @ (X204 @ (^[X277:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X278:$i]:(c_Empty))) @ (c_Inj1 @ c_Empty) @ (X201 @ (^[X279:$i > $i, X280:($i > $i > $i) > $i > $i, X281:$i, X282:$i > $i]:(c_Empty)) @ (^[X283:$i, X284:$i, X285:$i > $i]:(c_Empty))))) @ (X249 @ c_Empty) @ c_Empty)) @ X66 @ (X201 @ (^[X286:$i > $i, X287:($i > $i > $i) > $i > $i, X288:$i, X289:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[X290:$i, X291:$i, X292:$i > $i]:(c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X202 @ (^[X293:$i, X294:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (c_setsum @ c_Empty @ (X249 @ c_Empty)))=(X66)))=>(![X295:$i > $i > $i, X296:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i, X297:(($i > $i > $i) > $i > $i) > $i, X298:$i > $i]:(((X203 @ (^[X299:$i, X300:$i]:(X203 @ (^[X301:$i, X302:$i]:(c_Empty)) @ (^[X303:$i]:(X299)) @ (X298 @ c_Empty) @ (X297 @ (^[X168:$i > $i > $i, X304:$i]:(c_setsum @ c_Empty @ (X201 @ (^[X305:$i > $i, X306:($i > $i > $i) > $i > $i, X172:$i, X307:$i > $i]:(c_Empty)) @ (^[X308:$i, X309:$i, X310:$i > $i]:(c_Empty)))))) @ c_Empty)) @ (^[X311:$i]:(c_Empty)) @ (X296 @ (^[X312:($i > $i) > $i, X313:$i > $i, X314:$i]:(c_Empty)) @ c_Empty @ (X203 @ (^[X315:$i, X316:$i]:(X204 @ (^[X317:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X316)) @ (^[X318:$i]:(c_Inj0 @ c_Empty)))) @ (^[X319:$i]:(X204 @ (^[X320:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X297 @ (^[X168:$i > $i > $i, X321:$i]:(c_Empty)))) @ (^[X322:$i]:(c_Inj0 @ c_Empty)))) @ (X298 @ c_Empty) @ c_Empty @ (X296 @ (^[X323:($i > $i) > $i, X324:$i > $i, X325:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X298 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X296 @ (^[X326:($i > $i) > $i, X327:$i > $i, X328:$i]:(c_setsum @ c_Empty @ c_Empty)) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X298 @ (c_Inj1 @ c_Empty)))=(X298 @ (c_Inj0 @ c_Empty))))=>(![X66:$i, X329:$i > $i > ($i > $i) > $i > $i, X330:(($i > $i) > $i > $i) > $i, X331:$i]:(((X202 @ (^[X332:$i, X333:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X203 @ (^[X334:$i, X335:$i]:(c_Empty)) @ (^[X336:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X204 @ (^[X337:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X338:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ (X201 @ (^[X339:$i > $i, X340:($i > $i > $i) > $i > $i, X341:$i, X342:$i > $i]:(c_Empty)) @ (^[X343:$i, X344:$i, X345:$i > $i]:(c_Empty))) @ c_Empty) @ (X333 @ (^[X346:$i > $i, X347:$i]:(c_Inj0 @ c_Empty)) @ (X333 @ (^[X348:$i > $i, X349:$i]:(c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))) @ (X203 @ (^[X350:$i, X351:$i]:(c_Empty)) @ (^[X352:$i]:(X330 @ (^[X353:$i > $i, X354:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X203 @ (^[X355:$i, X356:$i]:(c_Empty)) @ (^[X357:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ X66 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))=(X203 @ (^[X358:$i, X359:$i]:(c_setsum @ X331 @ (c_Inj1 @ X331))) @ (^[X360:$i]:(X201 @ (^[X361:$i > $i, X362:($i > $i > $i) > $i > $i, X363:$i, X364:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[X365:$i, X366:$i, X367:$i > $i]:(c_Empty)))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X201 @ (^[X368:$i > $i, X369:($i > $i > $i) > $i > $i, X370:$i, X371:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[X372:$i, X373:$i, X374:$i > $i]:(c_Inj0 @ (X203 @ (^[X375:$i, X376:$i]:(c_Empty)) @ (^[X377:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ (c_Inj1 @ (X330 @ (^[X378:$i > $i, X379:$i]:(c_Inj1 @ c_Empty)))) @ (c_setsum @ (X204 @ (^[X380:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X380 @ (^[X381:$i > $i > $i, X382:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[X383:$i]:(c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))=>(![X384:$i > ($i > $i > $i) > $i > $i, X385:$i, X83:$i, X386:(($i > $i > $i) > $i > $i) > $i]:(((X202 @ (^[X387:$i, X388:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X202 @ (^[X389:$i, X390:(($i > $i) > $i > $i) > $i > $i > $i]:(X387)) @ (c_setsum @ (X203 @ (^[X391:$i, X392:$i]:(c_Empty)) @ (^[X393:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X202 @ (^[X394:$i, X395:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))) @ c_Empty)) @ (X203 @ (^[X396:$i, X397:$i]:(X397)) @ (^[X398:$i]:(X201 @ (^[X399:$i > $i, X400:($i > $i > $i) > $i > $i, X401:$i, X402:$i > $i]:(X401)) @ (^[X403:$i, X404:$i, X405:$i > $i]:(X204 @ (^[X406:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X406 @ (^[X171:$i > $i > $i, X407:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[X408:$i]:(c_Empty)))))) @ X385 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X203 @ (^[X409:$i, X410:$i]:(c_Empty)) @ (^[X411:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))=(X203 @ (^[X412:$i, X413:$i]:(c_Inj0 @ c_Empty)) @ (^[X414:$i]:(X202 @ (^[X415:$i, X416:(($i > $i) > $i > $i) > $i > $i > $i]:(X386 @ (^[X169:$i > $i > $i, X417:$i]:(X416 @ (^[X418:$i > $i, X172:$i]:(X203 @ (^[X173:$i, X174:$i]:(c_Empty)) @ (^[X173:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)) @ c_Empty @ (X202 @ (^[X419:$i, X420:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ c_Empty)) @ (c_Inj0 @ (X204 @ (^[X421:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[X422:$i]:(X204 @ (^[X423:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[X424:$i]:(X203 @ (^[X425:$i, X426:$i]:(c_Empty)) @ (^[X427:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X385 @ (X202 @ (^[X428:$i, X429:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (X203 @ (^[X430:$i, X431:$i]:(c_Empty)) @ (^[X432:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X202 @ (^[X433:$i, X434:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ (X201 @ (^[X435:$i > $i, X436:($i > $i > $i) > $i > $i, X437:$i, X438:$i > $i]:(c_Empty)) @ (^[X439:$i, X440:$i, X441:$i > $i]:(c_Empty))))) @ X385)) @ (c_setsum @ (c_setsum @ X83 @ (X203 @ (^[X442:$i, X443:$i]:(X443)) @ (^[X444:$i]:(X386 @ (^[X445:$i > $i > $i, X446:$i]:(c_Empty)))) @ (X384 @ c_Empty @ (^[X447:$i, X448:$i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X204 @ (^[X449:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X450:$i]:(c_Empty))))) @ (X384 @ (X204 @ (^[X451:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X452:$i]:(X201 @ (^[X453:$i > $i, X454:($i > $i > $i) > $i > $i, X455:$i, X456:$i > $i]:(c_Empty)) @ (^[X457:$i, X458:$i, X459:$i > $i]:(c_Empty))))) @ (^[X460:$i, X461:$i]:(X202 @ (^[X462:$i, X463:(($i > $i) > $i > $i) > $i > $i > $i]:(X463 @ (^[X464:$i > $i, X465:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ X461)) @ X385)))))=>(![X466:($i > $i) > $i, X82:$i > $i, X83:$i, X467:$i]:(((X201 @ (^[X468:$i > $i, X469:($i > $i > $i) > $i > $i, X470:$i, X471:$i > $i]:(c_Empty)) @ (^[X472:$i, X473:$i, X474:$i > $i]:(X201 @ (^[X475:$i > $i, X476:($i > $i > $i) > $i > $i, X477:$i, X478:$i > $i]:(X203 @ (^[X173:$i, X174:$i]:(X478 @ X477)) @ (^[X173:$i]:(X173)) @ c_Empty @ (X478 @ (X204 @ (^[X479:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[X173:$i]:(c_Empty)))) @ (X201 @ (^[X480:$i > $i, X481:($i > $i > $i) > $i > $i, X181:$i, X482:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[X173:$i, X174:$i, X483:$i > $i]:(X202 @ (^[X188:$i, X484:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (^[X485:$i, X486:$i, X487:$i > $i]:(c_Inj1 @ (X201 @ (^[X488:$i > $i, X489:($i > $i > $i) > $i > $i, X174:$i, X490:$i > $i]:(c_Empty)) @ (^[X172:$i, X173:$i, X491:$i > $i]:(X487 @ c_Empty))))))))=(X201 @ (^[X492:$i > $i, X493:($i > $i > $i) > $i > $i, X494:$i, X495:$i > $i]:(c_setsum @ (X201 @ (^[X496:$i > $i, X497:($i > $i > $i) > $i > $i, X172:$i, X498:$i > $i]:(c_Empty)) @ (^[X499:$i, X500:$i, X501:$i > $i]:(c_Empty))) @ c_Empty)) @ (^[X502:$i, X503:$i, X504:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))=>(![X66:$i, X505:$i, X83:$i, X506:$i]:(((X201 @ (^[X507:$i > $i, X508:($i > $i > $i) > $i > $i, X509:$i, X510:$i > $i]:(c_Empty)) @ (^[X511:$i, X512:$i, X513:$i > $i]:(c_Empty)))=(X66)))=>(c_False))))))))))), inference(assume_negation,[status(cth)],[conj])).
% 56.96/28.71 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])).
% 56.96/28.71 thf(c_0_10, plain, ![X827:$o]:(((~(c_not @ ((X827)))|(~(X827)|(c_False)))&(((X827)|(c_not @ ((X827))))&(~(c_False)|(c_not @ ((X827))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])).
% 56.96/28.71 thf(c_0_11, plain, ![X825:$o]:(((~(c_False)|(X825))&(~(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])])])])])).
% 56.96/28.71 thf(c_0_12, negated_conjecture, ~(![X201:(($i > $i) > (($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 > $i, X203:($i > $i > $i) > ($i > $i) > $i > $i > $i > $i, X204:(((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i]:((![X205:($i > $i > $i) > $i, X206:$i, X207:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i, X208:(($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i]:(((X204 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (X201 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(X202 @ (^[Z5:$i, Z6:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty))) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty))) @ (X202 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (X203 @ (^[Z1:$i, Z2:$i]:(X208 @ (^[Z3:$i > $i > $i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z1:$i]:(c_Empty)) @ (X207 @ (^[Z1:($i > $i) > $i, Z2:$i > $i, Z3:$i]:(c_Empty)) @ c_Empty) @ (X202 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Z0:$i]:(Z0)))=(c_Inj1 @ c_Empty)))=>(![X66:$i, X231:$i, X232:$i > $i, X233:$i]:(((X204 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ X232)=(X232 @ (c_setsum @ (X203 @ (^[Z0:$i, Z1:$i]:(X202 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Z0:$i]:(Z0)) @ X231 @ c_Empty @ c_Empty) @ (X202 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Empty)) @ Z0 @ (X203 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty)))))=>(![X66:$i, X248:($i > ($i > $i) > $i) > $i, X83:$i, X249:$i > $i]:(((X203 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(X203 @ (^[Z1:$i, Z2:$i]:(X203 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ (X201 @ (^[Z3:$i > $i, Z4:($i > $i > $i) > $i > $i, Z5:$i, Z6:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(X201 @ (^[Z6:$i > $i, Z7:($i > $i > $i) > $i > $i, Z8:$i, Z9:$i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:$i, Z8:$i > $i]:(c_Empty))))) @ (X249 @ Z2) @ Z2)) @ (^[Z1:$i]:(Z0)) @ (X202 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (X203 @ (^[Z1:$i, Z2:$i]:(c_Inj1 @ c_Empty)) @ (^[Z1:$i]:(X202 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty)) @ (X204 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i]:(c_Empty))) @ (c_Inj1 @ c_Empty) @ (X201 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty))))) @ (X249 @ c_Empty) @ c_Empty)) @ X66 @ (X201 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (X202 @ (^[Z3:$i, Z4:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (c_setsum @ c_Empty @ (X249 @ c_Empty)))=(X66)))=>(![X295:$i > $i > $i, X296:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i, X297:(($i > $i > $i) > $i > $i) > $i, X298:$i > $i]:(((X203 @ (^[Z0:$i, Z1:$i]:(X203 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(Z0)) @ (X298 @ c_Empty) @ (X297 @ (^[Z2:$i > $i > $i, Z3:$i]:(c_setsum @ c_Empty @ (X201 @ (^[Z4:$i > $i, Z5:($i > $i > $i) > $i > $i, Z6:$i, Z7:$i > $i]:(c_Empty)) @ (^[Z4:$i, Z5:$i, Z6:$i > $i]:(c_Empty)))))) @ c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ (X296 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_Empty)) @ c_Empty @ (X203 @ (^[Z0:$i, Z1:$i]:(X204 @ (^[Z2:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z1)) @ (^[Z2:$i]:(c_Inj0 @ c_Empty)))) @ (^[Z0:$i]:(X204 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X297 @ (^[Z2:$i > $i > $i, Z3:$i]:(c_Empty)))) @ (^[Z1:$i]:(c_Inj0 @ c_Empty)))) @ (X298 @ c_Empty) @ c_Empty @ (X296 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X298 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X296 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_setsum @ c_Empty @ c_Empty)) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X298 @ (c_Inj1 @ c_Empty)))=(X298 @ (c_Inj0 @ c_Empty))))=>(![X66:$i, X329:$i > $i > ($i > $i) > $i > $i, X330:(($i > $i) > $i > $i) > $i, X331:$i]:(((X202 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (X203 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X204 @ (^[Z2:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ (X201 @ (^[Z2:$i > $i, Z3:($i > $i > $i) > $i > $i, Z4:$i, Z5:$i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_Empty))) @ c_Empty) @ (Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Inj0 @ c_Empty)) @ (Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))) @ (X203 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(X330 @ (^[Z1:$i > $i, Z2:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X203 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ X66 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))=(X203 @ (^[Z0:$i, Z1:$i]:(c_setsum @ X331 @ (c_Inj1 @ X331))) @ (^[Z0:$i]:(X201 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty)))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (X201 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Inj0 @ (X203 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ (c_Inj1 @ (X330 @ (^[Z0:$i > $i, Z1:$i]:(c_Inj1 @ c_Empty)))) @ (c_setsum @ (X204 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z0 @ (^[Z1:$i > $i > $i, Z2:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z0:$i]:(c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))))))=>(![X384:$i > ($i > $i > $i) > $i > $i, X385:$i, X83:$i, X386:(($i > $i > $i) > $i > $i) > $i]:(((X202 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X202 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(Z0)) @ (c_setsum @ (X203 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (X202 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))) @ c_Empty)) @ (X203 @ (^[Z0:$i, Z1:$i]:(Z1)) @ (^[Z0:$i]:(X201 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(Z3)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(X204 @ (^[Z4:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z4 @ (^[Z5:$i > $i > $i, Z6:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z4:$i]:(c_Empty)))))) @ X385 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (X203 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))=(X203 @ (^[Z0:$i, Z1:$i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i]:(X202 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(X386 @ (^[Z3:$i > $i > $i, Z4:$i]:(Z2 @ (^[Z5:$i > $i, Z6:$i]:(X203 @ (^[Z7:$i, Z8:$i]:(c_Empty)) @ (^[Z7:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)) @ c_Empty @ (X202 @ (^[Z5:$i, Z6:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ c_Empty)) @ (c_Inj0 @ (X204 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Z0:$i]:(X204 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[Z1:$i]:(X203 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X385 @ (X202 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (X203 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (X202 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ (X201 @ (^[Z2:$i > $i, Z3:($i > $i > $i) > $i > $i, Z4:$i, Z5:$i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_Empty))))) @ X385)) @ (c_setsum @ (c_setsum @ X83 @ (X203 @ (^[Z0:$i, Z1:$i]:(Z1)) @ (^[Z0:$i]:(X386 @ (^[Z1:$i > $i > $i, Z2:$i]:(c_Empty)))) @ (X384 @ c_Empty @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (X204 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty))))) @ (X384 @ (X204 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i]:(X201 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty))))) @ (^[Z0:$i]:(X202 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(Z2 @ (^[Z3:$i > $i, Z4:$i]:(c_Empty)) @ c_Empty @ c_Empty)))) @ X385)))))=>(![X466:($i > $i) > $i, X82:$i > $i, X83:$i, X467:$i]:(((X201 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(X201 @ (^[Z3:$i > $i, Z4:($i > $i > $i) > $i > $i, Z5:$i, Z6:$i > $i]:(X203 @ (^[Z7:$i, Z8:$i]:(Z6 @ Z5)) @ (^[Z7:$i]:(Z7)) @ c_Empty @ (Z6 @ (X204 @ (^[Z7:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z7:$i]:(c_Empty)))) @ (X201 @ (^[Z7:$i > $i, Z8:($i > $i > $i) > $i > $i, Z9:$i, Z10:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[Z7:$i, Z8:$i, Z9:$i > $i]:(X202 @ (^[Z10:$i, Z11:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_Inj1 @ (X201 @ (^[Z6:$i > $i, Z7:($i > $i > $i) > $i > $i, Z8:$i, Z9:$i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:$i, Z8:$i > $i]:(Z5 @ c_Empty))))))))=(X201 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_setsum @ (X201 @ (^[Z4:$i > $i, Z5:($i > $i > $i) > $i > $i, Z6:$i, Z7:$i > $i]:(c_Empty)) @ (^[Z4:$i, Z5:$i, Z6:$i > $i]:(c_Empty))) @ c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))=>(![X66:$i, X505:$i, X83:$i, X506:$i]:(((X201 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Empty)))=(X66)))=>(c_False))))))))))), inference(fool_unroll,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_8])])).
% 56.96/28.71 thf(c_0_13, plain, ![X794:$i]:(((~(c_In @ X794 @ 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])])])])])).
% 56.96/28.71 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])])])).
% 56.96/28.71 thf(c_0_15, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11])])])).
% 56.96/28.71 thf(c_0_16, negated_conjecture, ![X1162:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i, X1163:(($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i, X1164:$i, X1165:$i > $i, X1166:$i, X1167:$i > $i, X1168:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i, X1169:(($i > $i > $i) > $i > $i) > $i, X1170:$i > $i, X1171:$i, X1172:(($i > $i) > $i > $i) > $i, X1173:$i, X1174:$i > ($i > $i > $i) > $i > $i, X1175:$i, X1176:$i, X1177:(($i > $i > $i) > $i > $i) > $i, X1178:$i]:((((esk55_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (esk52_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(esk53_0 @ (^[Z5:$i, Z6:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty))) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty))) @ (esk53_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (esk54_0 @ (^[Z1:$i, Z2:$i]:(X1163 @ (^[Z3:$i > $i > $i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z1:$i]:(c_Empty)) @ (X1162 @ (^[Z1:($i > $i) > $i, Z2:$i > $i, Z3:$i]:(c_Empty)) @ c_Empty) @ (esk53_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty))))) @ (^[Z0:$i]:(Z0)))=(c_Inj1 @ c_Empty))&(((esk55_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ X1165)=(X1165 @ (c_setsum @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(esk53_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Z0:$i]:(Z0)) @ X1164 @ c_Empty @ c_Empty) @ (esk53_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Empty)) @ Z0 @ (esk54_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty))))&(((esk54_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(esk54_0 @ (^[Z1:$i, Z2:$i]:(esk54_0 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ (esk52_0 @ (^[Z3:$i > $i, Z4:($i > $i > $i) > $i > $i, Z5:$i, Z6:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(esk52_0 @ (^[Z6:$i > $i, Z7:($i > $i > $i) > $i > $i, Z8:$i, Z9:$i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:$i, Z8:$i > $i]:(c_Empty))))) @ (X1167 @ Z2) @ Z2)) @ (^[Z1:$i]:(Z0)) @ (esk53_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (esk54_0 @ (^[Z1:$i, Z2:$i]:(c_Inj1 @ c_Empty)) @ (^[Z1:$i]:(esk53_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty)) @ (esk55_0 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i]:(c_Empty))) @ (c_Inj1 @ c_Empty) @ (esk52_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty))))) @ (X1167 @ c_Empty) @ c_Empty)) @ X1166 @ (esk52_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Inj0 @ (c_setsum @ (c_Inj0 @ c_Empty) @ (esk53_0 @ (^[Z3:$i, Z4:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (c_setsum @ c_Empty @ (X1167 @ c_Empty)))=(X1166))&(((esk54_0 @ (^[Z0:$i, Z1:$i]:(esk54_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(Z0)) @ (X1170 @ c_Empty) @ (X1169 @ (^[Z2:$i > $i > $i, Z3:$i]:(c_setsum @ c_Empty @ (esk52_0 @ (^[Z4:$i > $i, Z5:($i > $i > $i) > $i > $i, Z6:$i, Z7:$i > $i]:(c_Empty)) @ (^[Z4:$i, Z5:$i, Z6:$i > $i]:(c_Empty)))))) @ c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ (X1168 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_Empty)) @ c_Empty @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(esk55_0 @ (^[Z2:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z1)) @ (^[Z2:$i]:(c_Inj0 @ c_Empty)))) @ (^[Z0:$i]:(esk55_0 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X1169 @ (^[Z2:$i > $i > $i, Z3:$i]:(c_Empty)))) @ (^[Z1:$i]:(c_Inj0 @ c_Empty)))) @ (X1170 @ c_Empty) @ c_Empty @ (X1168 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (c_Inj0 @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X1170 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X1168 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_setsum @ c_Empty @ c_Empty)) @ c_Empty @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty)))) @ (X1170 @ (c_Inj1 @ c_Empty)))=(X1170 @ (c_Inj0 @ c_Empty)))&(((esk53_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (esk54_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (esk55_0 @ (^[Z2:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ (esk52_0 @ (^[Z2:$i > $i, Z3:($i > $i > $i) > $i > $i, Z4:$i, Z5:$i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_Empty))) @ c_Empty) @ (Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Inj0 @ c_Empty)) @ (Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty))))) @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(X1172 @ (^[Z1:$i > $i, Z2:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (esk54_0 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ X1171 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))=(esk54_0 @ (^[Z0:$i, Z1:$i]:(c_setsum @ X1173 @ (c_Inj1 @ X1173))) @ (^[Z0:$i]:(esk52_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty)))) @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ (esk52_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Inj1 @ c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Inj0 @ (esk54_0 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ (c_Inj1 @ (X1172 @ (^[Z0:$i > $i, Z1:$i]:(c_Inj1 @ c_Empty)))) @ (c_setsum @ (esk55_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z0 @ (^[Z1:$i > $i > $i, Z2:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z0:$i]:(c_Inj1 @ c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))&(((esk53_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (esk53_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(Z0)) @ (c_setsum @ (esk54_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (esk53_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))) @ c_Empty)) @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(Z1)) @ (^[Z0:$i]:(esk52_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(Z3)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(esk55_0 @ (^[Z4:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z4 @ (^[Z5:$i > $i > $i, Z6:$i > $i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z4:$i]:(c_Empty)))))) @ X1175 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))=(esk54_0 @ (^[Z0:$i, Z1:$i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i]:(esk53_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(X1177 @ (^[Z3:$i > $i > $i, Z4:$i]:(Z2 @ (^[Z5:$i > $i, Z6:$i]:(esk54_0 @ (^[Z7:$i, Z8:$i]:(c_Empty)) @ (^[Z7:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)) @ c_Empty @ (esk53_0 @ (^[Z5:$i, Z6:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ c_Empty)) @ (c_Inj0 @ (esk55_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Z0:$i]:(esk55_0 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[Z1:$i]:(esk54_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X1175 @ (esk53_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (esk53_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ (esk52_0 @ (^[Z2:$i > $i, Z3:($i > $i > $i) > $i > $i, Z4:$i, Z5:$i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_Empty))))) @ X1175)) @ (c_setsum @ (c_setsum @ X1176 @ (esk54_0 @ (^[Z0:$i, Z1:$i]:(Z1)) @ (^[Z0:$i]:(X1177 @ (^[Z1:$i > $i > $i, Z2:$i]:(c_Empty)))) @ (X1174 @ c_Empty @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (esk55_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty))))) @ (X1174 @ (esk55_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i]:(esk52_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty))))) @ (^[Z0:$i]:(esk53_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(Z2 @ (^[Z3:$i > $i, Z4:$i]:(c_Empty)) @ c_Empty @ c_Empty)))) @ X1175))))&(((esk52_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(esk52_0 @ (^[Z3:$i > $i, Z4:($i > $i > $i) > $i > $i, Z5:$i, Z6:$i > $i]:(esk54_0 @ (^[Z7:$i, Z8:$i]:(Z6 @ Z5)) @ (^[Z7:$i]:(Z7)) @ c_Empty @ (Z6 @ (esk55_0 @ (^[Z7:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z7:$i]:(c_Empty)))) @ (esk52_0 @ (^[Z7:$i > $i, Z8:($i > $i > $i) > $i > $i, Z9:$i, Z10:$i > $i]:(c_Inj0 @ c_Empty)) @ (^[Z7:$i, Z8:$i, Z9:$i > $i]:(esk53_0 @ (^[Z10:$i, Z11:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_Inj1 @ (esk52_0 @ (^[Z6:$i > $i, Z7:($i > $i > $i) > $i > $i, Z8:$i, Z9:$i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:$i, Z8:$i > $i]:(Z5 @ c_Empty))))))))=(esk52_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_setsum @ (esk52_0 @ (^[Z4:$i > $i, Z5:($i > $i > $i) > $i > $i, Z6:$i, Z7:$i > $i]:(c_Empty)) @ (^[Z4:$i, Z5:$i, Z6:$i > $i]:(c_Empty))) @ c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ c_Empty @ c_Empty))))&(((esk52_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_Empty)))=(X1178))&~(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])])])])])])).
% 56.96/28.71 thf(c_0_17, plain, ![X2313:$i > $i, X2312:$i, X2311:$i]:(((esk227_0 @ X2311 @ X2312 @ X2313)=(c_Empty))), introduced(definition)).
% 56.96/28.71 thf(c_0_18, plain, ![X2310:$i > $i, X2309:$i, X2308:($i > $i > $i) > $i > $i, X2307:$i > $i]:(((esk226_0 @ X2307 @ X2308 @ X2309 @ X2310)=(c_Empty))), introduced(definition)).
% 56.96/28.71 thf(c_0_19, plain, ![X586:$i, X587:$i]:(((c_Subq @ X586 @ X587)<=>![X9:$i]:(((c_In @ X9 @ X586)=>(c_In @ X9 @ X587))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 56.96/28.71 thf(c_0_20, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 56.96/28.71 thf(c_0_21, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 56.96/28.71 thf(c_0_22, negated_conjecture, ![X2:$i]:(((esk52_0 @ esk226_0 @ esk227_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])).
% 56.96/28.71 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])).
% 56.96/28.71 thf(c_0_24, plain, ![X842:$i, X843:$i, X844:$i, X845:$i, X846:$i]:(((~(c_Subq @ X842 @ X843)|(~(c_In @ X844 @ X842)|(c_In @ X844 @ X843)))&(((c_In @ (esk13_2 @ X845 @ X846) @ X845)|(c_Subq @ X845 @ X846))&(~(c_In @ (esk13_2 @ X845 @ X846) @ X846)|(c_Subq @ X845 @ X846))))), 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])])])])])])])).
% 56.96/28.71 thf(c_0_25, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_20, c_0_21])).
% 56.96/28.71 thf(c_0_26, negated_conjecture, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(spm,[status(thm)],[c_0_22, c_0_22])).
% 56.96/28.71 thf(c_0_27, plain, ![X802:$i, X803:$i]:((((~(c_Subq @ X803 @ X802)|(c_iff @ $true @ $true)|~(c_In @ X803 @ (c_Power @ X802)))&((c_Subq @ X803 @ X802)|(c_iff @ $true @ $false)|~(c_In @ X803 @ (c_Power @ X802))))&((~(c_Subq @ X803 @ X802)|(c_iff @ $false @ $true)|(c_In @ X803 @ (c_Power @ X802)))&((c_Subq @ X803 @ X802)|(c_iff @ $false @ $false)|(c_In @ X803 @ (c_Power @ X802)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_23])])])).
% 56.96/28.71 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])).
% 56.96/28.71 thf(c_0_29, negated_conjecture, ![X2:$i, X6:$i]:(~((c_In @ X2 @ X6))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 56.96/28.71 thf(c_0_30, plain, ![X790:$o, X791:$o]:(((~(X790)|(X791)|~(c_iff @ ((X790)) @ ((X791))))&(~(X791)|(X790)|~(c_iff @ ((X790)) @ ((X791)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 56.96/28.71 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])).
% 56.96/28.71 thf(c_0_32, plain, ![X2:$i, X6:$i]:((c_Subq @ X2 @ X6)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 56.96/28.71 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])])])).
% 56.96/28.71 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']).
% 56.96/28.71 % SZS output end CNFRefutation
% 56.96/28.71 % Parsed axioms : 213
% 56.96/28.71 % Removed by relevancy pruning/SinE : 0
% 56.96/28.71 % Initial clauses : 468742
% 56.96/28.71 % Removed in clause preprocessing : 463862
% 56.96/28.71 % Initial clauses in saturation : 4880
% 56.96/28.71 % Processed clauses : 4939
% 56.96/28.71 % ...of these trivial : 258
% 56.96/28.71 % ...subsumed : 3385
% 56.96/28.71 % ...remaining for further processing : 1295
% 56.96/28.71 % Other redundant clauses eliminated : 0
% 56.96/28.71 % Clauses deleted for lack of memory : 0
% 56.96/28.71 % Backward-subsumed : 190
% 56.96/28.71 % Backward-rewritten : 71
% 56.96/28.71 % Generated clauses : 8329
% 56.96/28.71 % ...of the previous two non-redundant : 7922
% 56.96/28.71 % ...aggressively subsumed : 0
% 56.96/28.71 % Contextual simplify-reflections : 21
% 56.96/28.71 % Paramodulations : 8314
% 56.96/28.71 % Factorizations : 0
% 56.96/28.71 % NegExts : 0
% 56.96/28.71 % Equation resolutions : 0
% 56.96/28.71 % Disequality decompositions : 0
% 56.96/28.71 % Total rewrite steps : 931
% 56.96/28.71 % ...of those cached : 720
% 56.96/28.71 % Propositional unsat checks : 0
% 56.96/28.71 % Propositional check models : 0
% 56.96/28.71 % Propositional check unsatisfiable : 0
% 56.96/28.71 % Propositional clauses : 0
% 56.96/28.71 % Propositional clauses after purity: 0
% 56.96/28.71 % Propositional unsat core size : 0
% 56.96/28.71 % Propositional preprocessing time : 0.000
% 56.96/28.71 % Propositional encoding time : 0.000
% 56.96/28.71 % Propositional solver time : 0.000
% 56.96/28.71 % Success case prop preproc time : 0.000
% 56.96/28.71 % Success case prop encoding time : 0.000
% 56.96/28.71 % Success case prop solver time : 0.000
% 56.96/28.71 % Current number of processed clauses : 1028
% 56.96/28.71 % Positive orientable unit clauses : 98
% 56.96/28.71 % Positive unorientable unit clauses: 3
% 56.96/28.71 % Negative unit clauses : 95
% 56.96/28.71 % Non-unit-clauses : 832
% 56.96/28.71 % Current number of unprocessed clauses: 7234
% 56.96/28.71 % ...number of literals in the above : 31224
% 56.96/28.71 % Current number of archived formulas : 0
% 56.96/28.71 % Current number of archived clauses : 267
% 56.96/28.71 % Clause-clause subsumption calls (NU) : 184208
% 56.96/28.71 % Rec. Clause-clause subsumption calls : 157802
% 56.96/28.71 % Non-unit clause-clause subsumptions : 3286
% 56.96/28.71 % Unit Clause-clause subsumption calls : 17722
% 56.96/28.71 % Rewrite failures with RHS unbound : 648
% 56.96/28.71 % BW rewrite match attempts : 2109
% 56.96/28.71 % BW rewrite match successes : 60
% 56.96/28.71 % Condensation attempts : 0
% 56.96/28.71 % Condensation successes : 0
% 56.96/28.71 % Termbank termtop insertions : 20018512
% 56.96/28.71 % Search garbage collected termcells : 2012504
% 56.96/28.71
% 56.96/28.71 % -------------------------------------------------
% 56.96/28.71 % User time : 26.291 s
% 56.96/28.71 % System time : 1.527 s
% 56.96/28.71 % Total time : 27.817 s
% 56.96/28.71 % Maximum resident set size: 1258172 pages
% 56.96/28.71
% 56.96/28.71 % -------------------------------------------------
% 56.96/28.71 % User time : 26.724 s
% 56.96/28.71 % System time : 1.804 s
% 56.96/28.71 % Total time : 28.528 s
% 56.96/28.71 % Maximum resident set size: 5376 pages
% 56.96/28.71 % E exiting
%------------------------------------------------------------------------------