%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : PHI043^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:08 AM UTC 2026
% Result : Theorem 0.23s 0.30s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI043^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n017.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 13:15:37 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 Running higher-order theorem proving
% 0.23/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.3ceWzd9iU6/E---3.1_309883.p
% 0.23/0.30 % Version: 3.5.1-ho
% 0.23/0.30 % Preprocessing class: HSMSSMSSMLMNHHN.
% 0.23/0.30 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.30 % Starting ehoh_best2_full_lfho with 1500s (5) cores
% 0.23/0.30 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.23/0.30 % Starting sh5l with 300s (1) cores
% 0.23/0.30 % Starting ho_unfolding_6 with 300s (1) cores
% 0.23/0.30 % lpo9_lambda_fix with pid 309915 completed with status 0
% 0.23/0.30 % Result found by lpo9_lambda_fix
% 0.23/0.30 % Preprocessing class: HSMSSMSSMLMNHHN.
% 0.23/0.30 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.30 % Starting ehoh_best2_full_lfho with 1500s (5) cores
% 0.23/0.30 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.23/0.30 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = gf500_gu_R04_F100_L20000)
% 0.23/0.30 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.23/0.30 % Search class: HGHNF-FFSF33-SHHSMSBN
% 0.23/0.30 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.30 % Starting SubtermCWHack with 28s (1) cores
% 0.23/0.30 % SubtermCWHack with pid 309924 completed with status 0
% 0.23/0.30 % Result found by SubtermCWHack
% 0.23/0.30 % Preprocessing class: HSMSSMSSMLMNHHN.
% 0.23/0.30 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.30 % Starting ehoh_best2_full_lfho with 1500s (5) cores
% 0.23/0.30 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.23/0.30 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = gf500_gu_R04_F100_L20000)
% 0.23/0.30 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.23/0.30 % Search class: HGHNF-FFSF33-SHHSMSBN
% 0.23/0.30 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.30 % Starting SubtermCWHack with 28s (1) cores
% 0.23/0.30 % Preprocessing time : 0.001 s
% 0.23/0.30
% 0.23/0.30 % Proof found!
% 0.23/0.30 % SZS status Theorem
% 0.23/0.30 % SZS output start CNFRefutation
% 0.23/0.30 thf(decl_sort1, type, mu: $tType).
% 0.23/0.30 thf(decl_26, type, mnot: ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_29, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_31, type, mequiv: ($i > $o) > ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_33, type, mforall_ind: (mu > $i > $o) > $i > $o).
% 0.23/0.30 thf(decl_34, type, mforall_indset: ((mu > $i > $o) > $i > $o) > $i > $o).
% 0.23/0.30 thf(decl_36, type, mexists_ind: (mu > $i > $o) > $i > $o).
% 0.23/0.30 thf(decl_39, type, mbox_generic: ($i > $i > $o) > ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_40, type, mdia_generic: ($i > $i > $o) > ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_41, type, rel: $i > $i > $o).
% 0.23/0.30 thf(decl_42, type, mbox: ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_43, type, mdia: ($i > $o) > $i > $o).
% 0.23/0.30 thf(decl_44, type, mvalid: ($i > $o) > $o).
% 0.23/0.30 thf(decl_46, type, p: (mu > $i > $o) > $i > $o).
% 0.23/0.30 thf(decl_47, type, esk1_0: $i).
% 0.23/0.30 thf(decl_48, type, epred1_0: mu > $i > $o).
% 0.23/0.30 thf(decl_49, type, esk2_3: $i > (mu > $i > $o) > (mu > $i > $o) > $i).
% 0.23/0.30 thf(decl_50, type, esk3_3: $i > (mu > $i > $o) > (mu > $i > $o) > mu).
% 0.23/0.30 thf(decl_51, type, epred2_0: mu > $i > $o).
% 0.23/0.30 thf(mdia_generic, axiom, ((mdia_generic)=(^[X15:$i > $i > $o, X4:$i > $o, X3:$i]:(?[X16:$i]:((((X15 @ X3 @ X16))&((X4 @ X16))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mdia_generic)).
% 0.23/0.30 thf(mbox_generic, axiom, ((mbox_generic)=(^[X15:$i > $i > $o, X4:$i > $o, X3:$i]:(![X16:$i]:(((~((X15 @ X3 @ X16)))|((X4 @ X16))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mbox_generic)).
% 0.23/0.30 thf(possible_instantiation_of_the_positive, conjecture, (mvalid @ (mforall_indset @ (^[X19:mu > $i > $o]:(mimplies @ (p @ X19) @ (mdia @ (mexists_ind @ (^[X1:mu]:(X19 @ X1)))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', possible_instantiation_of_the_positive)).
% 0.23/0.30 thf(mexists_ind, axiom, ((mexists_ind)=(^[X11:mu > $i > $o, X3:$i]:(?[X1:mu]:((X11 @ X1 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mexists_ind)).
% 0.23/0.30 thf(mdia, axiom, ((mdia)=(^[Z0:$i > $o, Z1:$i]:(?[X21:$i]:((((rel @ Z1 @ X21))&((Z0 @ X21))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mdia)).
% 0.23/0.30 thf(mimplies, axiom, ((mimplies)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))=>((X5 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mimplies)).
% 0.23/0.30 thf(mforall_indset, axiom, ((mforall_indset)=(^[X7:(mu > $i > $o) > $i > $o, X3:$i]:(![X8:mu > $i > $o]:((X7 @ X8 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mforall_indset)).
% 0.23/0.30 thf(mvalid, axiom, ((mvalid)=(^[X4:$i > $o]:(![X3:$i]:((X4 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mvalid)).
% 0.23/0.30 thf(mforall_ind, axiom, ((mforall_ind)=(^[X6:mu > $i > $o, X3:$i]:(![X1:mu]:((X6 @ X1 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mforall_ind)).
% 0.23/0.30 thf(mbox, axiom, ((mbox)=(^[Z0:$i > $o, Z1:$i]:(![X20:$i]:(((~((rel @ Z1 @ X20)))|((Z0 @ X20))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mbox)).
% 0.23/0.30 thf(mequiv, axiom, ((mequiv)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))<=>((X5 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mequiv)).
% 0.23/0.30 thf(ax17, axiom, (mvalid @ (mforall_indset @ (^[X17:mu > $i > $o]:(mforall_indset @ (^[X18:mu > $i > $o]:(mimplies @ (mbox @ (mforall_ind @ (^[X1:mu]:(mequiv @ (X17 @ X1) @ (X18 @ X1))))) @ (mequiv @ (p @ X17) @ (p @ X18)))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', ax17)).
% 0.23/0.30 thf(mnot, axiom, ((mnot)=(^[X4:$i > $o, X3:$i]:(~((X4 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', mnot)).
% 0.23/0.30 thf(ax16, axiom, (mvalid @ (mnot @ (p @ (^[X1:mu, X3:$i]:(((X1)!=(X1))))))), file('/export/starexec/sandbox2/tmp/tmp.3ceWzd9iU6/E---3.1_309883.p', ax16)).
% 0.23/0.30 thf(c_0_14, plain, ((mdia_generic)=(^[Z0:$i > $i > $o, Z1:$i > $o, Z2:$i]:(?[X16:$i]:((((Z0 @ Z2 @ X16))&((Z1 @ X16))))))), inference(fof_simplification,[status(thm)],[mdia_generic])).
% 0.23/0.30 thf(c_0_15, plain, ((mbox_generic)=(^[Z0:$i > $i > $o, Z1:$i > $o, Z2:$i]:(![X16:$i]:(((~((Z0 @ Z2 @ X16)))|((Z1 @ X16))))))), inference(fof_simplification,[status(thm)],[mbox_generic])).
% 0.23/0.30 thf(c_0_16, negated_conjecture, ~((mvalid @ (mforall_indset @ (^[X19:mu > $i > $o]:(mimplies @ (p @ X19) @ (mdia @ (mexists_ind @ (^[X1:mu]:(X19 @ X1))))))))), inference(assume_negation,[status(cth)],[possible_instantiation_of_the_positive])).
% 0.23/0.30 thf(c_0_17, plain, ((mexists_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(?[X1:mu]:((Z0 @ X1 @ Z1))))), inference(fof_simplification,[status(thm)],[mexists_ind])).
% 0.23/0.30 thf(c_0_18, axiom, ((mdia)=(^[Z0:$i > $o, Z1:$i]:(?[X21:$i]:((((rel @ Z1 @ X21))&((Z0 @ X21))))))), inference(apply_def,[status(thm)],[mdia, c_0_14])).
% 0.23/0.30 thf(c_0_19, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies])).
% 0.23/0.30 thf(c_0_20, plain, ((mforall_indset)=(^[Z0:(mu > $i > $o) > $i > $o, Z1:$i]:(![X8:mu > $i > $o]:((Z0 @ X8 @ Z1))))), inference(fof_simplification,[status(thm)],[mforall_indset])).
% 0.23/0.30 thf(c_0_21, plain, ((mvalid)=(^[Z0:$i > $o]:(![X3:$i]:((Z0 @ X3))))), inference(fof_simplification,[status(thm)],[mvalid])).
% 0.23/0.30 thf(c_0_22, plain, ((mforall_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(![X1:mu]:((Z0 @ X1 @ Z1))))), inference(fof_simplification,[status(thm)],[mforall_ind])).
% 0.23/0.30 thf(c_0_23, axiom, ((mbox)=(^[Z0:$i > $o, Z1:$i]:(![X20:$i]:(((~((rel @ Z1 @ X20)))|((Z0 @ X20))))))), inference(apply_def,[status(thm)],[mbox, c_0_15])).
% 0.23/0.30 thf(c_0_24, plain, ((mequiv)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))<=>((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mequiv])).
% 0.23/0.30 thf(c_0_25, negated_conjecture, ~(![X25:$i, X24:mu > $i > $o]:(((p @ X24 @ X25)=>?[X23:$i]:(((rel @ X25 @ X23)&?[X22:mu]:((X24 @ X22 @ X23))))))), 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_16]), c_0_17]), c_0_18]), c_0_19]), c_0_20]), c_0_21])).
% 0.23/0.30 thf(c_0_26, plain, ![X31:$i, X30:mu > $i > $o, X29:mu > $i > $o]:((![X28:$i]:((~(rel @ X31 @ X28)|![X27:mu]:(((X30 @ X27 @ X28)<=>(X29 @ X27 @ X28)))))=>((p @ X30 @ X31)<=>(p @ X29 @ X31)))), 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(fof_simplification,[status(thm)],[ax17]), c_0_22]), c_0_23]), c_0_24]), c_0_19]), c_0_20]), c_0_21])])).
% 0.23/0.30 thf(c_0_27, plain, ((mnot)=(^[Z0:$i > $o, Z1:$i]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot])).
% 0.23/0.30 thf(c_0_28, negated_conjecture, ![X34:$i, X35:mu]:(((p @ epred1_0 @ esk1_0)&(~(rel @ esk1_0 @ X34)|~(epred1_0 @ X35 @ X34)))), 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_25])])])])])).
% 0.23/0.30 thf(c_0_29, plain, ![X37:$i, X38:mu > $i > $o, X39:mu > $i > $o]:((((~(p @ X38 @ X37)|(p @ X39 @ X37)|(rel @ X37 @ (esk2_3 @ X37 @ X38 @ X39)))&(~(p @ X39 @ X37)|(p @ X38 @ X37)|(rel @ X37 @ (esk2_3 @ X37 @ X38 @ X39))))&(((~(p @ X38 @ X37)|(p @ X39 @ X37)|(~(X38 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39))|~(X39 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39))))&(~(p @ X39 @ X37)|(p @ X38 @ X37)|(~(X38 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39))|~(X39 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39)))))&((~(p @ X38 @ X37)|(p @ X39 @ X37)|((X38 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39))|(X39 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39))))&(~(p @ X39 @ X37)|(p @ X38 @ X37)|((X38 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39))|(X39 @ (esk3_3 @ X37 @ X38 @ X39) @ (esk2_3 @ X37 @ X38 @ X39)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])])])).
% 0.23/0.30 thf(c_0_30, plain, ![X26:$i]:(~(p @ (^[Z0:mu, Z1:$i]:(~((Z0)))) @ X26)), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[ax16]), c_0_27]), c_0_21])])).
% 0.23/0.30 thf(c_0_31, plain, ![X44:$i, X45:mu]:(((~(epred2_0 @ X45 @ X44)|((X45)!=(X45)))&(((X45)=(X45))|(epred2_0 @ X45 @ X44)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[])])])])).
% 0.23/0.30 thf(c_0_32, negated_conjecture, ![X1:mu, X3:$i]:((~((rel @ esk1_0 @ X3))|~((epred1_0 @ X1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.23/0.30 thf(c_0_33, plain, ![X8:mu > $i > $o, X6:mu > $i > $o, X3:$i]:(((p @ X8 @ X3)|(rel @ X3 @ (esk2_3 @ X3 @ X8 @ X6))|~((p @ X6 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.23/0.30 thf(c_0_34, plain, ![X8:mu > $i > $o, X6:mu > $i > $o, X3:$i]:(((p @ X8 @ X3)|(X8 @ (esk3_3 @ X3 @ X8 @ X6) @ (esk2_3 @ X3 @ X8 @ X6))|(X6 @ (esk3_3 @ X3 @ X8 @ X6) @ (esk2_3 @ X3 @ X8 @ X6))|~((p @ X6 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.23/0.30 thf(c_0_35, negated_conjecture, (p @ epred1_0 @ esk1_0), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.23/0.30 thf(c_0_36, plain, ![X36:$i]:(~(p @ (^[Z0:mu, Z1:$i]:(~((Z0)))) @ X36)), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_30])])).
% 0.23/0.30 thf(c_0_37, plain, ![X43:$i, X42:mu]:(((epred2_0 @ X42 @ X43)<=>~(((X42)=(X42))))), introduced(definition)).
% 0.23/0.30 thf(c_0_38, plain, ![X3:$i, X1:mu]:((~((epred2_0 @ X1 @ X3))|((X1)!=(X1)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.23/0.30 thf(c_0_39, negated_conjecture, ![X6:mu > $i > $o, X1:mu, X8:mu > $i > $o]:(((p @ X6 @ esk1_0)|~((epred1_0 @ X1 @ (esk2_3 @ esk1_0 @ X6 @ X8)))|~((p @ X8 @ esk1_0)))), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 0.23/0.30 thf(c_0_40, negated_conjecture, ![X6:mu > $i > $o]:(((epred1_0 @ (esk3_3 @ esk1_0 @ X6 @ epred1_0) @ (esk2_3 @ esk1_0 @ X6 @ epred1_0))|(X6 @ (esk3_3 @ esk1_0 @ X6 @ epred1_0) @ (esk2_3 @ esk1_0 @ X6 @ epred1_0))|(p @ X6 @ esk1_0))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 0.23/0.30 thf(c_0_41, plain, ![X3:$i]:(~((((p @ epred2_0 @ X3))=(($true))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_36]), c_0_37])).
% 0.23/0.30 thf(c_0_42, plain, ![X1:mu, X3:$i]:(~((epred2_0 @ X1 @ X3))), inference(cn,[status(thm)],[c_0_38])).
% 0.23/0.30 thf(c_0_43, negated_conjecture, ![X6:mu > $i > $o]:(((X6 @ (esk3_3 @ esk1_0 @ X6 @ epred1_0) @ (esk2_3 @ esk1_0 @ X6 @ epred1_0))|(p @ X6 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_35])])).
% 0.23/0.30 thf(c_0_44, plain, ![X3:$i]:(~((p @ epred2_0 @ X3))), inference(cn,[status(thm)],[c_0_41])).
% 0.23/0.30 thf(c_0_45, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_44]), ['proof']).
% 0.23/0.30 % SZS output end CNFRefutation
% 0.23/0.30 % Parsed axioms : 50
% 0.23/0.30 % Removed by relevancy pruning/SinE : 36
% 0.23/0.30 % Initial clauses : 11
% 0.23/0.30 % Removed in clause preprocessing : 1
% 0.23/0.30 % Initial clauses in saturation : 10
% 0.23/0.30 % Processed clauses : 12
% 0.23/0.30 % ...of these trivial : 0
% 0.23/0.30 % ...subsumed : 0
% 0.23/0.30 % ...remaining for further processing : 12
% 0.23/0.30 % Other redundant clauses eliminated : 0
% 0.23/0.30 % Clauses deleted for lack of memory : 0
% 0.23/0.30 % Backward-subsumed : 1
% 0.23/0.30 % Backward-rewritten : 0
% 0.23/0.30 % Generated clauses : 11
% 0.23/0.30 % ...of the previous two non-redundant : 5
% 0.23/0.30 % ...aggressively subsumed : 0
% 0.23/0.30 % Contextual simplify-reflections : 0
% 0.23/0.30 % Paramodulations : 9
% 0.23/0.30 % Factorizations : 2
% 0.23/0.30 % NegExts : 0
% 0.23/0.30 % Equation resolutions : 0
% 0.23/0.30 % Disequality decompositions : 0
% 0.23/0.30 % Total rewrite steps : 4
% 0.23/0.30 % ...of those cached : 3
% 0.23/0.30 % Propositional unsat checks : 0
% 0.23/0.30 % Propositional check models : 0
% 0.23/0.30 % Propositional check unsatisfiable : 0
% 0.23/0.30 % Propositional clauses : 0
% 0.23/0.30 % Propositional clauses after purity: 0
% 0.23/0.30 % Propositional unsat core size : 0
% 0.23/0.30 % Propositional preprocessing time : 0.000
% 0.23/0.30 % Propositional encoding time : 0.000
% 0.23/0.30 % Propositional solver time : 0.000
% 0.23/0.30 % Success case prop preproc time : 0.000
% 0.23/0.30 % Success case prop encoding time : 0.000
% 0.23/0.30 % Success case prop solver time : 0.000
% 0.23/0.30 % Current number of processed clauses : 11
% 0.23/0.30 % Positive orientable unit clauses : 1
% 0.23/0.30 % Positive unorientable unit clauses: 0
% 0.23/0.30 % Negative unit clauses : 2
% 0.23/0.30 % Non-unit-clauses : 8
% 0.23/0.30 % Current number of unprocessed clauses: 3
% 0.23/0.30 % ...number of literals in the above : 11
% 0.23/0.30 % Current number of archived formulas : 0
% 0.23/0.30 % Current number of archived clauses : 1
% 0.23/0.30 % Clause-clause subsumption calls (NU) : 7
% 0.23/0.30 % Rec. Clause-clause subsumption calls : 7
% 0.23/0.30 % Non-unit clause-clause subsumptions : 1
% 0.23/0.30 % Unit Clause-clause subsumption calls : 0
% 0.23/0.30 % Rewrite failures with RHS unbound : 0
% 0.23/0.30 % BW rewrite match attempts : 0
% 0.23/0.30 % BW rewrite match successes : 0
% 0.23/0.30 % Condensation attempts : 0
% 0.23/0.30 % Condensation successes : 0
% 0.23/0.30 % Termbank termtop insertions : 1934
% 0.23/0.30 % Search garbage collected termcells : 636
% 0.23/0.30
% 0.23/0.30 % -------------------------------------------------
% 0.23/0.30 % User time : 0.006 s
% 0.23/0.30 % System time : 0.003 s
% 0.23/0.30 % Total time : 0.009 s
% 0.23/0.30 % Maximum resident set size: 3684 pages
% 0.23/0.30
% 0.23/0.30 % -------------------------------------------------
% 0.23/0.30 % User time : 0.009 s
% 0.23/0.30 % System time : 0.006 s
% 0.23/0.30 % Total time : 0.015 s
% 0.23/0.30 % Maximum resident set size: 4864 pages
% 0.23/0.30 % E exiting
%------------------------------------------------------------------------------