%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO856^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 28.37s 14.07s
% Output : CNFRefutation 28.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYO856^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.02 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Tue Sep 29 17:18:33 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.13 Running higher-order theorem proving
% 0.08/0.15 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p
% 28.37/14.07 % Version: 3.5.1-ho
% 28.37/14.07 % partial match(2): HSLMSMSSSSLCHSA
% 28.37/14.07 % Preprocessing class: HSLMSLSSSSLCHHA.
% 28.37/14.07 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 28.37/14.07 % Starting pre_casc_6 with 1500s (5) cores
% 28.37/14.07 % Starting ehoh_best7 with 300s (1) cores
% 28.37/14.07 % Starting new_bool_8 with 300s (1) cores
% 28.37/14.07 % Starting new_ho_11 with 300s (1) cores
% 28.37/14.07 % new_bool_8 with pid 412446 completed with status 9
% 28.37/14.07 % pre_casc_6 with pid 412444 completed with status 0
% 28.37/14.07 % Result found by pre_casc_6
% 28.37/14.07 % partial match(2): HSLMSMSSSSLCHSA
% 28.37/14.07 % Preprocessing class: HSLMSLSSSSLCHHA.
% 28.37/14.07 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 28.37/14.07 % Starting pre_casc_6 with 1500s (5) cores
% 28.37/14.07 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 28.37/14.07 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 28.37/14.07 % Search class: HGHSM-SMLM31-DHHFFSBC
% 28.37/14.07 % partial match(2): HGHSM-SMLM32-DHFFFSBC
% 28.37/14.07 % Scheduled 7 strats onto 5 cores with 1487 seconds (1487 total)
% 28.37/14.07 % Starting SubtermCWHack with 134s (1) cores
% 28.37/14.07 % Starting pre_casc_6 with 149s (1) cores
% 28.37/14.07 % Starting ehoh_best_sine_rwall with 192s (1) cores
% 28.37/14.07 % Starting full_lambda_6 with 192s (1) cores
% 28.37/14.07 % Starting ehoh_best_sine with 192s (1) cores
% 28.37/14.07 % SubtermCWHack with pid 412505 completed with status 0
% 28.37/14.07 % Result found by SubtermCWHack
% 28.37/14.07 % partial match(2): HSLMSMSSSSLCHSA
% 28.37/14.07 % Preprocessing class: HSLMSLSSSSLCHHA.
% 28.37/14.07 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 28.37/14.07 % Starting pre_casc_6 with 1500s (5) cores
% 28.37/14.07 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 28.37/14.07 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 28.37/14.07 % Search class: HGHSM-SMLM31-DHHFFSBC
% 28.37/14.07 % partial match(2): HGHSM-SMLM32-DHFFFSBC
% 28.37/14.07 % Scheduled 7 strats onto 5 cores with 1487 seconds (1487 total)
% 28.37/14.07 % Starting SubtermCWHack with 134s (1) cores
% 28.37/14.07 % Preprocessing time : 0.032 s
% 28.37/14.07
% 28.37/14.07 % Proof found!
% 28.37/14.07 % SZS status Theorem
% 28.37/14.07 % SZS output start CNFRefutation
% 28.37/14.07 thf(decl_24, type, c_False: $o).
% 28.37/14.07 thf(decl_26, type, c_not: $o > $o).
% 28.37/14.07 thf(decl_29, type, c_iff: $o > $o > $o).
% 28.37/14.07 thf(decl_30, type, c_In: $i > $i > $o).
% 28.37/14.07 thf(decl_31, type, c_Subq: $i > $i > $o).
% 28.37/14.07 thf(decl_32, type, c_Empty: $i).
% 28.37/14.07 thf(decl_34, type, c_Power: $i > $i).
% 28.37/14.07 thf(decl_87, type, c_Inj1: $i > $i).
% 28.37/14.07 thf(decl_88, type, c_Inj0: $i > $i).
% 28.37/14.07 thf(decl_91, type, c_setsum: $i > $i > $i).
% 28.37/14.07 thf(decl_192, type, esk1_0: (($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i) > ($i > $i > ($i > $i) > $i) > $i).
% 28.37/14.07 thf(decl_193, type, esk2_0: ($i > ((($i > $i) > $i > $i) > $i > $i > $i) > $i) > $i > $i).
% 28.37/14.07 thf(decl_194, type, esk3_0: ($i > $i > $i) > ($i > $i) > $i > $i > $i > $i).
% 28.37/14.07 thf(decl_195, type, esk4_0: (((($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i) > $i) > ($i > $i) > $i).
% 28.37/14.07 thf(decl_197, type, esk5_0: $i).
% 28.37/14.07 thf(decl_205, type, esk13_2: $i > $i > $i).
% 28.37/14.07 thf(decl_237, type, esk42_0: ($i > $i) > (($i > $i > $i) > $i > $i) > $i > ($i > $i) > $i).
% 28.37/14.07 thf(decl_238, type, esk43_0: $i > $i > ($i > $i) > $i).
% 28.37/14.07 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/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p', conj)).
% 28.37/14.07 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p', ax13)).
% 28.37/14.07 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p', ax5)).
% 28.37/14.07 thf(ax17, axiom, ((c_Subq)=(^[X26:$i, X2:$i]:(![X9:$i]:((((c_In @ X9 @ X26))=>((c_In @ X9 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p', ax17)).
% 28.37/14.07 thf(ax7, axiom, ![X10:$i, X2:$i]:((c_iff @ ((c_In @ X2 @ (c_Power @ X10))) @ ((c_Subq @ X2 @ X10)))), file('/export/starexec/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p', ax7)).
% 28.37/14.07 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox/tmp/tmp.4SiwgCQBeJ/E---3.1_412407.p', ax3)).
% 28.37/14.07 thf(c_0_6, 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])).
% 28.37/14.07 thf(c_0_7, plain, ![X578:$o]:(((c_not @ ((X578)))<=>((X578)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 28.37/14.07 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 @ (^[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_6])])).
% 28.37/14.07 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])).
% 28.37/14.07 thf(c_0_10, plain, ![X701:$o]:(((~(c_not @ ((X701)))|(~(X701)|(c_False)))&(((X701)|(c_not @ ((X701))))&(~(c_False)|(c_not @ ((X701))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])).
% 28.37/14.07 thf(c_0_11, negated_conjecture, ![X682:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i, X683:(($i > $i > $i) > $i) > ($i > $i) > $i > $i > $i, X684:$i, X685:$i > $i, X686:$i, X687:$i > $i, X688:((($i > $i) > $i) > ($i > $i) > $i > $i) > $i > $i > $i > $i, X689:(($i > $i > $i) > $i > $i) > $i, X690:$i > $i, X691:$i, X692:(($i > $i) > $i > $i) > $i, X693:$i, X694:$i > ($i > $i > $i) > $i > $i, X695:$i, X696:$i, X697:(($i > $i > $i) > $i > $i) > $i, X698:$i]:((((esk4_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ (esk1_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(esk2_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))) @ (esk2_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (esk3_0 @ (^[Z1:$i, Z2:$i]:(X683 @ (^[Z3:$i > $i > $i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty)) @ (^[Z1:$i]:(c_Empty)) @ (X682 @ (^[Z1:($i > $i) > $i, Z2:$i > $i, Z3:$i]:(c_Empty)) @ c_Empty) @ (esk2_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))&(((esk4_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ X685)=(X685 @ (c_setsum @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(esk2_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (c_setsum @ c_Empty @ c_Empty))) @ (^[Z0:$i]:(Z0)) @ X684 @ c_Empty @ c_Empty) @ (esk2_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(Z1 @ (^[Z2:$i > $i, Z3:$i]:(c_Empty)) @ Z0 @ (esk3_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ c_Empty))))&(((esk3_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(esk3_0 @ (^[Z1:$i, Z2:$i]:(esk3_0 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ (esk1_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]:(esk1_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))))) @ (X687 @ Z2) @ Z2)) @ (^[Z1:$i]:(Z0)) @ (esk2_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ (esk3_0 @ (^[Z1:$i, Z2:$i]:(c_Inj1 @ c_Empty)) @ (^[Z1:$i]:(esk2_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty)) @ (esk4_0 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z1:$i]:(c_Empty))) @ (c_Inj1 @ c_Empty) @ (esk1_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))))) @ (X687 @ c_Empty) @ c_Empty)) @ X686 @ (esk1_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) @ (esk2_0 @ (^[Z3:$i, Z4:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (c_setsum @ c_Empty @ (X687 @ c_Empty)))=(X686))&(((esk3_0 @ (^[Z0:$i, Z1:$i]:(esk3_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(Z0)) @ (X690 @ c_Empty) @ (X689 @ (^[Z2:$i > $i > $i, Z3:$i]:(c_setsum @ c_Empty @ (esk1_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)) @ (X688 @ (^[Z0:($i > $i) > $i, Z1:$i > $i, Z2:$i]:(c_Empty)) @ c_Empty @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(esk4_0 @ (^[Z2:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(Z1)) @ (^[Z2:$i]:(c_Inj0 @ c_Empty)))) @ (^[Z0:$i]:(esk4_0 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(X689 @ (^[Z2:$i > $i > $i, Z3:$i]:(c_Empty)))) @ (^[Z1:$i]:(c_Inj0 @ c_Empty)))) @ (X690 @ c_Empty) @ c_Empty @ (X688 @ (^[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) @ (X690 @ c_Empty)))) @ (c_Inj1 @ (c_setsum @ c_Empty @ (X688 @ (^[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)))) @ (X690 @ (c_Inj1 @ c_Empty)))=(X690 @ (c_Inj0 @ c_Empty)))&(((esk2_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (c_setsum @ (c_setsum @ c_Empty @ c_Empty) @ (c_setsum @ (esk3_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (esk4_0 @ (^[Z2:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty))))) @ (c_setsum @ (c_setsum @ (esk1_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))))) @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(X692 @ (^[Z1:$i > $i, Z2:$i]:(c_setsum @ (c_Inj1 @ c_Empty) @ (esk3_0 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ X691 @ (c_Inj1 @ (c_setsum @ c_Empty @ c_Empty))) @ c_Empty @ (c_Inj0 @ c_Empty)))=(esk3_0 @ (^[Z0:$i, Z1:$i]:(c_setsum @ X693 @ (c_Inj1 @ X693))) @ (^[Z0:$i]:(esk1_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 @ (esk1_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 @ (esk3_0 @ (^[Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z3:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))))) @ (c_setsum @ (c_Inj1 @ (X692 @ (^[Z0:$i > $i, Z1:$i]:(c_Inj1 @ c_Empty)))) @ (c_setsum @ (esk4_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)))))&(((esk2_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_setsum @ (esk2_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(Z0)) @ (c_setsum @ (esk3_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty) @ (esk2_0 @ (^[Z2:$i, Z3:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))) @ c_Empty)) @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(Z1)) @ (^[Z0:$i]:(esk1_0 @ (^[Z1:$i > $i, Z2:($i > $i > $i) > $i > $i, Z3:$i, Z4:$i > $i]:(Z3)) @ (^[Z1:$i, Z2:$i, Z3:$i > $i]:(esk4_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)))))) @ X695 @ (c_Inj1 @ (c_Inj0 @ c_Empty)) @ (c_setsum @ c_Empty @ (c_Inj1 @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))=(esk3_0 @ (^[Z0:$i, Z1:$i]:(c_Inj0 @ c_Empty)) @ (^[Z0:$i]:(esk2_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(X697 @ (^[Z3:$i > $i > $i, Z4:$i]:(Z2 @ (^[Z5:$i > $i, Z6:$i]:(esk3_0 @ (^[Z7:$i, Z8:$i]:(c_Empty)) @ (^[Z7:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)) @ c_Empty @ (esk2_0 @ (^[Z5:$i, Z6:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ c_Empty)) @ (c_Inj0 @ (esk4_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]:(esk4_0 @ (^[Z1:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_setsum @ c_Empty @ c_Empty)) @ (^[Z1:$i]:(esk3_0 @ (^[Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty)))))) @ (c_setsum @ (c_setsum @ X695 @ (esk2_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ c_Empty)) @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty)) @ c_Empty @ c_Empty @ c_Empty))) @ (esk2_0 @ (^[Z0:$i, Z1:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Inj0 @ (esk1_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))))) @ X695)) @ (c_setsum @ (c_setsum @ X696 @ (esk3_0 @ (^[Z0:$i, Z1:$i]:(Z1)) @ (^[Z0:$i]:(X697 @ (^[Z1:$i > $i > $i, Z2:$i]:(c_Empty)))) @ (X694 @ c_Empty @ (^[Z0:$i, Z1:$i]:(c_Empty)) @ c_Empty) @ (c_Inj0 @ c_Empty) @ (esk4_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i]:(c_Empty))))) @ (X694 @ (esk4_0 @ (^[Z0:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z0:$i]:(esk1_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]:(esk2_0 @ (^[Z1:$i, Z2:(($i > $i) > $i > $i) > $i > $i > $i]:(Z2 @ (^[Z3:$i > $i, Z4:$i]:(c_Empty)) @ c_Empty @ c_Empty)))) @ X695))))&(((esk1_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_Empty)) @ (^[Z0:$i, Z1:$i, Z2:$i > $i]:(esk1_0 @ (^[Z3:$i > $i, Z4:($i > $i > $i) > $i > $i, Z5:$i, Z6:$i > $i]:(esk3_0 @ (^[Z7:$i, Z8:$i]:(Z6 @ Z5)) @ (^[Z7:$i]:(Z7)) @ c_Empty @ (Z6 @ (esk4_0 @ (^[Z7:(($i > $i > $i) > ($i > $i) > $i) > $i > $i > $i]:(c_Empty)) @ (^[Z7:$i]:(c_Empty)))) @ (esk1_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]:(esk2_0 @ (^[Z10:$i, Z11:(($i > $i) > $i > $i) > $i > $i > $i]:(c_Empty)) @ c_Empty))))) @ (^[Z3:$i, Z4:$i, Z5:$i > $i]:(c_Inj1 @ (esk1_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))))))))=(esk1_0 @ (^[Z0:$i > $i, Z1:($i > $i > $i) > $i > $i, Z2:$i, Z3:$i > $i]:(c_setsum @ (esk1_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))))&(((esk1_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)))=(X698))&~(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_8])])])])])])).
% 28.37/14.07 thf(c_0_12, plain, ![X702:$i]:(((~(c_In @ X702 @ c_Empty)|(c_not @ $true))&((c_In @ esk5_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])])])])])).
% 28.37/14.07 thf(c_0_13, plain, ((c_False)|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_10])])])).
% 28.37/14.07 thf(c_0_14, negated_conjecture, ~((c_False)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 28.37/14.07 thf(c_0_15, plain, ![X1103:$i > $i, X1102:$i, X1101:$i]:(((esk43_0 @ X1101 @ X1102 @ X1103)=(c_Empty))), introduced(definition)).
% 28.37/14.07 thf(c_0_16, plain, ![X1100:$i > $i, X1099:$i, X1098:($i > $i > $i) > $i > $i, X1097:$i > $i]:(((esk42_0 @ X1097 @ X1098 @ X1099 @ X1100)=(c_Empty))), introduced(definition)).
% 28.37/14.07 thf(c_0_17, plain, ![X582:$i, X583:$i]:(((c_Subq @ X582 @ X583)<=>![X9:$i]:(((c_In @ X9 @ X582)=>(c_In @ X9 @ X583))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 28.37/14.07 thf(c_0_18, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 28.37/14.07 thf(c_0_19, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_13, c_0_14])).
% 28.37/14.07 thf(c_0_20, negated_conjecture, ![X2:$i]:(((esk1_0 @ esk42_0 @ esk43_0)=(X2))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11]), c_0_15]), c_0_16])).
% 28.37/14.07 thf(c_0_21, 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])).
% 28.37/14.07 thf(c_0_22, plain, ![X721:$i, X722:$i, X723:$i, X724:$i, X725:$i]:(((~(c_Subq @ X721 @ X722)|(~(c_In @ X723 @ X721)|(c_In @ X723 @ X722)))&(((c_In @ (esk13_2 @ X724 @ X725) @ X724)|(c_Subq @ X724 @ X725))&(~(c_In @ (esk13_2 @ X724 @ X725) @ X725)|(c_Subq @ X724 @ X725))))), 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_17])])])])])])])).
% 28.37/14.07 thf(c_0_23, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_18, c_0_19])).
% 28.37/14.07 thf(c_0_24, negated_conjecture, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(spm,[status(thm)],[c_0_20, c_0_20])).
% 28.37/14.07 thf(c_0_25, plain, ![X743:$i, X744:$i]:((((~(c_Subq @ X744 @ X743)|(c_iff @ $true @ $true)|~(c_In @ X744 @ (c_Power @ X743)))&((c_Subq @ X744 @ X743)|(c_iff @ $true @ $false)|~(c_In @ X744 @ (c_Power @ X743))))&((~(c_Subq @ X744 @ X743)|(c_iff @ $false @ $true)|(c_In @ X744 @ (c_Power @ X743)))&((c_Subq @ X744 @ X743)|(c_iff @ $false @ $false)|(c_In @ X744 @ (c_Power @ X743)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_21])])])).
% 28.37/14.07 thf(c_0_26, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 28.37/14.07 thf(c_0_27, negated_conjecture, ![X2:$i, X6:$i]:(~((c_In @ X2 @ X6))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 28.37/14.07 thf(c_0_28, plain, ![X775:$o, X776:$o]:(((~(X775)|(X776)|~(c_iff @ ((X775)) @ ((X776))))&(~(X776)|(X775)|~(c_iff @ ((X775)) @ ((X776)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 28.37/14.07 thf(c_0_29, 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_25])).
% 28.37/14.07 thf(c_0_30, plain, ![X2:$i, X6:$i]:((c_Subq @ X2 @ X6)), inference(sr,[status(thm)],[c_0_26, c_0_27])).
% 28.37/14.07 thf(c_0_31, plain, ~((c_iff @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_28])])])).
% 28.37/14.07 thf(c_0_32, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])]), c_0_27]), c_0_31]), ['proof']).
% 28.37/14.07 % SZS output end CNFRefutation
% 28.37/14.07 % Parsed axioms : 213
% 28.37/14.07 % Removed by relevancy pruning/SinE : 145
% 28.37/14.07 % Initial clauses : 465178
% 28.37/14.07 % Removed in clause preprocessing : 463015
% 28.37/14.07 % Initial clauses in saturation : 2163
% 28.37/14.07 % Processed clauses : 395
% 28.37/14.07 % ...of these trivial : 77
% 28.37/14.07 % ...subsumed : 164
% 28.37/14.07 % ...remaining for further processing : 153
% 28.37/14.07 % Other redundant clauses eliminated : 0
% 28.37/14.07 % Clauses deleted for lack of memory : 0
% 28.37/14.07 % Backward-subsumed : 37
% 28.37/14.07 % Backward-rewritten : 12
% 28.37/14.07 % Generated clauses : 137
% 28.37/14.07 % ...of the previous two non-redundant : 98
% 28.37/14.07 % ...aggressively subsumed : 0
% 28.37/14.07 % Contextual simplify-reflections : 6
% 28.37/14.07 % Paramodulations : 128
% 28.37/14.07 % Factorizations : 0
% 28.37/14.07 % NegExts : 0
% 28.37/14.07 % Equation resolutions : 0
% 28.37/14.07 % Disequality decompositions : 0
% 28.37/14.07 % Total rewrite steps : 194
% 28.37/14.07 % ...of those cached : 164
% 28.37/14.07 % Propositional unsat checks : 0
% 28.37/14.07 % Propositional check models : 0
% 28.37/14.07 % Propositional check unsatisfiable : 0
% 28.37/14.07 % Propositional clauses : 0
% 28.37/14.07 % Propositional clauses after purity: 0
% 28.37/14.07 % Propositional unsat core size : 0
% 28.37/14.07 % Propositional preprocessing time : 0.000
% 28.37/14.07 % Propositional encoding time : 0.000
% 28.37/14.07 % Propositional solver time : 0.000
% 28.37/14.07 % Success case prop preproc time : 0.000
% 28.37/14.07 % Success case prop encoding time : 0.000
% 28.37/14.07 % Success case prop solver time : 0.000
% 28.37/14.07 % Current number of processed clauses : 104
% 28.37/14.07 % Positive orientable unit clauses : 26
% 28.37/14.07 % Positive unorientable unit clauses: 3
% 28.37/14.07 % Negative unit clauses : 14
% 28.37/14.07 % Non-unit-clauses : 61
% 28.37/14.07 % Current number of unprocessed clauses: 1837
% 28.37/14.07 % ...number of literals in the above : 9574
% 28.37/14.07 % Current number of archived formulas : 0
% 28.37/14.07 % Current number of archived clauses : 49
% 28.37/14.07 % Clause-clause subsumption calls (NU) : 2132
% 28.37/14.07 % Rec. Clause-clause subsumption calls : 1889
% 28.37/14.07 % Non-unit clause-clause subsumptions : 45
% 28.37/14.07 % Unit Clause-clause subsumption calls : 500
% 28.37/14.07 % Rewrite failures with RHS unbound : 624
% 28.37/14.07 % BW rewrite match attempts : 144
% 28.37/14.07 % BW rewrite match successes : 28
% 28.37/14.07 % Condensation attempts : 0
% 28.37/14.07 % Condensation successes : 0
% 28.37/14.07 % Termbank termtop insertions : 19581814
% 28.37/14.07 % Search garbage collected termcells : 1981990
% 28.37/14.07
% 28.37/14.07 % -------------------------------------------------
% 28.37/14.07 % User time : 12.603 s
% 28.37/14.07 % System time : 0.898 s
% 28.37/14.07 % Total time : 13.501 s
% 28.37/14.07 % Maximum resident set size: 1251516 pages
% 28.37/14.07
% 28.37/14.07 % -------------------------------------------------
% 28.37/14.07 % User time : 13.252 s
% 28.37/14.07 % System time : 1.314 s
% 28.37/14.07 % Total time : 14.567 s
% 28.37/14.07 % Maximum resident set size: 5376 pages
% 28.37/14.07 % E exiting
%------------------------------------------------------------------------------