%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : PHI004^4 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:07 AM UTC 2026
% Result : Theorem 0.22s 0.33s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI004^4 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n019.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 13:17:32 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/0.25 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.C1WwN0NdnD/E---3.1_742168.p
% 0.22/0.33 % Version: 3.5.1-ho
% 0.22/0.33 % Preprocessing class: HSMSSMSSSSMNHSA.
% 0.22/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.33 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.22/0.33 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 0.22/0.33 % Starting ehoh_best_nonlift_nonlambdatoforall with 300s (1) cores
% 0.22/0.33 % Starting ehoh_best8_lambda with 300s (1) cores
% 0.22/0.33 % ho_unfolding_3 with pid 742209 completed with status 0
% 0.22/0.33 % Result found by ho_unfolding_3
% 0.22/0.33 % Preprocessing class: HSMSSMSSSSMNHSA.
% 0.22/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.33 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.22/0.33 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.33 % No SInE strategy applied
% 0.22/0.33 % Search class: HGHNS-FFMF32-SHSFFSBN
% 0.22/0.33 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.22/0.33 % Starting SubtermCWHack with 151s (1) cores
% 0.22/0.33 % Starting ho_unfolding_3 with 901s (1) cores
% 0.22/0.33 % Starting ehoh_best_nonlift_rwall with 151s (1) cores
% 0.22/0.33 % Starting ehoh_best_nonlift_nonlambdatoforall with 151s (1) cores
% 0.22/0.33 % Starting ehoh_best8_lambda with 146s (1) cores
% 0.22/0.33 % ho_unfolding_3 with pid 742217 completed with status 0
% 0.22/0.33 % Result found by ho_unfolding_3
% 0.22/0.33 % Preprocessing class: HSMSSMSSSSMNHSA.
% 0.22/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.33 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.22/0.33 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.33 % No SInE strategy applied
% 0.22/0.33 % Search class: HGHNS-FFMF32-SHSFFSBN
% 0.22/0.33 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.22/0.33 % Starting SubtermCWHack with 151s (1) cores
% 0.22/0.33 % Starting ho_unfolding_3 with 901s (1) cores
% 0.22/0.33 % Preprocessing time : 0.001 s
% 0.22/0.33 % Presaturation interreduction done
% 0.22/0.33
% 0.22/0.33 % Proof found!
% 0.22/0.33 % SZS status Theorem
% 0.22/0.33 % SZS output start CNFRefutation
% 0.22/0.33 thf(decl_sort1, type, qML_mu: $tType).
% 0.22/0.33 thf(decl_sort2, type, qML_i: $tType).
% 0.22/0.33 thf(decl_23, type, scott_G: qML_mu > qML_i > $o).
% 0.22/0.33 thf(decl_25, type, scott_P: (qML_mu > qML_i > $o) > qML_i > $o).
% 0.22/0.33 thf(decl_26, type, scott_ess_QML_mu: (qML_mu > qML_i > $o) > qML_mu > qML_i > $o).
% 0.22/0.33 thf(decl_27, type, epred1_2: qML_mu > qML_i > qML_mu > qML_i > $o).
% 0.22/0.33 thf(decl_29, type, epred2_3: (qML_mu > qML_i > $o) > qML_mu > qML_i > qML_mu > qML_i > $o).
% 0.22/0.33 thf(decl_30, type, esk2_3: (qML_mu > qML_i > $o) > qML_mu > qML_i > qML_i).
% 0.22/0.33 thf(decl_31, type, esk3_3: (qML_mu > qML_i > $o) > qML_mu > qML_i > qML_mu).
% 0.22/0.33 thf(decl_37, type, esk8_0: qML_i).
% 0.22/0.33 thf(decl_38, type, esk9_0: qML_mu).
% 0.22/0.33 thf(decl_39, type, epred4_1: (qML_mu > qML_i > $o) > qML_mu > qML_i > $o).
% 0.22/0.33 thf(fact_5_A1b, axiom, ![X4:qML_i, X7:qML_mu > qML_i > $o]:((~((scott_P @ X7 @ X4))=>(scott_P @ (^[X12:qML_mu, X13:qML_i]:(~((X7 @ X12 @ X13)))) @ X4))), file('/export/starexec/sandbox/tmp/tmp.C1WwN0NdnD/E---3.1_742168.p', fact_5_A1b)).
% 0.22/0.33 thf(fact_0_G__def, axiom, ((scott_G)=(^[X1:qML_mu, X2:qML_i]:(![X3:qML_mu > qML_i > $o]:((((scott_P @ X3 @ X2))=>((X3 @ X1 @ X2))))))), file('/export/starexec/sandbox/tmp/tmp.C1WwN0NdnD/E---3.1_742168.p', fact_0_G__def)).
% 0.22/0.33 thf(conj_0, conjecture, ![X19:qML_i, X6:qML_mu]:((~((scott_G @ X6 @ X19))|(scott_ess_QML_mu @ scott_G @ X6 @ X19))), file('/export/starexec/sandbox/tmp/tmp.C1WwN0NdnD/E---3.1_742168.p', conj_0)).
% 0.22/0.33 thf(fact_4_ess__def, axiom, ((scott_ess_QML_mu)=(^[X9:qML_mu > qML_i > $o, X1:qML_mu, X2:qML_i]:((((X9 @ X1 @ X2))&(![X3:qML_mu > qML_i > $o]:((((X3 @ X1 @ X2))=>(![X10:qML_i, X11:qML_mu]:((((X9 @ X11 @ X10))=>((X3 @ X11 @ X10)))))))))))), file('/export/starexec/sandbox/tmp/tmp.C1WwN0NdnD/E---3.1_742168.p', fact_4_ess__def)).
% 0.22/0.33 thf(fact_2_A4, axiom, ![X4:qML_i, X7:qML_mu > qML_i > $o]:(((scott_P @ X7 @ X4)=>![X8:qML_i]:((scott_P @ X7 @ X8)))), file('/export/starexec/sandbox/tmp/tmp.C1WwN0NdnD/E---3.1_742168.p', fact_2_A4)).
% 0.22/0.33 thf(c_0_5, plain, ![X4:qML_i, X7:qML_mu > qML_i > $o]:((~(scott_P @ X7 @ X4)=>(scott_P @ (^[Z0:qML_mu, Z1:qML_i]:(~(X7 @ Z0 @ Z1))) @ X4))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_5_A1b])])).
% 0.22/0.33 thf(c_0_6, plain, ![X39:qML_mu, X40:qML_i]:(((scott_G @ X39 @ X40)<=>![X3:qML_mu > qML_i > $o]:(((scott_P @ X3 @ X40)=>(X3 @ X39 @ X40))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_0_G__def])])).
% 0.22/0.33 thf(c_0_7, plain, ![X70:qML_i, X71:qML_mu > qML_i > $o]:(((scott_P @ X71 @ X70)|(scott_P @ (^[Z0:qML_mu, Z1:qML_i]:(~(X71 @ Z0 @ Z1))) @ X70))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])).
% 0.22/0.33 thf(c_0_8, plain, ![X93:qML_i, X92:qML_mu, X3:qML_mu > qML_i > $o]:(((epred4_1 @ X3 @ X92 @ X93)<=>~((X3 @ X92 @ X93)))), introduced(definition)).
% 0.22/0.33 thf(c_0_9, negated_conjecture, ~(![X19:qML_i, X6:qML_mu]:((~((scott_G @ X6 @ X19))|(scott_ess_QML_mu @ scott_G @ X6 @ X19)))), inference(assume_negation,[status(cth)],[conj_0])).
% 0.22/0.33 thf(c_0_10, plain, ![X46:qML_mu, X47:qML_i, X48:qML_mu > qML_i > $o, X49:qML_mu, X50:qML_i]:(((~(scott_G @ X46 @ X47)|(~(scott_P @ X48 @ X47)|(X48 @ X46 @ X47)))&(((scott_P @ (epred1_2 @ X49 @ X50) @ X50)|(scott_G @ X49 @ X50))&(~(epred1_2 @ X49 @ X50 @ X49 @ X50)|(scott_G @ X49 @ X50))))), 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_6])])])])])])])).
% 0.22/0.33 thf(c_0_11, plain, ![X3:qML_mu > qML_i > $o, X2:qML_i]:(((scott_P @ X3 @ X2)|(((scott_P @ (epred4_1 @ X3) @ X2))=(($true))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_7]), c_0_8])).
% 0.22/0.33 thf(c_0_12, negated_conjecture, ~(![X19:qML_i, X6:qML_mu]:((~(scott_G @ X6 @ X19)|(scott_ess_QML_mu @ scott_G @ X6 @ X19)))), inference(fof_simplification,[status(thm)],[c_0_9])).
% 0.22/0.33 thf(c_0_13, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((X3 @ X1 @ X2)|~((scott_G @ X1 @ X2))|~((scott_P @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.22/0.33 thf(c_0_14, plain, ![X3:qML_mu > qML_i > $o, X2:qML_i]:(((scott_P @ (epred4_1 @ X3) @ X2)|(scott_P @ X3 @ X2))), inference(cn,[status(thm)],[c_0_11])).
% 0.22/0.33 thf(c_0_15, negated_conjecture, ((scott_G @ esk9_0 @ esk8_0)&~(scott_ess_QML_mu @ scott_G @ esk9_0 @ esk8_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])])])).
% 0.22/0.33 thf(c_0_16, plain, ![X96:qML_i, X97:qML_mu, X98:qML_mu > qML_i > $o]:(((~(epred4_1 @ X98 @ X97 @ X96)|~(X98 @ X97 @ X96))&((X98 @ X97 @ X96)|(epred4_1 @ X98 @ X97 @ X96)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 0.22/0.33 thf(c_0_17, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((epred4_1 @ X3 @ X1 @ X2)|(scott_P @ X3 @ X2)|~((scott_G @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.22/0.33 thf(c_0_18, negated_conjecture, (scott_G @ esk9_0 @ esk8_0), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.22/0.33 thf(c_0_19, plain, ![X41:qML_mu > qML_i > $o, X42:qML_mu, X43:qML_i]:(((scott_ess_QML_mu @ X41 @ X42 @ X43)<=>((X41 @ X42 @ X43)&![X3:qML_mu > qML_i > $o]:(((X3 @ X42 @ X43)=>![X10:qML_i, X11:qML_mu]:(((X41 @ X11 @ X10)=>(X3 @ X11 @ X10)))))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_4_ess__def])])).
% 0.22/0.33 thf(c_0_20, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:((~((epred4_1 @ X3 @ X1 @ X2))|~((X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.22/0.33 thf(c_0_21, negated_conjecture, ![X3:qML_mu > qML_i > $o]:(((epred4_1 @ X3 @ esk9_0 @ esk8_0)|(scott_P @ X3 @ esk8_0))), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.22/0.33 thf(c_0_22, plain, ![X58:qML_mu > qML_i > $o, X59:qML_mu, X60:qML_i, X61:qML_mu > qML_i > $o, X62:qML_i, X63:qML_mu, X64:qML_mu > qML_i > $o, X65:qML_mu, X66:qML_i]:(((((X58 @ X59 @ X60)|~(scott_ess_QML_mu @ X58 @ X59 @ X60))&(~(X61 @ X59 @ X60)|(~(X58 @ X63 @ X62)|(X61 @ X63 @ X62))|~(scott_ess_QML_mu @ X58 @ X59 @ X60)))&(((epred2_3 @ X64 @ X65 @ X66 @ X65 @ X66)|~(X64 @ X65 @ X66)|(scott_ess_QML_mu @ X64 @ X65 @ X66))&(((X64 @ (esk3_3 @ X64 @ X65 @ X66) @ (esk2_3 @ X64 @ X65 @ X66))|~(X64 @ X65 @ X66)|(scott_ess_QML_mu @ X64 @ X65 @ X66))&(~(epred2_3 @ X64 @ X65 @ X66 @ (esk3_3 @ X64 @ X65 @ X66) @ (esk2_3 @ X64 @ X65 @ X66))|~(X64 @ X65 @ X66)|(scott_ess_QML_mu @ X64 @ X65 @ X66)))))), 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_19])])])])])])])).
% 0.22/0.33 thf(c_0_23, plain, ![X3:qML_mu > qML_i > $o]:(((scott_P @ X3 @ esk8_0)|~((X3 @ esk9_0 @ esk8_0)))), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.22/0.33 thf(c_0_24, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((X3 @ X1 @ X2)|(epred4_1 @ X3 @ X1 @ X2))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.22/0.33 thf(c_0_25, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((epred2_3 @ X3 @ X1 @ X2 @ X1 @ X2)|(scott_ess_QML_mu @ X3 @ X1 @ X2)|~((X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.33 thf(c_0_26, negated_conjecture, ~((scott_ess_QML_mu @ scott_G @ esk9_0 @ esk8_0)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.22/0.33 thf(c_0_27, plain, ![X54:qML_i, X55:qML_mu > qML_i > $o, X56:qML_i]:((~(scott_P @ X55 @ X54)|(scott_P @ X55 @ X56))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_2_A4])])])])).
% 0.22/0.33 thf(c_0_28, plain, ![X3:qML_mu > qML_i > $o]:(((scott_P @ (epred4_1 @ X3) @ esk8_0)|(X3 @ esk9_0 @ esk8_0))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.22/0.33 thf(c_0_29, negated_conjecture, (epred2_3 @ scott_G @ esk9_0 @ esk8_0 @ esk9_0 @ esk8_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_18]), c_0_26])).
% 0.22/0.33 thf(c_0_30, plain, ![X4:qML_i, X3:qML_mu > qML_i > $o, X2:qML_i]:(((scott_P @ X3 @ X4)|~((scott_P @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.33 thf(c_0_31, negated_conjecture, (scott_P @ (epred4_1 @ (scott_ess_QML_mu @ scott_G)) @ esk8_0), inference(spm,[status(thm)],[c_0_26, c_0_28])).
% 0.22/0.33 thf(c_0_32, negated_conjecture, (scott_P @ (epred2_3 @ scott_G @ esk9_0 @ esk8_0) @ esk8_0), inference(spm,[status(thm)],[c_0_23, c_0_29])).
% 0.22/0.33 thf(c_0_33, negated_conjecture, ![X2:qML_i]:((scott_P @ (epred4_1 @ (scott_ess_QML_mu @ scott_G)) @ X2)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 0.22/0.33 thf(c_0_34, negated_conjecture, ![X2:qML_i]:((scott_P @ (epred2_3 @ scott_G @ esk9_0 @ esk8_0) @ X2)), inference(spm,[status(thm)],[c_0_30, c_0_32])).
% 0.22/0.33 thf(c_0_35, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((X3 @ (esk3_3 @ X3 @ X1 @ X2) @ (esk2_3 @ X3 @ X1 @ X2))|(scott_ess_QML_mu @ X3 @ X1 @ X2)|~((X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.33 thf(c_0_36, negated_conjecture, ![X1:qML_mu, X2:qML_i]:(((epred4_1 @ (scott_ess_QML_mu @ scott_G) @ X1 @ X2)|~((scott_G @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_13, c_0_33])).
% 0.22/0.33 thf(c_0_37, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((X3 @ X1 @ X2)|~((scott_ess_QML_mu @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.33 thf(c_0_38, plain, ![X1:qML_mu, X3:qML_mu > qML_i > $o, X2:qML_i]:(((scott_ess_QML_mu @ X3 @ X1 @ X2)|~((epred2_3 @ X3 @ X1 @ X2 @ (esk3_3 @ X3 @ X1 @ X2) @ (esk2_3 @ X3 @ X1 @ X2)))|~((X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.22/0.33 thf(c_0_39, negated_conjecture, ![X1:qML_mu, X2:qML_i]:(((epred2_3 @ scott_G @ esk9_0 @ esk8_0 @ X1 @ X2)|~((scott_G @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_13, c_0_34])).
% 0.22/0.33 thf(c_0_40, negated_conjecture, (scott_G @ (esk3_3 @ scott_G @ esk9_0 @ esk8_0) @ (esk2_3 @ scott_G @ esk9_0 @ esk8_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_18]), c_0_26])).
% 0.22/0.33 thf(c_0_41, plain, ![X1:qML_mu, X2:qML_i]:(~((scott_ess_QML_mu @ scott_G @ X1 @ X2))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_36]), c_0_37])).
% 0.22/0.33 thf(c_0_42, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_18]), c_0_40])]), c_0_41]), ['proof']).
% 0.22/0.33 % SZS output end CNFRefutation
% 0.22/0.33 % Parsed axioms : 17
% 0.22/0.33 % Removed by relevancy pruning/SinE : 0
% 0.22/0.33 % Initial clauses : 29
% 0.22/0.33 % Removed in clause preprocessing : 6
% 0.22/0.33 % Initial clauses in saturation : 23
% 0.22/0.33 % Processed clauses : 886
% 0.22/0.33 % ...of these trivial : 5
% 0.22/0.33 % ...subsumed : 195
% 0.22/0.33 % ...remaining for further processing : 686
% 0.22/0.33 % Other redundant clauses eliminated : 6
% 0.22/0.33 % Clauses deleted for lack of memory : 0
% 0.22/0.33 % Backward-subsumed : 30
% 0.22/0.33 % Backward-rewritten : 29
% 0.22/0.33 % Generated clauses : 2690
% 0.22/0.33 % ...of the previous two non-redundant : 2404
% 0.22/0.33 % ...aggressively subsumed : 0
% 0.22/0.33 % Contextual simplify-reflections : 1
% 0.22/0.33 % Paramodulations : 2091
% 0.22/0.33 % Factorizations : 0
% 0.22/0.33 % NegExts : 388
% 0.22/0.33 % Equation resolutions : 6
% 0.22/0.33 % Disequality decompositions : 0
% 0.22/0.33 % Total rewrite steps : 364
% 0.22/0.33 % ...of those cached : 249
% 0.22/0.33 % Propositional unsat checks : 0
% 0.22/0.33 % Propositional check models : 0
% 0.22/0.33 % Propositional check unsatisfiable : 0
% 0.22/0.33 % Propositional clauses : 0
% 0.22/0.33 % Propositional clauses after purity: 0
% 0.22/0.33 % Propositional unsat core size : 0
% 0.22/0.33 % Propositional preprocessing time : 0.000
% 0.22/0.33 % Propositional encoding time : 0.000
% 0.22/0.33 % Propositional solver time : 0.000
% 0.22/0.33 % Success case prop preproc time : 0.000
% 0.22/0.33 % Success case prop encoding time : 0.000
% 0.22/0.33 % Success case prop solver time : 0.000
% 0.22/0.33 % Current number of processed clauses : 510
% 0.22/0.33 % Positive orientable unit clauses : 71
% 0.22/0.33 % Positive unorientable unit clauses: 0
% 0.22/0.33 % Negative unit clauses : 206
% 0.22/0.33 % Non-unit-clauses : 233
% 0.22/0.33 % Current number of unprocessed clauses: 1503
% 0.22/0.33 % ...number of literals in the above : 2971
% 0.22/0.33 % Current number of archived formulas : 0
% 0.22/0.33 % Current number of archived clauses : 176
% 0.22/0.33 % Clause-clause subsumption calls (NU) : 3213
% 0.22/0.33 % Rec. Clause-clause subsumption calls : 2843
% 0.22/0.33 % Non-unit clause-clause subsumptions : 107
% 0.22/0.33 % Unit Clause-clause subsumption calls : 680
% 0.22/0.33 % Rewrite failures with RHS unbound : 0
% 0.22/0.33 % BW rewrite match attempts : 545
% 0.22/0.33 % BW rewrite match successes : 16
% 0.22/0.33 % Condensation attempts : 886
% 0.22/0.33 % Condensation successes : 0
% 0.22/0.33 % Termbank termtop insertions : 59787
% 0.22/0.33 % Search garbage collected termcells : 641
% 0.22/0.33
% 0.22/0.33 % -------------------------------------------------
% 0.22/0.33 % User time : 0.056 s
% 0.22/0.33 % System time : 0.006 s
% 0.22/0.33 % Total time : 0.062 s
% 0.22/0.33 % Maximum resident set size: 3600 pages
% 0.22/0.33
% 0.22/0.33 % -------------------------------------------------
% 0.22/0.33 % User time : 0.262 s
% 0.22/0.33 % System time : 0.027 s
% 0.22/0.33 % Total time : 0.290 s
% 0.22/0.33 % Maximum resident set size: 4864 pages
% 0.22/0.33 % E exiting
%------------------------------------------------------------------------------