%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO854^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 : n008.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 36.26s 18.31s
% Output : CNFRefutation 36.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYO854^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.25 % Computer : n008.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Tue Sep 29 17:19:24 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.32 Running higher-order theorem proving
% 0.22/0.37 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.IfXXGXUPnP/E---3.1_3460431.p
% 36.26/18.31 % Version: 3.5.1-ho
% 36.26/18.31 % partial match(2): HSLMSMSSSSLCHSA
% 36.26/18.31 % Preprocessing class: HSLMSLSSSSLCHHA.
% 36.26/18.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 36.26/18.31 % Starting pre_casc_6 with 1500s (5) cores
% 36.26/18.31 % Starting ehoh_best7 with 300s (1) cores
% 36.26/18.31 % Starting new_bool_8 with 300s (1) cores
% 36.26/18.31 % Starting new_ho_11 with 300s (1) cores
% 36.26/18.31 % new_bool_8 with pid 3460446 completed with status 9
% 36.26/18.31 % new_ho_11 with pid 3460447 completed with status 0
% 36.26/18.31 % Result found by new_ho_11
% 36.26/18.31 % partial match(2): HSLMSMSSSSLCHSA
% 36.26/18.31 % Preprocessing class: HSLMSLSSSSLCHHA.
% 36.26/18.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 36.26/18.31 % Starting pre_casc_6 with 1500s (5) cores
% 36.26/18.31 % Starting ehoh_best7 with 300s (1) cores
% 36.26/18.31 % Starting new_bool_8 with 300s (1) cores
% 36.26/18.31 % Starting new_ho_11 with 300s (1) cores
% 36.26/18.31 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 36.26/18.31 % No SInE strategy applied
% 36.26/18.31 % Search class: HGHSM-SMLM33-DHHFFSBC
% 36.26/18.31 % partial match(2): HGHSM-SMLM33-MHFFFSBC
% 36.26/18.31 % Scheduled 7 strats onto 1 cores with 284 seconds (284 total)
% 36.26/18.31 % Starting SubtermCWHack with 26s (1) cores
% 36.26/18.31 % SubtermCWHack with pid 3460530 completed with status 0
% 36.26/18.31 % Result found by SubtermCWHack
% 36.26/18.31 % partial match(2): HSLMSMSSSSLCHSA
% 36.26/18.31 % Preprocessing class: HSLMSLSSSSLCHHA.
% 36.26/18.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 36.26/18.31 % Starting pre_casc_6 with 1500s (5) cores
% 36.26/18.31 % Starting ehoh_best7 with 300s (1) cores
% 36.26/18.31 % Starting new_bool_8 with 300s (1) cores
% 36.26/18.31 % Starting new_ho_11 with 300s (1) cores
% 36.26/18.31 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 36.26/18.31 % No SInE strategy applied
% 36.26/18.31 % Search class: HGHSM-SMLM33-DHHFFSBC
% 36.26/18.31 % partial match(2): HGHSM-SMLM33-MHFFFSBC
% 36.26/18.31 % Scheduled 7 strats onto 1 cores with 284 seconds (284 total)
% 36.26/18.31 % Starting SubtermCWHack with 26s (1) cores
% 36.26/18.31 % Preprocessing time : 0.174 s
% 36.26/18.31
% 36.26/18.31 % Proof found!
% 36.26/18.31 % SZS status Theorem
% 36.26/18.31 % SZS output start CNFRefutation
% 36.26/18.31 thf(decl_24, type, c_False: $o).
% 36.26/18.31 thf(decl_26, type, c_not: $o > $o).
% 36.26/18.31 thf(decl_29, type, c_iff: $o > $o > $o).
% 36.26/18.31 thf(decl_30, type, c_In: $i > $i > $o).
% 36.26/18.31 thf(decl_31, type, c_Subq: $i > $i > $o).
% 36.26/18.31 thf(decl_32, type, c_Empty: $i).
% 36.26/18.31 thf(decl_34, type, c_Power: $i > $i).
% 36.26/18.31 thf(decl_87, type, c_Inj1: $i > $i).
% 36.26/18.31 thf(decl_88, type, c_Inj0: $i > $i).
% 36.26/18.31 thf(decl_91, type, c_setsum: $i > $i > $i).
% 36.26/18.31 thf(decl_269, type, esk1_0: $i).
% 36.26/18.31 thf(decl_281, type, epred143_0: $o).
% 36.26/18.31 thf(decl_284, type, esk13_2: $i > $i > $i).
% 36.26/18.31 thf(decl_327, type, esk52_0: ($i > $i) > ($i > $i > ($i > $i) > $i) > $i).
% 36.26/18.31 thf(decl_328, type, esk53_0: (($i > (($i > $i) > $i > $i) > $i > $i) > $i > $i > ($i > $i) > $i > $i) > (($i > ($i > $i) > $i) > $i) > $i).
% 36.26/18.31 thf(decl_329, type, esk54_0: (($i > (($i > $i) > $i > $i) > $i > $i > $i) > $i) > ($i > (($i > $i) > $i) > ($i > $i) > $i) > $i > $i).
% 36.26/18.31 thf(decl_330, type, esk55_0: (((($i > $i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i > $i).
% 36.26/18.31 thf(decl_504, type, esk221_1: $i > $i > $i).
% 36.26/18.31 thf(decl_550, type, esk262_0: ($i > (($i > $i) > $i > $i) > $i > $i) > $i > $i > ($i > $i) > $i > $i).
% 36.26/18.31 thf(decl_551, type, esk263_0: ($i > ($i > $i) > $i) > $i > $i > $i > $i).
% 36.26/18.31 thf(decl_552, type, esk264_1: (($i > $i > $i > $i) > $i) > ($i > ($i > $i) > $i) > $i).
% 36.26/18.31 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox2/tmp/tmp.IfXXGXUPnP/E---3.1_3460431.p', ax13)).
% 36.26/18.31 thf(conj, conjecture, ![X201:($i > $i) > ($i > $i > ($i > $i) > $i) > $i, X202:(($i > (($i > $i) > $i > $i) > $i > $i) > $i > $i > ($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, X204:(((($i > $i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i > $i]:((![X66:$i, X205:$i, X83:$i, X206:($i > $i) > $i]:(((X204 @ (^[X207:(($i > $i > $i) > $i > $i) > $i, X208:$i > $i > $i]:(X203 @ (^[X209:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X210:$i, X211:($i > $i) > $i, X212:$i > $i]:(c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X208 @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty)))) @ (X201 @ (^[X213:$i]:(X213)) @ (^[X214:$i, X215:$i, X216:$i > $i]:(c_setsum @ (X202 @ (^[X217:$i > (($i > $i) > $i > $i) > $i > $i, X172:$i, X173:$i, X218:$i > $i, X181:$i]:(c_Empty)) @ (^[X219:$i > ($i > $i) > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) @ (X203 @ (^[X220:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X204 @ (^[X221:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ X205) @ (X203 @ (^[X222:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X206 @ (^[X223:$i]:(c_Empty)))) @ (^[X224:$i, X225:($i > $i) > $i, X226:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (X201 @ (^[X227:$i]:(c_Empty)) @ (^[X228:$i, X229:$i, X230:$i > $i]:(c_Empty)))))) @ (^[X231:$i, X232:($i > $i) > $i, X233:$i > $i]:(X231)) @ X66))=(c_setsum @ X205 @ X66)))=>(![X234:($i > ($i > $i) > $i) > $i, X235:$i, X83:$i, X236:$i]:(((X204 @ (^[X237:(($i > $i > $i) > $i > $i) > $i, X238:$i > $i > $i]:(c_Empty)) @ c_Empty)=(c_setsum @ c_Empty @ (X234 @ (^[X239:$i, X240:$i > $i]:(c_Empty))))))=>(![X241:$i > ($i > $i) > ($i > $i) > $i > $i, X242:$i > $i > ($i > $i) > $i, X83:$i, X243:$i > $i]:(((X203 @ (^[X244:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X201 @ (^[X245:$i]:(c_Empty)) @ (^[X246:$i, X247:$i, X248:$i > $i]:(c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)))))) @ (^[X249:$i, X250:($i > $i) > $i, X251:$i > $i]:(c_setsum @ (X201 @ (^[X252:$i]:(c_setsum @ X252 @ (X202 @ (^[X253:$i > (($i > $i) > $i > $i) > $i > $i, X254:$i, X172:$i, X255:$i > $i, X174:$i]:(c_Empty)) @ (^[X256:$i > ($i > $i) > $i]:(c_Empty))))) @ (^[X257:$i, X258:$i, X259:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (X204 @ (^[X260:(($i > $i > $i) > $i > $i) > $i, X170:$i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (X241 @ (X204 @ (^[X261:(($i > $i > $i) > $i > $i) > $i, X262:$i > $i > $i]:(c_Empty)) @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (^[X263:$i]:(c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))) @ (^[X264:$i]:(c_setsum @ c_Empty @ (c_setsum @ c_Empty @ (X242 @ c_Empty @ c_Empty @ (^[X265:$i]:(c_Empty)))))) @ (X202 @ (^[X266:$i > (($i > $i) > $i > $i) > $i > $i, X267:$i, X268:$i, X269:$i > $i, X270:$i]:(c_Empty)) @ (^[X271:$i > ($i > $i) > $i]:(c_Empty)))))=(X201 @ (^[X272:$i]:(X201 @ (^[X273:$i]:(c_Empty)) @ (^[X274:$i, X275:$i, X276:$i > $i]:(c_setsum @ (X202 @ (^[X277:$i > (($i > $i) > $i > $i) > $i > $i, X278:$i, X172:$i, X279:$i > $i, X174:$i]:(c_Empty)) @ (^[X280:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj1 @ X275))))) @ (^[X281:$i, X282:$i, X283:$i > $i]:(c_setsum @ (X243 @ (c_setsum @ X282 @ (X202 @ (^[X284:$i > (($i > $i) > $i > $i) > $i > $i, X285:$i, X286:$i, X287:$i > $i, X173:$i]:(c_Empty)) @ (^[X288:$i > ($i > $i) > $i]:(c_Empty))))) @ c_Empty)))))=>(![X289:($i > ($i > $i) > $i > $i) > (($i > $i) > $i) > $i, X290:$i, X83:$i, X291:$i]:(((X203 @ (^[X292:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ (X203 @ (^[X293:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X294:$i, X295:($i > $i) > $i, X296:$i > $i]:(c_Empty)) @ c_Empty) @ (X204 @ (^[X297:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ c_Empty))) @ (^[X298:$i, X299:($i > $i) > $i, X300:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ X291) @ (X202 @ (^[X301:$i > (($i > $i) > $i > $i) > $i > $i, X302:$i, X303:$i, X304:$i > $i, X173:$i]:(X204 @ (^[X305:(($i > $i > $i) > $i > $i) > $i, X306:$i > $i > $i]:(X304 @ c_Empty)) @ X302)) @ (^[X307:$i > ($i > $i) > $i]:(c_Inj1 @ (X202 @ (^[X308:$i > (($i > $i) > $i > $i) > $i > $i, X309:$i, X172:$i, X310:$i > $i, X174:$i]:(c_Empty)) @ (^[X311:$i > ($i > $i) > $i]:(c_Empty)))))))) @ c_Empty)=(X289 @ (^[X312:$i, X313:$i > $i, X314:$i]:(X204 @ (^[X315:(($i > $i > $i) > $i > $i) > $i, X170:$i > $i > $i]:(X170 @ (X202 @ (^[X316:$i > (($i > $i) > $i > $i) > $i > $i, X172:$i, X173:$i, X317:$i > $i, X181:$i]:(X203 @ (^[X318:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X188:$i, X319:($i > $i) > $i, X320:$i > $i]:(c_Empty)) @ c_Empty)) @ (^[X321:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj0 @ c_Empty))) @ (X313 @ c_Empty))) @ (^[X322:$i > $i]:(c_Empty)))))=>(![X323:($i > $i > $i > $i) > $i, X324:$i, X83:$i, X325:($i > $i > $i > $i) > $i]:(((X202 @ (^[X326:$i > (($i > $i) > $i > $i) > $i > $i, X327:$i, X328:$i, X329:$i > $i, X330:$i]:(X327)) @ (^[X331:$i > ($i > $i) > $i]:(c_setsum @ c_Empty @ (c_setsum @ (X325 @ (^[X332:$i, X333:$i, X334:$i]:(X331 @ c_Empty @ (^[X335:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (X331 @ c_Empty @ (^[X336:$i]:(c_Empty))))))))=(X324)))=>(![X337:((($i > $i) > $i > $i) > $i > $i > $i) > $i > $i > $i, X338:(($i > $i) > $i) > $i, X339:$i > $i, X340:$i > (($i > $i) > $i) > ($i > $i) > $i > $i]:(((X202 @ (^[X341:$i > (($i > $i) > $i > $i) > $i > $i, X342:$i, X343:$i, X344:$i > $i, X345:$i]:(c_setsum @ (X203 @ (^[X346:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X203 @ (^[X347:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X348:($i > $i) > $i, X349:$i > $i]:(c_Empty)) @ c_Empty))) @ (^[X350:$i, X351:($i > $i) > $i, X352:$i > $i]:(X203 @ (^[X353:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X351 @ (^[X181:$i]:(c_Empty)))) @ (^[X174:$i, X354:($i > $i) > $i, X355:$i > $i]:(X203 @ (^[X356:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X357:$i, X358:($i > $i) > $i, X359:$i > $i]:(c_Empty)) @ c_Empty)) @ (X351 @ (^[X174:$i]:(c_Empty))))) @ (c_Inj0 @ (X344 @ c_Empty))) @ X342)) @ (^[X360:$i > ($i > $i) > $i]:(X360 @ c_Empty @ (^[X361:$i]:(c_Empty)))))=(X337 @ (^[X362:($i > $i) > $i > $i, X363:$i, X364:$i]:(X202 @ (^[X365:$i > (($i > $i) > $i > $i) > $i > $i, X366:$i, X367:$i, X368:$i > $i, X173:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X204 @ (^[X369:(($i > $i > $i) > $i > $i) > $i, X370:$i > $i > $i]:(X203 @ (^[X371:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X188:$i, X319:($i > $i) > $i, X320:$i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj1 @ c_Empty)))) @ (^[X372:$i > ($i > $i) > $i]:(X204 @ (^[X373:(($i > $i > $i) > $i > $i) > $i, X171:$i > $i > $i]:(c_setsum @ (X373 @ (^[X374:$i > $i > $i, X173:$i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (X204 @ (^[X375:(($i > $i > $i) > $i > $i) > $i, X376:$i > $i > $i]:(X201 @ (^[X377:$i]:(X375 @ (^[X169:$i > $i > $i, X378:$i]:(X202 @ (^[X379:$i > (($i > $i) > $i > $i) > $i > $i, X172:$i, X173:$i, X380:$i > $i, X181:$i]:(c_Empty)) @ (^[X381:$i > ($i > $i) > $i]:(c_Empty)))))) @ (^[X382:$i, X383:$i, X384:$i > $i]:(X201 @ (^[X385:$i]:(X201 @ (^[X172:$i]:(c_Empty)) @ (^[X172:$i, X173:$i, X386:$i > $i]:(c_Empty)))) @ (^[X387:$i, X172:$i, X388:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X339 @ (X340 @ c_Empty @ (^[X389:$i > $i]:(c_Empty)) @ (^[X390:$i]:(c_Empty)) @ c_Empty)))) @ (X338 @ (^[X391:$i > $i]:(c_setsum @ c_Empty @ c_Empty))))))=>(![X66:$i, X82:$i > $i, X392:$i > (($i > $i) > $i) > $i, X393:($i > ($i > $i) > $i) > $i > ($i > $i) > $i]:(((X201 @ (^[X394:$i]:(X204 @ (^[X395:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj0 @ (X203 @ (^[X396:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X397:$i, X398:($i > $i) > $i, X399:$i > $i]:(c_Empty)) @ c_Empty))))) @ (^[X400:$i, X401:$i, X402:$i > $i]:(X203 @ (^[X403:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X404:$i, X405:($i > $i) > $i, X406:$i > $i]:(c_setsum @ (X203 @ (^[X407:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X408:($i > $i) > $i, X409:$i > $i]:(c_Empty)) @ (X405 @ (^[X172:$i]:(c_Empty)))) @ (c_Inj1 @ (X202 @ (^[X410:$i > (($i > $i) > $i > $i) > $i > $i, X173:$i, X174:$i, X411:$i > $i, X188:$i]:(c_Empty)) @ (^[X412:$i > ($i > $i) > $i]:(c_Empty)))))) @ c_Empty)))=(X203 @ (^[X413:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X413 @ c_Empty @ (^[X414:$i > $i, X415:$i]:(c_Inj1 @ (c_Inj0 @ c_Empty))) @ (c_setsum @ c_Empty @ (X204 @ (^[X416:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj0 @ (c_Inj0 @ c_Empty))) @ (X202 @ (^[X417:$i > (($i > $i) > $i > $i) > $i > $i, X418:$i, X419:$i, X420:$i > $i, X421:$i]:(c_Inj0 @ c_Empty)) @ (^[X422:$i > ($i > $i) > $i]:(c_Inj1 @ (X204 @ (^[X423:(($i > $i > $i) > $i > $i) > $i, X169:$i > $i > $i]:(c_Empty)) @ c_Empty)))))) @ (^[X424:$i, X425:($i > $i) > $i, X426:$i > $i]:(c_setsum @ (X203 @ (^[X427:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X428:$i, X429:($i > $i) > $i, X430:$i > $i]:(c_Inj1 @ (X203 @ (^[X431:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X432:($i > $i) > $i, X433:$i > $i]:(c_Empty)) @ c_Empty))) @ (X393 @ (^[X434:$i, X435:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (X203 @ (^[X436:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X437:$i, X438:($i > $i) > $i, X439:$i > $i]:(c_Empty)) @ c_Empty) @ (^[X440:$i]:(X424)))) @ (X425 @ (^[X441:$i]:(c_Inj1 @ (X201 @ (^[X442:$i]:(c_Empty)) @ (^[X443:$i, X444:$i, X445:$i > $i]:(c_Empty)))))))) @ (X203 @ (^[X446:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X82 @ (X82 @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X447:$i, X448:($i > $i) > $i, X449:$i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty)))))=>(![X66:$i, X450:$i, X83:$i, X451:$i]:(((X201 @ (^[X452:$i]:(X452)) @ (^[X453:$i, X454:$i, X455:$i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ c_Empty))))=(c_Inj0 @ c_Empty)))=>(c_False)))))))))), file('/export/starexec/sandbox2/tmp/tmp.IfXXGXUPnP/E---3.1_3460431.p', conj)).
% 36.26/18.31 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox2/tmp/tmp.IfXXGXUPnP/E---3.1_3460431.p', ax5)).
% 36.26/18.31 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox2/tmp/tmp.IfXXGXUPnP/E---3.1_3460431.p', ax11)).
% 36.26/18.31 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.IfXXGXUPnP/E---3.1_3460431.p', ax17)).
% 36.26/18.31 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.IfXXGXUPnP/E---3.1_3460431.p', ax7)).
% 36.26/18.31 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox2/tmp/tmp.IfXXGXUPnP/E---3.1_3460431.p', ax3)).
% 36.26/18.31 thf(c_0_7, plain, ![X521:$o]:(((c_not @ ((X521)))<=>((X521)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 36.26/18.31 thf(c_0_8, negated_conjecture, ~(![X201:($i > $i) > ($i > $i > ($i > $i) > $i) > $i, X202:(($i > (($i > $i) > $i > $i) > $i > $i) > $i > $i > ($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, X204:(((($i > $i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i > $i]:((![X66:$i, X205:$i, X83:$i, X206:($i > $i) > $i]:(((X204 @ (^[X207:(($i > $i > $i) > $i > $i) > $i, X208:$i > $i > $i]:(X203 @ (^[X209:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X210:$i, X211:($i > $i) > $i, X212:$i > $i]:(c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (X208 @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty)))) @ (X201 @ (^[X213:$i]:(X213)) @ (^[X214:$i, X215:$i, X216:$i > $i]:(c_setsum @ (X202 @ (^[X217:$i > (($i > $i) > $i > $i) > $i > $i, X172:$i, X173:$i, X218:$i > $i, X181:$i]:(c_Empty)) @ (^[X219:$i > ($i > $i) > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) @ (X203 @ (^[X220:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X204 @ (^[X221:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ X205) @ (X203 @ (^[X222:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X206 @ (^[X223:$i]:(c_Empty)))) @ (^[X224:$i, X225:($i > $i) > $i, X226:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (X201 @ (^[X227:$i]:(c_Empty)) @ (^[X228:$i, X229:$i, X230:$i > $i]:(c_Empty)))))) @ (^[X231:$i, X232:($i > $i) > $i, X233:$i > $i]:(X231)) @ X66))=(c_setsum @ X205 @ X66)))=>(![X234:($i > ($i > $i) > $i) > $i, X235:$i, X83:$i, X236:$i]:(((X204 @ (^[X237:(($i > $i > $i) > $i > $i) > $i, X238:$i > $i > $i]:(c_Empty)) @ c_Empty)=(c_setsum @ c_Empty @ (X234 @ (^[X239:$i, X240:$i > $i]:(c_Empty))))))=>(![X241:$i > ($i > $i) > ($i > $i) > $i > $i, X242:$i > $i > ($i > $i) > $i, X83:$i, X243:$i > $i]:(((X203 @ (^[X244:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X201 @ (^[X245:$i]:(c_Empty)) @ (^[X246:$i, X247:$i, X248:$i > $i]:(c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)))))) @ (^[X249:$i, X250:($i > $i) > $i, X251:$i > $i]:(c_setsum @ (X201 @ (^[X252:$i]:(c_setsum @ X252 @ (X202 @ (^[X253:$i > (($i > $i) > $i > $i) > $i > $i, X254:$i, X172:$i, X255:$i > $i, X174:$i]:(c_Empty)) @ (^[X256:$i > ($i > $i) > $i]:(c_Empty))))) @ (^[X257:$i, X258:$i, X259:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (X204 @ (^[X260:(($i > $i > $i) > $i > $i) > $i, X170:$i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (X241 @ (X204 @ (^[X261:(($i > $i > $i) > $i > $i) > $i, X262:$i > $i > $i]:(c_Empty)) @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (^[X263:$i]:(c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))) @ (^[X264:$i]:(c_setsum @ c_Empty @ (c_setsum @ c_Empty @ (X242 @ c_Empty @ c_Empty @ (^[X265:$i]:(c_Empty)))))) @ (X202 @ (^[X266:$i > (($i > $i) > $i > $i) > $i > $i, X267:$i, X268:$i, X269:$i > $i, X270:$i]:(c_Empty)) @ (^[X271:$i > ($i > $i) > $i]:(c_Empty)))))=(X201 @ (^[X272:$i]:(X201 @ (^[X273:$i]:(c_Empty)) @ (^[X274:$i, X275:$i, X276:$i > $i]:(c_setsum @ (X202 @ (^[X277:$i > (($i > $i) > $i > $i) > $i > $i, X278:$i, X172:$i, X279:$i > $i, X174:$i]:(c_Empty)) @ (^[X280:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj1 @ X275))))) @ (^[X281:$i, X282:$i, X283:$i > $i]:(c_setsum @ (X243 @ (c_setsum @ X282 @ (X202 @ (^[X284:$i > (($i > $i) > $i > $i) > $i > $i, X285:$i, X286:$i, X287:$i > $i, X173:$i]:(c_Empty)) @ (^[X288:$i > ($i > $i) > $i]:(c_Empty))))) @ c_Empty)))))=>(![X289:($i > ($i > $i) > $i > $i) > (($i > $i) > $i) > $i, X290:$i, X83:$i, X291:$i]:(((X203 @ (^[X292:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ (X203 @ (^[X293:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X294:$i, X295:($i > $i) > $i, X296:$i > $i]:(c_Empty)) @ c_Empty) @ (X204 @ (^[X297:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ c_Empty))) @ (^[X298:$i, X299:($i > $i) > $i, X300:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ X291) @ (X202 @ (^[X301:$i > (($i > $i) > $i > $i) > $i > $i, X302:$i, X303:$i, X304:$i > $i, X173:$i]:(X204 @ (^[X305:(($i > $i > $i) > $i > $i) > $i, X306:$i > $i > $i]:(X304 @ c_Empty)) @ X302)) @ (^[X307:$i > ($i > $i) > $i]:(c_Inj1 @ (X202 @ (^[X308:$i > (($i > $i) > $i > $i) > $i > $i, X309:$i, X172:$i, X310:$i > $i, X174:$i]:(c_Empty)) @ (^[X311:$i > ($i > $i) > $i]:(c_Empty)))))))) @ c_Empty)=(X289 @ (^[X312:$i, X313:$i > $i, X314:$i]:(X204 @ (^[X315:(($i > $i > $i) > $i > $i) > $i, X170:$i > $i > $i]:(X170 @ (X202 @ (^[X316:$i > (($i > $i) > $i > $i) > $i > $i, X172:$i, X173:$i, X317:$i > $i, X181:$i]:(X203 @ (^[X318:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X188:$i, X319:($i > $i) > $i, X320:$i > $i]:(c_Empty)) @ c_Empty)) @ (^[X321:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj0 @ c_Empty))) @ (X313 @ c_Empty))) @ (^[X322:$i > $i]:(c_Empty)))))=>(![X323:($i > $i > $i > $i) > $i, X324:$i, X83:$i, X325:($i > $i > $i > $i) > $i]:(((X202 @ (^[X326:$i > (($i > $i) > $i > $i) > $i > $i, X327:$i, X328:$i, X329:$i > $i, X330:$i]:(X327)) @ (^[X331:$i > ($i > $i) > $i]:(c_setsum @ c_Empty @ (c_setsum @ (X325 @ (^[X332:$i, X333:$i, X334:$i]:(X331 @ c_Empty @ (^[X335:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (X331 @ c_Empty @ (^[X336:$i]:(c_Empty))))))))=(X324)))=>(![X337:((($i > $i) > $i > $i) > $i > $i > $i) > $i > $i > $i, X338:(($i > $i) > $i) > $i, X339:$i > $i, X340:$i > (($i > $i) > $i) > ($i > $i) > $i > $i]:(((X202 @ (^[X341:$i > (($i > $i) > $i > $i) > $i > $i, X342:$i, X343:$i, X344:$i > $i, X345:$i]:(c_setsum @ (X203 @ (^[X346:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X203 @ (^[X347:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X348:($i > $i) > $i, X349:$i > $i]:(c_Empty)) @ c_Empty))) @ (^[X350:$i, X351:($i > $i) > $i, X352:$i > $i]:(X203 @ (^[X353:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X351 @ (^[X181:$i]:(c_Empty)))) @ (^[X174:$i, X354:($i > $i) > $i, X355:$i > $i]:(X203 @ (^[X356:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X357:$i, X358:($i > $i) > $i, X359:$i > $i]:(c_Empty)) @ c_Empty)) @ (X351 @ (^[X174:$i]:(c_Empty))))) @ (c_Inj0 @ (X344 @ c_Empty))) @ X342)) @ (^[X360:$i > ($i > $i) > $i]:(X360 @ c_Empty @ (^[X361:$i]:(c_Empty)))))=(X337 @ (^[X362:($i > $i) > $i > $i, X363:$i, X364:$i]:(X202 @ (^[X365:$i > (($i > $i) > $i > $i) > $i > $i, X366:$i, X367:$i, X368:$i > $i, X173:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X204 @ (^[X369:(($i > $i > $i) > $i > $i) > $i, X370:$i > $i > $i]:(X203 @ (^[X371:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X188:$i, X319:($i > $i) > $i, X320:$i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj1 @ c_Empty)))) @ (^[X372:$i > ($i > $i) > $i]:(X204 @ (^[X373:(($i > $i > $i) > $i > $i) > $i, X171:$i > $i > $i]:(c_setsum @ (X373 @ (^[X374:$i > $i > $i, X173:$i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (X204 @ (^[X375:(($i > $i > $i) > $i > $i) > $i, X376:$i > $i > $i]:(X201 @ (^[X377:$i]:(X375 @ (^[X169:$i > $i > $i, X378:$i]:(X202 @ (^[X379:$i > (($i > $i) > $i > $i) > $i > $i, X172:$i, X173:$i, X380:$i > $i, X181:$i]:(c_Empty)) @ (^[X381:$i > ($i > $i) > $i]:(c_Empty)))))) @ (^[X382:$i, X383:$i, X384:$i > $i]:(X201 @ (^[X385:$i]:(X201 @ (^[X172:$i]:(c_Empty)) @ (^[X172:$i, X173:$i, X386:$i > $i]:(c_Empty)))) @ (^[X387:$i, X172:$i, X388:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X339 @ (X340 @ c_Empty @ (^[X389:$i > $i]:(c_Empty)) @ (^[X390:$i]:(c_Empty)) @ c_Empty)))) @ (X338 @ (^[X391:$i > $i]:(c_setsum @ c_Empty @ c_Empty))))))=>(![X66:$i, X82:$i > $i, X392:$i > (($i > $i) > $i) > $i, X393:($i > ($i > $i) > $i) > $i > ($i > $i) > $i]:(((X201 @ (^[X394:$i]:(X204 @ (^[X395:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj0 @ (X203 @ (^[X396:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X397:$i, X398:($i > $i) > $i, X399:$i > $i]:(c_Empty)) @ c_Empty))))) @ (^[X400:$i, X401:$i, X402:$i > $i]:(X203 @ (^[X403:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X404:$i, X405:($i > $i) > $i, X406:$i > $i]:(c_setsum @ (X203 @ (^[X407:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X408:($i > $i) > $i, X409:$i > $i]:(c_Empty)) @ (X405 @ (^[X172:$i]:(c_Empty)))) @ (c_Inj1 @ (X202 @ (^[X410:$i > (($i > $i) > $i > $i) > $i > $i, X173:$i, X174:$i, X411:$i > $i, X188:$i]:(c_Empty)) @ (^[X412:$i > ($i > $i) > $i]:(c_Empty)))))) @ c_Empty)))=(X203 @ (^[X413:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X413 @ c_Empty @ (^[X414:$i > $i, X415:$i]:(c_Inj1 @ (c_Inj0 @ c_Empty))) @ (c_setsum @ c_Empty @ (X204 @ (^[X416:(($i > $i > $i) > $i > $i) > $i, X168:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj0 @ (c_Inj0 @ c_Empty))) @ (X202 @ (^[X417:$i > (($i > $i) > $i > $i) > $i > $i, X418:$i, X419:$i, X420:$i > $i, X421:$i]:(c_Inj0 @ c_Empty)) @ (^[X422:$i > ($i > $i) > $i]:(c_Inj1 @ (X204 @ (^[X423:(($i > $i > $i) > $i > $i) > $i, X169:$i > $i > $i]:(c_Empty)) @ c_Empty)))))) @ (^[X424:$i, X425:($i > $i) > $i, X426:$i > $i]:(c_setsum @ (X203 @ (^[X427:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X428:$i, X429:($i > $i) > $i, X430:$i > $i]:(c_Inj1 @ (X203 @ (^[X431:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X172:$i, X432:($i > $i) > $i, X433:$i > $i]:(c_Empty)) @ c_Empty))) @ (X393 @ (^[X434:$i, X435:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (X203 @ (^[X436:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[X437:$i, X438:($i > $i) > $i, X439:$i > $i]:(c_Empty)) @ c_Empty) @ (^[X440:$i]:(X424)))) @ (X425 @ (^[X441:$i]:(c_Inj1 @ (X201 @ (^[X442:$i]:(c_Empty)) @ (^[X443:$i, X444:$i, X445:$i > $i]:(c_Empty)))))))) @ (X203 @ (^[X446:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X82 @ (X82 @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[X447:$i, X448:($i > $i) > $i, X449:$i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty)))))=>(![X66:$i, X450:$i, X83:$i, X451:$i]:(((X201 @ (^[X452:$i]:(X452)) @ (^[X453:$i, X454:$i, X455:$i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ c_Empty))))=(c_Inj0 @ c_Empty)))=>(c_False))))))))))), inference(assume_negation,[status(cth)],[conj])).
% 36.26/18.31 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])).
% 36.26/18.31 thf(c_0_10, plain, ![X769:$o]:(((~(c_not @ ((X769)))|(~(X769)|(c_False)))&(((X769)|(c_not @ ((X769))))&(~(c_False)|(c_not @ ((X769))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])).
% 36.26/18.31 thf(c_0_11, plain, ![X767:$o]:(((~(c_False)|(X767))&(~(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])])])])])).
% 36.26/18.31 thf(c_0_12, negated_conjecture, ~(![X201:($i > $i) > ($i > $i > ($i > $i) > $i) > $i, X202:(($i > (($i > $i) > $i > $i) > $i > $i) > $i > $i > ($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, X204:(((($i > $i > $i) > $i > $i) > $i) > ($i > $i > $i) > $i) > $i > $i]:((![X66:$i, X205:$i, X83:$i, X206:($i > $i) > $i]:(((X204 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(X203 @ (^[Z2:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:($i > $i) > $i, Z4:$i > $i]:(c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (Z1 @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty)))) @ (X201 @ (^[Z2:$i]:(Z2)) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_setsum @ (X202 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i, Z6:$i, Z7:$i, Z8:$i > $i, Z9:$i]:(c_Empty)) @ (^[Z5:$i > ($i > $i) > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) @ (X203 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (X204 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ X205) @ (X203 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X206 @ (^[Z2:$i]:(c_Empty)))) @ (^[Z1:$i, Z2:($i > $i) > $i, Z3:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (X201 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty)))))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(Z0)) @ X66))=(c_setsum @ X205 @ X66)))=>(![X234:($i > ($i > $i) > $i) > $i, X235:$i, X83:$i, X236:$i]:(((X204 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(c_Empty)) @ c_Empty)=(c_setsum @ c_Empty @ (X234 @ (^[Z0:$i, Z1:$i > $i]:(c_Empty))))))=>(![X241:$i > ($i > $i) > ($i > $i) > $i > $i, X242:$i > $i > ($i > $i) > $i, X83:$i, X243:$i > $i]:(((X203 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X201 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)))))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_setsum @ (X201 @ (^[Z3:$i]:(c_setsum @ Z3 @ (X202 @ (^[Z4:$i > (($i > $i) > $i > $i) > $i > $i, Z5:$i, Z6:$i, Z7:$i > $i, Z8:$i]:(c_Empty)) @ (^[Z4:$i > ($i > $i) > $i]:(c_Empty))))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (X204 @ (^[Z3:(($i > $i > $i) > $i > $i) > $i, Z4:$i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (X241 @ (X204 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(c_Empty)) @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (^[Z0:$i]:(c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))) @ (^[Z0:$i]:(c_setsum @ c_Empty @ (c_setsum @ c_Empty @ (X242 @ c_Empty @ c_Empty @ (^[Z1:$i]:(c_Empty)))))) @ (X202 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i, Z1:$i, Z2:$i, Z3:$i > $i, Z4:$i]:(c_Empty)) @ (^[Z0:$i > ($i > $i) > $i]:(c_Empty)))))=(X201 @ (^[Z0:$i]:(X201 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_setsum @ (X202 @ (^[Z4:$i > (($i > $i) > $i > $i) > $i > $i, Z5:$i, Z6:$i, Z7:$i > $i, Z8:$i]:(c_Empty)) @ (^[Z4:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj1 @ Z2))))) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ (X243 @ (c_setsum @ Z1 @ (X202 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i, Z4:$i, Z5:$i, Z6:$i > $i, Z7:$i]:(c_Empty)) @ (^[Z3:$i > ($i > $i) > $i]:(c_Empty))))) @ c_Empty)))))=>(![X289:($i > ($i > $i) > $i > $i) > (($i > $i) > $i) > $i, X290:$i, X83:$i, X291:$i]:(((X203 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ (X203 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:($i > $i) > $i, Z3:$i > $i]:(c_Empty)) @ c_Empty) @ (X204 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ c_Empty))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ X291) @ (X202 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i, Z4:$i, Z5:$i, Z6:$i > $i, Z7:$i]:(X204 @ (^[Z8:(($i > $i > $i) > $i > $i) > $i, Z9:$i > $i > $i]:(Z6 @ c_Empty)) @ Z4)) @ (^[Z3:$i > ($i > $i) > $i]:(c_Inj1 @ (X202 @ (^[Z4:$i > (($i > $i) > $i > $i) > $i > $i, Z5:$i, Z6:$i, Z7:$i > $i, Z8:$i]:(c_Empty)) @ (^[Z4:$i > ($i > $i) > $i]:(c_Empty)))))))) @ c_Empty)=(X289 @ (^[Z0:$i, Z1:$i > $i, Z2:$i]:(X204 @ (^[Z3:(($i > $i > $i) > $i > $i) > $i, Z4:$i > $i > $i]:(Z4 @ (X202 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i, Z6:$i, Z7:$i, Z8:$i > $i, Z9:$i]:(X203 @ (^[Z10:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z10:$i, Z11:($i > $i) > $i, Z12:$i > $i]:(c_Empty)) @ c_Empty)) @ (^[Z5:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj0 @ c_Empty))) @ (Z1 @ c_Empty))) @ (^[Z0:$i > $i]:(c_Empty)))))=>(![X323:($i > $i > $i > $i) > $i, X324:$i, X83:$i, X325:($i > $i > $i > $i) > $i]:(((X202 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i, Z1:$i, Z2:$i, Z3:$i > $i, Z4:$i]:(Z1)) @ (^[Z0:$i > ($i > $i) > $i]:(c_setsum @ c_Empty @ (c_setsum @ (X325 @ (^[Z1:$i, Z2:$i, Z3:$i]:(Z0 @ c_Empty @ (^[Z4:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (Z0 @ c_Empty @ (^[Z1:$i]:(c_Empty))))))))=(X324)))=>(![X337:((($i > $i) > $i > $i) > $i > $i > $i) > $i > $i > $i, X338:(($i > $i) > $i) > $i, X339:$i > $i, X340:$i > (($i > $i) > $i) > ($i > $i) > $i > $i]:(((X202 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i, Z1:$i, Z2:$i, Z3:$i > $i, Z4:$i]:(c_setsum @ (X203 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X203 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:($i > $i) > $i, Z8:$i > $i]:(c_Empty)) @ c_Empty))) @ (^[Z5:$i, Z6:($i > $i) > $i, Z7:$i > $i]:(X203 @ (^[Z8:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(Z6 @ (^[Z9:$i]:(c_Empty)))) @ (^[Z8:$i, Z9:($i > $i) > $i, Z10:$i > $i]:(X203 @ (^[Z11:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z11:$i, Z12:($i > $i) > $i, Z13:$i > $i]:(c_Empty)) @ c_Empty)) @ (Z6 @ (^[Z8:$i]:(c_Empty))))) @ (c_Inj0 @ (Z3 @ c_Empty))) @ Z1)) @ (^[Z0:$i > ($i > $i) > $i]:(Z0 @ c_Empty @ (^[Z1:$i]:(c_Empty)))))=(X337 @ (^[Z0:($i > $i) > $i > $i, Z1:$i, Z2:$i]:(X202 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i, Z4:$i, Z5:$i, Z6:$i > $i, Z7:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (X204 @ (^[Z8:(($i > $i > $i) > $i > $i) > $i, Z9:$i > $i > $i]:(X203 @ (^[Z10:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z10:$i, Z11:($i > $i) > $i, Z12:$i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj1 @ c_Empty)))) @ (^[Z3:$i > ($i > $i) > $i]:(X204 @ (^[Z4:(($i > $i > $i) > $i > $i) > $i, Z5:$i > $i > $i]:(c_setsum @ (Z4 @ (^[Z6:$i > $i > $i, Z7:$i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (X204 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(X201 @ (^[Z2:$i]:(Z0 @ (^[Z3:$i > $i > $i, Z4:$i]:(X202 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i, Z6:$i, Z7:$i, Z8:$i > $i, Z9:$i]:(c_Empty)) @ (^[Z5:$i > ($i > $i) > $i]:(c_Empty)))))) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(X201 @ (^[Z5:$i]:(X201 @ (^[Z6:$i]:(c_Empty)) @ (^[Z6:$i, Z7:$i, Z8:$i > $i]:(c_Empty)))) @ (^[Z5:$i, Z6:$i, Z7:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X339 @ (X340 @ c_Empty @ (^[Z0:$i > $i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty)))) @ (X338 @ (^[Z0:$i > $i]:(c_setsum @ c_Empty @ c_Empty))))))=>(![X66:$i, X82:$i > $i, X392:$i > (($i > $i) > $i) > $i, X393:($i > ($i > $i) > $i) > $i > ($i > $i) > $i]:(((X201 @ (^[Z0:$i]:(X204 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj0 @ (X203 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:($i > $i) > $i, Z3:$i > $i]:(c_Empty)) @ c_Empty))))) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(X203 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z3:$i, Z4:($i > $i) > $i, Z5:$i > $i]:(c_setsum @ (X203 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:($i > $i) > $i, Z8:$i > $i]:(c_Empty)) @ (Z4 @ (^[Z6:$i]:(c_Empty)))) @ (c_Inj1 @ (X202 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i, Z7:$i, Z8:$i, Z9:$i > $i, Z10:$i]:(c_Empty)) @ (^[Z6:$i > ($i > $i) > $i]:(c_Empty)))))) @ c_Empty)))=(X203 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (Z0 @ c_Empty @ (^[Z1:$i > $i, Z2:$i]:(c_Inj1 @ (c_Inj0 @ c_Empty))) @ (c_setsum @ c_Empty @ (X204 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj0 @ (c_Inj0 @ c_Empty))) @ (X202 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i, Z2:$i, Z3:$i, Z4:$i > $i, Z5:$i]:(c_Inj0 @ c_Empty)) @ (^[Z1:$i > ($i > $i) > $i]:(c_Inj1 @ (X204 @ (^[Z2:(($i > $i > $i) > $i > $i) > $i, Z3:$i > $i > $i]:(c_Empty)) @ c_Empty)))))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_setsum @ (X203 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z3:$i, Z4:($i > $i) > $i, Z5:$i > $i]:(c_Inj1 @ (X203 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:($i > $i) > $i, Z8:$i > $i]:(c_Empty)) @ c_Empty))) @ (X393 @ (^[Z3:$i, Z4:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (X203 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z3:$i, Z4:($i > $i) > $i, Z5:$i > $i]:(c_Empty)) @ c_Empty) @ (^[Z3:$i]:(Z0)))) @ (Z1 @ (^[Z3:$i]:(c_Inj1 @ (X201 @ (^[Z4:$i]:(c_Empty)) @ (^[Z4:$i, Z5:$i, Z6:$i > $i]:(c_Empty)))))))) @ (X203 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X82 @ (X82 @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty)))))=>(![X66:$i, X450:$i, X83:$i, X451:$i]:(((X201 @ (^[Z0:$i]:(Z0)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ c_Empty))))=(c_Inj0 @ c_Empty)))=>(c_False))))))))))), inference(fof_simplification,[status(thm)],[c_0_8])).
% 36.26/18.31 thf(c_0_13, plain, ![X736:$i]:(((~(c_In @ X736 @ 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])])])])])).
% 36.26/18.31 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])])])).
% 36.26/18.31 thf(c_0_15, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11])])])).
% 36.26/18.31 thf(c_0_16, negated_conjecture, ![X1104:$i, X1105:$i, X1106:($i > $i) > $i, X1107:($i > ($i > $i) > $i) > $i, X1108:$i > ($i > $i) > ($i > $i) > $i > $i, X1109:$i > $i > ($i > $i) > $i, X1110:$i > $i, X1111:($i > ($i > $i) > $i > $i) > (($i > $i) > $i) > $i, X1112:$i, X1113:$i, X1114:($i > $i > $i > $i) > $i, X1115:((($i > $i) > $i > $i) > $i > $i > $i) > $i > $i > $i, X1116:(($i > $i) > $i) > $i, X1117:$i > $i, X1118:$i > (($i > $i) > $i) > ($i > $i) > $i > $i, X1119:$i > $i, X1120:($i > ($i > $i) > $i) > $i > ($i > $i) > $i]:((((esk55_0 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(esk54_0 @ (^[Z2:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i, Z3:($i > $i) > $i, Z4:$i > $i]:(c_setsum @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (Z1 @ (c_Inj1 @ c_Empty) @ (c_Inj0 @ c_Empty)))) @ (esk52_0 @ (^[Z2:$i]:(Z2)) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(c_setsum @ (esk53_0 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i, Z6:$i, Z7:$i, Z8:$i > $i, Z9:$i]:(c_Empty)) @ (^[Z5:$i > ($i > $i) > $i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty)))))) @ (esk54_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (esk55_0 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ X1105) @ (esk54_0 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X1106 @ (^[Z2:$i]:(c_Empty)))) @ (^[Z1:$i, Z2:($i > $i) > $i, Z3:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (esk52_0 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Empty)))))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(Z0)) @ X1104))=(c_setsum @ X1105 @ X1104))&(((esk55_0 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(c_Empty)) @ c_Empty)=(c_setsum @ c_Empty @ (X1107 @ (^[Z0:$i, Z1:$i > $i]:(c_Empty)))))&(((esk54_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(esk52_0 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_Inj0 @ (c_Inj0 @ (c_setsum @ c_Empty @ c_Empty)))))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_setsum @ (esk52_0 @ (^[Z3:$i]:(c_setsum @ Z3 @ (esk53_0 @ (^[Z4:$i > (($i > $i) > $i > $i) > $i > $i, Z5:$i, Z6:$i, Z7:$i > $i, Z8:$i]:(c_Empty)) @ (^[Z4:$i > ($i > $i) > $i]:(c_Empty))))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_Inj1 @ c_Empty)))) @ (c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (esk55_0 @ (^[Z3:(($i > $i > $i) > $i > $i) > $i, Z4:$i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (X1108 @ (esk55_0 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(c_Empty)) @ (c_setsum @ (c_Inj0 @ c_Empty) @ c_Empty)) @ (^[Z0:$i]:(c_setsum @ c_Empty @ (c_Inj0 @ c_Empty))) @ (^[Z0:$i]:(c_setsum @ c_Empty @ (c_setsum @ c_Empty @ (X1109 @ c_Empty @ c_Empty @ (^[Z1:$i]:(c_Empty)))))) @ (esk53_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i, Z1:$i, Z2:$i, Z3:$i > $i, Z4:$i]:(c_Empty)) @ (^[Z0:$i > ($i > $i) > $i]:(c_Empty)))))=(esk52_0 @ (^[Z0:$i]:(esk52_0 @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(c_setsum @ (esk53_0 @ (^[Z4:$i > (($i > $i) > $i > $i) > $i > $i, Z5:$i, Z6:$i, Z7:$i > $i, Z8:$i]:(c_Empty)) @ (^[Z4:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj1 @ Z2))))) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ (X1110 @ (c_setsum @ Z1 @ (esk53_0 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i, Z4:$i, Z5:$i, Z6:$i > $i, Z7:$i]:(c_Empty)) @ (^[Z3:$i > ($i > $i) > $i]:(c_Empty))))) @ c_Empty))))&(((esk54_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ (c_setsum @ (c_setsum @ (esk54_0 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:($i > $i) > $i, Z3:$i > $i]:(c_Empty)) @ c_Empty) @ (esk55_0 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ c_Empty))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_setsum @ (c_setsum @ c_Empty @ X1112) @ (esk53_0 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i, Z4:$i, Z5:$i, Z6:$i > $i, Z7:$i]:(esk55_0 @ (^[Z8:(($i > $i > $i) > $i > $i) > $i, Z9:$i > $i > $i]:(Z6 @ c_Empty)) @ Z4)) @ (^[Z3:$i > ($i > $i) > $i]:(c_Inj1 @ (esk53_0 @ (^[Z4:$i > (($i > $i) > $i > $i) > $i > $i, Z5:$i, Z6:$i, Z7:$i > $i, Z8:$i]:(c_Empty)) @ (^[Z4:$i > ($i > $i) > $i]:(c_Empty)))))))) @ c_Empty)=(X1111 @ (^[Z0:$i, Z1:$i > $i, Z2:$i]:(esk55_0 @ (^[Z3:(($i > $i > $i) > $i > $i) > $i, Z4:$i > $i > $i]:(Z4 @ (esk53_0 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i, Z6:$i, Z7:$i, Z8:$i > $i, Z9:$i]:(esk54_0 @ (^[Z10:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z10:$i, Z11:($i > $i) > $i, Z12:$i > $i]:(c_Empty)) @ c_Empty)) @ (^[Z5:$i > ($i > $i) > $i]:(c_Empty))) @ (c_Inj0 @ c_Empty))) @ (Z1 @ c_Empty))) @ (^[Z0:$i > $i]:(c_Empty))))&(((esk53_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i, Z1:$i, Z2:$i, Z3:$i > $i, Z4:$i]:(Z1)) @ (^[Z0:$i > ($i > $i) > $i]:(c_setsum @ c_Empty @ (c_setsum @ (X1114 @ (^[Z1:$i, Z2:$i, Z3:$i]:(Z0 @ c_Empty @ (^[Z4:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (Z0 @ c_Empty @ (^[Z1:$i]:(c_Empty))))))))=(X1113))&(((esk53_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i, Z1:$i, Z2:$i, Z3:$i > $i, Z4:$i]:(c_setsum @ (esk54_0 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (esk54_0 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:($i > $i) > $i, Z8:$i > $i]:(c_Empty)) @ c_Empty))) @ (^[Z5:$i, Z6:($i > $i) > $i, Z7:$i > $i]:(esk54_0 @ (^[Z8:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(Z6 @ (^[Z9:$i]:(c_Empty)))) @ (^[Z8:$i, Z9:($i > $i) > $i, Z10:$i > $i]:(esk54_0 @ (^[Z11:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z11:$i, Z12:($i > $i) > $i, Z13:$i > $i]:(c_Empty)) @ c_Empty)) @ (Z6 @ (^[Z8:$i]:(c_Empty))))) @ (c_Inj0 @ (Z3 @ c_Empty))) @ Z1)) @ (^[Z0:$i > ($i > $i) > $i]:(Z0 @ c_Empty @ (^[Z1:$i]:(c_Empty)))))=(X1115 @ (^[Z0:($i > $i) > $i > $i, Z1:$i, Z2:$i]:(esk53_0 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i, Z4:$i, Z5:$i, Z6:$i > $i, Z7:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (esk55_0 @ (^[Z8:(($i > $i > $i) > $i > $i) > $i, Z9:$i > $i > $i]:(esk54_0 @ (^[Z10:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z10:$i, Z11:($i > $i) > $i, Z12:$i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj1 @ c_Empty)))) @ (^[Z3:$i > ($i > $i) > $i]:(esk55_0 @ (^[Z4:(($i > $i > $i) > $i > $i) > $i, Z5:$i > $i > $i]:(c_setsum @ (Z4 @ (^[Z6:$i > $i > $i, Z7:$i]:(c_Empty))) @ (c_setsum @ c_Empty @ c_Empty))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (c_Inj1 @ c_Empty)))))) @ (esk55_0 @ (^[Z0:(($i > $i > $i) > $i > $i) > $i, Z1:$i > $i > $i]:(esk52_0 @ (^[Z2:$i]:(Z0 @ (^[Z3:$i > $i > $i, Z4:$i]:(esk53_0 @ (^[Z5:$i > (($i > $i) > $i > $i) > $i > $i, Z6:$i, Z7:$i, Z8:$i > $i, Z9:$i]:(c_Empty)) @ (^[Z5:$i > ($i > $i) > $i]:(c_Empty)))))) @ (^[Z2:$i, Z3:$i, Z4:$i > $i]:(esk52_0 @ (^[Z5:$i]:(esk52_0 @ (^[Z6:$i]:(c_Empty)) @ (^[Z6:$i, Z7:$i, Z8:$i > $i]:(c_Empty)))) @ (^[Z5:$i, Z6:$i, Z7:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_Inj1 @ c_Empty) @ (X1117 @ (X1118 @ c_Empty @ (^[Z0:$i > $i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty)))) @ (X1116 @ (^[Z0:$i > $i]:(c_setsum @ c_Empty @ c_Empty)))))&(((esk52_0 @ (^[Z0:$i]:(esk55_0 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj0 @ (esk54_0 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i, Z2:($i > $i) > $i, Z3:$i > $i]:(c_Empty)) @ c_Empty))))) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(esk54_0 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z3:$i, Z4:($i > $i) > $i, Z5:$i > $i]:(c_setsum @ (esk54_0 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:($i > $i) > $i, Z8:$i > $i]:(c_Empty)) @ (Z4 @ (^[Z6:$i]:(c_Empty)))) @ (c_Inj1 @ (esk53_0 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i, Z7:$i, Z8:$i, Z9:$i > $i, Z10:$i]:(c_Empty)) @ (^[Z6:$i > ($i > $i) > $i]:(c_Empty)))))) @ c_Empty)))=(esk54_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (Z0 @ c_Empty @ (^[Z1:$i > $i, Z2:$i]:(c_Inj1 @ (c_Inj0 @ c_Empty))) @ (c_setsum @ c_Empty @ (esk55_0 @ (^[Z1:(($i > $i > $i) > $i > $i) > $i, Z2:$i > $i > $i]:(c_Empty)) @ c_Empty)) @ (c_Inj0 @ (c_Inj0 @ c_Empty))) @ (esk53_0 @ (^[Z1:$i > (($i > $i) > $i > $i) > $i > $i, Z2:$i, Z3:$i, Z4:$i > $i, Z5:$i]:(c_Inj0 @ c_Empty)) @ (^[Z1:$i > ($i > $i) > $i]:(c_Inj1 @ (esk55_0 @ (^[Z2:(($i > $i > $i) > $i > $i) > $i, Z3:$i > $i > $i]:(c_Empty)) @ c_Empty)))))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_setsum @ (esk54_0 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z3:$i, Z4:($i > $i) > $i, Z5:$i > $i]:(c_Inj1 @ (esk54_0 @ (^[Z6:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z6:$i, Z7:($i > $i) > $i, Z8:$i > $i]:(c_Empty)) @ c_Empty))) @ (X1120 @ (^[Z3:$i, Z4:$i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (esk54_0 @ (^[Z3:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z3:$i, Z4:($i > $i) > $i, Z5:$i > $i]:(c_Empty)) @ c_Empty) @ (^[Z3:$i]:(Z0)))) @ (Z1 @ (^[Z3:$i]:(c_Inj1 @ (esk52_0 @ (^[Z4:$i]:(c_Empty)) @ (^[Z4:$i, Z5:$i, Z6:$i > $i]:(c_Empty)))))))) @ (esk54_0 @ (^[Z0:$i > (($i > $i) > $i > $i) > $i > $i > $i]:(X1119 @ (X1119 @ (c_setsum @ c_Empty @ c_Empty)))) @ (^[Z0:$i, Z1:($i > $i) > $i, Z2:$i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty))))&(((esk52_0 @ (^[Z0:$i]:(Z0)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(c_setsum @ (c_Inj0 @ c_Empty) @ (c_Inj0 @ c_Empty))))=(c_Inj0 @ 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])])])])])])).
% 36.26/18.31 thf(c_0_17, plain, ![X2401:$i > ($i > $i) > $i, X323:($i > $i > $i > $i) > $i]:(((esk264_1 @ X323 @ X2401)=(c_setsum @ c_Empty @ (c_setsum @ (X323 @ (esk263_0 @ X2401)) @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (X2401 @ c_Empty @ (esk221_1 @ c_Empty))))))), introduced(definition)).
% 36.26/18.31 thf(c_0_18, plain, ![X2222:$i, X6:$i]:(((esk221_1 @ X6 @ X2222)=(X6))), introduced(definition)).
% 36.26/18.31 thf(c_0_19, plain, ![X2398:$i, X2397:$i, X2396:$i, X2399:$i > ($i > $i) > $i]:(((esk263_0 @ X2399 @ X2396 @ X2397 @ X2398)=(X2399 @ c_Empty @ (esk221_1 @ c_Empty)))), introduced(definition)).
% 36.26/18.31 thf(c_0_20, plain, ![X2394:$i, X2393:$i > $i, X2392:$i, X2391:$i, X2390:$i > (($i > $i) > $i > $i) > $i > $i]:(((esk262_0 @ X2390 @ X2391 @ X2392 @ X2393 @ X2394)=(X2391))), introduced(definition)).
% 36.26/18.31 thf(c_0_21, plain, ![X528:$i, X529:$i]:(((c_Subq @ X528 @ X529)<=>![X9:$i]:(((c_In @ X9 @ X528)=>(c_In @ X9 @ X529))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 36.26/18.31 thf(c_0_22, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 36.26/18.31 thf(c_0_23, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 36.26/18.31 thf(c_0_24, negated_conjecture, ![X323:($i > $i > $i > $i) > $i, X2:$i]:(((esk53_0 @ esk262_0 @ (esk264_1 @ X323))=(X2))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16]), c_0_17]), c_0_18]), c_0_19]), c_0_18]), c_0_20])).
% 36.26/18.31 thf(c_0_25, 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])).
% 36.26/18.31 thf(c_0_26, plain, ![X784:$i, X785:$i, X786:$i, X787:$i, X788:$i]:(((~(c_Subq @ X784 @ X785)|(~(c_In @ X786 @ X784)|(c_In @ X786 @ X785)))&(((c_In @ (esk13_2 @ X787 @ X788) @ X787)|(c_Subq @ X787 @ X788))&(~(c_In @ (esk13_2 @ X787 @ X788) @ X788)|(c_Subq @ X787 @ X788))))), 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_21])])])])])])])).
% 36.26/18.31 thf(c_0_27, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_22, c_0_23])).
% 36.26/18.31 thf(c_0_28, negated_conjecture, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(spm,[status(thm)],[c_0_24, c_0_24])).
% 36.26/18.31 thf(c_0_29, plain, ![X744:$i, X745:$i]:((((~(c_Subq @ X745 @ X744)|(c_iff @ $true @ $true)|~(c_In @ X745 @ (c_Power @ X744)))&((c_Subq @ X745 @ X744)|(c_iff @ $true @ $false)|~(c_In @ X745 @ (c_Power @ X744))))&((~(c_Subq @ X745 @ X744)|(c_iff @ $false @ $true)|(c_In @ X745 @ (c_Power @ X744)))&((c_Subq @ X745 @ X744)|(c_iff @ $false @ $false)|(c_In @ X745 @ (c_Power @ X744)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_25])])])).
% 36.26/18.31 thf(c_0_30, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 36.26/18.31 thf(c_0_31, negated_conjecture, ![X2:$i, X6:$i]:(~((c_In @ X2 @ X6))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 36.26/18.31 thf(c_0_32, plain, ![X732:$o, X733:$o]:(((~(X732)|(X733)|~(c_iff @ ((X732)) @ ((X733))))&(~(X733)|(X732)|~(c_iff @ ((X732)) @ ((X733)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 36.26/18.31 thf(c_0_33, 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_29])).
% 36.26/18.31 thf(c_0_34, plain, ![X2:$i, X6:$i]:((c_Subq @ X2 @ X6)), inference(sr,[status(thm)],[c_0_30, c_0_31])).
% 36.26/18.31 thf(c_0_35, plain, ~((c_iff @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_32])])])).
% 36.26/18.31 thf(c_0_36, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])]), c_0_31]), c_0_35]), ['proof']).
% 36.26/18.31 % SZS output end CNFRefutation
% 36.26/18.31 % Parsed axioms : 213
% 36.26/18.31 % Removed by relevancy pruning/SinE : 0
% 36.26/18.31 % Initial clauses : 468753
% 36.26/18.31 % Removed in clause preprocessing : 463862
% 36.26/18.31 % Initial clauses in saturation : 4891
% 36.26/18.31 % Processed clauses : 4939
% 36.26/18.31 % ...of these trivial : 258
% 36.26/18.31 % ...subsumed : 3356
% 36.26/18.31 % ...remaining for further processing : 1324
% 36.26/18.31 % Other redundant clauses eliminated : 2
% 36.26/18.31 % Clauses deleted for lack of memory : 0
% 36.26/18.31 % Backward-subsumed : 214
% 36.26/18.31 % Backward-rewritten : 78
% 36.26/18.31 % Generated clauses : 8347
% 36.26/18.31 % ...of the previous two non-redundant : 7936
% 36.26/18.31 % ...aggressively subsumed : 0
% 36.26/18.31 % Contextual simplify-reflections : 21
% 36.26/18.31 % Paramodulations : 8330
% 36.26/18.31 % Factorizations : 0
% 36.26/18.31 % NegExts : 0
% 36.26/18.31 % Equation resolutions : 2
% 36.26/18.31 % Disequality decompositions : 0
% 36.26/18.31 % Total rewrite steps : 941
% 36.26/18.31 % ...of those cached : 724
% 36.26/18.31 % Propositional unsat checks : 0
% 36.26/18.31 % Propositional check models : 0
% 36.26/18.31 % Propositional check unsatisfiable : 0
% 36.26/18.31 % Propositional clauses : 0
% 36.26/18.31 % Propositional clauses after purity: 0
% 36.26/18.31 % Propositional unsat core size : 0
% 36.26/18.31 % Propositional preprocessing time : 0.000
% 36.26/18.31 % Propositional encoding time : 0.000
% 36.26/18.31 % Propositional solver time : 0.000
% 36.26/18.31 % Success case prop preproc time : 0.000
% 36.26/18.31 % Success case prop encoding time : 0.000
% 36.26/18.31 % Success case prop solver time : 0.000
% 36.26/18.31 % Current number of processed clauses : 1024
% 36.26/18.31 % Positive orientable unit clauses : 97
% 36.26/18.31 % Positive unorientable unit clauses: 3
% 36.26/18.31 % Negative unit clauses : 95
% 36.26/18.31 % Non-unit-clauses : 829
% 36.26/18.31 % Current number of unprocessed clauses: 7206
% 36.26/18.31 % ...number of literals in the above : 31103
% 36.26/18.31 % Current number of archived formulas : 0
% 36.26/18.31 % Current number of archived clauses : 298
% 36.26/18.31 % Clause-clause subsumption calls (NU) : 221183
% 36.26/18.31 % Rec. Clause-clause subsumption calls : 189387
% 36.26/18.31 % Non-unit clause-clause subsumptions : 3274
% 36.26/18.31 % Unit Clause-clause subsumption calls : 14400
% 36.26/18.31 % Rewrite failures with RHS unbound : 718
% 36.26/18.31 % BW rewrite match attempts : 2377
% 36.26/18.31 % BW rewrite match successes : 175
% 36.26/18.31 % Condensation attempts : 0
% 36.26/18.31 % Condensation successes : 0
% 36.26/18.31 % Termbank termtop insertions : 20018545
% 36.26/18.31 % Search garbage collected termcells : 2012548
% 36.26/18.31
% 36.26/18.31 % -------------------------------------------------
% 36.26/18.31 % User time : 16.471 s
% 36.26/18.31 % System time : 1.092 s
% 36.26/18.31 % Total time : 17.563 s
% 36.26/18.31 % Maximum resident set size: 1258876 pages
% 36.26/18.31
% 36.26/18.31 % -------------------------------------------------
% 36.26/18.31 % User time : 16.764 s
% 36.26/18.31 % System time : 1.375 s
% 36.26/18.31 % Total time : 18.139 s
% 36.26/18.31 % Maximum resident set size: 5376 pages
% 36.26/18.31 % E exiting
%------------------------------------------------------------------------------