%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU695^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:25:14 AM UTC 2026
% Result : Theorem 0.27s 0.26s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU695^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n008.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 14:11:54 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.07/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.5QBZiAlmvS/E---3.1_3216964.p
% 0.27/0.26 % Version: 3.5.1-ho
% 0.27/0.26 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.27/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.27/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.27/0.26 % Starting new_ho_7 with 300s (1) cores
% 0.27/0.26 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.27/0.26 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.27/0.26 % lpo9_lambda_fix with pid 3216980 completed with status 0
% 0.27/0.26 % Result found by lpo9_lambda_fix
% 0.27/0.26 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.27/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.27/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.27/0.26 % Starting new_ho_7 with 300s (1) cores
% 0.27/0.26 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.27/0.26 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.27/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = gf500_gu_R04_F100_L20000)
% 0.27/0.26 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.27/0.26 % Search class: HGUSS-FFSF33-SHSFMSBN
% 0.27/0.26 % partial match(2): HGUSM-FFSF32-SHSFMSBN
% 0.27/0.26 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.27/0.26 % Starting SubtermCWHack with 28s (1) cores
% 0.27/0.26 % SubtermCWHack with pid 3216985 completed with status 0
% 0.27/0.26 % Result found by SubtermCWHack
% 0.27/0.26 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.27/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.27/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.27/0.26 % Starting new_ho_7 with 300s (1) cores
% 0.27/0.26 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.27/0.26 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.27/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = gf500_gu_R04_F100_L20000)
% 0.27/0.26 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.27/0.26 % Search class: HGUSS-FFSF33-SHSFMSBN
% 0.27/0.26 % partial match(2): HGUSM-FFSF32-SHSFMSBN
% 0.27/0.26 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.27/0.26 % Starting SubtermCWHack with 28s (1) cores
% 0.27/0.26 % Preprocessing time : 0.001 s
% 0.27/0.26
% 0.27/0.26 % Proof found!
% 0.27/0.26 % SZS status Theorem
% 0.27/0.26 % SZS output start CNFRefutation
% 0.27/0.26 thf(decl_23, type, in: $i > $i > $o).
% 0.27/0.26 thf(decl_24, type, kpair: $i > $i > $i).
% 0.27/0.26 thf(decl_25, type, dpsetconstr: $i > $i > ($i > $i > $o) > $i).
% 0.27/0.26 thf(decl_26, type, dpsetconstrI: $o).
% 0.27/0.26 thf(decl_27, type, func: $i > $i > $i > $o).
% 0.27/0.26 thf(decl_28, type, ap: $i > $i > $i > $i > $i).
% 0.27/0.26 thf(decl_29, type, lam: $i > $i > ($i > $i) > $i).
% 0.27/0.26 thf(decl_30, type, lamp: $o).
% 0.27/0.26 thf(decl_31, type, funcGraphProp2: $o).
% 0.27/0.26 thf(decl_32, type, esk1_3: $i > $i > ($i > $i) > $i).
% 0.27/0.26 thf(decl_33, type, esk2_0: $i).
% 0.27/0.26 thf(decl_34, type, esk3_0: $i).
% 0.27/0.26 thf(decl_35, type, esk4_0: $i > $i).
% 0.27/0.26 thf(decl_36, type, esk5_0: $i).
% 0.27/0.26 thf(decl_37, type, epred1_1: ($i > $i) > $i > $i > $o).
% 0.27/0.26 thf(beta1, conjecture, ((dpsetconstrI)=>((lamp)=>((funcGraphProp2)=>![X1:$i, X2:$i, X8:$i > $i]:((![X4:$i]:(((in @ X4 @ X1)=>(in @ (X8 @ X4) @ X2)))=>![X4:$i]:(((in @ X4 @ X1)=>((ap @ X1 @ X2 @ (lam @ X1 @ X2 @ (^[X5:$i]:(X8 @ X5))) @ X4)=(X8 @ X4))))))))), file('/export/starexec/sandbox2/tmp/tmp.5QBZiAlmvS/E---3.1_3216964.p', beta1)).
% 0.27/0.26 thf(dpsetconstrI, axiom, ((dpsetconstrI)<=>![X1:$i, X2:$i, X3:$i > $i > $o, X4:$i]:(((in @ X4 @ X1)=>![X5:$i]:(((in @ X5 @ X2)=>((X3 @ X4 @ X5)=>(in @ (kpair @ X4 @ X5) @ (dpsetconstr @ X1 @ X2 @ (^[X6:$i, X7:$i]:((X3 @ X6 @ X7))))))))))), file('/export/starexec/sandbox2/tmp/tmp.5QBZiAlmvS/E---3.1_3216964.p', dpsetconstrI)).
% 0.27/0.26 thf(lamp, axiom, ((lamp)<=>![X1:$i, X2:$i, X8:$i > $i]:((![X4:$i]:(((in @ X4 @ X1)=>(in @ (X8 @ X4) @ X2)))=>(func @ X1 @ X2 @ (lam @ X1 @ X2 @ (^[X4:$i]:(X8 @ X4))))))), file('/export/starexec/sandbox2/tmp/tmp.5QBZiAlmvS/E---3.1_3216964.p', lamp)).
% 0.27/0.26 thf(funcGraphProp2, axiom, ((funcGraphProp2)<=>![X1:$i, X2:$i, X9:$i]:(((func @ X1 @ X2 @ X9)=>![X4:$i]:(((in @ X4 @ X1)=>![X5:$i]:(((in @ X5 @ X2)=>((in @ (kpair @ X4 @ X5) @ X9)=>((ap @ X1 @ X2 @ X9 @ X4)=(X5)))))))))), file('/export/starexec/sandbox2/tmp/tmp.5QBZiAlmvS/E---3.1_3216964.p', funcGraphProp2)).
% 0.27/0.26 thf(lam, axiom, ((lam)=(^[X1:$i, X2:$i, X8:$i > $i]:(dpsetconstr @ X1 @ X2 @ (^[X4:$i, X5:$i]:(((X8 @ X4)=(X5))))))), file('/export/starexec/sandbox2/tmp/tmp.5QBZiAlmvS/E---3.1_3216964.p', lam)).
% 0.27/0.26 thf(c_0_5, negated_conjecture, ~(((dpsetconstrI)=>((lamp)=>((funcGraphProp2)=>![X1:$i, X2:$i, X8:$i > $i]:((![X4:$i]:(((in @ X4 @ X1)=>(in @ (X8 @ X4) @ X2)))=>![X4:$i]:(((in @ X4 @ X1)=>((ap @ X1 @ X2 @ (lam @ X1 @ X2 @ (^[X5:$i]:(X8 @ X5))) @ X4)=(X8 @ X4)))))))))), inference(assume_negation,[status(cth)],[beta1])).
% 0.27/0.26 thf(c_0_6, plain, ((dpsetconstrI)<=>![X1:$i, X2:$i, X3:$i > $i > $o, X4:$i]:(((in @ X4 @ X1)=>![X5:$i]:(((in @ X5 @ X2)=>((X3 @ X4 @ X5)=>(in @ (kpair @ X4 @ X5) @ (dpsetconstr @ X1 @ X2 @ (^[Z0:$i, Z1:$i]:((X3 @ Z0 @ Z1))))))))))), inference(fof_simplification,[status(thm)],[dpsetconstrI])).
% 0.27/0.26 thf(c_0_7, plain, ((lamp)<=>![X1:$i, X2:$i, X8:$i > $i]:((![X4:$i]:(((in @ X4 @ X1)=>(in @ (X8 @ X4) @ X2)))=>(func @ X1 @ X2 @ (lam @ X1 @ X2 @ (^[Z0:$i]:(X8 @ Z0))))))), inference(fof_simplification,[status(thm)],[lamp])).
% 0.27/0.26 thf(c_0_8, negated_conjecture, ~((![X29:$i, X30:$i, X31:$i > $i > $o, X32:$i]:(((in @ X32 @ X29)=>![X33:$i]:(((in @ X33 @ X30)=>((X31 @ X32 @ X33)=>(in @ (kpair @ X32 @ X33) @ (dpsetconstr @ X29 @ X30 @ X31)))))))=>(![X34:$i, X35:$i, X36:$i > $i]:((![X37:$i]:(((in @ X37 @ X34)=>(in @ (X36 @ X37) @ X35)))=>(func @ X34 @ X35 @ (lam @ X34 @ X35 @ X36))))=>(![X38:$i, X39:$i, X40:$i]:(((func @ X38 @ X39 @ X40)=>![X41:$i]:(((in @ X41 @ X38)=>![X42:$i]:(((in @ X42 @ X39)=>((in @ (kpair @ X41 @ X42) @ X40)=>((ap @ X38 @ X39 @ X40 @ X41)=(X42)))))))))=>![X1:$i, X2:$i, X8:$i > $i]:((![X4:$i]:(((in @ X4 @ X1)=>(in @ (X8 @ X4) @ X2)))=>![X4:$i]:(((in @ X4 @ X1)=>((ap @ X1 @ X2 @ (lam @ X1 @ X2 @ X8) @ X4)=(X8 @ X4)))))))))), inference(fool_unroll,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_5]), c_0_6]), c_0_7]), funcGraphProp2])])).
% 0.27/0.26 thf(c_0_9, plain, ![X43:$i, X44:$i, X45:$i > $i]:(((lam @ X43 @ X44 @ X45)=(dpsetconstr @ X43 @ X44 @ (^[Z0:$i]:($eq @ (X45 @ Z0)))))), inference(fool_unroll,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[lam])])])).
% 0.27/0.26 thf(c_0_10, negated_conjecture, ![X46:$i, X47:$i, X48:$i > $i > $o, X49:$i, X50:$i, X51:$i, X52:$i, X53:$i > $i, X55:$i, X56:$i, X57:$i, X58:$i, X59:$i, X63:$i]:(((~(in @ X49 @ X46)|(~(in @ X50 @ X47)|(~(X48 @ X49 @ X50)|(in @ (kpair @ X49 @ X50) @ (dpsetconstr @ X46 @ X47 @ X48)))))&((((in @ (esk1_3 @ X51 @ X52 @ X53) @ X51)|(func @ X51 @ X52 @ (lam @ X51 @ X52 @ X53)))&(~(in @ (X53 @ (esk1_3 @ X51 @ X52 @ X53)) @ X52)|(func @ X51 @ X52 @ (lam @ X51 @ X52 @ X53))))&((~(func @ X55 @ X56 @ X57)|(~(in @ X58 @ X55)|(~(in @ X59 @ X56)|(~(in @ (kpair @ X58 @ X59) @ X57)|((ap @ X55 @ X56 @ X57 @ X58)=(X59))))))&((~(in @ X63 @ esk2_0)|(in @ (esk4_0 @ X63) @ esk3_0))&((in @ esk5_0 @ esk2_0)&((ap @ esk2_0 @ esk3_0 @ (lam @ esk2_0 @ esk3_0 @ esk4_0) @ esk5_0)!=(esk4_0 @ esk5_0)))))))), 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_8])])])])])])).
% 0.27/0.26 thf(c_0_11, plain, ![X65:$i, X66:$i, X67:$i > $i]:(((lam @ X65 @ X66 @ X67)=(dpsetconstr @ X65 @ X66 @ (^[Z0:$i]:($eq @ (X67 @ Z0)))))), inference(variable_rename,[status(thm)],[c_0_9])).
% 0.27/0.26 thf(c_0_12, plain, ![X68:$i, X8:$i > $i]:(((epred1_1 @ X8 @ X68)=($eq @ (X8 @ X68)))), introduced(definition)).
% 0.27/0.26 thf(c_0_13, plain, ![X69:$i, X70:$i > $i]:(((epred1_1 @ X70 @ X69)=($eq @ (X70 @ X69)))), inference(variable_rename,[status(thm)],[])).
% 0.27/0.26 thf(c_0_14, negated_conjecture, ![X1:$i, X3:$i > $i > $o, X2:$i, X5:$i, X4:$i]:(((in @ (kpair @ X1 @ X4) @ (dpsetconstr @ X2 @ X5 @ X3))|~((in @ X1 @ X2))|~((in @ X4 @ X5))|~((X3 @ X1 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_15, plain, ![X1:$i, X2:$i, X8:$i > $i]:(((lam @ X1 @ X2 @ X8)=(dpsetconstr @ X1 @ X2 @ (epred1_1 @ X8)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_11]), c_0_12])).
% 0.27/0.26 thf(c_0_16, plain, ![X8:$i > $i, X1:$i]:(((epred1_1 @ X8 @ X1)=($eq @ (X8 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.27/0.26 thf(c_0_17, negated_conjecture, ![X1:$i, X2:$i, X6:$i, X5:$i, X4:$i]:((((ap @ X1 @ X2 @ X4 @ X5)=(X6))|~((func @ X1 @ X2 @ X4))|~((in @ X5 @ X1))|~((in @ X6 @ X2))|~((in @ (kpair @ X5 @ X6) @ X4)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_18, negated_conjecture, ![X1:$i, X2:$i, X8:$i > $i, X5:$i, X4:$i]:(((in @ (kpair @ X1 @ X2) @ (lam @ X4 @ X5 @ X8))|~((epred1_1 @ X8 @ X1 @ X2))|~((in @ X2 @ X5))|~((in @ X1 @ X4)))), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 0.27/0.26 thf(c_0_19, plain, ![X1:$i, X8:$i > $i, X71:$i]:((((X8 @ X1)=(X71))<=>(epred1_1 @ X8 @ X1 @ X71))), inference(arg_cong,[status(thm)],[c_0_16])).
% 0.27/0.26 thf(c_0_20, negated_conjecture, ![X1:$i, X2:$i, X8:$i > $i, X7:$i, X6:$i, X5:$i, X4:$i]:((((ap @ X1 @ X2 @ (lam @ X4 @ X5 @ X8) @ X6)=(X7))|~((func @ X1 @ X2 @ (lam @ X4 @ X5 @ X8)))|~((epred1_1 @ X8 @ X6 @ X7))|~((in @ X7 @ X2))|~((in @ X6 @ X1))|~((in @ X7 @ X5))|~((in @ X6 @ X4)))), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.27/0.26 thf(c_0_21, plain, ![X8:$i > $i, X1:$i]:((epred1_1 @ X8 @ X1 @ (X8 @ X1))), inference(er,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_19])])).
% 0.27/0.26 thf(c_0_22, negated_conjecture, ((ap @ esk2_0 @ esk3_0 @ (lam @ esk2_0 @ esk3_0 @ esk4_0) @ esk5_0)!=(esk4_0 @ esk5_0)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_23, plain, ![X1:$i, X2:$i, X8:$i > $i, X6:$i, X5:$i, X4:$i]:((((ap @ X1 @ X2 @ (lam @ X4 @ X5 @ X8) @ X6)=(X8 @ X6))|~((func @ X1 @ X2 @ (lam @ X4 @ X5 @ X8)))|~((in @ (X8 @ X6) @ X2))|~((in @ (X8 @ X6) @ X5))|~((in @ X6 @ X1))|~((in @ X6 @ X4)))), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 0.27/0.26 thf(c_0_24, negated_conjecture, (in @ esk5_0 @ esk2_0), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_25, negated_conjecture, ![X1:$i, X8:$i > $i, X2:$i]:(((func @ X1 @ X2 @ (lam @ X1 @ X2 @ X8))|~((in @ (X8 @ (esk1_3 @ X1 @ X2 @ X8)) @ X2)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_26, negated_conjecture, ![X1:$i]:(((in @ (esk4_0 @ X1) @ esk3_0)|~((in @ X1 @ esk2_0)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_27, negated_conjecture, (~((func @ esk2_0 @ esk3_0 @ (lam @ esk2_0 @ esk3_0 @ esk4_0)))|~((in @ (esk4_0 @ esk5_0) @ esk3_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_24])])).
% 0.27/0.26 thf(c_0_28, negated_conjecture, ![X1:$i, X2:$i, X8:$i > $i]:(((in @ (esk1_3 @ X1 @ X2 @ X8) @ X1)|(func @ X1 @ X2 @ (lam @ X1 @ X2 @ X8)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.27/0.26 thf(c_0_29, negated_conjecture, ![X1:$i]:(((func @ X1 @ esk3_0 @ (lam @ X1 @ esk3_0 @ esk4_0))|~((in @ (esk1_3 @ X1 @ esk3_0 @ esk4_0) @ esk2_0)))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 0.27/0.26 thf(c_0_30, negated_conjecture, ((in @ (esk1_3 @ esk2_0 @ esk3_0 @ esk4_0) @ esk2_0)|~((in @ (esk4_0 @ esk5_0) @ esk3_0))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 0.27/0.26 thf(c_0_31, negated_conjecture, ~((in @ (esk4_0 @ esk5_0) @ esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_29]), c_0_30])).
% 0.27/0.26 thf(c_0_32, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_26]), c_0_24])]), ['proof']).
% 0.27/0.26 % SZS output end CNFRefutation
% 0.27/0.26 % Parsed axioms : 14
% 0.27/0.26 % Removed by relevancy pruning/SinE : 9
% 0.27/0.26 % Initial clauses : 9
% 0.27/0.26 % Removed in clause preprocessing : 0
% 0.27/0.26 % Initial clauses in saturation : 9
% 0.27/0.26 % Processed clauses : 31
% 0.27/0.26 % ...of these trivial : 0
% 0.27/0.26 % ...subsumed : 4
% 0.27/0.26 % ...remaining for further processing : 27
% 0.27/0.26 % Other redundant clauses eliminated : 1
% 0.27/0.26 % Clauses deleted for lack of memory : 0
% 0.27/0.26 % Backward-subsumed : 2
% 0.27/0.26 % Backward-rewritten : 0
% 0.27/0.26 % Generated clauses : 40
% 0.27/0.26 % ...of the previous two non-redundant : 38
% 0.27/0.26 % ...aggressively subsumed : 0
% 0.27/0.26 % Contextual simplify-reflections : 1
% 0.27/0.26 % Paramodulations : 34
% 0.27/0.26 % Factorizations : 0
% 0.27/0.26 % NegExts : 0
% 0.27/0.26 % Equation resolutions : 1
% 0.27/0.26 % Disequality decompositions : 0
% 0.27/0.26 % Total rewrite steps : 3
% 0.27/0.26 % ...of those cached : 1
% 0.27/0.26 % Propositional unsat checks : 0
% 0.27/0.26 % Propositional check models : 0
% 0.27/0.26 % Propositional check unsatisfiable : 0
% 0.27/0.26 % Propositional clauses : 0
% 0.27/0.26 % Propositional clauses after purity: 0
% 0.27/0.26 % Propositional unsat core size : 0
% 0.27/0.26 % Propositional preprocessing time : 0.000
% 0.27/0.26 % Propositional encoding time : 0.000
% 0.27/0.26 % Propositional solver time : 0.000
% 0.27/0.26 % Success case prop preproc time : 0.000
% 0.27/0.26 % Success case prop encoding time : 0.000
% 0.27/0.26 % Success case prop solver time : 0.000
% 0.27/0.26 % Current number of processed clauses : 24
% 0.27/0.26 % Positive orientable unit clauses : 4
% 0.27/0.26 % Positive unorientable unit clauses: 0
% 0.27/0.26 % Negative unit clauses : 2
% 0.27/0.26 % Non-unit-clauses : 18
% 0.27/0.26 % Current number of unprocessed clauses: 16
% 0.27/0.26 % ...number of literals in the above : 115
% 0.27/0.26 % Current number of archived formulas : 0
% 0.27/0.26 % Current number of archived clauses : 3
% 0.27/0.26 % Clause-clause subsumption calls (NU) : 157
% 0.27/0.26 % Rec. Clause-clause subsumption calls : 46
% 0.27/0.26 % Non-unit clause-clause subsumptions : 5
% 0.27/0.26 % Unit Clause-clause subsumption calls : 2
% 0.27/0.26 % Rewrite failures with RHS unbound : 0
% 0.27/0.26 % BW rewrite match attempts : 1
% 0.27/0.26 % BW rewrite match successes : 0
% 0.27/0.26 % Condensation attempts : 0
% 0.27/0.26 % Condensation successes : 0
% 0.27/0.26 % Termbank termtop insertions : 2837
% 0.27/0.26 % Search garbage collected termcells : 560
% 0.27/0.26
% 0.27/0.26 % -------------------------------------------------
% 0.27/0.26 % User time : 0.005 s
% 0.27/0.26 % System time : 0.003 s
% 0.27/0.26 % Total time : 0.008 s
% 0.27/0.26 % Maximum resident set size: 3648 pages
% 0.27/0.26
% 0.27/0.26 % -------------------------------------------------
% 0.27/0.26 % User time : 0.006 s
% 0.27/0.26 % System time : 0.008 s
% 0.27/0.26 % Total time : 0.014 s
% 0.27/0.26 % Maximum resident set size: 4864 pages
% 0.27/0.26 % E exiting
%------------------------------------------------------------------------------