%------------------------------------------------------------------------------
% File : E-SAT---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 : n003.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:26:05 AM UTC 2026
% Result : Theorem 0.21s 0.26s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU463^1 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n003.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 13:43:43 UTC 2026
% 0.08/0.17 % 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.23 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.or3lB4Q9vG/E---3.1_2518671.p
% 0.21/0.26 % Version: 3.5.1-ho
% 0.21/0.26 % Preprocessing class: HSMSSMSSMLSNHSA.
% 0.21/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.26 % Starting sh5l with 300s (1) cores
% 0.21/0.26 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.26 % Starting new_bool_2 with 300s (1) cores
% 0.21/0.26 % sh5l with pid 2518685 completed with status 0
% 0.21/0.26 % Result found by sh5l
% 0.21/0.26 % Preprocessing class: HSMSSMSSMLSNHSA.
% 0.21/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.26 % Starting sh5l with 300s (1) cores
% 0.21/0.26 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 0.21/0.26 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.21/0.26 % Search class: HGUNF-FFMF33-SHSSMMBN
% 0.21/0.26 % partial match(2): HGUNS-FFMF32-SHSSMMBN
% 0.21/0.26 % Scheduled 6 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.26 % Starting SubtermCWHack with 31s (1) cores
% 0.21/0.26 % SubtermCWHack with pid 2518691 completed with status 0
% 0.21/0.26 % Result found by SubtermCWHack
% 0.21/0.26 % Preprocessing class: HSMSSMSSMLSNHSA.
% 0.21/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.26 % Starting sh5l with 300s (1) cores
% 0.21/0.26 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 0.21/0.26 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.21/0.26 % Search class: HGUNF-FFMF33-SHSSMMBN
% 0.21/0.26 % partial match(2): HGUNS-FFMF32-SHSSMMBN
% 0.21/0.26 % Scheduled 6 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.26 % Starting SubtermCWHack with 31s (1) cores
% 0.21/0.26 % Preprocessing time : 0.001 s
% 0.21/0.26
% 0.21/0.26 % Proof found!
% 0.21/0.26 % SZS status Theorem
% 0.21/0.26 % SZS output start CNFRefutation
% 0.21/0.26 thf(decl_23, type, subrel: ($i > $i > $o) > ($i > $i > $o) > $o).
% 0.21/0.26 thf(decl_35, type, trans: ($i > $i > $o) > $o).
% 0.21/0.26 thf(decl_36, type, tc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.26 thf(decl_52, type, epred1_5: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $o).
% 0.21/0.26 thf(decl_53, type, epred2_0: $i > $i > $o).
% 0.21/0.26 thf(decl_54, type, esk1_0: $i).
% 0.21/0.26 thf(decl_55, type, esk2_0: $i).
% 0.21/0.26 thf(decl_56, type, esk3_0: $i).
% 0.21/0.26 thf(decl_57, type, epred3_0: $i > $i > $o).
% 0.21/0.26 thf(decl_58, type, esk4_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_59, type, esk5_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_60, type, esk6_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_61, type, esk7_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_62, type, esk8_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_63, type, esk9_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_64, type, esk10_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_65, type, esk11_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_66, type, esk12_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 thf(decl_67, type, esk13_6: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.26 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.or3lB4Q9vG/E---3.1_2518671.p', transitive_closure)).
% 0.21/0.26 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.or3lB4Q9vG/E---3.1_2518671.p', transitive)).
% 0.21/0.26 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.or3lB4Q9vG/E---3.1_2518671.p', subrel)).
% 0.21/0.26 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.or3lB4Q9vG/E---3.1_2518671.p', transitive_closure_is_transitive3)).
% 0.21/0.26 thf(c_0_4, plain, ((tc)=(^[Z0:$i > $i > $o, Z1:$i, Z2:$i]:(![X2:$i > $i > $o]:((((((![X20:$i, X21:$i, X22:$i]:((((((X2 @ X20 @ X21))&((X2 @ X21 @ X22))))=>((X2 @ X20 @ X22))))))&((![X23:$i, X24:$i]:((((Z0 @ X23 @ X24))=>((X2 @ X23 @ X24))))))))=>((X2 @ Z1 @ Z2))))))), inference(fof_simplification,[status(thm)],[transitive_closure])).
% 0.21/0.26 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.26 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.26 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)<=>(((![X162:$i, X163:$i, X164:$i]:((((X2 @ X162 @ X163)&(X2 @ X163 @ X164))=>(X2 @ X162 @ X164)))&![X165:$i, X166:$i]:(((X1 @ X165 @ X166)=>(X2 @ X165 @ X166))))&![X167:$i > $i > $o]:(((![X168:$i, X169:$i, X170:$i]:((((X167 @ X168 @ X169)&(X167 @ X169 @ X170))=>(X167 @ X168 @ X170)))&![X171:$i, X172:$i]:(((X1 @ X171 @ X172)=>(X167 @ X171 @ X172))))=>(X167 @ X3 @ X4))))&![X173:$i > $i > $o]:(((![X174:$i, X175:$i, X176:$i]:((((X173 @ X174 @ X175)&(X173 @ X175 @ X176))=>(X173 @ X174 @ X176)))&![X177:$i, X178:$i]:(((X1 @ X177 @ X178)=>(X173 @ X177 @ X178))))=>(X173 @ X4 @ X6)))))), introduced(definition)).
% 0.21/0.26 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.26 thf(c_0_9, plain, ((tc)=(^[Z0:$i > $i > $o, Z1:$i, Z2:$i]:(![X2:$i > $i > $o]:((((((![X20:$i, X21:$i, X22:$i]:((((((X2 @ X20 @ X21))&((X2 @ X21 @ X22))))=>((X2 @ X20 @ X22))))))&((![X23:$i, X24:$i]:((((Z0 @ X23 @ X24))=>((X2 @ X23 @ X24))))))))=>((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.26 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)=>(((![X162:$i, X163:$i, X164:$i]:((((X2 @ X162 @ X163)&(X2 @ X163 @ X164))=>(X2 @ X162 @ X164)))&![X165:$i, X166:$i]:(((X1 @ X165 @ X166)=>(X2 @ X165 @ X166))))&![X167:$i > $i > $o]:(((![X168:$i, X169:$i, X170:$i]:((((X167 @ X168 @ X169)&(X167 @ X169 @ X170))=>(X167 @ X168 @ X170)))&![X171:$i, X172:$i]:(((X1 @ X171 @ X172)=>(X167 @ X171 @ X172))))=>(X167 @ X3 @ X4))))&![X173:$i > $i > $o]:(((![X174:$i, X175:$i, X176:$i]:((((X173 @ X174 @ X175)&(X173 @ X175 @ X176))=>(X173 @ X174 @ X176)))&![X177:$i, X178:$i]:(((X1 @ X177 @ X178)=>(X173 @ X177 @ X178))))=>(X173 @ X4 @ X6)))))), inference(split_equiv,[status(thm)],[c_0_7])).
% 0.21/0.26 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.26 thf(c_0_12, plain, ![X184:$i > $i > $o, X185:$i > $i > $o, X186:$i, X187:$i, X188:$i, X189:$i, X190:$i, X191:$i, X192:$i, X193:$i, X194:$i > $i > $o, X200:$i > $i > $o]:(((((~(X185 @ X189 @ X190)|~(X185 @ X190 @ X191)|(X185 @ X189 @ X191)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X184 @ X192 @ X193)|(X185 @ X192 @ X193)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185)))&(((((X184 @ (esk7_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk8_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ (esk4_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk5_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ X186 @ X187)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X194 @ (esk7_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk8_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ (esk4_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk5_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ X186 @ X187)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185)))&(((X184 @ (esk7_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk8_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ (esk5_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk6_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ X186 @ X187)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X194 @ (esk7_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk8_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ (esk5_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk6_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ X186 @ X187)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))))&(((X184 @ (esk7_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk8_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|~(X194 @ (esk4_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk6_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ X186 @ X187)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X194 @ (esk7_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk8_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|~(X194 @ (esk4_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194) @ (esk6_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X194))|(X194 @ X186 @ X187)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185)))))&(((((X184 @ (esk12_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk13_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ (esk9_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk10_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ X187 @ X188)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X200 @ (esk12_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk13_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ (esk9_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk10_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ X187 @ X188)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185)))&(((X184 @ (esk12_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk13_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ (esk10_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk11_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ X187 @ X188)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X200 @ (esk12_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk13_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ (esk10_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk11_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ X187 @ X188)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))))&(((X184 @ (esk12_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk13_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|~(X200 @ (esk9_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk11_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ X187 @ X188)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185))&(~(X200 @ (esk12_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk13_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|~(X200 @ (esk9_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200) @ (esk11_6 @ X184 @ X185 @ X186 @ X187 @ X188 @ X200))|(X200 @ X187 @ X188)|~(epred1_5 @ X188 @ X187 @ X186 @ X184 @ X185)))))), 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 : 35
% 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 : 7875
% 0.21/0.27 % Search garbage collected termcells : 1150
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.011 s
% 0.21/0.27 % System time : 0.002 s
% 0.21/0.27 % Total time : 0.013 s
% 0.21/0.27 % Maximum resident set size: 4200 pages
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.016 s
% 0.21/0.27 % System time : 0.004 s
% 0.21/0.27 % Total time : 0.020 s
% 0.21/0.27 % Maximum resident set size: 4864 pages
% 0.21/0.27 % E exiting
%------------------------------------------------------------------------------