%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GEG011^1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 07:49:19 AM UTC 2026
% Result : Theorem 0.21s 0.29s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEG011^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n009.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 18:34:15 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.24 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.KDIcDYY7vl/E---3.1_190859.p
% 0.21/0.29 % Version: 3.5.1-ho
% 0.21/0.29 % Preprocessing class: HSMSSMSSMLLNHSN.
% 0.21/0.29 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.29 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.21/0.29 % Starting post_as_ho3 with 300s (1) cores
% 0.21/0.29 % Starting new_ho_12 with 300s (1) cores
% 0.21/0.29 % Starting new_bool_2 with 300s (1) cores
% 0.21/0.29 % new_ho_10_cnf2 with pid 190890 completed with status 0
% 0.21/0.29 % Result found by new_ho_10_cnf2
% 0.21/0.29 % Preprocessing class: HSMSSMSSMLLNHSN.
% 0.21/0.29 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.29 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.21/0.29 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.29 % No SInE strategy applied
% 0.21/0.29 % Search class: HGHNF-FFMF21-SHSSMSBN
% 0.21/0.29 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.21/0.29 % Starting SubtermCWHack with 136s (1) cores
% 0.21/0.29 % Starting new_ho_10_cnf2 with 151s (1) cores
% 0.21/0.29 % Starting post_as_ho11 with 136s (1) cores
% 0.21/0.29 % Starting pre_casc_8 with 136s (1) cores
% 0.21/0.29 % Starting post_as_ho2 with 136s (1) cores
% 0.21/0.29 % pre_casc_8 with pid 190899 completed with status 0
% 0.21/0.29 % Result found by pre_casc_8
% 0.21/0.29 % Preprocessing class: HSMSSMSSMLLNHSN.
% 0.21/0.29 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.29 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.21/0.29 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.29 % No SInE strategy applied
% 0.21/0.29 % Search class: HGHNF-FFMF21-SHSSMSBN
% 0.21/0.29 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.21/0.29 % Starting SubtermCWHack with 136s (1) cores
% 0.21/0.29 % Starting new_ho_10_cnf2 with 151s (1) cores
% 0.21/0.29 % Starting post_as_ho11 with 136s (1) cores
% 0.21/0.29 % Starting pre_casc_8 with 136s (1) cores
% 0.21/0.29 % Preprocessing time : 0.003 s
% 0.21/0.29 % Presaturation interreduction done
% 0.21/0.29
% 0.21/0.29 % Proof found!
% 0.21/0.29 % SZS status Theorem
% 0.21/0.29 % SZS output start CNFRefutation
% 0.21/0.29 thf(decl_sort1, type, reg: $tType).
% 0.21/0.29 thf(decl_38, type, mbox: ($i > $i > $o) > ($i > $o) > $i > $o).
% 0.21/0.29 thf(decl_50, type, mvalid: ($i > $o) > $o).
% 0.21/0.29 thf(decl_54, type, c: reg > reg > $o).
% 0.21/0.29 thf(decl_56, type, p: reg > reg > $o).
% 0.21/0.29 thf(decl_58, type, o: reg > reg > $o).
% 0.21/0.29 thf(decl_60, type, ec: reg > reg > $o).
% 0.21/0.29 thf(decl_61, type, pp: reg > reg > $o).
% 0.21/0.29 thf(decl_62, type, tpp: reg > reg > $o).
% 0.21/0.29 thf(decl_63, type, ntpp: reg > reg > $o).
% 0.21/0.29 thf(decl_64, type, catalunya: reg).
% 0.21/0.29 thf(decl_65, type, france: reg).
% 0.21/0.29 thf(decl_66, type, spain: reg).
% 0.21/0.29 thf(decl_67, type, paris: reg).
% 0.21/0.29 thf(decl_68, type, a: $i > $i > $o).
% 0.21/0.29 thf(decl_70, type, epred1_1: reg > $o).
% 0.21/0.29 thf(decl_74, type, esk4_0: reg).
% 0.21/0.29 thf(decl_75, type, esk5_0: reg).
% 0.21/0.29 thf(decl_76, type, esk6_1: reg > reg).
% 0.21/0.29 thf(decl_77, type, esk7_1: reg > reg).
% 0.21/0.29 thf(decl_78, type, esk8_1: reg > reg).
% 0.21/0.29 thf(decl_79, type, esk9_1: reg > reg).
% 0.21/0.29 thf(decl_82, type, esk12_0: reg).
% 0.21/0.29 thf(decl_83, type, esk13_1: reg > reg).
% 0.21/0.29 thf(decl_84, type, esk14_1: reg > reg).
% 0.21/0.29 thf(decl_85, type, esk15_0: $i).
% 0.21/0.29 thf(decl_86, type, esk16_0: $i).
% 0.21/0.29 thf(decl_87, type, esk17_0: reg).
% 0.21/0.29 thf(decl_88, type, esk18_0: reg).
% 0.21/0.29 thf(decl_89, type, esk19_0: reg).
% 0.21/0.29 thf(decl_90, type, esk20_1: reg > reg).
% 0.21/0.29 thf(decl_91, type, esk21_2: reg > reg > reg).
% 0.21/0.29 thf(decl_92, type, esk22_2: reg > reg > reg).
% 0.21/0.29 thf(decl_93, type, esk23_1: reg > reg).
% 0.21/0.29 thf(decl_94, type, esk24_2: reg > reg > reg).
% 0.21/0.29 thf(decl_95, type, esk25_2: reg > reg > reg).
% 0.21/0.29 thf(o, axiom, ((o)=(^[X28:reg, X29:reg]:(?[X25:reg]:((((p @ X25 @ X28))&((p @ X25 @ X29))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', o)).
% 0.21/0.29 thf(p, axiom, ((p)=(^[X23:reg, X24:reg]:(![X25:reg]:((((c @ X25 @ X23))=>((c @ X25 @ X24))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', p)).
% 0.21/0.29 thf(ec, axiom, ((ec)=(^[X32:reg, X33:reg]:((((c @ X32 @ X33))&(~((o @ X32 @ X33))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', ec)).
% 0.21/0.29 thf(pp, axiom, ((pp)=(^[X34:reg, X35:reg]:((((p @ X34 @ X35))&(~((p @ X35 @ X34))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', pp)).
% 0.21/0.29 thf(ntpp, axiom, ((ntpp)=(^[X38:reg, X39:reg]:((((pp @ X38 @ X39))&(~(?[X25:reg]:((((ec @ X25 @ X38))&((ec @ X25 @ X39)))))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', ntpp)).
% 0.21/0.29 thf(mbox, axiom, ((mbox)=(^[X13:$i > $i > $o, X6:$i > $o, X3:$i]:(![X14:$i]:(((~((X13 @ X3 @ X14)))|((X6 @ X14))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', mbox)).
% 0.21/0.29 thf(mvalid, axiom, ((mvalid)=(^[X6:$i > $o]:(![X3:$i]:((X6 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', mvalid)).
% 0.21/0.29 thf(con, conjecture, (mvalid @ (mbox @ a @ (^[X44:$i]:(![X25:reg]:((((((ntpp @ france @ X25))&((ntpp @ spain @ X25))))=>((((pp @ paris @ X25))&((pp @ catalunya @ X25)))))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', con)).
% 0.21/0.29 thf(tpp, axiom, ((tpp)=(^[X36:reg, X37:reg]:((((pp @ X36 @ X37))&(?[X25:reg]:((((ec @ X25 @ X36))&((ec @ X25 @ X37))))))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', tpp)).
% 0.21/0.29 thf(ax3, axiom, (mvalid @ (mbox @ a @ (^[X43:$i]:((ntpp @ paris @ france))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', ax3)).
% 0.21/0.29 thf(ax1, axiom, (mvalid @ (mbox @ a @ (^[X41:$i]:((tpp @ catalunya @ spain))))), file('/export/starexec/sandbox2/tmp/tmp.KDIcDYY7vl/E---3.1_190859.p', ax1)).
% 0.21/0.29 thf(c_0_11, plain, ((o)=(^[Z0:reg, Z1:reg]:(?[X25:reg]:((((![X53:reg]:((((c @ X53 @ X25))=>((c @ X53 @ Z0))))))&((![X54:reg]:((((c @ X54 @ X25))=>((c @ X54 @ Z1))))))))))), inference(fof_simplification,[status(thm)],[o])).
% 0.21/0.29 thf(c_0_12, plain, ((p)=(^[Z0:reg, Z1:reg]:(![X25:reg]:((((c @ X25 @ Z0))=>((c @ X25 @ Z1))))))), inference(fof_simplification,[status(thm)],[p])).
% 0.21/0.29 thf(c_0_13, plain, ((ec)=(^[Z0:reg, Z1:reg]:((((c @ Z0 @ Z1))&(~((?[X60:reg]:((((![X61:reg]:((((c @ X61 @ X60))=>((c @ X61 @ Z0))))))&((![X62:reg]:((((c @ X62 @ X60))=>((c @ X62 @ Z1))))))))))))))), inference(fof_simplification,[status(thm)],[ec])).
% 0.21/0.29 thf(c_0_14, plain, ((o)=(^[Z0:reg, Z1:reg]:(?[X25:reg]:((((![X53:reg]:((((c @ X53 @ X25))=>((c @ X53 @ Z0))))))&((![X54:reg]:((((c @ X54 @ X25))=>((c @ X54 @ Z1))))))))))), inference(apply_def,[status(thm)],[c_0_11, c_0_12])).
% 0.21/0.29 thf(c_0_15, plain, ((pp)=(^[Z0:reg, Z1:reg]:((((![X63:reg]:((((c @ X63 @ Z0))=>((c @ X63 @ Z1))))))&(~((![X64:reg]:((((c @ X64 @ Z1))=>((c @ X64 @ Z0))))))))))), inference(fof_simplification,[status(thm)],[pp])).
% 0.21/0.29 thf(c_0_16, plain, ((ntpp)=(^[Z0:reg, Z1:reg]:(((((((![X73:reg]:((((c @ X73 @ Z0))=>((c @ X73 @ Z1))))))&(~((![X74:reg]:((((c @ X74 @ Z1))=>((c @ X74 @ Z0))))))))))&(~(?[X25:reg]:(((((((c @ X25 @ Z0))&(~((?[X75:reg]:((((![X76:reg]:((((c @ X76 @ X75))=>((c @ X76 @ X25))))))&((![X77:reg]:((((c @ X77 @ X75))=>((c @ X77 @ Z0))))))))))))))&(((((c @ X25 @ Z1))&(~((?[X78:reg]:((((![X79:reg]:((((c @ X79 @ X78))=>((c @ X79 @ X25))))))&((![X80:reg]:((((c @ X80 @ X78))=>((c @ X80 @ Z1)))))))))))))))))))))), inference(fof_simplification,[status(thm)],[ntpp])).
% 0.21/0.29 thf(c_0_17, plain, ((ec)=(^[Z0:reg, Z1:reg]:((((c @ Z0 @ Z1))&(~((?[X60:reg]:((((![X61:reg]:((((c @ X61 @ X60))=>((c @ X61 @ Z0))))))&((![X62:reg]:((((c @ X62 @ X60))=>((c @ X62 @ Z1))))))))))))))), inference(apply_def,[status(thm)],[c_0_13, c_0_14])).
% 0.21/0.29 thf(c_0_18, plain, ((pp)=(^[Z0:reg, Z1:reg]:((((![X63:reg]:((((c @ X63 @ Z0))=>((c @ X63 @ Z1))))))&(~((![X64:reg]:((((c @ X64 @ Z1))=>((c @ X64 @ Z0))))))))))), inference(apply_def,[status(thm)],[c_0_15, c_0_12])).
% 0.21/0.29 thf(c_0_19, plain, ((mbox)=(^[Z0:$i > $i > $o, Z1:$i > $o, Z2:$i]:(![X14:$i]:(((~((Z0 @ Z2 @ X14)))|((Z1 @ X14))))))), inference(fof_simplification,[status(thm)],[mbox])).
% 0.21/0.29 thf(c_0_20, plain, ((mvalid)=(^[Z0:$i > $o]:(![X3:$i]:((Z0 @ X3))))), inference(fof_simplification,[status(thm)],[mvalid])).
% 0.21/0.29 thf(c_0_21, plain, ((ntpp)=(^[Z0:reg, Z1:reg]:(((((((![X73:reg]:((((c @ X73 @ Z0))=>((c @ X73 @ Z1))))))&(~((![X74:reg]:((((c @ X74 @ Z1))=>((c @ X74 @ Z0))))))))))&(~(?[X25:reg]:(((((((c @ X25 @ Z0))&(~((?[X75:reg]:((((![X76:reg]:((((c @ X76 @ X75))=>((c @ X76 @ X25))))))&((![X77:reg]:((((c @ X77 @ X75))=>((c @ X77 @ Z0))))))))))))))&(((((c @ X25 @ Z1))&(~((?[X78:reg]:((((![X79:reg]:((((c @ X79 @ X78))=>((c @ X79 @ X25))))))&((![X80:reg]:((((c @ X80 @ X78))=>((c @ X80 @ Z1)))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_16, c_0_17]), c_0_18])).
% 0.21/0.29 thf(c_0_22, negated_conjecture, ~((mvalid @ (mbox @ a @ (^[X44:$i]:(![X25:reg]:((((((ntpp @ france @ X25))&((ntpp @ spain @ X25))))=>((((pp @ paris @ X25))&((pp @ catalunya @ X25))))))))))), inference(assume_negation,[status(cth)],[con])).
% 0.21/0.29 thf(c_0_23, plain, ![X25:reg]:(((epred1_1 @ X25)<=>(((![X120:reg]:(((c @ X120 @ france)=>(c @ X120 @ X25)))&~(![X121:reg]:(((c @ X121 @ X25)=>(c @ X121 @ france)))))&~(?[X122:reg]:((((c @ X122 @ france)&~(?[X123:reg]:((![X124:reg]:(((c @ X124 @ X123)=>(c @ X124 @ X122)))&![X125:reg]:(((c @ X125 @ X123)=>(c @ X125 @ france)))))))&((c @ X122 @ X25)&~(?[X126:reg]:((![X127:reg]:(((c @ X127 @ X126)=>(c @ X127 @ X122)))&![X128:reg]:(((c @ X128 @ X126)=>(c @ X128 @ X25)))))))))))&((![X129:reg]:(((c @ X129 @ spain)=>(c @ X129 @ X25)))&~(![X130:reg]:(((c @ X130 @ X25)=>(c @ X130 @ spain)))))&~(?[X131:reg]:((((c @ X131 @ spain)&~(?[X132:reg]:((![X133:reg]:(((c @ X133 @ X132)=>(c @ X133 @ X131)))&![X134:reg]:(((c @ X134 @ X132)=>(c @ X134 @ spain)))))))&((c @ X131 @ X25)&~(?[X135:reg]:((![X136:reg]:(((c @ X136 @ X135)=>(c @ X136 @ X131)))&![X137:reg]:(((c @ X137 @ X135)=>(c @ X137 @ X25)))))))))))))), introduced(definition)).
% 0.21/0.29 thf(c_0_24, plain, ((tpp)=(^[Z0:reg, Z1:reg]:(((((((![X65:reg]:((((c @ X65 @ Z0))=>((c @ X65 @ Z1))))))&(~((![X66:reg]:((((c @ X66 @ Z1))=>((c @ X66 @ Z0))))))))))&(?[X25:reg]:(((((((c @ X25 @ Z0))&(~((?[X67:reg]:((((![X68:reg]:((((c @ X68 @ X67))=>((c @ X68 @ X25))))))&((![X69:reg]:((((c @ X69 @ X67))=>((c @ X69 @ Z0))))))))))))))&(((((c @ X25 @ Z1))&(~((?[X70:reg]:((((![X71:reg]:((((c @ X71 @ X70))=>((c @ X71 @ X25))))))&((![X72:reg]:((((c @ X72 @ X70))=>((c @ X72 @ Z1))))))))))))))))))))), inference(fof_simplification,[status(thm)],[tpp])).
% 0.21/0.29 thf(c_0_25, plain, ![X119:$i, X118:$i]:((~(a @ X119 @ X118)|((![X109:reg]:(((c @ X109 @ paris)=>(c @ X109 @ france)))&~(![X110:reg]:(((c @ X110 @ france)=>(c @ X110 @ paris)))))&~(?[X111:reg]:((((c @ X111 @ paris)&~(?[X112:reg]:((![X113:reg]:(((c @ X113 @ X112)=>(c @ X113 @ X111)))&![X114:reg]:(((c @ X114 @ X112)=>(c @ X114 @ paris)))))))&((c @ X111 @ france)&~(?[X115:reg]:((![X116:reg]:(((c @ X116 @ X115)=>(c @ X116 @ X111)))&![X117:reg]:(((c @ X117 @ X115)=>(c @ X117 @ france))))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[ax3]), c_0_19]), c_0_20]), c_0_21])])).
% 0.21/0.29 thf(c_0_26, negated_conjecture, ~(![X143:$i, X142:$i]:((~(a @ X143 @ X142)|![X25:reg]:(((epred1_1 @ X25)=>((![X138:reg]:(((c @ X138 @ paris)=>(c @ X138 @ X25)))&~(![X139:reg]:(((c @ X139 @ X25)=>(c @ X139 @ paris)))))&(![X140:reg]:(((c @ X140 @ catalunya)=>(c @ X140 @ X25)))&~(![X141:reg]:(((c @ X141 @ X25)=>(c @ X141 @ catalunya))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_22]), c_0_19]), c_0_20]), c_0_18]), c_0_21])]), c_0_23])).
% 0.21/0.29 thf(c_0_27, plain, ((tpp)=(^[Z0:reg, Z1:reg]:(((((((![X65:reg]:((((c @ X65 @ Z0))=>((c @ X65 @ Z1))))))&(~((![X66:reg]:((((c @ X66 @ Z1))=>((c @ X66 @ Z0))))))))))&(?[X25:reg]:(((((((c @ X25 @ Z0))&(~((?[X67:reg]:((((![X68:reg]:((((c @ X68 @ X67))=>((c @ X68 @ X25))))))&((![X69:reg]:((((c @ X69 @ X67))=>((c @ X69 @ Z0))))))))))))))&(((((c @ X25 @ Z1))&(~((?[X70:reg]:((((![X71:reg]:((((c @ X71 @ X70))=>((c @ X71 @ X25))))))&((![X72:reg]:((((c @ X72 @ X70))=>((c @ X72 @ Z1))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_24, c_0_17]), c_0_18])).
% 0.21/0.29 thf(c_0_28, plain, ![X25:reg]:(((epred1_1 @ X25)=>(((![X120:reg]:(((c @ X120 @ france)=>(c @ X120 @ X25)))&~(![X121:reg]:(((c @ X121 @ X25)=>(c @ X121 @ france)))))&~(?[X122:reg]:((((c @ X122 @ france)&~(?[X123:reg]:((![X124:reg]:(((c @ X124 @ X123)=>(c @ X124 @ X122)))&![X125:reg]:(((c @ X125 @ X123)=>(c @ X125 @ france)))))))&((c @ X122 @ X25)&~(?[X126:reg]:((![X127:reg]:(((c @ X127 @ X126)=>(c @ X127 @ X122)))&![X128:reg]:(((c @ X128 @ X126)=>(c @ X128 @ X25)))))))))))&((![X129:reg]:(((c @ X129 @ spain)=>(c @ X129 @ X25)))&~(![X130:reg]:(((c @ X130 @ X25)=>(c @ X130 @ spain)))))&~(?[X131:reg]:((((c @ X131 @ spain)&~(?[X132:reg]:((![X133:reg]:(((c @ X133 @ X132)=>(c @ X133 @ X131)))&![X134:reg]:(((c @ X134 @ X132)=>(c @ X134 @ spain)))))))&((c @ X131 @ X25)&~(?[X135:reg]:((![X136:reg]:(((c @ X136 @ X135)=>(c @ X136 @ X131)))&![X137:reg]:(((c @ X137 @ X135)=>(c @ X137 @ X25)))))))))))))), inference(split_equiv,[status(thm)],[c_0_23])).
% 0.21/0.29 thf(c_0_29, plain, ![X175:$i, X176:$i, X177:reg, X179:reg, X181:reg, X182:reg, X184:reg, X185:reg]:((((~(c @ X177 @ paris)|(c @ X177 @ france)|~(a @ X175 @ X176))&(((c @ esk12_0 @ france)|~(a @ X175 @ X176))&(~(c @ esk12_0 @ paris)|~(a @ X175 @ X176))))&(((~(c @ X184 @ (esk14_1 @ X179))|(c @ X184 @ X179)|~(c @ X179 @ france)|(~(c @ X181 @ (esk13_1 @ X179))|(c @ X181 @ X179)|~(c @ X179 @ paris))|~(a @ X175 @ X176))&(~(c @ X185 @ (esk14_1 @ X179))|(c @ X185 @ france)|~(c @ X179 @ france)|(~(c @ X181 @ (esk13_1 @ X179))|(c @ X181 @ X179)|~(c @ X179 @ paris))|~(a @ X175 @ X176)))&((~(c @ X184 @ (esk14_1 @ X179))|(c @ X184 @ X179)|~(c @ X179 @ france)|(~(c @ X182 @ (esk13_1 @ X179))|(c @ X182 @ paris)|~(c @ X179 @ paris))|~(a @ X175 @ X176))&(~(c @ X185 @ (esk14_1 @ X179))|(c @ X185 @ france)|~(c @ X179 @ france)|(~(c @ X182 @ (esk13_1 @ X179))|(c @ X182 @ paris)|~(c @ X179 @ paris))|~(a @ X175 @ X176)))))), 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_25])])])])])])])).
% 0.21/0.29 thf(c_0_30, negated_conjecture, ![X190:reg, X192:reg]:(((a @ esk15_0 @ esk16_0)&((epred1_1 @ esk17_0)&((((c @ esk19_0 @ catalunya)|(~(c @ X192 @ esk17_0)|(c @ X192 @ catalunya))|((c @ esk18_0 @ paris)|(~(c @ X190 @ esk17_0)|(c @ X190 @ paris))))&(~(c @ esk19_0 @ esk17_0)|(~(c @ X192 @ esk17_0)|(c @ X192 @ catalunya))|((c @ esk18_0 @ paris)|(~(c @ X190 @ esk17_0)|(c @ X190 @ paris)))))&(((c @ esk19_0 @ catalunya)|(~(c @ X192 @ esk17_0)|(c @ X192 @ catalunya))|(~(c @ esk18_0 @ esk17_0)|(~(c @ X190 @ esk17_0)|(c @ X190 @ paris))))&(~(c @ esk19_0 @ esk17_0)|(~(c @ X192 @ esk17_0)|(c @ X192 @ catalunya))|(~(c @ esk18_0 @ esk17_0)|(~(c @ X190 @ esk17_0)|(c @ X190 @ paris))))))))), inference(distribute,[status(thm)],[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_26])])])])])])).
% 0.21/0.29 thf(c_0_31, plain, ![X103:$i, X102:$i]:((~(a @ X103 @ X102)|((![X93:reg]:(((c @ X93 @ catalunya)=>(c @ X93 @ spain)))&~(![X94:reg]:(((c @ X94 @ spain)=>(c @ X94 @ catalunya)))))&?[X95:reg]:((((c @ X95 @ catalunya)&~(?[X96:reg]:((![X97:reg]:(((c @ X97 @ X96)=>(c @ X97 @ X95)))&![X98:reg]:(((c @ X98 @ X96)=>(c @ X98 @ catalunya)))))))&((c @ X95 @ spain)&~(?[X99:reg]:((![X100:reg]:(((c @ X100 @ X99)=>(c @ X100 @ X95)))&![X101:reg]:(((c @ X101 @ X99)=>(c @ X101 @ spain)))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[ax1]), c_0_19]), c_0_20]), c_0_27])])).
% 0.21/0.29 thf(c_0_32, plain, ![X193:reg, X194:reg, X196:reg, X198:reg, X199:reg, X201:reg, X202:reg, X203:reg, X205:reg, X207:reg, X208:reg, X210:reg, X211:reg]:(((((~(c @ X194 @ france)|(c @ X194 @ X193)|~(epred1_1 @ X193))&(((c @ (esk20_1 @ X193) @ X193)|~(epred1_1 @ X193))&(~(c @ (esk20_1 @ X193) @ france)|~(epred1_1 @ X193))))&(((~(c @ X201 @ (esk22_2 @ X193 @ X196))|(c @ X201 @ X196)|~(c @ X196 @ X193)|(~(c @ X198 @ (esk21_2 @ X193 @ X196))|(c @ X198 @ X196)|~(c @ X196 @ france))|~(epred1_1 @ X193))&(~(c @ X202 @ (esk22_2 @ X193 @ X196))|(c @ X202 @ X193)|~(c @ X196 @ X193)|(~(c @ X198 @ (esk21_2 @ X193 @ X196))|(c @ X198 @ X196)|~(c @ X196 @ france))|~(epred1_1 @ X193)))&((~(c @ X201 @ (esk22_2 @ X193 @ X196))|(c @ X201 @ X196)|~(c @ X196 @ X193)|(~(c @ X199 @ (esk21_2 @ X193 @ X196))|(c @ X199 @ france)|~(c @ X196 @ france))|~(epred1_1 @ X193))&(~(c @ X202 @ (esk22_2 @ X193 @ X196))|(c @ X202 @ X193)|~(c @ X196 @ X193)|(~(c @ X199 @ (esk21_2 @ X193 @ X196))|(c @ X199 @ france)|~(c @ X196 @ france))|~(epred1_1 @ X193)))))&(((~(c @ X203 @ spain)|(c @ X203 @ X193)|~(epred1_1 @ X193))&(((c @ (esk23_1 @ X193) @ X193)|~(epred1_1 @ X193))&(~(c @ (esk23_1 @ X193) @ spain)|~(epred1_1 @ X193))))&(((~(c @ X210 @ (esk25_2 @ X193 @ X205))|(c @ X210 @ X205)|~(c @ X205 @ X193)|(~(c @ X207 @ (esk24_2 @ X193 @ X205))|(c @ X207 @ X205)|~(c @ X205 @ spain))|~(epred1_1 @ X193))&(~(c @ X211 @ (esk25_2 @ X193 @ X205))|(c @ X211 @ X193)|~(c @ X205 @ X193)|(~(c @ X207 @ (esk24_2 @ X193 @ X205))|(c @ X207 @ X205)|~(c @ X205 @ spain))|~(epred1_1 @ X193)))&((~(c @ X210 @ (esk25_2 @ X193 @ X205))|(c @ X210 @ X205)|~(c @ X205 @ X193)|(~(c @ X208 @ (esk24_2 @ X193 @ X205))|(c @ X208 @ spain)|~(c @ X205 @ spain))|~(epred1_1 @ X193))&(~(c @ X211 @ (esk25_2 @ X193 @ X205))|(c @ X211 @ X193)|~(c @ X205 @ X193)|(~(c @ X208 @ (esk24_2 @ X193 @ X205))|(c @ X208 @ spain)|~(c @ X205 @ spain))|~(epred1_1 @ X193))))))), inference(distribute,[status(thm)],[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_28])])])])])])).
% 0.21/0.29 thf(c_0_33, plain, ![X3:$i, X14:$i]:(((c @ esk12_0 @ france)|~((a @ X3 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.21/0.29 thf(c_0_34, negated_conjecture, (a @ esk15_0 @ esk16_0), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.21/0.29 thf(c_0_35, plain, ![X159:$i, X160:$i, X161:reg, X164:reg, X167:reg]:((((~(c @ X161 @ catalunya)|(c @ X161 @ spain)|~(a @ X159 @ X160))&(((c @ esk4_0 @ spain)|~(a @ X159 @ X160))&(~(c @ esk4_0 @ catalunya)|~(a @ X159 @ X160))))&((((c @ esk5_0 @ catalunya)|~(a @ X159 @ X160))&((((c @ (esk7_1 @ X164) @ X164)|(c @ (esk6_1 @ X164) @ X164)|~(a @ X159 @ X160))&(~(c @ (esk7_1 @ X164) @ catalunya)|(c @ (esk6_1 @ X164) @ X164)|~(a @ X159 @ X160)))&(((c @ (esk7_1 @ X164) @ X164)|~(c @ (esk6_1 @ X164) @ esk5_0)|~(a @ X159 @ X160))&(~(c @ (esk7_1 @ X164) @ catalunya)|~(c @ (esk6_1 @ X164) @ esk5_0)|~(a @ X159 @ X160)))))&(((c @ esk5_0 @ spain)|~(a @ X159 @ X160))&((((c @ (esk9_1 @ X167) @ X167)|(c @ (esk8_1 @ X167) @ X167)|~(a @ X159 @ X160))&(~(c @ (esk9_1 @ X167) @ spain)|(c @ (esk8_1 @ X167) @ X167)|~(a @ X159 @ X160)))&(((c @ (esk9_1 @ X167) @ X167)|~(c @ (esk8_1 @ X167) @ esk5_0)|~(a @ X159 @ X160))&(~(c @ (esk9_1 @ X167) @ spain)|~(c @ (esk8_1 @ X167) @ esk5_0)|~(a @ X159 @ X160)))))))), 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_31])])])])])])])).
% 0.21/0.29 thf(c_0_36, plain, ![X18:reg, X19:reg]:(((c @ X18 @ X19)|~((c @ X18 @ france))|~((epred1_1 @ X19)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.21/0.29 thf(c_0_37, negated_conjecture, (c @ esk12_0 @ france), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.21/0.29 thf(c_0_38, plain, ![X3:$i, X14:$i]:(((c @ esk4_0 @ spain)|~((a @ X3 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.21/0.29 thf(c_0_39, plain, ![X18:reg]:(((c @ esk12_0 @ X18)|~((epred1_1 @ X18)))), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.21/0.29 thf(c_0_40, negated_conjecture, (epred1_1 @ esk17_0), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.21/0.29 thf(c_0_41, plain, ![X3:$i, X14:$i]:((~((c @ esk12_0 @ paris))|~((a @ X3 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.21/0.29 thf(c_0_42, plain, ![X18:reg, X19:reg]:(((c @ X18 @ X19)|~((c @ X18 @ spain))|~((epred1_1 @ X19)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.21/0.29 thf(c_0_43, negated_conjecture, (c @ esk4_0 @ spain), inference(spm,[status(thm)],[c_0_38, c_0_34])).
% 0.21/0.29 thf(c_0_44, negated_conjecture, ![X18:reg, X19:reg]:(((c @ esk19_0 @ catalunya)|(c @ X18 @ catalunya)|(c @ esk18_0 @ paris)|(c @ X19 @ paris)|~((c @ X18 @ esk17_0))|~((c @ X19 @ esk17_0)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.21/0.29 thf(c_0_45, negated_conjecture, (c @ esk12_0 @ esk17_0), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 0.21/0.29 thf(c_0_46, negated_conjecture, ~((c @ esk12_0 @ paris)), inference(spm,[status(thm)],[c_0_41, c_0_34])).
% 0.21/0.29 thf(c_0_47, negated_conjecture, ![X18:reg]:(((c @ esk4_0 @ X18)|~((epred1_1 @ X18)))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 0.21/0.29 thf(c_0_48, plain, ![X3:$i, X14:$i]:((~((c @ esk4_0 @ catalunya))|~((a @ X3 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.21/0.29 thf(c_0_49, plain, ![X18:reg, X3:$i, X14:$i]:(((c @ X18 @ spain)|~((c @ X18 @ catalunya))|~((a @ X3 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.21/0.29 thf(c_0_50, negated_conjecture, ![X18:reg]:(((c @ esk19_0 @ catalunya)|(c @ esk18_0 @ paris)|(c @ X18 @ catalunya)|~((c @ X18 @ esk17_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_46])).
% 0.21/0.29 thf(c_0_51, negated_conjecture, (c @ esk4_0 @ esk17_0), inference(spm,[status(thm)],[c_0_47, c_0_40])).
% 0.21/0.29 thf(c_0_52, negated_conjecture, ~((c @ esk4_0 @ catalunya)), inference(spm,[status(thm)],[c_0_48, c_0_34])).
% 0.21/0.29 thf(c_0_53, negated_conjecture, ![X18:reg]:(((c @ X18 @ spain)|~((c @ X18 @ catalunya)))), inference(spm,[status(thm)],[c_0_49, c_0_34])).
% 0.21/0.29 thf(c_0_54, negated_conjecture, ((c @ esk18_0 @ paris)|(c @ esk19_0 @ catalunya)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_52])).
% 0.21/0.29 thf(c_0_55, negated_conjecture, ![X18:reg, X19:reg]:(((c @ X18 @ catalunya)|(c @ esk18_0 @ paris)|(c @ X19 @ paris)|~((c @ esk19_0 @ esk17_0))|~((c @ X18 @ esk17_0))|~((c @ X19 @ esk17_0)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.21/0.29 thf(c_0_56, negated_conjecture, ((c @ esk18_0 @ paris)|(c @ esk19_0 @ spain)), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 0.21/0.29 thf(c_0_57, negated_conjecture, ![X18:reg]:(((c @ esk18_0 @ paris)|(c @ X18 @ catalunya)|~((c @ esk19_0 @ esk17_0))|~((c @ X18 @ esk17_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_45]), c_0_46])).
% 0.21/0.29 thf(c_0_58, plain, ![X18:reg, X3:$i, X14:$i]:(((c @ X18 @ france)|~((c @ X18 @ paris))|~((a @ X3 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.21/0.29 thf(c_0_59, plain, ![X18:reg]:(((c @ esk18_0 @ paris)|(c @ esk19_0 @ X18)|~((epred1_1 @ X18)))), inference(spm,[status(thm)],[c_0_42, c_0_56])).
% 0.21/0.29 thf(c_0_60, negated_conjecture, ((c @ esk18_0 @ paris)|~((c @ esk19_0 @ esk17_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_51]), c_0_52])).
% 0.21/0.29 thf(c_0_61, negated_conjecture, ![X18:reg]:(((c @ X18 @ france)|~((c @ X18 @ paris)))), inference(spm,[status(thm)],[c_0_58, c_0_34])).
% 0.21/0.29 thf(c_0_62, negated_conjecture, (c @ esk18_0 @ paris), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_40]), c_0_60])).
% 0.21/0.29 thf(c_0_63, negated_conjecture, ![X18:reg, X19:reg]:(((c @ esk19_0 @ catalunya)|(c @ X18 @ catalunya)|(c @ X19 @ paris)|~((c @ X18 @ esk17_0))|~((c @ esk18_0 @ esk17_0))|~((c @ X19 @ esk17_0)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.21/0.29 thf(c_0_64, negated_conjecture, (c @ esk18_0 @ france), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 0.21/0.29 thf(c_0_65, negated_conjecture, ![X18:reg]:(((c @ esk19_0 @ catalunya)|(c @ X18 @ catalunya)|~((c @ esk18_0 @ esk17_0))|~((c @ X18 @ esk17_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_45]), c_0_46])).
% 0.21/0.29 thf(c_0_66, plain, ![X18:reg]:(((c @ esk18_0 @ X18)|~((epred1_1 @ X18)))), inference(spm,[status(thm)],[c_0_36, c_0_64])).
% 0.21/0.29 thf(c_0_67, negated_conjecture, ((c @ esk19_0 @ catalunya)|~((c @ esk18_0 @ esk17_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_51]), c_0_52])).
% 0.21/0.29 thf(c_0_68, negated_conjecture, (c @ esk18_0 @ esk17_0), inference(spm,[status(thm)],[c_0_66, c_0_40])).
% 0.21/0.29 thf(c_0_69, negated_conjecture, ![X18:reg, X19:reg]:(((c @ X18 @ catalunya)|(c @ X19 @ paris)|~((c @ esk19_0 @ esk17_0))|~((c @ X18 @ esk17_0))|~((c @ esk18_0 @ esk17_0))|~((c @ X19 @ esk17_0)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.21/0.29 thf(c_0_70, negated_conjecture, (c @ esk19_0 @ catalunya), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_68])])).
% 0.21/0.29 thf(c_0_71, negated_conjecture, ![X18:reg]:(((c @ X18 @ catalunya)|~((c @ esk18_0 @ esk17_0))|~((c @ esk19_0 @ esk17_0))|~((c @ X18 @ esk17_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_45]), c_0_46])).
% 0.21/0.29 thf(c_0_72, negated_conjecture, (c @ esk19_0 @ spain), inference(spm,[status(thm)],[c_0_53, c_0_70])).
% 0.21/0.29 thf(c_0_73, negated_conjecture, (~((c @ esk18_0 @ esk17_0))|~((c @ esk19_0 @ esk17_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_51]), c_0_52])).
% 0.21/0.29 thf(c_0_74, plain, ![X18:reg]:(((c @ esk19_0 @ X18)|~((epred1_1 @ X18)))), inference(spm,[status(thm)],[c_0_42, c_0_72])).
% 0.21/0.29 thf(c_0_75, negated_conjecture, ~((c @ esk19_0 @ esk17_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_68])])).
% 0.21/0.29 thf(c_0_76, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_40]), c_0_75]), ['proof']).
% 0.21/0.29 % SZS output end CNFRefutation
% 0.21/0.29 % Parsed axioms : 98
% 0.21/0.29 % Removed by relevancy pruning/SinE : 0
% 0.21/0.29 % Initial clauses : 102
% 0.21/0.29 % Removed in clause preprocessing : 49
% 0.21/0.29 % Initial clauses in saturation : 53
% 0.21/0.29 % Processed clauses : 201
% 0.21/0.29 % ...of these trivial : 0
% 0.21/0.29 % ...subsumed : 5
% 0.21/0.29 % ...remaining for further processing : 196
% 0.21/0.29 % Other redundant clauses eliminated : 0
% 0.21/0.29 % Clauses deleted for lack of memory : 0
% 0.21/0.29 % Backward-subsumed : 26
% 0.21/0.29 % Backward-rewritten : 13
% 0.21/0.29 % Generated clauses : 231
% 0.21/0.29 % ...of the previous two non-redundant : 188
% 0.21/0.29 % ...aggressively subsumed : 0
% 0.21/0.29 % Contextual simplify-reflections : 13
% 0.21/0.29 % Paramodulations : 231
% 0.21/0.29 % Factorizations : 0
% 0.21/0.29 % NegExts : 0
% 0.21/0.29 % Equation resolutions : 0
% 0.21/0.29 % Disequality decompositions : 0
% 0.21/0.29 % Total rewrite steps : 58
% 0.21/0.29 % ...of those cached : 23
% 0.21/0.29 % Propositional unsat checks : 0
% 0.21/0.29 % Propositional check models : 0
% 0.21/0.29 % Propositional check unsatisfiable : 0
% 0.21/0.29 % Propositional clauses : 0
% 0.21/0.29 % Propositional clauses after purity: 0
% 0.21/0.29 % Propositional unsat core size : 0
% 0.21/0.29 % Propositional preprocessing time : 0.000
% 0.21/0.29 % Propositional encoding time : 0.000
% 0.21/0.29 % Propositional solver time : 0.000
% 0.21/0.29 % Success case prop preproc time : 0.000
% 0.21/0.29 % Success case prop encoding time : 0.000
% 0.21/0.29 % Success case prop solver time : 0.000
% 0.21/0.29 % Current number of processed clauses : 104
% 0.21/0.29 % Positive orientable unit clauses : 47
% 0.21/0.29 % Positive unorientable unit clauses: 0
% 0.21/0.29 % Negative unit clauses : 3
% 0.21/0.29 % Non-unit-clauses : 54
% 0.21/0.29 % Current number of unprocessed clauses: 77
% 0.21/0.29 % ...number of literals in the above : 345
% 0.21/0.29 % Current number of archived formulas : 0
% 0.21/0.29 % Current number of archived clauses : 92
% 0.21/0.29 % Clause-clause subsumption calls (NU) : 3011
% 0.21/0.29 % Rec. Clause-clause subsumption calls : 1258
% 0.21/0.29 % Non-unit clause-clause subsumptions : 39
% 0.21/0.29 % Unit Clause-clause subsumption calls : 151
% 0.21/0.29 % Rewrite failures with RHS unbound : 0
% 0.21/0.29 % BW rewrite match attempts : 17
% 0.21/0.29 % BW rewrite match successes : 8
% 0.21/0.29 % Condensation attempts : 201
% 0.21/0.29 % Condensation successes : 0
% 0.21/0.29 % Termbank termtop insertions : 13856
% 0.21/0.29 % Search garbage collected termcells : 2582
% 0.21/0.29
% 0.21/0.29 % -------------------------------------------------
% 0.21/0.29 % User time : 0.024 s
% 0.21/0.29 % System time : 0.009 s
% 0.21/0.29 % Total time : 0.034 s
% 0.21/0.29 % Maximum resident set size: 4196 pages
% 0.21/0.29
% 0.21/0.29 % -------------------------------------------------
% 0.21/0.29 % User time : 0.122 s
% 0.21/0.29 % System time : 0.026 s
% 0.21/0.29 % Total time : 0.148 s
% 0.21/0.29 % Maximum resident set size: 4864 pages
% 0.21/0.29 % E exiting
%------------------------------------------------------------------------------