%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO250^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:42:38 AM UTC 2026
% Result : Theorem 0.06s 0.19s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO250^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.14 % Computer : n012.cluster.edu
% 0.06/0.14 % Model : x86_64 x86_64
% 0.06/0.14 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.14 % Memory : 8046.5625MB
% 0.06/0.14 % OS : Linux 6.8.0-71-generic
% 0.06/0.14 % CPULimit : 300
% 0.06/0.14 % WCLimit : 300
% 0.06/0.14 % DateTime : Tue Sep 29 16:41:03 UTC 2026
% 0.06/0.14 % CPUTime :
% 0.06/0.14 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 Running higher-order theorem proving
% 0.06/0.18 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.UsbxUnHKGH/E---3.1_347192.p
% 0.06/0.19 % Version: 3.5.1-ho
% 0.06/0.19 % Preprocessing class: HSMSSMSSSSSNSSA.
% 0.06/0.19 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.06/0.19 % Starting post_as_ho1 with 1500s (5) cores
% 0.06/0.19 % Starting post_as_ho12 with 300s (1) cores
% 0.06/0.19 % Starting new_ho_3 with 300s (1) cores
% 0.06/0.19 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.06/0.19 % post_as_ho12 with pid 347206 completed with status 0
% 0.06/0.19 % Result found by post_as_ho12
% 0.06/0.19 % Preprocessing class: HSMSSMSSSSSNSSA.
% 0.06/0.19 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.06/0.19 % Starting post_as_ho1 with 1500s (5) cores
% 0.06/0.19 % Starting post_as_ho12 with 300s (1) cores
% 0.06/0.19 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.06/0.19 % No SInE strategy applied
% 0.06/0.19 % Search class: HGHSM-FFMF33-SSSFFFNN
% 0.06/0.19 % partial match(3): FGHSM-FFMF33-SFFFFFNN
% 0.06/0.19 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.06/0.19 % Starting SubtermCWHack with 28s (1) cores
% 0.06/0.19 % SubtermCWHack with pid 347209 completed with status 0
% 0.06/0.19 % Result found by SubtermCWHack
% 0.06/0.19 % Preprocessing class: HSMSSMSSSSSNSSA.
% 0.06/0.19 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.06/0.19 % Starting post_as_ho1 with 1500s (5) cores
% 0.06/0.19 % Starting post_as_ho12 with 300s (1) cores
% 0.06/0.19 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.06/0.19 % No SInE strategy applied
% 0.06/0.19 % Search class: HGHSM-FFMF33-SSSFFFNN
% 0.06/0.19 % partial match(3): FGHSM-FFMF33-SFFFFFNN
% 0.06/0.19 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.06/0.19 % Starting SubtermCWHack with 28s (1) cores
% 0.06/0.19 % Preprocessing time : 0.001 s
% 0.06/0.19
% 0.06/0.19 % Proof found!
% 0.06/0.19 % SZS status Theorem
% 0.06/0.19 % SZS output start CNFRefutation
% 0.06/0.19 thf(decl_23, type, epred1_13: $i > $i > ($i > $i) > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $o).
% 0.06/0.19 thf(decl_24, type, esk1_12: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i).
% 0.06/0.19 thf(cSIXFRIENDS, conjecture, ?[X1:$i, X2:$i, X3:$i, X4:$i, X5:$i, X6:$i, X7:$i, X8:$i, X9:$i, X10:$i, X11:$i, X12:$i]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((X1)!=(X2))&((X1)!=(X3)))&((X1)!=(X4)))&((X1)!=(X5)))&((X1)!=(X6)))&((X1)!=(X7)))&((X1)!=(X8)))&((X1)!=(X9)))&((X1)!=(X10)))&((X1)!=(X11)))&((X1)!=(X12)))&((X2)!=(X3)))&((X2)!=(X4)))&((X2)!=(X5)))&((X2)!=(X6)))&((X2)!=(X7)))&((X2)!=(X8)))&((X2)!=(X9)))&((X2)!=(X10)))&((X2)!=(X11)))&((X2)!=(X12)))&((X3)!=(X4)))&((X3)!=(X5)))&((X3)!=(X6)))&((X3)!=(X7)))&((X3)!=(X8)))&((X3)!=(X9)))&((X3)!=(X10)))&((X3)!=(X11)))&((X3)!=(X12)))&((X5)!=(X6)))&((X5)!=(X7)))&((X5)!=(X8)))&((X5)!=(X9)))&((X5)!=(X10)))&((X5)!=(X11)))&((X5)!=(X12)))&((X6)!=(X7)))&((X6)!=(X8)))&((X6)!=(X9)))&((X6)!=(X10)))&((X6)!=(X11)))&((X6)!=(X12)))&((X7)!=(X8)))&((X7)!=(X9)))&((X7)!=(X10)))&((X7)!=(X11)))&((X7)!=(X12)))&((X8)!=(X9)))&((X8)!=(X10)))&((X8)!=(X11)))&((X8)!=(X12)))&((X9)!=(X10)))&((X9)!=(X11)))&((X9)!=(X12)))&((X10)!=(X11)))&((X10)!=(X12)))&((X11)!=(X12)))=>![X13:$i > $i]:((((((((((((X13 @ X1)=(X13 @ X2))&((X13 @ X3)=(X13 @ X4)))&((X13 @ X9)=(X13 @ X12)))=>((X13 @ X5)=(X13 @ X8)))&(((((X13 @ X1)=(X13 @ X2))&((X13 @ X11)=(X13 @ X12)))&((X13 @ X3)=(X13 @ X6)))=>((X13 @ X7)!=(X13 @ X10))))&((((((X13 @ X5)=(X13 @ X6))&((X13 @ X6)=(X13 @ X7)))&((X13 @ X7)=(X13 @ X8)))&((X13 @ X1)!=(X13 @ X4)))=>((X13 @ X9)!=(X13 @ X12))))&(((((X13 @ X1)=(X13 @ X2))&((X13 @ X7)=(X13 @ X8)))&((X13 @ X3)!=(X13 @ X6)))=>((X13 @ X9)=(X13 @ X12))))&(((((X13 @ X9)=(X13 @ X10))&((X13 @ X11)=(X13 @ X12)))&((X13 @ X5)=(X13 @ X8)))=>((X13 @ X1)!=(X13 @ X4))))&((((((X13 @ X3)=(X13 @ X4))&((X13 @ X4)=(X13 @ X5)))&((X13 @ X5)=(X13 @ X6)))&((X13 @ X9)!=(X13 @ X12)))=>((X13 @ X7)=(X13 @ X10))))=>(((X13 @ X1)!=(X13 @ X2))|((X13 @ X3)!=(X13 @ X4))|((X13 @ X5)!=(X13 @ X6))|((X13 @ X7)!=(X13 @ X8))|((X13 @ X9)!=(X13 @ X10))|((X13 @ X11)!=(X13 @ X12))))))), file('/export/starexec/sandbox2/tmp/tmp.UsbxUnHKGH/E---3.1_347192.p', cSIXFRIENDS)).
% 0.06/0.19 thf(c_0_1, negated_conjecture, ~(?[X1:$i, X2:$i, X3:$i, X4:$i, X5:$i, X6:$i, X7:$i, X8:$i, X9:$i, X10:$i, X11:$i, X12:$i]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((X1)!=(X2))&((X1)!=(X3)))&((X1)!=(X4)))&((X1)!=(X5)))&((X1)!=(X6)))&((X1)!=(X7)))&((X1)!=(X8)))&((X1)!=(X9)))&((X1)!=(X10)))&((X1)!=(X11)))&((X1)!=(X12)))&((X2)!=(X3)))&((X2)!=(X4)))&((X2)!=(X5)))&((X2)!=(X6)))&((X2)!=(X7)))&((X2)!=(X8)))&((X2)!=(X9)))&((X2)!=(X10)))&((X2)!=(X11)))&((X2)!=(X12)))&((X3)!=(X4)))&((X3)!=(X5)))&((X3)!=(X6)))&((X3)!=(X7)))&((X3)!=(X8)))&((X3)!=(X9)))&((X3)!=(X10)))&((X3)!=(X11)))&((X3)!=(X12)))&((X5)!=(X6)))&((X5)!=(X7)))&((X5)!=(X8)))&((X5)!=(X9)))&((X5)!=(X10)))&((X5)!=(X11)))&((X5)!=(X12)))&((X6)!=(X7)))&((X6)!=(X8)))&((X6)!=(X9)))&((X6)!=(X10)))&((X6)!=(X11)))&((X6)!=(X12)))&((X7)!=(X8)))&((X7)!=(X9)))&((X7)!=(X10)))&((X7)!=(X11)))&((X7)!=(X12)))&((X8)!=(X9)))&((X8)!=(X10)))&((X8)!=(X11)))&((X8)!=(X12)))&((X9)!=(X10)))&((X9)!=(X11)))&((X9)!=(X12)))&((X10)!=(X11)))&((X10)!=(X12)))&((X11)!=(X12)))=>![X13:$i > $i]:((((((((((((X13 @ X1)=(X13 @ X2))&((X13 @ X3)=(X13 @ X4)))&((X13 @ X9)=(X13 @ X12)))=>((X13 @ X5)=(X13 @ X8)))&(((((X13 @ X1)=(X13 @ X2))&((X13 @ X11)=(X13 @ X12)))&((X13 @ X3)=(X13 @ X6)))=>((X13 @ X7)!=(X13 @ X10))))&((((((X13 @ X5)=(X13 @ X6))&((X13 @ X6)=(X13 @ X7)))&((X13 @ X7)=(X13 @ X8)))&((X13 @ X1)!=(X13 @ X4)))=>((X13 @ X9)!=(X13 @ X12))))&(((((X13 @ X1)=(X13 @ X2))&((X13 @ X7)=(X13 @ X8)))&((X13 @ X3)!=(X13 @ X6)))=>((X13 @ X9)=(X13 @ X12))))&(((((X13 @ X9)=(X13 @ X10))&((X13 @ X11)=(X13 @ X12)))&((X13 @ X5)=(X13 @ X8)))=>((X13 @ X1)!=(X13 @ X4))))&((((((X13 @ X3)=(X13 @ X4))&((X13 @ X4)=(X13 @ X5)))&((X13 @ X5)=(X13 @ X6)))&((X13 @ X9)!=(X13 @ X12)))=>((X13 @ X7)=(X13 @ X10))))=>(((X13 @ X1)!=(X13 @ X2))|((X13 @ X3)!=(X13 @ X4))|((X13 @ X5)!=(X13 @ X6))|((X13 @ X7)!=(X13 @ X8))|((X13 @ X9)!=(X13 @ X10))|((X13 @ X11)!=(X13 @ X12)))))))), inference(assume_negation,[status(cth)],[cSIXFRIENDS])).
% 0.06/0.19 thf(c_0_2, plain, ![X1:$i, X2:$i, X3:$i, X4:$i, X5:$i, X6:$i, X7:$i, X8:$i, X9:$i, X13:$i > $i, X12:$i, X11:$i, X10:$i]:(((epred1_13 @ X10 @ X12 @ X13 @ X11 @ X9 @ X7 @ X8 @ X6 @ X5 @ X4 @ X3 @ X1 @ X2)<=>((((((((((X13 @ X1)=(X13 @ X2))&((X13 @ X3)=(X13 @ X4)))&((X13 @ X9)=(X13 @ X12)))=>((X13 @ X5)=(X13 @ X8)))&(((((X13 @ X1)=(X13 @ X2))&((X13 @ X11)=(X13 @ X12)))&((X13 @ X3)=(X13 @ X6)))=>((X13 @ X7)!=(X13 @ X10))))&((((((X13 @ X5)=(X13 @ X6))&((X13 @ X6)=(X13 @ X7)))&((X13 @ X7)=(X13 @ X8)))&((X13 @ X1)!=(X13 @ X4)))=>((X13 @ X9)!=(X13 @ X12))))&(((((X13 @ X1)=(X13 @ X2))&((X13 @ X7)=(X13 @ X8)))&((X13 @ X3)!=(X13 @ X6)))=>((X13 @ X9)=(X13 @ X12))))&(((((X13 @ X9)=(X13 @ X10))&((X13 @ X11)=(X13 @ X12)))&((X13 @ X5)=(X13 @ X8)))=>((X13 @ X1)!=(X13 @ X4))))&((((((X13 @ X3)=(X13 @ X4))&((X13 @ X4)=(X13 @ X5)))&((X13 @ X5)=(X13 @ X6)))&((X13 @ X9)!=(X13 @ X12)))=>((X13 @ X7)=(X13 @ X10)))))), introduced(definition)).
% 0.06/0.19 thf(c_0_3, negated_conjecture, ~(?[X1:$i, X2:$i, X3:$i, X4:$i, X5:$i, X6:$i, X7:$i, X8:$i, X9:$i, X10:$i, X11:$i, X12:$i]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((X1)!=(X2))&((X1)!=(X3)))&((X1)!=(X4)))&((X1)!=(X5)))&((X1)!=(X6)))&((X1)!=(X7)))&((X1)!=(X8)))&((X1)!=(X9)))&((X1)!=(X10)))&((X1)!=(X11)))&((X1)!=(X12)))&((X2)!=(X3)))&((X2)!=(X4)))&((X2)!=(X5)))&((X2)!=(X6)))&((X2)!=(X7)))&((X2)!=(X8)))&((X2)!=(X9)))&((X2)!=(X10)))&((X2)!=(X11)))&((X2)!=(X12)))&((X3)!=(X4)))&((X3)!=(X5)))&((X3)!=(X6)))&((X3)!=(X7)))&((X3)!=(X8)))&((X3)!=(X9)))&((X3)!=(X10)))&((X3)!=(X11)))&((X3)!=(X12)))&((X5)!=(X6)))&((X5)!=(X7)))&((X5)!=(X8)))&((X5)!=(X9)))&((X5)!=(X10)))&((X5)!=(X11)))&((X5)!=(X12)))&((X6)!=(X7)))&((X6)!=(X8)))&((X6)!=(X9)))&((X6)!=(X10)))&((X6)!=(X11)))&((X6)!=(X12)))&((X7)!=(X8)))&((X7)!=(X9)))&((X7)!=(X10)))&((X7)!=(X11)))&((X7)!=(X12)))&((X8)!=(X9)))&((X8)!=(X10)))&((X8)!=(X11)))&((X8)!=(X12)))&((X9)!=(X10)))&((X9)!=(X11)))&((X9)!=(X12)))&((X10)!=(X11)))&((X10)!=(X12)))&((X11)!=(X12)))=>![X13:$i > $i]:(((epred1_13 @ X10 @ X12 @ X13 @ X11 @ X9 @ X7 @ X8 @ X6 @ X5 @ X4 @ X3 @ X1 @ X2)=>(((X13 @ X1)!=(X13 @ X2))|((X13 @ X3)!=(X13 @ X4))|((X13 @ X5)!=(X13 @ X6))|((X13 @ X7)!=(X13 @ X8))|((X13 @ X9)!=(X13 @ X10))|((X13 @ X11)!=(X13 @ X12)))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_1]), c_0_2])).
% 0.06/0.19 thf(c_0_4, negated_conjecture, ![X27:$i, X28:$i, X29:$i, X30:$i, X31:$i, X32:$i, X33:$i, X34:$i, X35:$i, X36:$i, X37:$i, X38:$i]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((X27)!=(X28))&((X27)!=(X29)))&((X27)!=(X30)))&((X27)!=(X31)))&((X27)!=(X32)))&((X27)!=(X33)))&((X27)!=(X34)))&((X27)!=(X35)))&((X27)!=(X36)))&((X27)!=(X37)))&((X27)!=(X38)))&((X28)!=(X29)))&((X28)!=(X30)))&((X28)!=(X31)))&((X28)!=(X32)))&((X28)!=(X33)))&((X28)!=(X34)))&((X28)!=(X35)))&((X28)!=(X36)))&((X28)!=(X37)))&((X28)!=(X38)))&((X29)!=(X30)))&((X29)!=(X31)))&((X29)!=(X32)))&((X29)!=(X33)))&((X29)!=(X34)))&((X29)!=(X35)))&((X29)!=(X36)))&((X29)!=(X37)))&((X29)!=(X38)))&((X31)!=(X32)))&((X31)!=(X33)))&((X31)!=(X34)))&((X31)!=(X35)))&((X31)!=(X36)))&((X31)!=(X37)))&((X31)!=(X38)))&((X32)!=(X33)))&((X32)!=(X34)))&((X32)!=(X35)))&((X32)!=(X36)))&((X32)!=(X37)))&((X32)!=(X38)))&((X33)!=(X34)))&((X33)!=(X35)))&((X33)!=(X36)))&((X33)!=(X37)))&((X33)!=(X38)))&((X34)!=(X35)))&((X34)!=(X36)))&((X34)!=(X37)))&((X34)!=(X38)))&((X35)!=(X36)))&((X35)!=(X37)))&((X35)!=(X38)))&((X36)!=(X37)))&((X36)!=(X38)))&((X37)!=(X38)))&((epred1_13 @ X36 @ X38 @ (esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38) @ X37 @ X35 @ X33 @ X34 @ X32 @ X31 @ X30 @ X29 @ X27 @ X28)&(((((((esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X27)=(esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X28))&((esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X29)=(esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X30)))&((esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X31)=(esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X32)))&((esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X33)=(esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X34)))&((esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X35)=(esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X36)))&((esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X37)=(esk1_12 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @ X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X38)))))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])).
% 0.06/0.19 thf(c_0_5, negated_conjecture, ![X1:$i, X2:$i]:(((X1)!=(X2))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.06/0.19 thf(c_0_6, negated_conjecture, ($false), inference(flex_resolve,[status(thm)],[c_0_5]), ['proof']).
% 0.06/0.19 % SZS output end CNFRefutation
% 0.06/0.19 % Parsed axioms : 1
% 0.06/0.19 % Removed by relevancy pruning/SinE : 0
% 0.06/0.19 % Initial clauses : 71
% 0.06/0.19 % Removed in clause preprocessing : 0
% 0.06/0.19 % Initial clauses in saturation : 71
% 0.06/0.19 % Processed clauses : 1
% 0.06/0.19 % ...of these trivial : 0
% 0.06/0.19 % ...subsumed : 0
% 0.06/0.19 % ...remaining for further processing : 0
% 0.06/0.19 % Other redundant clauses eliminated : 0
% 0.06/0.19 % Clauses deleted for lack of memory : 0
% 0.06/0.19 % Backward-subsumed : 0
% 0.06/0.19 % Backward-rewritten : 0
% 0.06/0.19 % Generated clauses : 0
% 0.06/0.19 % ...of the previous two non-redundant : 0
% 0.06/0.19 % ...aggressively subsumed : 0
% 0.06/0.19 % Contextual simplify-reflections : 0
% 0.06/0.19 % Paramodulations : 0
% 0.06/0.19 % Factorizations : 0
% 0.06/0.19 % NegExts : 0
% 0.06/0.19 % Equation resolutions : 0
% 0.06/0.19 % Disequality decompositions : 0
% 0.06/0.19 % Total rewrite steps : 0
% 0.06/0.19 % ...of those cached : 0
% 0.06/0.19 % Propositional unsat checks : 0
% 0.06/0.19 % Propositional check models : 0
% 0.06/0.19 % Propositional check unsatisfiable : 0
% 0.06/0.19 % Propositional clauses : 0
% 0.06/0.19 % Propositional clauses after purity: 0
% 0.06/0.19 % Propositional unsat core size : 0
% 0.06/0.19 % Propositional preprocessing time : 0.000
% 0.06/0.19 % Propositional encoding time : 0.000
% 0.06/0.19 % Propositional solver time : 0.000
% 0.06/0.19 % Success case prop preproc time : 0.000
% 0.06/0.19 % Success case prop encoding time : 0.000
% 0.06/0.19 % Success case prop solver time : 0.000
% 0.06/0.19 % Current number of processed clauses : 0
% 0.06/0.19 % Positive orientable unit clauses : 0
% 0.06/0.19 % Positive unorientable unit clauses: 0
% 0.06/0.19 % Negative unit clauses : 0
% 0.06/0.19 % Non-unit-clauses : 0
% 0.06/0.19 % Current number of unprocessed clauses: 70
% 0.06/0.19 % ...number of literals in the above : 96
% 0.06/0.19 % Current number of archived formulas : 0
% 0.06/0.19 % Current number of archived clauses : 0
% 0.06/0.19 % Clause-clause subsumption calls (NU) : 0
% 0.06/0.19 % Rec. Clause-clause subsumption calls : 0
% 0.06/0.19 % Non-unit clause-clause subsumptions : 0
% 0.06/0.19 % Unit Clause-clause subsumption calls : 0
% 0.06/0.19 % Rewrite failures with RHS unbound : 0
% 0.06/0.19 % BW rewrite match attempts : 0
% 0.06/0.19 % BW rewrite match successes : 0
% 0.06/0.19 % Condensation attempts : 0
% 0.06/0.19 % Condensation successes : 0
% 0.06/0.19 % Termbank termtop insertions : 3222
% 0.06/0.19 % Search garbage collected termcells : 1260
% 0.06/0.19
% 0.06/0.19 % -------------------------------------------------
% 0.06/0.19 % User time : 0.004 s
% 0.06/0.19 % System time : 0.000 s
% 0.06/0.19 % Total time : 0.004 s
% 0.06/0.19 % Maximum resident set size: 3912 pages
% 0.06/0.19
% 0.06/0.19 % -------------------------------------------------
% 0.06/0.19 % User time : 0.005 s
% 0.06/0.19 % System time : 0.003 s
% 0.06/0.19 % Total time : 0.008 s
% 0.06/0.19 % Maximum resident set size: 4608 pages
% 0.06/0.19 % E exiting
%------------------------------------------------------------------------------