%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU463^1 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:23:52 AM UTC 2026
% Result : Theorem 0.21s 0.27s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU463^1 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 13:42:01 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.24 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.CUz68hE36u/E---3.1_112673.p
% 0.21/0.27 % Version: 3.5.1-ho
% 0.21/0.27 % Preprocessing class: HSMSSMSSMLSNHSA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.27 % Starting sh5l with 300s (1) cores
% 0.21/0.27 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.27 % Starting new_bool_2 with 300s (1) cores
% 0.21/0.27 % new_bool_1 with pid 112697 completed with status 0
% 0.21/0.27 % Result found by new_bool_1
% 0.21/0.27 % Preprocessing class: HSMSSMSSMLSNHSA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.27 % Starting sh5l with 300s (1) cores
% 0.21/0.27 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.27 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.21/0.27 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.21/0.27 % Search class: HGUNF-FFMF33-SHSSMMBN
% 0.21/0.27 % partial match(2): HGUNS-FFMF32-SHSSMMBN
% 0.21/0.27 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.27 % SubtermCWHack with pid 112699 completed with status 0
% 0.21/0.27 % Result found by SubtermCWHack
% 0.21/0.27 % Preprocessing class: HSMSSMSSMLSNHSA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.27 % Starting sh5l with 300s (1) cores
% 0.21/0.27 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.27 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.21/0.27 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.21/0.27 % Search class: HGUNF-FFMF33-SHSSMMBN
% 0.21/0.27 % partial match(2): HGUNS-FFMF32-SHSSMMBN
% 0.21/0.27 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.27 % Preprocessing time : 0.001 s
% 0.21/0.27
% 0.21/0.27 % Proof found!
% 0.21/0.27 % SZS status Theorem
% 0.21/0.27 % SZS output start CNFRefutation
% 0.21/0.27 thf(decl_23, type, subrel: ($i > $i > $o) > ($i > $i > $o) > $o).
% 0.21/0.27 thf(decl_35, type, trans: ($i > $i > $o) > $o).
% 0.21/0.27 thf(decl_36, type, tc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.27 thf(decl_52, type, epred1_5: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $o).
% 0.21/0.27 thf(decl_53, type, epred2_0: $i > $i > $o).
% 0.21/0.27 thf(decl_54, type, esk1_0: $i).
% 0.21/0.27 thf(decl_55, type, esk2_0: $i).
% 0.21/0.27 thf(decl_56, type, esk3_0: $i).
% 0.21/0.27 thf(decl_57, type, epred3_0: $i > $i > $o).
% 0.21/0.27 thf(decl_58, type, esk4_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_59, type, esk5_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_60, type, esk6_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_61, type, esk7_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_62, type, esk8_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_63, type, esk9_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_64, type, esk10_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_65, type, esk11_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_66, type, esk12_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_67, type, esk13_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(transitive_closure, axiom, ((tc)=(^[X1:$i > $i > $o, X3:$i, X4:$i]:(![X2:$i > $i > $o]:((((((trans @ X2))&((subrel @ X1 @ X2))))=>((X2 @ X3 @ X4))))))), file('/export/starexec/sandbox/tmp/tmp.CUz68hE36u/E---3.1_112673.p', transitive_closure)).
% 0.21/0.27 thf(transitive, axiom, ((trans)=(^[X1:$i > $i > $o]:(![X3:$i, X4:$i, X6:$i]:((((((X1 @ X3 @ X4))&((X1 @ X4 @ X6))))=>((X1 @ X3 @ X6))))))), file('/export/starexec/sandbox/tmp/tmp.CUz68hE36u/E---3.1_112673.p', transitive)).
% 0.21/0.27 thf(subrel, axiom, ((subrel)=(^[X1:$i > $i > $o, X2:$i > $i > $o]:(![X3:$i, X4:$i]:((((X1 @ X3 @ X4))=>((X2 @ X3 @ X4))))))), file('/export/starexec/sandbox/tmp/tmp.CUz68hE36u/E---3.1_112673.p', subrel)).
% 0.21/0.27 thf(transitive_closure_is_transitive3, conjecture, ![X1:$i > $i > $o, X3:$i, X4:$i, X6:$i, X2:$i > $i > $o]:((((((trans @ X2)&(subrel @ X1 @ X2))&(tc @ X1 @ X3 @ X4))&(tc @ X1 @ X4 @ X6))=>(X2 @ X3 @ X6))), file('/export/starexec/sandbox/tmp/tmp.CUz68hE36u/E---3.1_112673.p', transitive_closure_is_transitive3)).
% 0.21/0.27 thf(c_0_4, plain, ((tc)=(^[Z0:$i > $i > $o, Z1:$i, Z2:$i]:(![X2:$i > $i > $o]:((((((![X14:$i, X15:$i, X16:$i]:((((((X2 @ X14 @ X15))&((X2 @ X15 @ X16))))=>((X2 @ X14 @ X16))))))&((![X17:$i, X18:$i]:((((Z0 @ X17 @ X18))=>((X2 @ X17 @ X18))))))))=>((X2 @ Z1 @ Z2))))))), inference(fof_simplification,[status(thm)],[transitive_closure])).
% 0.21/0.27 thf(c_0_5, plain, ((trans)=(^[Z0:$i > $i > $o]:(![X3:$i, X4:$i, X6:$i]:((((((Z0 @ X3 @ X4))&((Z0 @ X4 @ X6))))=>((Z0 @ X3 @ X6))))))), inference(fof_simplification,[status(thm)],[transitive])).
% 0.21/0.27 thf(c_0_6, plain, ((subrel)=(^[Z0:$i > $i > $o, Z1:$i > $i > $o]:(![X3:$i, X4:$i]:((((Z0 @ X3 @ X4))=>((Z1 @ X3 @ X4))))))), inference(fof_simplification,[status(thm)],[subrel])).
% 0.21/0.27 thf(c_0_7, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X3:$i, X4:$i, X6:$i]:(((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)<=>(((![X19:$i, X20:$i, X21:$i]:((((X2 @ X19 @ X20)&(X2 @ X20 @ X21))=>(X2 @ X19 @ X21)))&![X22:$i, X23:$i]:(((X1 @ X22 @ X23)=>(X2 @ X22 @ X23))))&![X24:$i > $i > $o]:(((![X25:$i, X26:$i, X27:$i]:((((X24 @ X25 @ X26)&(X24 @ X26 @ X27))=>(X24 @ X25 @ X27)))&![X28:$i, X29:$i]:(((X1 @ X28 @ X29)=>(X24 @ X28 @ X29))))=>(X24 @ X3 @ X4))))&![X30:$i > $i > $o]:(((![X31:$i, X32:$i, X33:$i]:((((X30 @ X31 @ X32)&(X30 @ X32 @ X33))=>(X30 @ X31 @ X33)))&![X34:$i, X35:$i]:(((X1 @ X34 @ X35)=>(X30 @ X34 @ X35))))=>(X30 @ X4 @ X6)))))), introduced(definition)).
% 0.21/0.27 thf(c_0_8, negated_conjecture, ~(![X1:$i > $i > $o, X3:$i, X4:$i, X6:$i, X2:$i > $i > $o]:((((((trans @ X2)&(subrel @ X1 @ X2))&(tc @ X1 @ X3 @ X4))&(tc @ X1 @ X4 @ X6))=>(X2 @ X3 @ X6)))), inference(assume_negation,[status(cth)],[transitive_closure_is_transitive3])).
% 0.21/0.27 thf(c_0_9, plain, ((tc)=(^[Z0:$i > $i > $o, Z1:$i, Z2:$i]:(![X2:$i > $i > $o]:((((((![X14:$i, X15:$i, X16:$i]:((((((X2 @ X14 @ X15))&((X2 @ X15 @ X16))))=>((X2 @ X14 @ X16))))))&((![X17:$i, X18:$i]:((((Z0 @ X17 @ X18))=>((X2 @ X17 @ X18))))))))=>((X2 @ Z1 @ Z2))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_4, c_0_5]), c_0_6])).
% 0.21/0.27 thf(c_0_10, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X3:$i, X4:$i, X6:$i]:(((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)=>(((![X19:$i, X20:$i, X21:$i]:((((X2 @ X19 @ X20)&(X2 @ X20 @ X21))=>(X2 @ X19 @ X21)))&![X22:$i, X23:$i]:(((X1 @ X22 @ X23)=>(X2 @ X22 @ X23))))&![X24:$i > $i > $o]:(((![X25:$i, X26:$i, X27:$i]:((((X24 @ X25 @ X26)&(X24 @ X26 @ X27))=>(X24 @ X25 @ X27)))&![X28:$i, X29:$i]:(((X1 @ X28 @ X29)=>(X24 @ X28 @ X29))))=>(X24 @ X3 @ X4))))&![X30:$i > $i > $o]:(((![X31:$i, X32:$i, X33:$i]:((((X30 @ X31 @ X32)&(X30 @ X32 @ X33))=>(X30 @ X31 @ X33)))&![X34:$i, X35:$i]:(((X1 @ X34 @ X35)=>(X30 @ X34 @ X35))))=>(X30 @ X4 @ X6)))))), inference(split_equiv,[status(thm)],[c_0_7])).
% 0.21/0.27 thf(c_0_11, negated_conjecture, ~(![X1:$i > $i > $o, X3:$i, X4:$i, X6:$i, X2:$i > $i > $o]:(((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)=>(X2 @ X3 @ X6)))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_8, c_0_5]), c_0_6]), c_0_9]), c_0_7])).
% 0.21/0.27 thf(c_0_12, plain, ![X41:$i > $i > $o, X42:$i > $i > $o, X43:$i, X44:$i, X45:$i, X46:$i, X47:$i, X48:$i, X49:$i, X50:$i, X51:$i > $i > $o, X57:$i > $i > $o]:(((((~(X42 @ X46 @ X47)|~(X42 @ X47 @ X48)|(X42 @ X46 @ X48)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X41 @ X49 @ X50)|(X42 @ X49 @ X50)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42)))&(((((X41 @ (esk7_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk8_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ (esk4_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk5_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ X43 @ X44)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X51 @ (esk7_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk8_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ (esk4_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk5_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ X43 @ X44)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42)))&(((X41 @ (esk7_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk8_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ (esk5_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk6_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ X43 @ X44)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X51 @ (esk7_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk8_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ (esk5_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk6_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ X43 @ X44)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))))&(((X41 @ (esk7_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk8_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|~(X51 @ (esk4_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk6_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ X43 @ X44)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X51 @ (esk7_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk8_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|~(X51 @ (esk4_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51) @ (esk6_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X51))|(X51 @ X43 @ X44)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42)))))&(((((X41 @ (esk12_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk13_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ (esk9_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk10_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ X44 @ X45)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X57 @ (esk12_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk13_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ (esk9_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk10_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ X44 @ X45)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42)))&(((X41 @ (esk12_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk13_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ (esk10_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk11_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ X44 @ X45)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X57 @ (esk12_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk13_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ (esk10_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk11_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ X44 @ X45)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))))&(((X41 @ (esk12_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk13_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|~(X57 @ (esk9_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk11_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ X44 @ X45)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42))&(~(X57 @ (esk12_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk13_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|~(X57 @ (esk9_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57) @ (esk11_6 @ X41 @ X42 @ X43 @ X44 @ X45 @ X57))|(X57 @ X44 @ X45)|~(epred1_5 @ X45 @ X44 @ X43 @ X41 @ X42)))))), 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_10])])])])])])).
% 0.21/0.27 thf(c_0_13, negated_conjecture, ((epred1_5 @ esk3_0 @ esk2_0 @ esk1_0 @ epred2_0 @ epred3_0)&~(epred3_0 @ esk1_0 @ esk3_0)), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])])).
% 0.21/0.27 thf(c_0_14, plain, ![X4:$i, X3:$i, X10:$i, X6:$i, X12:$i, X11:$i, X2:$i > $i > $o, X1:$i > $i > $o]:(((X1 @ X3 @ X6)|~((X1 @ X3 @ X4))|~((X1 @ X4 @ X6))|~((epred1_5 @ X10 @ X11 @ X12 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_15, negated_conjecture, (epred1_5 @ esk3_0 @ esk2_0 @ esk1_0 @ epred2_0 @ epred3_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.21/0.27 thf(c_0_16, plain, ![X1:$i > $i > $o, X9:$i > $i > $o, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((X1 @ (esk12_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk13_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ (esk10_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk11_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ X4 @ X6)|~((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_17, negated_conjecture, ![X3:$i, X4:$i, X6:$i]:(((epred3_0 @ X3 @ X4)|~((epred3_0 @ X6 @ X4))|~((epred3_0 @ X3 @ X6)))), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 0.21/0.27 thf(c_0_18, negated_conjecture, ![X1:$i > $i > $o]:(((epred2_0 @ (esk12_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk13_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ (esk10_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk11_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_16, c_0_15])).
% 0.21/0.27 thf(c_0_19, plain, ![X1:$i > $i > $o, X9:$i > $i > $o, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((X1 @ (esk12_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk13_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ (esk9_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk10_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ X4 @ X6)|~((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_20, plain, ![X1:$i > $i > $o, X9:$i > $i > $o, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((X1 @ (esk7_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk8_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ (esk5_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk6_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ X3 @ X4)|~((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_21, negated_conjecture, ![X3:$i]:(((epred2_0 @ (esk12_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk13_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ X3 @ (esk11_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk2_0 @ esk3_0)|~((epred3_0 @ X3 @ (esk10_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))))), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.21/0.27 thf(c_0_22, negated_conjecture, ![X1:$i > $i > $o]:(((epred2_0 @ (esk12_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk13_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ (esk9_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk10_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ esk2_0 @ esk3_0))), inference(spm,[status(thm)],[c_0_19, c_0_15])).
% 0.21/0.27 thf(c_0_23, negated_conjecture, ![X1:$i > $i > $o]:(((epred2_0 @ (esk7_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk8_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ (esk5_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk6_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_20, c_0_15])).
% 0.21/0.27 thf(c_0_24, plain, ![X1:$i > $i > $o, X9:$i > $i > $o, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((X1 @ (esk7_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk8_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ (esk4_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk5_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ X3 @ X4)|~((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_25, plain, ![X1:$i > $i > $o, X3:$i, X6:$i, X11:$i, X10:$i, X4:$i, X2:$i > $i > $o]:(((X2 @ X3 @ X4)|~((X1 @ X3 @ X4))|~((epred1_5 @ X6 @ X10 @ X11 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_26, plain, ![X1:$i > $i > $o, X9:$i > $i > $o, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((X1 @ (esk12_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk13_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ X4 @ X6)|~((X9 @ (esk9_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk11_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9)))|~((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_27, negated_conjecture, ((epred3_0 @ (esk9_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk11_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred2_0 @ (esk12_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk13_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk2_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.21/0.27 thf(c_0_28, negated_conjecture, ![X3:$i]:(((epred2_0 @ (esk7_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk8_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ X3 @ (esk6_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk1_0 @ esk2_0)|~((epred3_0 @ X3 @ (esk5_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))))), inference(spm,[status(thm)],[c_0_17, c_0_23])).
% 0.21/0.27 thf(c_0_29, negated_conjecture, ![X1:$i > $i > $o]:(((epred2_0 @ (esk7_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk8_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ (esk4_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1) @ (esk5_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ X1))|(X1 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_24, c_0_15])).
% 0.21/0.27 thf(c_0_30, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X4:$i, X6:$i, X3:$i, X9:$i > $i > $o]:(((X1 @ (esk10_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk11_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1))|(X1 @ X4 @ X6)|~((X1 @ (esk12_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk13_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((epred1_5 @ X6 @ X4 @ X3 @ X2 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_31, negated_conjecture, ![X3:$i, X4:$i]:(((epred3_0 @ X3 @ X4)|~((epred2_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_25, c_0_15])).
% 0.21/0.27 thf(c_0_32, negated_conjecture, ((epred2_0 @ (esk12_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk13_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk2_0 @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_15])])).
% 0.21/0.27 thf(c_0_33, plain, ![X1:$i > $i > $o, X9:$i > $i > $o, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((X1 @ (esk7_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk8_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9))|(X9 @ X3 @ X4)|~((X9 @ (esk4_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9) @ (esk6_6 @ X1 @ X2 @ X3 @ X4 @ X6 @ X9)))|~((epred1_5 @ X6 @ X4 @ X3 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_34, negated_conjecture, ((epred3_0 @ (esk4_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk6_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred2_0 @ (esk7_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk8_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.21/0.27 thf(c_0_35, negated_conjecture, ![X1:$i > $i > $o, X10:$i, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((epred3_0 @ X3 @ (esk11_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0))|(epred3_0 @ X6 @ X10)|~((epred3_0 @ (esk12_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0) @ (esk13_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0)))|~((epred3_0 @ X3 @ (esk10_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0)))|~((epred1_5 @ X10 @ X6 @ X4 @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_17, c_0_30])).
% 0.21/0.27 thf(c_0_36, negated_conjecture, ((epred3_0 @ (esk12_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk13_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk2_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 0.21/0.27 thf(c_0_37, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X4:$i, X6:$i, X3:$i, X9:$i > $i > $o]:(((X1 @ (esk5_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk6_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1))|(X1 @ X3 @ X4)|~((X1 @ (esk7_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk8_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((epred1_5 @ X6 @ X4 @ X3 @ X2 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_38, negated_conjecture, ((epred2_0 @ (esk7_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk8_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk1_0 @ esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_34]), c_0_15])])).
% 0.21/0.27 thf(c_0_39, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X4:$i, X6:$i, X3:$i, X9:$i > $i > $o]:(((X1 @ X4 @ X6)|~((X1 @ (esk12_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk13_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((X1 @ (esk9_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk11_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((epred1_5 @ X6 @ X4 @ X3 @ X2 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_40, negated_conjecture, ![X3:$i]:(((epred3_0 @ X3 @ (esk11_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk2_0 @ esk3_0)|~((epred3_0 @ X3 @ (esk10_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_15])])).
% 0.21/0.27 thf(c_0_41, negated_conjecture, ![X1:$i > $i > $o, X10:$i, X6:$i, X4:$i, X3:$i, X2:$i > $i > $o]:(((epred3_0 @ X3 @ (esk6_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0))|(epred3_0 @ X4 @ X6)|~((epred3_0 @ (esk7_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0) @ (esk8_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0)))|~((epred3_0 @ X3 @ (esk5_6 @ X1 @ X2 @ X4 @ X6 @ X10 @ epred3_0)))|~((epred1_5 @ X10 @ X6 @ X4 @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_17, c_0_37])).
% 0.21/0.27 thf(c_0_42, negated_conjecture, ((epred3_0 @ (esk7_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk8_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_31, c_0_38])).
% 0.21/0.27 thf(c_0_43, plain, ((epred3_0 @ esk2_0 @ esk3_0)|~((epred3_0 @ (esk9_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk10_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_15])]), c_0_36])).
% 0.21/0.27 thf(c_0_44, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X4:$i, X6:$i, X3:$i, X9:$i > $i > $o]:(((X1 @ (esk9_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk10_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1))|(X1 @ X4 @ X6)|~((X1 @ (esk12_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk13_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((epred1_5 @ X6 @ X4 @ X3 @ X2 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_45, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X4:$i, X6:$i, X3:$i, X9:$i > $i > $o]:(((X1 @ X3 @ X4)|~((X1 @ (esk7_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk8_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((X1 @ (esk4_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk6_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((epred1_5 @ X6 @ X4 @ X3 @ X2 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_46, negated_conjecture, ![X3:$i]:(((epred3_0 @ X3 @ (esk6_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))|(epred3_0 @ esk1_0 @ esk2_0)|~((epred3_0 @ X3 @ (esk5_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_15])])).
% 0.21/0.27 thf(c_0_47, plain, (epred3_0 @ esk2_0 @ esk3_0), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_15])]), c_0_36])).
% 0.21/0.27 thf(c_0_48, plain, ((epred3_0 @ esk1_0 @ esk2_0)|~((epred3_0 @ (esk4_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0) @ (esk5_6 @ epred2_0 @ epred3_0 @ esk1_0 @ esk2_0 @ esk3_0 @ epred3_0)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_46]), c_0_15])]), c_0_42])).
% 0.21/0.27 thf(c_0_49, plain, ![X1:$i > $i > $o, X2:$i > $i > $o, X4:$i, X6:$i, X3:$i, X9:$i > $i > $o]:(((X1 @ (esk4_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk5_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1))|(X1 @ X3 @ X4)|~((X1 @ (esk7_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1) @ (esk8_6 @ X2 @ X9 @ X3 @ X4 @ X6 @ X1)))|~((epred1_5 @ X6 @ X4 @ X3 @ X2 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.21/0.27 thf(c_0_50, negated_conjecture, ![X3:$i]:(((epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk2_0)))), inference(spm,[status(thm)],[c_0_17, c_0_47])).
% 0.21/0.27 thf(c_0_51, plain, (epred3_0 @ esk1_0 @ esk2_0), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_15])]), c_0_42])).
% 0.21/0.27 thf(c_0_52, negated_conjecture, ~((epred3_0 @ esk1_0 @ esk3_0)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.21/0.27 thf(c_0_53, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_52]), ['proof']).
% 0.21/0.27 % SZS output end CNFRefutation
% 0.21/0.27 % Parsed axioms : 59
% 0.21/0.27 % Removed by relevancy pruning/SinE : 55
% 0.21/0.27 % Initial clauses : 16
% 0.21/0.27 % Removed in clause preprocessing : 0
% 0.21/0.27 % Initial clauses in saturation : 16
% 0.21/0.27 % Processed clauses : 76
% 0.21/0.27 % ...of these trivial : 0
% 0.21/0.27 % ...subsumed : 3
% 0.21/0.27 % ...remaining for further processing : 73
% 0.21/0.27 % Other redundant clauses eliminated : 0
% 0.21/0.27 % Clauses deleted for lack of memory : 0
% 0.21/0.27 % Backward-subsumed : 8
% 0.21/0.27 % Backward-rewritten : 20
% 0.21/0.27 % Generated clauses : 79
% 0.21/0.27 % ...of the previous two non-redundant : 76
% 0.21/0.27 % ...aggressively subsumed : 0
% 0.21/0.27 % Contextual simplify-reflections : 4
% 0.21/0.27 % Paramodulations : 79
% 0.21/0.27 % Factorizations : 0
% 0.21/0.27 % NegExts : 0
% 0.21/0.27 % Equation resolutions : 0
% 0.21/0.27 % Disequality decompositions : 0
% 0.21/0.27 % Total rewrite steps : 40
% 0.21/0.27 % ...of those cached : 37
% 0.21/0.27 % Propositional unsat checks : 0
% 0.21/0.27 % Propositional check models : 0
% 0.21/0.27 % Propositional check unsatisfiable : 0
% 0.21/0.27 % Propositional clauses : 0
% 0.21/0.27 % Propositional clauses after purity: 0
% 0.21/0.27 % Propositional unsat core size : 0
% 0.21/0.27 % Propositional preprocessing time : 0.000
% 0.21/0.27 % Propositional encoding time : 0.000
% 0.21/0.27 % Propositional solver time : 0.000
% 0.21/0.27 % Success case prop preproc time : 0.000
% 0.21/0.27 % Success case prop encoding time : 0.000
% 0.21/0.27 % Success case prop solver time : 0.000
% 0.21/0.27 % Current number of processed clauses : 45
% 0.21/0.27 % Positive orientable unit clauses : 3
% 0.21/0.27 % Positive unorientable unit clauses: 0
% 0.21/0.27 % Negative unit clauses : 1
% 0.21/0.27 % Non-unit-clauses : 41
% 0.21/0.27 % Current number of unprocessed clauses: 10
% 0.21/0.27 % ...number of literals in the above : 39
% 0.21/0.27 % Current number of archived formulas : 0
% 0.21/0.27 % Current number of archived clauses : 28
% 0.21/0.27 % Clause-clause subsumption calls (NU) : 1165
% 0.21/0.27 % Rec. Clause-clause subsumption calls : 585
% 0.21/0.27 % Non-unit clause-clause subsumptions : 15
% 0.21/0.27 % Unit Clause-clause subsumption calls : 83
% 0.21/0.27 % Rewrite failures with RHS unbound : 0
% 0.21/0.27 % BW rewrite match attempts : 2
% 0.21/0.27 % BW rewrite match successes : 2
% 0.21/0.27 % Condensation attempts : 0
% 0.21/0.27 % Condensation successes : 0
% 0.21/0.27 % Termbank termtop insertions : 6224
% 0.21/0.27 % Search garbage collected termcells : 818
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.010 s
% 0.21/0.27 % System time : 0.002 s
% 0.21/0.27 % Total time : 0.012 s
% 0.21/0.27 % Maximum resident set size: 3688 pages
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.012 s
% 0.21/0.27 % System time : 0.007 s
% 0.21/0.27 % Total time : 0.019 s
% 0.21/0.27 % Maximum resident set size: 4864 pages
% 0.21/0.27 % E exiting
%------------------------------------------------------------------------------