%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : PLA054^4 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:20:23 AM UTC 2026
% Result : Theorem 0.22s 0.31s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA054^4 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n010.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 13:21:18 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running higher-order theorem proving
% 0.22/0.27 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.RXbXKhH6ZE/E---3.1_2831733.p
% 0.22/0.31 % Version: 3.5.1-ho
% 0.22/0.31 % Preprocessing class: HSMSSMSSMLMNHSN.
% 0.22/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.22/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.22/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.22/0.31 % Starting post_as_ho1 with 300s (1) cores
% 0.22/0.31 % almost_fo_3_lam with pid 2831748 completed with status 0
% 0.22/0.31 % Result found by almost_fo_3_lam
% 0.22/0.31 % Preprocessing class: HSMSSMSSMLMNHSN.
% 0.22/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.22/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.22/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.22/0.31 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.31 % No SInE strategy applied
% 0.22/0.31 % Search class: HGHNS-FFSF32-SHSSMFNN
% 0.22/0.31 % partial match(2): HGHNF-FFSF22-SHSSMFNN
% 0.22/0.31 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.22/0.31 % Starting SubtermCWHack with 28s (1) cores
% 0.22/0.31 % SubtermCWHack with pid 2831756 completed with status 0
% 0.22/0.31 % Result found by SubtermCWHack
% 0.22/0.31 % Preprocessing class: HSMSSMSSMLMNHSN.
% 0.22/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.22/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.22/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.22/0.31 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.31 % No SInE strategy applied
% 0.22/0.31 % Search class: HGHNS-FFSF32-SHSSMFNN
% 0.22/0.31 % partial match(2): HGHNF-FFSF22-SHSSMFNN
% 0.22/0.31 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.22/0.31 % Starting SubtermCWHack with 28s (1) cores
% 0.22/0.31 % Preprocessing time : 0.002 s
% 0.22/0.31
% 0.22/0.31 % Proof found!
% 0.22/0.31 % SZS status Theorem
% 0.22/0.31 % SZS output start CNFRefutation
% 0.22/0.31 thf(decl_sort1, type, mworld: $tType).
% 0.22/0.31 thf(decl_23, type, mrel: mworld > mworld > $o).
% 0.22/0.31 thf(decl_24, type, mactual: mworld).
% 0.22/0.31 thf(decl_25, type, mlocal: (mworld > $o) > $o).
% 0.22/0.31 thf(decl_26, type, mnot: (mworld > $o) > mworld > $o).
% 0.22/0.31 thf(decl_27, type, mand: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.22/0.31 thf(decl_29, type, mimplies: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.22/0.31 thf(decl_31, type, mbox: (mworld > $o) > mworld > $o).
% 0.22/0.31 thf(decl_33, type, mforall_di: ($i > mworld > $o) > mworld > $o).
% 0.22/0.31 thf(decl_34, type, mexists_di: ($i > mworld > $o) > mworld > $o).
% 0.22/0.31 thf(decl_35, type, d: $i).
% 0.22/0.31 thf(decl_37, type, o: $i).
% 0.22/0.31 thf(decl_38, type, h: $i > mworld > $o).
% 0.22/0.31 thf(decl_39, type, closed: $i > mworld > $o).
% 0.22/0.31 thf(decl_40, type, combo: $i > $i > mworld > $o).
% 0.22/0.31 thf(decl_41, type, open: $i > mworld > $o).
% 0.22/0.31 thf(decl_42, type, epred1_1: mworld > $o).
% 0.22/0.31 thf(decl_44, type, esk2_0: mworld).
% 0.22/0.31 thf(decl_45, type, esk3_2: $i > $i > mworld).
% 0.22/0.31 thf(decl_46, type, esk4_3: mworld > $i > $i > $i).
% 0.22/0.31 thf(con, conjecture, (mlocal @ (mbox @ (mexists_di @ (^[X14:$i]:(mexists_di @ (^[X12:$i]:(mimplies @ (mbox @ (mand @ (combo @ d @ X14) @ (h @ X12))) @ (mbox @ (open @ d))))))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', con)).
% 0.22/0.31 thf(mlocal_def, axiom, ((mlocal)=(^[X1:mworld > $o]:((X1 @ mactual)))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mlocal_def)).
% 0.22/0.31 thf(mand_def, axiom, ((mand)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))&((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mand_def)).
% 0.22/0.31 thf(mimplies_def, axiom, ((mimplies)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))=>((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mimplies_def)).
% 0.22/0.31 thf(mbox_def, axiom, ((mbox)=(^[X1:mworld > $o, X3:mworld]:(![X5:mworld]:((((mrel @ X3 @ X5))=>((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mbox_def)).
% 0.22/0.31 thf(mexists_di_def, axiom, ((mexists_di)=(^[X9:$i > mworld > $o, X3:mworld]:(?[X8:$i]:((X9 @ X8 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mexists_di_def)).
% 0.22/0.31 thf(ax2, axiom, (mlocal @ (mbox @ (closed @ d))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', ax2)).
% 0.22/0.31 thf(mnot_def, axiom, ((mnot)=(^[X2:mworld > $o, X3:mworld]:(~((X2 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mnot_def)).
% 0.22/0.31 thf(mforall_di_def, axiom, ((mforall_di)=(^[X7:$i > mworld > $o, X3:mworld]:(![X8:$i]:((X7 @ X8 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mforall_di_def)).
% 0.22/0.31 thf(mrel_reflexive, axiom, ![X3:mworld]:((mrel @ X3 @ X3)), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', mrel_reflexive)).
% 0.22/0.31 thf(ax1, axiom, (mlocal @ (mbox @ (mforall_di @ (^[X10:$i]:(mforall_di @ (^[X11:$i]:(mexists_di @ (^[X12:$i]:(mand @ (mbox @ (mimplies @ (mand @ (closed @ X10) @ (mand @ (combo @ X10 @ X11) @ (h @ X12))) @ (mbox @ (open @ X10)))) @ (mbox @ (mimplies @ (mand @ (closed @ X10) @ (mand @ (mnot @ (combo @ X10 @ X11)) @ (h @ o))) @ (mbox @ (closed @ X10))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.RXbXKhH6ZE/E---3.1_2831733.p', ax1)).
% 0.22/0.31 thf(c_0_11, plain, ![X26:mworld]:(((epred1_1 @ X26)<=>![X25:$i, X24:$i]:(?[X23:$i]:((![X20:mworld]:(((mrel @ X26 @ X20)=>(((closed @ X25 @ X20)&((combo @ X25 @ X24 @ X20)&(h @ X23 @ X20)))=>![X19:mworld]:(((mrel @ X20 @ X19)=>(open @ X25 @ X19))))))&![X22:mworld]:(((mrel @ X26 @ X22)=>(((closed @ X25 @ X22)&(~(combo @ X25 @ X24 @ X22)&(h @ o @ X22)))=>![X21:mworld]:(((mrel @ X22 @ X21)=>(closed @ X25 @ X21))))))))))), introduced(definition)).
% 0.22/0.31 thf(c_0_12, negated_conjecture, ~((mlocal @ (mbox @ (mexists_di @ (^[X14:$i]:(mexists_di @ (^[X12:$i]:(mimplies @ (mbox @ (mand @ (combo @ d @ X14) @ (h @ X12))) @ (mbox @ (open @ d)))))))))), inference(assume_negation,[status(cth)],[con])).
% 0.22/0.31 thf(c_0_13, plain, ((mlocal)=(^[Z0:mworld > $o]:((Z0 @ mactual)))), inference(fof_simplification,[status(thm)],[mlocal_def])).
% 0.22/0.31 thf(c_0_14, plain, ((mand)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand_def])).
% 0.22/0.31 thf(c_0_15, plain, ((mimplies)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies_def])).
% 0.22/0.31 thf(c_0_16, plain, ((mbox)=(^[Z0:mworld > $o, Z1:mworld]:(![X5:mworld]:((((mrel @ Z1 @ X5))=>((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mbox_def])).
% 0.22/0.31 thf(c_0_17, plain, ((mexists_di)=(^[Z0:$i > mworld > $o, Z1:mworld]:(?[X8:$i]:((Z0 @ X8 @ Z1))))), inference(fof_simplification,[status(thm)],[mexists_di_def])).
% 0.22/0.31 thf(c_0_18, plain, ![X26:mworld]:(((epred1_1 @ X26)=>![X25:$i, X24:$i]:(?[X23:$i]:((![X20:mworld]:(((mrel @ X26 @ X20)=>(((closed @ X25 @ X20)&((combo @ X25 @ X24 @ X20)&(h @ X23 @ X20)))=>![X19:mworld]:(((mrel @ X20 @ X19)=>(open @ X25 @ X19))))))&![X22:mworld]:(((mrel @ X26 @ X22)=>(((closed @ X25 @ X22)&(~(combo @ X25 @ X24 @ X22)&(h @ o @ X22)))=>![X21:mworld]:(((mrel @ X22 @ X21)=>(closed @ X25 @ X21))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 0.22/0.31 thf(c_0_19, negated_conjecture, ~(![X37:mworld]:(((mrel @ mactual @ X37)=>?[X36:$i, X35:$i]:((![X33:mworld]:(((mrel @ X37 @ X33)=>((combo @ d @ X36 @ X33)&(h @ X35 @ X33))))=>![X34:mworld]:(((mrel @ X37 @ X34)=>(open @ d @ X34)))))))), inference(apply_def,[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_12]), c_0_13]), c_0_14]), c_0_15]), c_0_16]), c_0_17])).
% 0.22/0.31 thf(c_0_20, plain, ![X54:mworld, X55:$i, X56:$i, X58:mworld, X59:mworld, X60:$i, X61:$i, X62:mworld, X63:mworld]:(((~(mrel @ X54 @ X58)|(~(closed @ X55 @ X58)|(~(combo @ X55 @ X56 @ X58)|~(h @ (esk4_3 @ X54 @ X55 @ X56) @ X58))|(~(mrel @ X58 @ X59)|(open @ X55 @ X59)))|~(epred1_1 @ X54))&(~(mrel @ X54 @ X62)|(~(closed @ X60 @ X62)|((combo @ X60 @ X61 @ X62)|~(h @ o @ X62))|(~(mrel @ X62 @ X63)|(closed @ X60 @ X63)))|~(epred1_1 @ X54)))), 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_18])])])])])])])).
% 0.22/0.31 thf(c_0_21, negated_conjecture, ![X50:$i, X51:$i, X52:mworld]:(((mrel @ mactual @ esk2_0)&((((combo @ d @ X50 @ X52)|~(mrel @ esk2_0 @ X52))&((h @ X51 @ X52)|~(mrel @ esk2_0 @ X52)))&((mrel @ esk2_0 @ (esk3_2 @ X50 @ X51))&~(open @ d @ (esk3_2 @ X50 @ X51)))))), 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_19])])])])])])).
% 0.22/0.31 thf(c_0_22, plain, ![X10:$i, X8:$i, X6:mworld, X5:mworld, X3:mworld]:(((open @ X8 @ X6)|~((mrel @ X3 @ X5))|~((closed @ X8 @ X5))|~((combo @ X8 @ X10 @ X5))|~((h @ (esk4_3 @ X3 @ X8 @ X10) @ X5))|~((mrel @ X5 @ X6))|~((epred1_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.22/0.31 thf(c_0_23, negated_conjecture, ![X8:$i, X3:mworld]:(((h @ X8 @ X3)|~((mrel @ esk2_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.31 thf(c_0_24, plain, ![X27:mworld]:(((mrel @ mactual @ X27)=>(closed @ d @ X27))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[ax2, c_0_13]), c_0_16])).
% 0.22/0.31 thf(c_0_25, negated_conjecture, ![X10:$i, X8:$i, X3:mworld, X5:mworld, X6:mworld]:(((open @ X8 @ X3)|~((combo @ X8 @ X10 @ X5))|~((mrel @ esk2_0 @ X5))|~((closed @ X8 @ X5))|~((mrel @ X5 @ X3))|~((mrel @ X6 @ X5))|~((epred1_1 @ X6)))), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.22/0.31 thf(c_0_26, negated_conjecture, ![X8:$i, X3:mworld]:(((combo @ d @ X8 @ X3)|~((mrel @ esk2_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.31 thf(c_0_27, plain, ![X43:mworld]:((~(mrel @ mactual @ X43)|(closed @ d @ X43))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])])).
% 0.22/0.31 thf(c_0_28, plain, ((mnot)=(^[Z0:mworld > $o, Z1:mworld]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot_def])).
% 0.22/0.31 thf(c_0_29, plain, ((mforall_di)=(^[Z0:$i > mworld > $o, Z1:mworld]:(![X8:$i]:((Z0 @ X8 @ Z1))))), inference(fof_simplification,[status(thm)],[mforall_di_def])).
% 0.22/0.31 thf(c_0_30, negated_conjecture, ![X3:mworld, X5:mworld, X6:mworld]:(((open @ d @ X3)|~((mrel @ esk2_0 @ X5))|~((closed @ d @ X5))|~((mrel @ X5 @ X3))|~((mrel @ X6 @ X5))|~((epred1_1 @ X6)))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 0.22/0.31 thf(c_0_31, plain, ![X3:mworld]:(((closed @ d @ X3)|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.31 thf(c_0_32, plain, ![X38:mworld]:((mrel @ X38 @ X38)), inference(variable_rename,[status(thm)],[mrel_reflexive])).
% 0.22/0.31 thf(c_0_33, plain, ![X26:mworld]:(((mrel @ mactual @ X26)=>(epred1_1 @ X26))), 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(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[ax1]), c_0_13]), c_0_28]), c_0_14]), c_0_15]), c_0_16]), c_0_29]), c_0_17])]), c_0_11])).
% 0.22/0.31 thf(c_0_34, negated_conjecture, ![X3:mworld, X5:mworld, X6:mworld]:(((open @ d @ X3)|~((mrel @ esk2_0 @ X5))|~((mrel @ mactual @ X5))|~((mrel @ X5 @ X3))|~((mrel @ X6 @ X5))|~((epred1_1 @ X6)))), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 0.22/0.31 thf(c_0_35, plain, ![X3:mworld]:((mrel @ X3 @ X3)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.22/0.31 thf(c_0_36, negated_conjecture, (mrel @ mactual @ esk2_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.31 thf(c_0_37, plain, ![X42:mworld]:((~(mrel @ mactual @ X42)|(epred1_1 @ X42))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])).
% 0.22/0.31 thf(c_0_38, negated_conjecture, ![X3:mworld, X5:mworld]:(((open @ d @ X3)|~((mrel @ esk2_0 @ X3))|~((mrel @ X5 @ esk2_0))|~((epred1_1 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_36])])).
% 0.22/0.31 thf(c_0_39, plain, ![X3:mworld]:(((epred1_1 @ X3)|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_37])).
% 0.22/0.31 thf(c_0_40, negated_conjecture, ![X3:mworld, X5:mworld]:(((open @ d @ X3)|~((mrel @ esk2_0 @ X3))|~((mrel @ X5 @ esk2_0))|~((mrel @ mactual @ X5)))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 0.22/0.31 thf(c_0_41, negated_conjecture, ![X8:$i, X10:$i]:(~((open @ d @ (esk3_2 @ X8 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.31 thf(c_0_42, negated_conjecture, ![X3:mworld]:(((open @ d @ X3)|~((mrel @ esk2_0 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_36]), c_0_35])])).
% 0.22/0.31 thf(c_0_43, negated_conjecture, ![X8:$i, X10:$i]:((mrel @ esk2_0 @ (esk3_2 @ X8 @ X10))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.22/0.31 thf(c_0_44, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43])]), ['proof']).
% 0.22/0.31 % SZS output end CNFRefutation
% 0.22/0.31 % Parsed axioms : 38
% 0.22/0.31 % Removed by relevancy pruning/SinE : 0
% 0.22/0.31 % Initial clauses : 34
% 0.22/0.31 % Removed in clause preprocessing : 21
% 0.22/0.31 % Initial clauses in saturation : 13
% 0.22/0.31 % Processed clauses : 40
% 0.22/0.31 % ...of these trivial : 0
% 0.22/0.31 % ...subsumed : 4
% 0.22/0.31 % ...remaining for further processing : 36
% 0.22/0.31 % Other redundant clauses eliminated : 0
% 0.22/0.31 % Clauses deleted for lack of memory : 0
% 0.22/0.31 % Backward-subsumed : 6
% 0.22/0.31 % Backward-rewritten : 0
% 0.22/0.31 % Generated clauses : 51
% 0.22/0.31 % ...of the previous two non-redundant : 46
% 0.22/0.31 % ...aggressively subsumed : 0
% 0.22/0.31 % Contextual simplify-reflections : 0
% 0.22/0.31 % Paramodulations : 51
% 0.22/0.31 % Factorizations : 0
% 0.22/0.31 % NegExts : 0
% 0.22/0.31 % Equation resolutions : 0
% 0.22/0.31 % Disequality decompositions : 0
% 0.22/0.31 % Total rewrite steps : 19
% 0.22/0.31 % ...of those cached : 14
% 0.22/0.31 % Propositional unsat checks : 0
% 0.22/0.31 % Propositional check models : 0
% 0.22/0.31 % Propositional check unsatisfiable : 0
% 0.22/0.31 % Propositional clauses : 0
% 0.22/0.31 % Propositional clauses after purity: 0
% 0.22/0.31 % Propositional unsat core size : 0
% 0.22/0.31 % Propositional preprocessing time : 0.000
% 0.22/0.31 % Propositional encoding time : 0.000
% 0.22/0.31 % Propositional solver time : 0.000
% 0.22/0.31 % Success case prop preproc time : 0.000
% 0.22/0.31 % Success case prop encoding time : 0.000
% 0.22/0.31 % Success case prop solver time : 0.000
% 0.22/0.31 % Current number of processed clauses : 30
% 0.22/0.31 % Positive orientable unit clauses : 3
% 0.22/0.31 % Positive unorientable unit clauses: 0
% 0.22/0.31 % Negative unit clauses : 1
% 0.22/0.31 % Non-unit-clauses : 26
% 0.22/0.31 % Current number of unprocessed clauses: 16
% 0.22/0.31 % ...number of literals in the above : 95
% 0.22/0.31 % Current number of archived formulas : 0
% 0.22/0.31 % Current number of archived clauses : 6
% 0.22/0.31 % Clause-clause subsumption calls (NU) : 407
% 0.22/0.31 % Rec. Clause-clause subsumption calls : 81
% 0.22/0.31 % Non-unit clause-clause subsumptions : 10
% 0.22/0.31 % Unit Clause-clause subsumption calls : 0
% 0.22/0.31 % Rewrite failures with RHS unbound : 0
% 0.22/0.31 % BW rewrite match attempts : 1
% 0.22/0.31 % BW rewrite match successes : 0
% 0.22/0.31 % Condensation attempts : 0
% 0.22/0.31 % Condensation successes : 0
% 0.22/0.31 % Termbank termtop insertions : 4452
% 0.22/0.31 % Search garbage collected termcells : 1248
% 0.22/0.31
% 0.22/0.31 % -------------------------------------------------
% 0.22/0.31 % User time : 0.013 s
% 0.22/0.31 % System time : 0.005 s
% 0.22/0.31 % Total time : 0.019 s
% 0.22/0.31 % Maximum resident set size: 3924 pages
% 0.22/0.31
% 0.22/0.31 % -------------------------------------------------
% 0.22/0.31 % User time : 0.017 s
% 0.22/0.31 % System time : 0.009 s
% 0.22/0.31 % Total time : 0.026 s
% 0.22/0.31 % Maximum resident set size: 4608 pages
% 0.22/0.31 % E exiting
%------------------------------------------------------------------------------