%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO858^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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:43:27 AM UTC 2026
% Result : Theorem 53.54s 26.52s
% Output : CNFRefutation 53.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO858^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n026.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:21:57 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.21/0.28 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.MdlW2Dnvn6/E---3.1_901530.p
% 53.54/26.52 % Version: 3.5.1-ho
% 53.54/26.52 % partial match(2): HSLMSMSSSSLCHSA
% 53.54/26.52 % Preprocessing class: HSLMSLSSSSLCHHA.
% 53.54/26.52 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 53.54/26.52 % Starting pre_casc_6 with 1500s (5) cores
% 53.54/26.52 % Starting ehoh_best7 with 300s (1) cores
% 53.54/26.52 % Starting new_bool_8 with 300s (1) cores
% 53.54/26.52 % Starting new_ho_11 with 300s (1) cores
% 53.54/26.52 % new_bool_8 with pid 901545 completed with status 9
% 53.54/26.52 % pre_casc_6 with pid 901543 completed with status 0
% 53.54/26.52 % Result found by pre_casc_6
% 53.54/26.52 % partial match(2): HSLMSMSSSSLCHSA
% 53.54/26.52 % Preprocessing class: HSLMSLSSSSLCHHA.
% 53.54/26.52 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 53.54/26.52 % Starting pre_casc_6 with 1500s (5) cores
% 53.54/26.52 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 53.54/26.52 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 53.54/26.52 % Search class: HGHSM-SMLM31-DHHFFSBC
% 53.54/26.52 % partial match(2): HGHSM-SMLM32-DHFFFSBC
% 53.54/26.52 % Scheduled 7 strats onto 5 cores with 1475 seconds (1475 total)
% 53.54/26.52 % Starting SubtermCWHack with 133s (1) cores
% 53.54/26.52 % Starting pre_casc_6 with 148s (1) cores
% 53.54/26.52 % Starting ehoh_best_sine_rwall with 190s (1) cores
% 53.54/26.52 % Starting full_lambda_6 with 190s (1) cores
% 53.54/26.52 % Starting ehoh_best_sine with 190s (1) cores
% 53.54/26.52 % SubtermCWHack with pid 901601 completed with status 0
% 53.54/26.52 % Result found by SubtermCWHack
% 53.54/26.52 % partial match(2): HSLMSMSSSSLCHSA
% 53.54/26.52 % Preprocessing class: HSLMSLSSSSLCHHA.
% 53.54/26.52 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 53.54/26.52 % Starting pre_casc_6 with 1500s (5) cores
% 53.54/26.52 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,3,,5,20000,1.0,true))
% 53.54/26.52 % SinE strategy is GSinE(CountFormulas,hypos,3,,5,20000,1.0,true)
% 53.54/26.52 % Search class: HGHSM-SMLM31-DHHFFSBC
% 53.54/26.52 % partial match(2): HGHSM-SMLM32-DHFFFSBC
% 53.54/26.52 % Scheduled 7 strats onto 5 cores with 1475 seconds (1475 total)
% 53.54/26.52 % Starting SubtermCWHack with 133s (1) cores
% 53.54/26.52 % Preprocessing time : 0.048 s
% 53.54/26.52
% 53.54/26.52 % Proof found!
% 53.54/26.52 % SZS status Theorem
% 53.54/26.52 % SZS output start CNFRefutation
% 53.54/26.52 thf(decl_24, type, c_False: $o).
% 53.54/26.52 thf(decl_26, type, c_not: $o > $o).
% 53.54/26.52 thf(decl_29, type, c_iff: $o > $o > $o).
% 53.54/26.53 thf(decl_30, type, c_In: $i > $i > $o).
% 53.54/26.53 thf(decl_31, type, c_Subq: $i > $i > $o).
% 53.54/26.53 thf(decl_32, type, c_Empty: $i).
% 53.54/26.53 thf(decl_34, type, c_Power: $i > $i).
% 53.54/26.53 thf(decl_87, type, c_Inj1: $i > $i).
% 53.54/26.53 thf(decl_88, type, c_Inj0: $i > $i).
% 53.54/26.53 thf(decl_91, type, c_setsum: $i > $i > $i).
% 53.54/26.53 thf(decl_192, type, esk1_0: ($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i).
% 53.54/26.53 thf(decl_193, type, esk2_0: ($i > $i) > $i > $i).
% 53.54/26.53 thf(decl_194, type, esk3_0: ((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i).
% 53.54/26.53 thf(decl_195, type, esk4_0: ($i > $i) > ($i > $i) > $i).
% 53.54/26.53 thf(decl_197, type, esk5_0: $i).
% 53.54/26.53 thf(decl_205, type, esk13_2: $i > $i > $i).
% 53.54/26.53 thf(decl_237, type, esk42_0: $i > (($i > $i > $i > $i) > $i) > $i > $i).
% 53.54/26.53 thf(decl_238, type, esk43_0: $i > $i > $i).
% 53.54/26.53 thf(decl_239, type, esk44_0: $i > $i > $i > $i).
% 53.54/26.53 thf(decl_240, type, esk45_1: ($i > $i) > $i > $i).
% 53.54/26.53 thf(decl_241, type, esk46_0: ($i > $i > $i) > $i).
% 53.54/26.53 thf(decl_246, type, esk51_0: (($i > $i > $i > $i) > $i) > $i > $i).
% 53.54/26.53 thf(conj, conjecture, ![X201:($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i, X202:($i > $i) > $i > $i, X203:((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i, X204:($i > $i) > ($i > $i) > $i]:((![X205:$i > (($i > $i) > $i) > $i, X206:($i > $i) > $i, X207:(($i > $i > $i) > ($i > $i) > $i) > $i, X208:$i]:(((X204 @ (^[X209:$i]:(c_Inj1 @ c_Empty)) @ (^[X210:$i]:(c_setsum @ c_Empty @ c_Empty)))=(c_Inj1 @ c_Empty)))=>(![X66:$i, X211:$i, X83:$i, X212:$i]:(((X204 @ (^[X213:$i]:(X83)) @ (^[X214:$i]:(X212)))=(c_setsum @ (X203 @ (^[X215:($i > $i > $i > $i) > $i, X216:$i]:(c_Empty)) @ (X201 @ (^[X217:$i, X218:$i, X219:$i]:(X204 @ (^[X220:$i]:(X219)) @ (^[X221:$i]:(c_Empty)))) @ (^[X222:$i]:(c_Empty)) @ (^[X223:$i > $i > $i]:(c_Empty)))) @ c_Empty)))=>(![X224:$i > $i, X225:$i > $i > $i, X226:$i > $i, X227:$i]:(((X203 @ (^[X228:($i > $i > $i > $i) > $i, X229:$i]:(X227)) @ c_Empty)=(X227)))=>(![X230:$i > ($i > $i > $i) > $i, X82:$i > $i, X231:((($i > $i) > $i) > $i) > $i, X232:$i > $i]:(((X203 @ (^[X233:($i > $i > $i > $i) > $i, X234:$i]:(X232 @ (X203 @ (^[X235:($i > $i > $i > $i) > $i, X236:$i]:(X201 @ (^[X237:$i, X238:$i, X172:$i]:(c_Inj1 @ c_Empty)) @ (^[X239:$i]:(c_Inj0 @ c_Empty)) @ (^[X170:$i > $i > $i]:(X204 @ (^[X240:$i]:(c_Empty)) @ (^[X241:$i]:(c_Empty)))))) @ (c_Inj0 @ (X201 @ (^[X242:$i, X243:$i, X244:$i]:(c_Empty)) @ (^[X245:$i]:(c_Empty)) @ (^[X168:$i > $i > $i]:(c_Empty))))))) @ (X204 @ (^[X246:$i]:(c_setsum @ X246 @ c_Empty)) @ (^[X247:$i]:(c_Empty))))=(c_setsum @ (X232 @ (X82 @ (X201 @ (^[X248:$i, X249:$i, X250:$i]:(c_Inj1 @ c_Empty)) @ (^[X251:$i]:(X201 @ (^[X252:$i, X253:$i, X254:$i]:(c_Empty)) @ (^[X255:$i]:(c_Empty)) @ (^[X256:$i > $i > $i]:(c_Empty)))) @ (^[X257:$i > $i > $i]:(c_setsum @ c_Empty @ c_Empty))))) @ (X202 @ (^[X258:$i]:(X232 @ c_Empty)) @ (X82 @ (X230 @ (X202 @ (^[X259:$i]:(c_Empty)) @ c_Empty) @ (^[X260:$i, X261:$i]:(c_Empty))))))))=>(![X262:(($i > $i) > $i > $i) > $i, X263:$i, X83:$i, X264:$i]:(((X202 @ (^[X265:$i]:(c_Inj1 @ (X202 @ (^[X266:$i]:(c_Inj0 @ (X201 @ (^[X267:$i, X268:$i, X269:$i]:(c_Empty)) @ (^[X270:$i]:(c_Empty)) @ (^[X168:$i > $i > $i]:(c_Empty))))) @ (c_Inj1 @ X264)))) @ (c_Inj0 @ (X203 @ (^[X271:($i > $i > $i > $i) > $i, X272:$i]:(X272)) @ X263)))=(c_Inj0 @ (X203 @ (^[X273:($i > $i > $i > $i) > $i, X274:$i]:(X264)) @ (c_setsum @ c_Empty @ c_Empty)))))=>(![X275:(($i > $i) > $i) > $i, X276:$i > $i > ($i > $i) > $i, X83:$i, X277:($i > $i) > ($i > $i) > $i]:(((X202 @ (^[X278:$i]:(X277 @ (^[X279:$i]:(c_setsum @ X279 @ X278)) @ (^[X280:$i]:(c_Empty)))) @ c_Empty)=(X277 @ (^[X281:$i]:(c_setsum @ (X203 @ (^[X282:($i > $i > $i > $i) > $i, X283:$i]:(c_Empty)) @ (X204 @ (^[X284:$i]:(X203 @ (^[X285:($i > $i > $i > $i) > $i, X286:$i]:(c_Empty)) @ c_Empty)) @ (^[X287:$i]:(X202 @ (^[X288:$i]:(c_Empty)) @ c_Empty)))) @ (X203 @ (^[X289:($i > $i > $i > $i) > $i, X290:$i]:(c_Empty)) @ (X203 @ (^[X291:($i > $i > $i > $i) > $i, X292:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (X203 @ (^[X293:($i > $i > $i > $i) > $i, X294:$i]:(c_Empty)) @ c_Empty))))) @ (^[X295:$i]:(c_Inj1 @ (X202 @ (^[X296:$i]:(X277 @ (^[X297:$i]:(X202 @ (^[X298:$i]:(c_Empty)) @ c_Empty)) @ (^[X299:$i]:(c_Inj1 @ c_Empty)))) @ X83))))))=>(![X300:$i > (($i > $i) > $i > $i) > $i, X301:$i, X83:$i, X302:$i]:(((X201 @ (^[X303:$i, X304:$i, X305:$i]:(X302)) @ (^[X306:$i]:(X83)) @ (^[X307:$i > $i > $i]:(c_Empty)))=(X83)))=>(![X66:$i, X308:$i, X309:$i > ($i > $i) > $i, X310:$i > $i]:(((X201 @ (^[X311:$i, X312:$i, X313:$i]:(X202 @ (^[X314:$i]:(X203 @ (^[X315:($i > $i > $i > $i) > $i, X316:$i]:(X313)) @ (X203 @ (^[X317:($i > $i > $i > $i) > $i, X318:$i]:(c_setsum @ c_Empty @ c_Empty)) @ X314))) @ (c_Inj1 @ c_Empty))) @ (^[X319:$i]:(X310 @ c_Empty)) @ (^[X320:$i > $i > $i]:(c_Empty)))=(X310 @ X66)))=>(c_False)))))))))), file('/export/starexec/sandbox/tmp/tmp.MdlW2Dnvn6/E---3.1_901530.p', conj)).
% 53.54/26.53 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox/tmp/tmp.MdlW2Dnvn6/E---3.1_901530.p', ax13)).
% 53.54/26.53 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox/tmp/tmp.MdlW2Dnvn6/E---3.1_901530.p', ax5)).
% 53.54/26.53 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.MdlW2Dnvn6/E---3.1_901530.p', ax17)).
% 53.54/26.53 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.MdlW2Dnvn6/E---3.1_901530.p', ax7)).
% 53.54/26.53 thf(ax3, axiom, ![X4:$o, X5:$o]:(((c_iff @ ((X4)) @ ((X5)))=>((X4)<=>(X5)))), file('/export/starexec/sandbox/tmp/tmp.MdlW2Dnvn6/E---3.1_901530.p', ax3)).
% 53.54/26.53 thf(c_0_6, negated_conjecture, ~(![X201:($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i, X202:($i > $i) > $i > $i, X203:((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i, X204:($i > $i) > ($i > $i) > $i]:((![X205:$i > (($i > $i) > $i) > $i, X206:($i > $i) > $i, X207:(($i > $i > $i) > ($i > $i) > $i) > $i, X208:$i]:(((X204 @ (^[X209:$i]:(c_Inj1 @ c_Empty)) @ (^[X210:$i]:(c_setsum @ c_Empty @ c_Empty)))=(c_Inj1 @ c_Empty)))=>(![X66:$i, X211:$i, X83:$i, X212:$i]:(((X204 @ (^[X213:$i]:(X83)) @ (^[X214:$i]:(X212)))=(c_setsum @ (X203 @ (^[X215:($i > $i > $i > $i) > $i, X216:$i]:(c_Empty)) @ (X201 @ (^[X217:$i, X218:$i, X219:$i]:(X204 @ (^[X220:$i]:(X219)) @ (^[X221:$i]:(c_Empty)))) @ (^[X222:$i]:(c_Empty)) @ (^[X223:$i > $i > $i]:(c_Empty)))) @ c_Empty)))=>(![X224:$i > $i, X225:$i > $i > $i, X226:$i > $i, X227:$i]:(((X203 @ (^[X228:($i > $i > $i > $i) > $i, X229:$i]:(X227)) @ c_Empty)=(X227)))=>(![X230:$i > ($i > $i > $i) > $i, X82:$i > $i, X231:((($i > $i) > $i) > $i) > $i, X232:$i > $i]:(((X203 @ (^[X233:($i > $i > $i > $i) > $i, X234:$i]:(X232 @ (X203 @ (^[X235:($i > $i > $i > $i) > $i, X236:$i]:(X201 @ (^[X237:$i, X238:$i, X172:$i]:(c_Inj1 @ c_Empty)) @ (^[X239:$i]:(c_Inj0 @ c_Empty)) @ (^[X170:$i > $i > $i]:(X204 @ (^[X240:$i]:(c_Empty)) @ (^[X241:$i]:(c_Empty)))))) @ (c_Inj0 @ (X201 @ (^[X242:$i, X243:$i, X244:$i]:(c_Empty)) @ (^[X245:$i]:(c_Empty)) @ (^[X168:$i > $i > $i]:(c_Empty))))))) @ (X204 @ (^[X246:$i]:(c_setsum @ X246 @ c_Empty)) @ (^[X247:$i]:(c_Empty))))=(c_setsum @ (X232 @ (X82 @ (X201 @ (^[X248:$i, X249:$i, X250:$i]:(c_Inj1 @ c_Empty)) @ (^[X251:$i]:(X201 @ (^[X252:$i, X253:$i, X254:$i]:(c_Empty)) @ (^[X255:$i]:(c_Empty)) @ (^[X256:$i > $i > $i]:(c_Empty)))) @ (^[X257:$i > $i > $i]:(c_setsum @ c_Empty @ c_Empty))))) @ (X202 @ (^[X258:$i]:(X232 @ c_Empty)) @ (X82 @ (X230 @ (X202 @ (^[X259:$i]:(c_Empty)) @ c_Empty) @ (^[X260:$i, X261:$i]:(c_Empty))))))))=>(![X262:(($i > $i) > $i > $i) > $i, X263:$i, X83:$i, X264:$i]:(((X202 @ (^[X265:$i]:(c_Inj1 @ (X202 @ (^[X266:$i]:(c_Inj0 @ (X201 @ (^[X267:$i, X268:$i, X269:$i]:(c_Empty)) @ (^[X270:$i]:(c_Empty)) @ (^[X168:$i > $i > $i]:(c_Empty))))) @ (c_Inj1 @ X264)))) @ (c_Inj0 @ (X203 @ (^[X271:($i > $i > $i > $i) > $i, X272:$i]:(X272)) @ X263)))=(c_Inj0 @ (X203 @ (^[X273:($i > $i > $i > $i) > $i, X274:$i]:(X264)) @ (c_setsum @ c_Empty @ c_Empty)))))=>(![X275:(($i > $i) > $i) > $i, X276:$i > $i > ($i > $i) > $i, X83:$i, X277:($i > $i) > ($i > $i) > $i]:(((X202 @ (^[X278:$i]:(X277 @ (^[X279:$i]:(c_setsum @ X279 @ X278)) @ (^[X280:$i]:(c_Empty)))) @ c_Empty)=(X277 @ (^[X281:$i]:(c_setsum @ (X203 @ (^[X282:($i > $i > $i > $i) > $i, X283:$i]:(c_Empty)) @ (X204 @ (^[X284:$i]:(X203 @ (^[X285:($i > $i > $i > $i) > $i, X286:$i]:(c_Empty)) @ c_Empty)) @ (^[X287:$i]:(X202 @ (^[X288:$i]:(c_Empty)) @ c_Empty)))) @ (X203 @ (^[X289:($i > $i > $i > $i) > $i, X290:$i]:(c_Empty)) @ (X203 @ (^[X291:($i > $i > $i > $i) > $i, X292:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (X203 @ (^[X293:($i > $i > $i > $i) > $i, X294:$i]:(c_Empty)) @ c_Empty))))) @ (^[X295:$i]:(c_Inj1 @ (X202 @ (^[X296:$i]:(X277 @ (^[X297:$i]:(X202 @ (^[X298:$i]:(c_Empty)) @ c_Empty)) @ (^[X299:$i]:(c_Inj1 @ c_Empty)))) @ X83))))))=>(![X300:$i > (($i > $i) > $i > $i) > $i, X301:$i, X83:$i, X302:$i]:(((X201 @ (^[X303:$i, X304:$i, X305:$i]:(X302)) @ (^[X306:$i]:(X83)) @ (^[X307:$i > $i > $i]:(c_Empty)))=(X83)))=>(![X66:$i, X308:$i, X309:$i > ($i > $i) > $i, X310:$i > $i]:(((X201 @ (^[X311:$i, X312:$i, X313:$i]:(X202 @ (^[X314:$i]:(X203 @ (^[X315:($i > $i > $i > $i) > $i, X316:$i]:(X313)) @ (X203 @ (^[X317:($i > $i > $i > $i) > $i, X318:$i]:(c_setsum @ c_Empty @ c_Empty)) @ X314))) @ (c_Inj1 @ c_Empty))) @ (^[X319:$i]:(X310 @ c_Empty)) @ (^[X320:$i > $i > $i]:(c_Empty)))=(X310 @ X66)))=>(c_False))))))))))), inference(assume_negation,[status(cth)],[conj])).
% 53.54/26.53 thf(c_0_7, plain, ![X385:$o]:(((c_not @ ((X385)))<=>((X385)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 53.54/26.53 thf(c_0_8, negated_conjecture, ~(![X201:($i > $i > $i > $i) > ($i > $i) > (($i > $i > $i) > $i) > $i, X202:($i > $i) > $i > $i, X203:((($i > $i > $i > $i) > $i) > $i > $i) > $i > $i, X204:($i > $i) > ($i > $i) > $i]:((![X205:$i > (($i > $i) > $i) > $i, X206:($i > $i) > $i, X207:(($i > $i > $i) > ($i > $i) > $i) > $i, X208:$i]:(((X204 @ (^[Z0:$i]:(c_Inj1 @ c_Empty)) @ (^[Z0:$i]:(c_setsum @ c_Empty @ c_Empty)))=(c_Inj1 @ c_Empty)))=>(![X66:$i, X211:$i, X83:$i, X212:$i]:(((X204 @ (^[Z0:$i]:(X83)) @ (^[Z0:$i]:(X212)))=(c_setsum @ (X203 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(c_Empty)) @ (X201 @ (^[Z0:$i, Z1:$i, Z2:$i]:(X204 @ (^[Z3:$i]:(Z2)) @ (^[Z3:$i]:(c_Empty)))) @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i > $i > $i]:(c_Empty)))) @ c_Empty)))=>(![X224:$i > $i, X225:$i > $i > $i, X226:$i > $i, X227:$i]:(((X203 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(X227)) @ c_Empty)=(X227)))=>(![X230:$i > ($i > $i > $i) > $i, X82:$i > $i, X231:((($i > $i) > $i) > $i) > $i, X232:$i > $i]:(((X203 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(X232 @ (X203 @ (^[Z2:($i > $i > $i > $i) > $i, Z3:$i]:(X201 @ (^[Z4:$i, Z5:$i, Z6:$i]:(c_Inj1 @ c_Empty)) @ (^[Z4:$i]:(c_Inj0 @ c_Empty)) @ (^[Z4:$i > $i > $i]:(X204 @ (^[Z5:$i]:(c_Empty)) @ (^[Z5:$i]:(c_Empty)))))) @ (c_Inj0 @ (X201 @ (^[Z2:$i, Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ (^[Z2:$i > $i > $i]:(c_Empty))))))) @ (X204 @ (^[Z0:$i]:(c_setsum @ Z0 @ c_Empty)) @ (^[Z0:$i]:(c_Empty))))=(c_setsum @ (X232 @ (X82 @ (X201 @ (^[Z0:$i, Z1:$i, Z2:$i]:(c_Inj1 @ c_Empty)) @ (^[Z0:$i]:(X201 @ (^[Z1:$i, Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i > $i > $i]:(c_Empty)))) @ (^[Z0:$i > $i > $i]:(c_setsum @ c_Empty @ c_Empty))))) @ (X202 @ (^[Z0:$i]:(X232 @ c_Empty)) @ (X82 @ (X230 @ (X202 @ (^[Z0:$i]:(c_Empty)) @ c_Empty) @ (^[Z0:$i, Z1:$i]:(c_Empty))))))))=>(![X262:(($i > $i) > $i > $i) > $i, X263:$i, X83:$i, X264:$i]:(((X202 @ (^[Z0:$i]:(c_Inj1 @ (X202 @ (^[Z1:$i]:(c_Inj0 @ (X201 @ (^[Z2:$i, Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ (^[Z2:$i > $i > $i]:(c_Empty))))) @ (c_Inj1 @ X264)))) @ (c_Inj0 @ (X203 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(Z1)) @ X263)))=(c_Inj0 @ (X203 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(X264)) @ (c_setsum @ c_Empty @ c_Empty)))))=>(![X275:(($i > $i) > $i) > $i, X276:$i > $i > ($i > $i) > $i, X83:$i, X277:($i > $i) > ($i > $i) > $i]:(((X202 @ (^[Z0:$i]:(X277 @ (^[Z1:$i]:(c_setsum @ Z1 @ Z0)) @ (^[Z1:$i]:(c_Empty)))) @ c_Empty)=(X277 @ (^[Z0:$i]:(c_setsum @ (X203 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_Empty)) @ (X204 @ (^[Z1:$i]:(X203 @ (^[Z2:($i > $i > $i > $i) > $i, Z3:$i]:(c_Empty)) @ c_Empty)) @ (^[Z1:$i]:(X202 @ (^[Z2:$i]:(c_Empty)) @ c_Empty)))) @ (X203 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_Empty)) @ (X203 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (X203 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_Empty)) @ c_Empty))))) @ (^[Z0:$i]:(c_Inj1 @ (X202 @ (^[Z1:$i]:(X277 @ (^[Z2:$i]:(X202 @ (^[Z3:$i]:(c_Empty)) @ c_Empty)) @ (^[Z2:$i]:(c_Inj1 @ c_Empty)))) @ X83))))))=>(![X300:$i > (($i > $i) > $i > $i) > $i, X301:$i, X83:$i, X302:$i]:(((X201 @ (^[Z0:$i, Z1:$i, Z2:$i]:(X302)) @ (^[Z0:$i]:(X83)) @ (^[Z0:$i > $i > $i]:(c_Empty)))=(X83)))=>(![X66:$i, X308:$i, X309:$i > ($i > $i) > $i, X310:$i > $i]:(((X201 @ (^[Z0:$i, Z1:$i, Z2:$i]:(X202 @ (^[Z3:$i]:(X203 @ (^[Z4:($i > $i > $i > $i) > $i, Z5:$i]:(Z2)) @ (X203 @ (^[Z4:($i > $i > $i > $i) > $i, Z5:$i]:(c_setsum @ c_Empty @ c_Empty)) @ Z3))) @ (c_Inj1 @ c_Empty))) @ (^[Z0:$i]:(X310 @ c_Empty)) @ (^[Z0:$i > $i > $i]:(c_Empty)))=(X310 @ X66)))=>(c_False))))))))))), inference(fof_simplification,[status(thm)],[c_0_6])).
% 53.54/26.53 thf(c_0_9, axiom, ((~(?[X7:$i]:((c_In @ X7 @ c_Empty)))|(c_not @ $true))&(?[X7:$i]:((c_In @ X7 @ c_Empty))|(c_not @ $false))), inference(fool_unroll,[status(thm)],[ax5])).
% 53.54/26.53 thf(c_0_10, plain, ![X505:$o]:(((~(c_not @ ((X505)))|(~(X505)|(c_False)))&(((X505)|(c_not @ ((X505))))&(~(c_False)|(c_not @ ((X505))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])).
% 53.54/26.53 thf(c_0_11, negated_conjecture, ![X489:$i, X490:$i, X491:$i, X492:$i > ($i > $i > $i) > $i, X493:$i > $i, X494:$i > $i, X495:$i, X496:$i, X497:$i, X498:($i > $i) > ($i > $i) > $i, X499:$i, X500:$i, X501:$i, X502:$i > $i]:((((esk4_0 @ (^[Z0:$i]:(c_Inj1 @ c_Empty)) @ (^[Z0:$i]:(c_setsum @ c_Empty @ c_Empty)))=(c_Inj1 @ c_Empty))&(((esk4_0 @ (^[Z0:$i]:(X489)) @ (^[Z0:$i]:(X490)))=(c_setsum @ (esk3_0 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(c_Empty)) @ (esk1_0 @ (^[Z0:$i, Z1:$i, Z2:$i]:(esk4_0 @ (^[Z3:$i]:(Z2)) @ (^[Z3:$i]:(c_Empty)))) @ (^[Z0:$i]:(c_Empty)) @ (^[Z0:$i > $i > $i]:(c_Empty)))) @ c_Empty))&(((esk3_0 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(X491)) @ c_Empty)=(X491))&(((esk3_0 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(X494 @ (esk3_0 @ (^[Z2:($i > $i > $i > $i) > $i, Z3:$i]:(esk1_0 @ (^[Z4:$i, Z5:$i, Z6:$i]:(c_Inj1 @ c_Empty)) @ (^[Z4:$i]:(c_Inj0 @ c_Empty)) @ (^[Z4:$i > $i > $i]:(esk4_0 @ (^[Z5:$i]:(c_Empty)) @ (^[Z5:$i]:(c_Empty)))))) @ (c_Inj0 @ (esk1_0 @ (^[Z2:$i, Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ (^[Z2:$i > $i > $i]:(c_Empty))))))) @ (esk4_0 @ (^[Z0:$i]:(c_setsum @ Z0 @ c_Empty)) @ (^[Z0:$i]:(c_Empty))))=(c_setsum @ (X494 @ (X493 @ (esk1_0 @ (^[Z0:$i, Z1:$i, Z2:$i]:(c_Inj1 @ c_Empty)) @ (^[Z0:$i]:(esk1_0 @ (^[Z1:$i, Z2:$i, Z3:$i]:(c_Empty)) @ (^[Z1:$i]:(c_Empty)) @ (^[Z1:$i > $i > $i]:(c_Empty)))) @ (^[Z0:$i > $i > $i]:(c_setsum @ c_Empty @ c_Empty))))) @ (esk2_0 @ (^[Z0:$i]:(X494 @ c_Empty)) @ (X493 @ (X492 @ (esk2_0 @ (^[Z0:$i]:(c_Empty)) @ c_Empty) @ (^[Z0:$i, Z1:$i]:(c_Empty)))))))&(((esk2_0 @ (^[Z0:$i]:(c_Inj1 @ (esk2_0 @ (^[Z1:$i]:(c_Inj0 @ (esk1_0 @ (^[Z2:$i, Z3:$i, Z4:$i]:(c_Empty)) @ (^[Z2:$i]:(c_Empty)) @ (^[Z2:$i > $i > $i]:(c_Empty))))) @ (c_Inj1 @ X496)))) @ (c_Inj0 @ (esk3_0 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(Z1)) @ X495)))=(c_Inj0 @ (esk3_0 @ (^[Z0:($i > $i > $i > $i) > $i, Z1:$i]:(X496)) @ (c_setsum @ c_Empty @ c_Empty))))&(((esk2_0 @ (^[Z0:$i]:(X498 @ (^[Z1:$i]:(c_setsum @ Z1 @ Z0)) @ (^[Z1:$i]:(c_Empty)))) @ c_Empty)=(X498 @ (^[Z0:$i]:(c_setsum @ (esk3_0 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_Empty)) @ (esk4_0 @ (^[Z1:$i]:(esk3_0 @ (^[Z2:($i > $i > $i > $i) > $i, Z3:$i]:(c_Empty)) @ c_Empty)) @ (^[Z1:$i]:(esk2_0 @ (^[Z2:$i]:(c_Empty)) @ c_Empty)))) @ (esk3_0 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_Empty)) @ (esk3_0 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_setsum @ c_Empty @ c_Empty)) @ (esk3_0 @ (^[Z1:($i > $i > $i > $i) > $i, Z2:$i]:(c_Empty)) @ c_Empty))))) @ (^[Z0:$i]:(c_Inj1 @ (esk2_0 @ (^[Z1:$i]:(X498 @ (^[Z2:$i]:(esk2_0 @ (^[Z3:$i]:(c_Empty)) @ c_Empty)) @ (^[Z2:$i]:(c_Inj1 @ c_Empty)))) @ X497)))))&(((esk1_0 @ (^[Z0:$i, Z1:$i, Z2:$i]:(X500)) @ (^[Z0:$i]:(X499)) @ (^[Z0:$i > $i > $i]:(c_Empty)))=(X499))&(((esk1_0 @ (^[Z0:$i, Z1:$i, Z2:$i]:(esk2_0 @ (^[Z3:$i]:(esk3_0 @ (^[Z4:($i > $i > $i > $i) > $i, Z5:$i]:(Z2)) @ (esk3_0 @ (^[Z4:($i > $i > $i > $i) > $i, Z5:$i]:(c_setsum @ c_Empty @ c_Empty)) @ Z3))) @ (c_Inj1 @ c_Empty))) @ (^[Z0:$i]:(X502 @ c_Empty)) @ (^[Z0:$i > $i > $i]:(c_Empty)))=(X502 @ X501))&~(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])])])])])])).
% 53.54/26.53 thf(c_0_12, plain, ![X506:$i]:(((~(c_In @ X506 @ 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])])])])])).
% 53.54/26.53 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])])])).
% 53.54/26.53 thf(c_0_14, negated_conjecture, ~((c_False)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 53.54/26.53 thf(c_0_15, plain, ![X389:$i, X390:$i]:(((c_Subq @ X389 @ X390)<=>![X9:$i]:(((c_In @ X9 @ X389)=>(c_In @ X9 @ X390))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 53.54/26.53 thf(c_0_16, plain, ![X912:$i > $i > $i]:(((esk46_0 @ X912)=(c_Empty))), introduced(definition)).
% 53.54/26.53 thf(c_0_17, plain, ![X911:$i, X12:$i > $i]:(((esk45_1 @ X12 @ X911)=(X12 @ c_Empty))), introduced(definition)).
% 53.54/26.53 thf(c_0_18, plain, ![X910:$i, X909:$i, X908:$i]:(((esk44_0 @ X908 @ X909 @ X910)=(esk2_0 @ (esk43_0 @ X910) @ (c_Inj1 @ c_Empty)))), introduced(definition)).
% 53.54/26.53 thf(c_0_19, plain, ![X906:$i, X907:$i]:(((esk43_0 @ X907 @ X906)=(esk3_0 @ (esk42_0 @ X907) @ (esk3_0 @ (esk42_0 @ (c_setsum @ c_Empty @ c_Empty)) @ X906)))), introduced(definition)).
% 53.54/26.53 thf(c_0_20, plain, ![X902:$i, X901:($i > $i > $i > $i) > $i, X903:$i]:(((esk42_0 @ X903 @ X901 @ X902)=(X903))), introduced(definition)).
% 53.54/26.53 thf(c_0_21, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 53.54/26.53 thf(c_0_22, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_13, c_0_14])).
% 53.54/26.53 thf(c_0_23, plain, ![X525:$i, X526:$i, X527:$i, X528:$i, X529:$i]:(((~(c_Subq @ X525 @ X526)|(~(c_In @ X527 @ X525)|(c_In @ X527 @ X526)))&(((c_In @ (esk13_2 @ X528 @ X529) @ X528)|(c_Subq @ X528 @ X529))&(~(c_In @ (esk13_2 @ X528 @ X529) @ X529)|(c_Subq @ X528 @ X529))))), 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_15])])])])])])])).
% 53.54/26.53 thf(c_0_24, plain, ![X1087:$i, X1088:($i > $i > $i > $i) > $i]:(((esk51_0 @ X1088 @ X1087)=(X1087))), inference(variable_rename,[status(thm)],[])).
% 53.54/26.53 thf(c_0_25, negated_conjecture, ![X12:$i > $i, X2:$i]:(((esk1_0 @ esk44_0 @ (esk45_1 @ X12) @ esk46_0)=(X12 @ 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(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11]), c_0_16]), c_0_17]), c_0_18]), c_0_19]), c_0_20]), c_0_20])).
% 53.54/26.53 thf(c_0_26, axiom, ![X10:$i, X2:$i]:(((~(c_In @ X2 @ (c_Power @ X10))|((~(c_Subq @ X2 @ X10)|(c_iff @ $true @ $true))&((c_Subq @ X2 @ X10)|(c_iff @ $true @ $false))))&((c_In @ X2 @ (c_Power @ X10))|((~(c_Subq @ X2 @ X10)|(c_iff @ $false @ $true))&((c_Subq @ X2 @ X10)|(c_iff @ $false @ $false)))))), inference(fool_unroll,[status(thm)],[ax7])).
% 53.54/26.53 thf(c_0_27, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_21, c_0_22])).
% 53.54/26.53 thf(c_0_28, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 53.54/26.53 thf(c_0_29, plain, ![X215:($i > $i > $i > $i) > $i, X2:$i]:(((esk51_0 @ X215 @ X2)=(X2))), inference(split_conjunct,[status(thm)],[c_0_24])).
% 53.54/26.53 thf(c_0_30, negated_conjecture, ![X2:$i, X12:$i > $i, X6:$i]:(((X12 @ X2)=(X12 @ X6))), inference(spm,[status(thm)],[c_0_25, c_0_25])).
% 53.54/26.53 thf(c_0_31, plain, ![X547:$i, X548:$i]:((((~(c_Subq @ X548 @ X547)|(c_iff @ $true @ $true)|~(c_In @ X548 @ (c_Power @ X547)))&((c_Subq @ X548 @ X547)|(c_iff @ $true @ $false)|~(c_In @ X548 @ (c_Power @ X547))))&((~(c_Subq @ X548 @ X547)|(c_iff @ $false @ $true)|(c_In @ X548 @ (c_Power @ X547)))&((c_Subq @ X548 @ X547)|(c_iff @ $false @ $false)|(c_In @ X548 @ (c_Power @ X547)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_26])])])).
% 53.54/26.53 thf(c_0_32, plain, ![X2:$i]:((c_Subq @ c_Empty @ X2)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 53.54/26.53 thf(c_0_33, plain, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_29])).
% 53.54/26.53 thf(c_0_34, plain, ![X579:$o, X580:$o]:(((~(X579)|(X580)|~(c_iff @ ((X579)) @ ((X580))))&(~(X580)|(X579)|~(c_iff @ ((X579)) @ ((X580)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3])])])])).
% 53.54/26.53 thf(c_0_35, 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_31])).
% 53.54/26.53 thf(c_0_36, plain, ![X2:$i, X6:$i]:((c_Subq @ X2 @ X6)), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 53.54/26.53 thf(c_0_37, plain, ![X2:$i, X6:$i]:(~((c_In @ X2 @ X6))), inference(spm,[status(thm)],[c_0_27, c_0_33])).
% 53.54/26.53 thf(c_0_38, plain, ~((c_iff @ (~($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_34])])])).
% 53.54/26.53 thf(c_0_39, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])]), c_0_37]), c_0_38]), ['proof']).
% 53.54/26.53 % SZS output end CNFRefutation
% 53.54/26.53 % Parsed axioms : 213
% 53.54/26.53 % Removed by relevancy pruning/SinE : 145
% 53.54/26.53 % Initial clauses : 465131
% 53.54/26.53 % Removed in clause preprocessing : 463015
% 53.54/26.53 % Initial clauses in saturation : 2116
% 53.54/26.53 % Processed clauses : 433
% 53.54/26.53 % ...of these trivial : 78
% 53.54/26.53 % ...subsumed : 121
% 53.54/26.53 % ...remaining for further processing : 233
% 53.54/26.53 % Other redundant clauses eliminated : 2
% 53.54/26.53 % Clauses deleted for lack of memory : 0
% 53.54/26.53 % Backward-subsumed : 97
% 53.54/26.53 % Backward-rewritten : 29
% 53.54/26.53 % Generated clauses : 428
% 53.54/26.53 % ...of the previous two non-redundant : 354
% 53.54/26.53 % ...aggressively subsumed : 0
% 53.54/26.53 % Contextual simplify-reflections : 6
% 53.54/26.53 % Paramodulations : 416
% 53.54/26.53 % Factorizations : 0
% 53.54/26.53 % NegExts : 0
% 53.54/26.53 % Equation resolutions : 2
% 53.54/26.53 % Disequality decompositions : 0
% 53.54/26.53 % Total rewrite steps : 293
% 53.54/26.53 % ...of those cached : 195
% 53.54/26.53 % Propositional unsat checks : 0
% 53.54/26.53 % Propositional check models : 0
% 53.54/26.53 % Propositional check unsatisfiable : 0
% 53.54/26.53 % Propositional clauses : 0
% 53.54/26.53 % Propositional clauses after purity: 0
% 53.54/26.53 % Propositional unsat core size : 0
% 53.54/26.53 % Propositional preprocessing time : 0.000
% 53.54/26.53 % Propositional encoding time : 0.000
% 53.54/26.53 % Propositional solver time : 0.000
% 53.54/26.53 % Success case prop preproc time : 0.000
% 53.54/26.53 % Success case prop encoding time : 0.000
% 53.54/26.53 % Success case prop solver time : 0.000
% 53.54/26.53 % Current number of processed clauses : 104
% 53.54/26.53 % Positive orientable unit clauses : 25
% 53.54/26.53 % Positive unorientable unit clauses: 3
% 53.54/26.53 % Negative unit clauses : 13
% 53.54/26.53 % Non-unit-clauses : 63
% 53.54/26.53 % Current number of unprocessed clauses: 1850
% 53.54/26.53 % ...number of literals in the above : 9588
% 53.54/26.53 % Current number of archived formulas : 0
% 53.54/26.53 % Current number of archived clauses : 127
% 53.54/26.53 % Clause-clause subsumption calls (NU) : 3626
% 53.54/26.53 % Rec. Clause-clause subsumption calls : 3174
% 53.54/26.53 % Non-unit clause-clause subsumptions : 61
% 53.54/26.53 % Unit Clause-clause subsumption calls : 1329
% 53.54/26.53 % Rewrite failures with RHS unbound : 531
% 53.54/26.53 % BW rewrite match attempts : 1278
% 53.54/26.53 % BW rewrite match successes : 421
% 53.54/26.53 % Condensation attempts : 0
% 53.54/26.53 % Condensation successes : 0
% 53.54/26.53 % Termbank termtop insertions : 19578132
% 53.54/26.53 % Search garbage collected termcells : 1981326
% 53.54/26.53
% 53.54/26.53 % -------------------------------------------------
% 53.54/26.53 % User time : 24.109 s
% 53.54/26.53 % System time : 1.488 s
% 53.54/26.53 % Total time : 25.597 s
% 53.54/26.53 % Maximum resident set size: 1249832 pages
% 53.54/26.53
% 53.54/26.53 % -------------------------------------------------
% 53.54/26.53 % User time : 25.237 s
% 53.54/26.53 % System time : 2.150 s
% 53.54/26.53 % Total time : 27.387 s
% 53.54/26.53 % Maximum resident set size: 5376 pages
% 53.54/26.53 % E exiting
%------------------------------------------------------------------------------