%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SYO179^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:43:57 AM UTC 2026
% Result : Theorem 0.21s 0.28s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO179^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n016.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.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 16:42:04 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 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.iUA3cbwpfE/E---3.1_586557.p
% 0.21/0.28 % Version: 3.5.1-ho
% 0.21/0.28 % Preprocessing class: HSMSSMSSSSSNFFN.
% 0.21/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.28 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.28 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.28 % Starting full_lambda_5 with 300s (1) cores
% 0.21/0.28 % Starting new_ho_10_unif with 300s (1) cores
% 0.21/0.28 % full_lambda_5 with pid 586572 completed with status 0
% 0.21/0.28 % Result found by full_lambda_5
% 0.21/0.28 % Preprocessing class: HSMSSMSSSSSNFFN.
% 0.21/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.28 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.28 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.28 % Starting full_lambda_5 with 300s (1) cores
% 0.21/0.28 % (lift_lambdas = 1, lambda_to_forall = 0,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.28 % No SInE strategy applied
% 0.21/0.28 % Search class: HGHNF-FFSF00-SFFFFFNN
% 0.21/0.28 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.28 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.28 % SubtermCWHack with pid 586577 completed with status 0
% 0.21/0.28 % Result found by SubtermCWHack
% 0.21/0.28 % Preprocessing class: HSMSSMSSSSSNFFN.
% 0.21/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.28 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.28 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.28 % Starting full_lambda_5 with 300s (1) cores
% 0.21/0.28 % (lift_lambdas = 1, lambda_to_forall = 0,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.28 % No SInE strategy applied
% 0.21/0.28 % Search class: HGHNF-FFSF00-SFFFFFNN
% 0.21/0.28 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.28 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.28 % Preprocessing time : 0.001 s
% 0.21/0.28
% 0.21/0.28 % Proof found!
% 0.21/0.28 % SZS status Theorem
% 0.21/0.28 % SZS output start CNFRefutation
% 0.21/0.28 thf(decl_23, type, cG: $i > $i > $o).
% 0.21/0.28 thf(decl_24, type, cR: $i > $i > $o).
% 0.21/0.28 thf(decl_25, type, cF: $i).
% 0.21/0.28 thf(decl_26, type, cE: $i).
% 0.21/0.28 thf(decl_27, type, cD: $i).
% 0.21/0.28 thf(decl_28, type, cC: $i).
% 0.21/0.28 thf(decl_29, type, cB: $i).
% 0.21/0.28 thf(decl_30, type, cA: $i).
% 0.21/0.28 thf(decl_31, type, epred1_0: $o).
% 0.21/0.28 thf(cSIX_THEOREM_B, conjecture, (((((((((((((((((cR @ cA @ cB)|(cG @ cA @ cB))&((cR @ cA @ cC)|(cG @ cA @ cC)))&((cR @ cA @ cD)|(cG @ cA @ cD)))&((cR @ cA @ cE)|(cG @ cA @ cE)))&((cR @ cA @ cF)|(cG @ cA @ cF)))&((cR @ cB @ cC)|(cG @ cB @ cC)))&((cR @ cB @ cD)|(cG @ cB @ cD)))&((cR @ cB @ cE)|(cG @ cB @ cE)))&((cR @ cB @ cF)|(cG @ cB @ cF)))&((cR @ cC @ cD)|(cG @ cC @ cD)))&((cR @ cC @ cE)|(cG @ cC @ cE)))&((cR @ cC @ cF)|(cG @ cC @ cF)))&((cR @ cD @ cE)|(cG @ cD @ cE)))&((cR @ cD @ cF)|(cG @ cD @ cF)))&((cR @ cE @ cF)|(cG @ cE @ cF)))=>(?[X1:$i, X2:$i, X3:$i]:((((cR @ X1 @ X2)&(cR @ X1 @ X3))&(cR @ X2 @ X3)))|?[X1:$i, X2:$i, X3:$i]:((((cG @ X1 @ X2)&(cG @ X1 @ X3))&(cG @ X2 @ X3))))), file('/export/starexec/sandbox/tmp/tmp.iUA3cbwpfE/E---3.1_586557.p', cSIX_THEOREM_B)).
% 0.21/0.28 thf(c_0_1, plain, ((epred1_0)<=>((((((((((((((((cR @ cA @ cB)|(cG @ cA @ cB))&((cR @ cA @ cC)|(cG @ cA @ cC)))&((cR @ cA @ cD)|(cG @ cA @ cD)))&((cR @ cA @ cE)|(cG @ cA @ cE)))&((cR @ cA @ cF)|(cG @ cA @ cF)))&((cR @ cB @ cC)|(cG @ cB @ cC)))&((cR @ cB @ cD)|(cG @ cB @ cD)))&((cR @ cB @ cE)|(cG @ cB @ cE)))&((cR @ cB @ cF)|(cG @ cB @ cF)))&((cR @ cC @ cD)|(cG @ cC @ cD)))&((cR @ cC @ cE)|(cG @ cC @ cE)))&((cR @ cC @ cF)|(cG @ cC @ cF)))&((cR @ cD @ cE)|(cG @ cD @ cE)))&((cR @ cD @ cF)|(cG @ cD @ cF)))&((cR @ cE @ cF)|(cG @ cE @ cF)))), introduced(definition)).
% 0.21/0.28 thf(c_0_2, negated_conjecture, ~((((((((((((((((((cR @ cA @ cB)|(cG @ cA @ cB))&((cR @ cA @ cC)|(cG @ cA @ cC)))&((cR @ cA @ cD)|(cG @ cA @ cD)))&((cR @ cA @ cE)|(cG @ cA @ cE)))&((cR @ cA @ cF)|(cG @ cA @ cF)))&((cR @ cB @ cC)|(cG @ cB @ cC)))&((cR @ cB @ cD)|(cG @ cB @ cD)))&((cR @ cB @ cE)|(cG @ cB @ cE)))&((cR @ cB @ cF)|(cG @ cB @ cF)))&((cR @ cC @ cD)|(cG @ cC @ cD)))&((cR @ cC @ cE)|(cG @ cC @ cE)))&((cR @ cC @ cF)|(cG @ cC @ cF)))&((cR @ cD @ cE)|(cG @ cD @ cE)))&((cR @ cD @ cF)|(cG @ cD @ cF)))&((cR @ cE @ cF)|(cG @ cE @ cF)))=>(?[X1:$i, X2:$i, X3:$i]:((((cR @ X1 @ X2)&(cR @ X1 @ X3))&(cR @ X2 @ X3)))|?[X1:$i, X2:$i, X3:$i]:((((cG @ X1 @ X2)&(cG @ X1 @ X3))&(cG @ X2 @ X3)))))), inference(assume_negation,[status(cth)],[cSIX_THEOREM_B])).
% 0.21/0.28 thf(c_0_3, plain, ((epred1_0)=>((((((((((((((((cR @ cA @ cB)|(cG @ cA @ cB))&((cR @ cA @ cC)|(cG @ cA @ cC)))&((cR @ cA @ cD)|(cG @ cA @ cD)))&((cR @ cA @ cE)|(cG @ cA @ cE)))&((cR @ cA @ cF)|(cG @ cA @ cF)))&((cR @ cB @ cC)|(cG @ cB @ cC)))&((cR @ cB @ cD)|(cG @ cB @ cD)))&((cR @ cB @ cE)|(cG @ cB @ cE)))&((cR @ cB @ cF)|(cG @ cB @ cF)))&((cR @ cC @ cD)|(cG @ cC @ cD)))&((cR @ cC @ cE)|(cG @ cC @ cE)))&((cR @ cC @ cF)|(cG @ cC @ cF)))&((cR @ cD @ cE)|(cG @ cD @ cE)))&((cR @ cD @ cF)|(cG @ cD @ cF)))&((cR @ cE @ cF)|(cG @ cE @ cF)))), inference(split_equiv,[status(thm)],[c_0_1])).
% 0.21/0.28 thf(c_0_4, negated_conjecture, ~(((epred1_0)=>(?[X1:$i, X2:$i, X3:$i]:((((cR @ X1 @ X2)&(cR @ X1 @ X3))&(cR @ X2 @ X3)))|?[X1:$i, X2:$i, X3:$i]:((((cG @ X1 @ X2)&(cG @ X1 @ X3))&(cG @ X2 @ X3)))))), inference(apply_def,[status(thm)],[c_0_2, c_0_1])).
% 0.21/0.28 thf(c_0_5, plain, ((((((((((((((((cR @ cA @ cB)|(cG @ cA @ cB)|~(epred1_0))&((cR @ cA @ cC)|(cG @ cA @ cC)|~(epred1_0)))&((cR @ cA @ cD)|(cG @ cA @ cD)|~(epred1_0)))&((cR @ cA @ cE)|(cG @ cA @ cE)|~(epred1_0)))&((cR @ cA @ cF)|(cG @ cA @ cF)|~(epred1_0)))&((cR @ cB @ cC)|(cG @ cB @ cC)|~(epred1_0)))&((cR @ cB @ cD)|(cG @ cB @ cD)|~(epred1_0)))&((cR @ cB @ cE)|(cG @ cB @ cE)|~(epred1_0)))&((cR @ cB @ cF)|(cG @ cB @ cF)|~(epred1_0)))&((cR @ cC @ cD)|(cG @ cC @ cD)|~(epred1_0)))&((cR @ cC @ cE)|(cG @ cC @ cE)|~(epred1_0)))&((cR @ cC @ cF)|(cG @ cC @ cF)|~(epred1_0)))&((cR @ cD @ cE)|(cG @ cD @ cE)|~(epred1_0)))&((cR @ cD @ cF)|(cG @ cD @ cF)|~(epred1_0)))&((cR @ cE @ cF)|(cG @ cE @ cF)|~(epred1_0))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])).
% 0.21/0.28 thf(c_0_6, negated_conjecture, ![X10:$i, X11:$i, X12:$i, X13:$i, X14:$i, X15:$i]:(((epred1_0)&((~(cR @ X10 @ X11)|~(cR @ X10 @ X12)|~(cR @ X11 @ X12))&(~(cG @ X13 @ X14)|~(cG @ X13 @ X15)|~(cG @ X14 @ X15))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])).
% 0.21/0.28 thf(c_0_7, plain, ((cR @ cE @ cF)|(cG @ cE @ cF)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_8, negated_conjecture, (epred1_0), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.21/0.28 thf(c_0_9, negated_conjecture, ![X1:$i, X2:$i, X3:$i]:((~((cR @ X1 @ X2))|~((cR @ X1 @ X3))|~((cR @ X2 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.21/0.28 thf(c_0_10, plain, ((cR @ cE @ cF)|(cG @ cE @ cF)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_7, c_0_8])])).
% 0.21/0.28 thf(c_0_11, plain, ((cR @ cD @ cF)|(cG @ cD @ cF)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_12, plain, ((cR @ cD @ cE)|(cG @ cD @ cE)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_13, plain, ![X1:$i]:(((cG @ cE @ cF)|~((cR @ X1 @ cF))|~((cR @ X1 @ cE)))), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 0.21/0.28 thf(c_0_14, plain, ((cR @ cD @ cF)|(cG @ cD @ cF)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_8])])).
% 0.21/0.28 thf(c_0_15, plain, ((cR @ cD @ cE)|(cG @ cD @ cE)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_8])])).
% 0.21/0.28 thf(c_0_16, plain, ((cR @ cB @ cD)|(cG @ cB @ cD)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_17, plain, ((cR @ cB @ cF)|(cG @ cB @ cF)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_18, plain, ((cR @ cC @ cD)|(cG @ cC @ cD)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_19, plain, ((cR @ cC @ cF)|(cG @ cC @ cF)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_20, plain, ((cG @ cD @ cF)|(cG @ cE @ cF)|~((cR @ cD @ cE))), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.21/0.28 thf(c_0_21, plain, ![X1:$i]:(((cG @ cD @ cE)|~((cR @ X1 @ cE))|~((cR @ X1 @ cD)))), inference(spm,[status(thm)],[c_0_9, c_0_15])).
% 0.21/0.28 thf(c_0_22, plain, ((cR @ cB @ cD)|(cG @ cB @ cD)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_8])])).
% 0.21/0.28 thf(c_0_23, plain, ((cR @ cB @ cE)|(cG @ cB @ cE)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_24, plain, ((cR @ cB @ cF)|(cG @ cB @ cF)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_8])])).
% 0.21/0.28 thf(c_0_25, plain, ((cR @ cB @ cC)|(cG @ cB @ cC)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_26, plain, ((cR @ cA @ cD)|(cG @ cA @ cD)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_27, plain, ((cR @ cA @ cF)|(cG @ cA @ cF)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_28, plain, ((cR @ cC @ cD)|(cG @ cC @ cD)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_8])])).
% 0.21/0.28 thf(c_0_29, plain, ((cR @ cC @ cE)|(cG @ cC @ cE)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_30, plain, ((cR @ cC @ cF)|(cG @ cC @ cF)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_8])])).
% 0.21/0.28 thf(c_0_31, negated_conjecture, ![X1:$i, X2:$i, X3:$i]:((~((cG @ X1 @ X2))|~((cG @ X1 @ X3))|~((cG @ X2 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.21/0.28 thf(c_0_32, plain, ((cG @ cD @ cE)|(cG @ cE @ cF)|(cG @ cD @ cF)), inference(spm,[status(thm)],[c_0_20, c_0_15])).
% 0.21/0.28 thf(c_0_33, plain, ((cG @ cB @ cD)|(cG @ cD @ cE)|~((cR @ cB @ cE))), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.21/0.28 thf(c_0_34, plain, ((cR @ cB @ cE)|(cG @ cB @ cE)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_8])])).
% 0.21/0.28 thf(c_0_35, plain, ((cG @ cB @ cF)|(cG @ cE @ cF)|~((cR @ cB @ cE))), inference(spm,[status(thm)],[c_0_13, c_0_24])).
% 0.21/0.28 thf(c_0_36, plain, ((cR @ cB @ cC)|(cG @ cB @ cC)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_8])])).
% 0.21/0.28 thf(c_0_37, plain, ((cR @ cA @ cB)|(cG @ cA @ cB)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_38, plain, ((cR @ cA @ cD)|(cG @ cA @ cD)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_8])])).
% 0.21/0.28 thf(c_0_39, plain, ((cR @ cA @ cE)|(cG @ cA @ cE)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_40, plain, ((cR @ cA @ cF)|(cG @ cA @ cF)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_8])])).
% 0.21/0.28 thf(c_0_41, plain, ((cG @ cC @ cD)|(cG @ cD @ cE)|~((cR @ cC @ cE))), inference(spm,[status(thm)],[c_0_21, c_0_28])).
% 0.21/0.28 thf(c_0_42, plain, ((cR @ cC @ cE)|(cG @ cC @ cE)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_8])])).
% 0.21/0.28 thf(c_0_43, plain, ((cG @ cC @ cF)|(cG @ cE @ cF)|~((cR @ cC @ cE))), inference(spm,[status(thm)],[c_0_13, c_0_30])).
% 0.21/0.28 thf(c_0_44, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|(cG @ cD @ cE)|~((cG @ X1 @ cF))|~((cG @ X1 @ cD)))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 0.21/0.28 thf(c_0_45, plain, ((cG @ cB @ cE)|(cG @ cD @ cE)|(cG @ cB @ cD)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.21/0.28 thf(c_0_46, plain, ((cG @ cB @ cE)|(cG @ cE @ cF)|(cG @ cB @ cF)), inference(spm,[status(thm)],[c_0_35, c_0_34])).
% 0.21/0.28 thf(c_0_47, plain, ![X1:$i]:(((cG @ cB @ cC)|~((cR @ X1 @ cC))|~((cR @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_9, c_0_36])).
% 0.21/0.28 thf(c_0_48, plain, ((cR @ cA @ cB)|(cG @ cA @ cB)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_8])])).
% 0.21/0.28 thf(c_0_49, plain, ((cR @ cA @ cC)|(cG @ cA @ cC)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_5])).
% 0.21/0.28 thf(c_0_50, plain, ((cG @ cA @ cD)|(cG @ cD @ cE)|~((cR @ cA @ cE))), inference(spm,[status(thm)],[c_0_21, c_0_38])).
% 0.21/0.28 thf(c_0_51, plain, ((cR @ cA @ cE)|(cG @ cA @ cE)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_8])])).
% 0.21/0.28 thf(c_0_52, plain, ((cG @ cA @ cF)|(cG @ cE @ cF)|~((cR @ cA @ cE))), inference(spm,[status(thm)],[c_0_13, c_0_40])).
% 0.21/0.28 thf(c_0_53, plain, ((cG @ cC @ cE)|(cG @ cD @ cE)|(cG @ cC @ cD)), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 0.21/0.28 thf(c_0_54, plain, ((cG @ cC @ cE)|(cG @ cE @ cF)|(cG @ cC @ cF)), inference(spm,[status(thm)],[c_0_43, c_0_42])).
% 0.21/0.28 thf(c_0_55, plain, ((cG @ cB @ cE)|(cG @ cD @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_46])).
% 0.21/0.28 thf(c_0_56, plain, ((cG @ cA @ cB)|(cG @ cB @ cC)|~((cR @ cA @ cC))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.21/0.28 thf(c_0_57, plain, ((cR @ cA @ cC)|(cG @ cA @ cC)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_8])])).
% 0.21/0.28 thf(c_0_58, plain, ((cG @ cA @ cE)|(cG @ cD @ cE)|(cG @ cA @ cD)), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 0.21/0.28 thf(c_0_59, plain, ((cG @ cA @ cE)|(cG @ cE @ cF)|(cG @ cA @ cF)), inference(spm,[status(thm)],[c_0_52, c_0_51])).
% 0.21/0.28 thf(c_0_60, plain, ![X1:$i]:(((cG @ cC @ cE)|~((cR @ X1 @ cE))|~((cR @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_9, c_0_42])).
% 0.21/0.28 thf(c_0_61, plain, ((cG @ cC @ cE)|(cG @ cD @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_53]), c_0_54])).
% 0.21/0.28 thf(c_0_62, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|(cG @ cD @ cE)|~((cG @ X1 @ cE))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_55])).
% 0.21/0.28 thf(c_0_63, plain, ((cG @ cA @ cC)|(cG @ cB @ cC)|(cG @ cA @ cB)), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 0.21/0.28 thf(c_0_64, plain, ((cG @ cA @ cE)|(cG @ cD @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_58]), c_0_59])).
% 0.21/0.28 thf(c_0_65, plain, ((cG @ cB @ cC)|(cG @ cC @ cE)|~((cR @ cB @ cE))), inference(spm,[status(thm)],[c_0_60, c_0_36])).
% 0.21/0.28 thf(c_0_66, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|(cG @ cD @ cE)|~((cG @ X1 @ cE))|~((cG @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_31, c_0_61])).
% 0.21/0.28 thf(c_0_67, plain, ((cG @ cB @ cC)|(cG @ cA @ cC)|(cG @ cD @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_64])).
% 0.21/0.28 thf(c_0_68, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|(cG @ cC @ cE)|~((cG @ X1 @ cF))|~((cG @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_31, c_0_54])).
% 0.21/0.28 thf(c_0_69, plain, ((cG @ cB @ cE)|(cG @ cC @ cE)|(cG @ cB @ cC)), inference(spm,[status(thm)],[c_0_65, c_0_34])).
% 0.21/0.28 thf(c_0_70, plain, ![X1:$i]:(((cG @ cB @ cD)|~((cR @ X1 @ cD))|~((cR @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_9, c_0_22])).
% 0.21/0.28 thf(c_0_71, plain, ((cG @ cA @ cC)|(cG @ cC @ cE)|~((cR @ cA @ cE))), inference(spm,[status(thm)],[c_0_60, c_0_57])).
% 0.21/0.28 thf(c_0_72, negated_conjecture, ((cG @ cB @ cC)|(cG @ cD @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_64])).
% 0.21/0.28 thf(c_0_73, plain, ((cG @ cB @ cE)|(cG @ cC @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_46])).
% 0.21/0.28 thf(c_0_74, plain, ((cG @ cA @ cB)|(cG @ cB @ cD)|~((cR @ cA @ cD))), inference(spm,[status(thm)],[c_0_70, c_0_48])).
% 0.21/0.28 thf(c_0_75, plain, ((cG @ cA @ cE)|(cG @ cC @ cE)|(cG @ cA @ cC)), inference(spm,[status(thm)],[c_0_71, c_0_51])).
% 0.21/0.28 thf(c_0_76, negated_conjecture, ((cG @ cD @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_72]), c_0_55])).
% 0.21/0.28 thf(c_0_77, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|(cG @ cC @ cE)|~((cG @ X1 @ cE))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_73])).
% 0.21/0.28 thf(c_0_78, plain, ((cG @ cA @ cD)|(cG @ cB @ cD)|(cG @ cA @ cB)), inference(spm,[status(thm)],[c_0_74, c_0_38])).
% 0.21/0.28 thf(c_0_79, plain, ((cG @ cA @ cE)|(cG @ cC @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_75]), c_0_59])).
% 0.21/0.28 thf(c_0_80, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|~((cG @ X1 @ cE))|~((cG @ X1 @ cD)))), inference(spm,[status(thm)],[c_0_31, c_0_76])).
% 0.21/0.28 thf(c_0_81, plain, ((cG @ cB @ cD)|(cG @ cA @ cD)|(cG @ cC @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_78]), c_0_79])).
% 0.21/0.28 thf(c_0_82, plain, ((cG @ cC @ cE)|(cG @ cB @ cD)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_81]), c_0_79])).
% 0.21/0.28 thf(c_0_83, plain, ![X1:$i]:(((cG @ cC @ cD)|~((cR @ X1 @ cD))|~((cR @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_9, c_0_28])).
% 0.21/0.28 thf(c_0_84, plain, ![X1:$i]:(((cG @ cB @ cE)|~((cR @ X1 @ cE))|~((cR @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_9, c_0_34])).
% 0.21/0.28 thf(c_0_85, negated_conjecture, ((cG @ cC @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_82]), c_0_73])).
% 0.21/0.28 thf(c_0_86, plain, ((cG @ cA @ cC)|(cG @ cC @ cD)|~((cR @ cA @ cD))), inference(spm,[status(thm)],[c_0_83, c_0_57])).
% 0.21/0.28 thf(c_0_87, plain, ((cG @ cA @ cB)|(cG @ cB @ cE)|~((cR @ cA @ cE))), inference(spm,[status(thm)],[c_0_84, c_0_48])).
% 0.21/0.28 thf(c_0_88, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|~((cG @ X1 @ cE))|~((cG @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_31, c_0_85])).
% 0.21/0.28 thf(c_0_89, plain, ((cG @ cA @ cD)|(cG @ cC @ cD)|(cG @ cA @ cC)), inference(spm,[status(thm)],[c_0_86, c_0_38])).
% 0.21/0.28 thf(c_0_90, negated_conjecture, ![X1:$i]:(((cG @ cE @ cF)|(cG @ cB @ cE)|~((cG @ X1 @ cF))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_46])).
% 0.21/0.28 thf(c_0_91, plain, ((cG @ cA @ cE)|(cG @ cB @ cE)|(cG @ cA @ cB)), inference(spm,[status(thm)],[c_0_87, c_0_51])).
% 0.21/0.28 thf(c_0_92, plain, ((cG @ cB @ cC)|(cG @ cC @ cD)|~((cR @ cB @ cD))), inference(spm,[status(thm)],[c_0_83, c_0_36])).
% 0.21/0.28 thf(c_0_93, plain, ((cG @ cC @ cD)|(cG @ cE @ cF)|~((cG @ cA @ cE))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_89]), c_0_80])).
% 0.21/0.28 thf(c_0_94, plain, ((cG @ cA @ cE)|(cG @ cB @ cE)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_91]), c_0_59])).
% 0.21/0.28 thf(c_0_95, plain, ![X1:$i]:(((cG @ cD @ cF)|~((cR @ X1 @ cF))|~((cR @ X1 @ cD)))), inference(spm,[status(thm)],[c_0_9, c_0_14])).
% 0.21/0.28 thf(c_0_96, plain, ((cG @ cB @ cD)|(cG @ cC @ cD)|(cG @ cB @ cC)), inference(spm,[status(thm)],[c_0_92, c_0_22])).
% 0.21/0.28 thf(c_0_97, plain, ((cG @ cB @ cE)|(cG @ cE @ cF)|(cG @ cC @ cD)), inference(spm,[status(thm)],[c_0_93, c_0_94])).
% 0.21/0.28 thf(c_0_98, plain, ((cG @ cC @ cD)|(cG @ cD @ cF)|~((cR @ cC @ cF))), inference(spm,[status(thm)],[c_0_95, c_0_28])).
% 0.21/0.28 thf(c_0_99, plain, ![X1:$i]:(((cG @ cC @ cF)|~((cR @ X1 @ cF))|~((cR @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_9, c_0_30])).
% 0.21/0.28 thf(c_0_100, plain, ((cG @ cC @ cD)|(cG @ cB @ cD)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_96]), c_0_97])).
% 0.21/0.28 thf(c_0_101, plain, ((cG @ cC @ cF)|(cG @ cD @ cF)|(cG @ cC @ cD)), inference(spm,[status(thm)],[c_0_98, c_0_30])).
% 0.21/0.28 thf(c_0_102, plain, ((cG @ cB @ cC)|(cG @ cC @ cF)|~((cR @ cB @ cF))), inference(spm,[status(thm)],[c_0_99, c_0_36])).
% 0.21/0.28 thf(c_0_103, plain, ((cG @ cB @ cD)|(cG @ cD @ cF)|~((cR @ cB @ cF))), inference(spm,[status(thm)],[c_0_95, c_0_22])).
% 0.21/0.28 thf(c_0_104, negated_conjecture, ((cG @ cC @ cD)|(cG @ cE @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_100]), c_0_97])).
% 0.21/0.28 thf(c_0_105, plain, ((cG @ cA @ cC)|(cG @ cC @ cF)|~((cR @ cA @ cF))), inference(spm,[status(thm)],[c_0_99, c_0_57])).
% 0.21/0.28 thf(c_0_106, plain, ((cG @ cA @ cD)|(cG @ cD @ cF)|~((cR @ cA @ cF))), inference(spm,[status(thm)],[c_0_95, c_0_38])).
% 0.21/0.28 thf(c_0_107, negated_conjecture, ![X1:$i]:(((cG @ cD @ cF)|(cG @ cC @ cF)|~((cG @ X1 @ cD))|~((cG @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_31, c_0_101])).
% 0.21/0.28 thf(c_0_108, plain, ((cG @ cB @ cF)|(cG @ cC @ cF)|(cG @ cB @ cC)), inference(spm,[status(thm)],[c_0_102, c_0_24])).
% 0.21/0.28 thf(c_0_109, plain, ((cG @ cB @ cF)|(cG @ cD @ cF)|(cG @ cB @ cD)), inference(spm,[status(thm)],[c_0_103, c_0_24])).
% 0.21/0.28 thf(c_0_110, negated_conjecture, ![X1:$i]:(((cG @ cD @ cE)|(cG @ cC @ cE)|~((cG @ X1 @ cD))|~((cG @ X1 @ cC)))), inference(spm,[status(thm)],[c_0_31, c_0_53])).
% 0.21/0.28 thf(c_0_111, plain, ![X1:$i]:(((cG @ cB @ cF)|~((cR @ X1 @ cF))|~((cR @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_9, c_0_24])).
% 0.21/0.28 thf(c_0_112, negated_conjecture, (cG @ cE @ cF), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_104]), c_0_85])).
% 0.21/0.28 thf(c_0_113, plain, ((cG @ cA @ cF)|(cG @ cC @ cF)|(cG @ cA @ cC)), inference(spm,[status(thm)],[c_0_105, c_0_40])).
% 0.21/0.28 thf(c_0_114, plain, ((cG @ cA @ cF)|(cG @ cD @ cF)|(cG @ cA @ cD)), inference(spm,[status(thm)],[c_0_106, c_0_40])).
% 0.21/0.28 thf(c_0_115, plain, ((cG @ cB @ cF)|(cG @ cC @ cF)|(cG @ cD @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_108]), c_0_109])).
% 0.21/0.28 thf(c_0_116, plain, ((cG @ cB @ cE)|(cG @ cC @ cE)|(cG @ cD @ cE)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_69]), c_0_45])).
% 0.21/0.28 thf(c_0_117, plain, ((cG @ cA @ cB)|(cG @ cB @ cF)|~((cR @ cA @ cF))), inference(spm,[status(thm)],[c_0_111, c_0_48])).
% 0.21/0.28 thf(c_0_118, negated_conjecture, ![X1:$i]:((~((cG @ X1 @ cF))|~((cG @ X1 @ cE)))), inference(spm,[status(thm)],[c_0_31, c_0_112])).
% 0.21/0.28 thf(c_0_119, plain, ((cG @ cA @ cF)|(cG @ cC @ cF)|(cG @ cD @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_113]), c_0_114])).
% 0.21/0.28 thf(c_0_120, negated_conjecture, ![X1:$i]:(((cG @ cD @ cF)|(cG @ cC @ cF)|~((cG @ X1 @ cF))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_115])).
% 0.21/0.28 thf(c_0_121, negated_conjecture, ![X1:$i]:(((cG @ cD @ cE)|(cG @ cC @ cE)|~((cG @ X1 @ cE))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_116])).
% 0.21/0.28 thf(c_0_122, plain, ((cG @ cA @ cF)|(cG @ cB @ cF)|(cG @ cA @ cB)), inference(spm,[status(thm)],[c_0_117, c_0_40])).
% 0.21/0.28 thf(c_0_123, plain, ((cG @ cA @ cE)|(cG @ cC @ cE)|(cG @ cD @ cE)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_75]), c_0_58])).
% 0.21/0.28 thf(c_0_124, plain, ((cG @ cD @ cF)|(cG @ cC @ cF)|~((cG @ cA @ cE))), inference(spm,[status(thm)],[c_0_118, c_0_119])).
% 0.21/0.28 thf(c_0_125, plain, ((cG @ cB @ cE)|(cG @ cA @ cE)|(cG @ cC @ cF)|(cG @ cD @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_91]), c_0_119])).
% 0.21/0.28 thf(c_0_126, plain, ((cG @ cD @ cF)|(cG @ cC @ cF)|~((cG @ cB @ cE))), inference(spm,[status(thm)],[c_0_118, c_0_115])).
% 0.21/0.28 thf(c_0_127, plain, ((cG @ cB @ cF)|(cG @ cA @ cF)|(cG @ cC @ cE)|(cG @ cD @ cE)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_122]), c_0_123])).
% 0.21/0.28 thf(c_0_128, plain, ((cG @ cC @ cF)|(cG @ cD @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_125]), c_0_126])).
% 0.21/0.28 thf(c_0_129, plain, ((cG @ cD @ cE)|(cG @ cC @ cE)|(cG @ cB @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_127]), c_0_123])).
% 0.21/0.28 thf(c_0_130, negated_conjecture, ((cG @ cD @ cF)|~((cG @ cC @ cE))), inference(spm,[status(thm)],[c_0_118, c_0_128])).
% 0.21/0.28 thf(c_0_131, negated_conjecture, ((cG @ cC @ cE)|(cG @ cD @ cE)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_129]), c_0_116])).
% 0.21/0.28 thf(c_0_132, negated_conjecture, ((cG @ cD @ cE)|(cG @ cD @ cF)), inference(spm,[status(thm)],[c_0_130, c_0_131])).
% 0.21/0.28 thf(c_0_133, negated_conjecture, ![X1:$i]:(((cG @ cD @ cE)|~((cG @ X1 @ cF))|~((cG @ X1 @ cD)))), inference(spm,[status(thm)],[c_0_31, c_0_132])).
% 0.21/0.28 thf(c_0_134, negated_conjecture, ![X1:$i]:(((cG @ cC @ cF)|(cG @ cB @ cF)|~((cG @ X1 @ cC))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_108])).
% 0.21/0.28 thf(c_0_135, plain, ((cG @ cD @ cE)|~((cG @ cA @ cF))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_133, c_0_58]), c_0_118])).
% 0.21/0.28 thf(c_0_136, plain, ((cG @ cA @ cF)|(cG @ cB @ cF)|(cG @ cC @ cF)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_134, c_0_122]), c_0_113])).
% 0.21/0.28 thf(c_0_137, plain, ((cG @ cD @ cE)|~((cG @ cB @ cF))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_133, c_0_45]), c_0_118])).
% 0.21/0.28 thf(c_0_138, plain, ((cG @ cC @ cF)|(cG @ cD @ cE)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_136]), c_0_137])).
% 0.21/0.28 thf(c_0_139, negated_conjecture, (cG @ cD @ cE), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_138]), c_0_131])).
% 0.21/0.28 thf(c_0_140, negated_conjecture, ![X1:$i]:((~((cG @ X1 @ cE))|~((cG @ X1 @ cD)))), inference(spm,[status(thm)],[c_0_31, c_0_139])).
% 0.21/0.28 thf(c_0_141, negated_conjecture, ![X1:$i]:(((cG @ cC @ cE)|(cG @ cB @ cE)|~((cG @ X1 @ cC))|~((cG @ X1 @ cB)))), inference(spm,[status(thm)],[c_0_31, c_0_69])).
% 0.21/0.28 thf(c_0_142, plain, ((cG @ cD @ cF)|~((cG @ cA @ cE))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_140, c_0_114]), c_0_118])).
% 0.21/0.28 thf(c_0_143, plain, ((cG @ cA @ cE)|(cG @ cB @ cE)|(cG @ cC @ cE)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_141, c_0_91]), c_0_75])).
% 0.21/0.28 thf(c_0_144, plain, ((cG @ cD @ cF)|~((cG @ cB @ cE))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_140, c_0_109]), c_0_118])).
% 0.21/0.28 thf(c_0_145, plain, (cG @ cD @ cF), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142, c_0_143]), c_0_130]), c_0_144])).
% 0.21/0.28 thf(c_0_146, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_145]), c_0_139])]), ['proof']).
% 0.21/0.28 % SZS output end CNFRefutation
% 0.21/0.28 % Parsed axioms : 9
% 0.21/0.28 % Removed by relevancy pruning/SinE : 0
% 0.21/0.28 % Initial clauses : 26
% 0.21/0.28 % Removed in clause preprocessing : 8
% 0.21/0.28 % Initial clauses in saturation : 18
% 0.21/0.28 % Processed clauses : 218
% 0.21/0.28 % ...of these trivial : 0
% 0.21/0.28 % ...subsumed : 12
% 0.21/0.28 % ...remaining for further processing : 206
% 0.21/0.28 % Other redundant clauses eliminated : 0
% 0.21/0.28 % Clauses deleted for lack of memory : 0
% 0.21/0.28 % Backward-subsumed : 62
% 0.21/0.28 % Backward-rewritten : 63
% 0.21/0.28 % Generated clauses : 526
% 0.21/0.28 % ...of the previous two non-redundant : 471
% 0.21/0.28 % ...aggressively subsumed : 0
% 0.21/0.28 % Contextual simplify-reflections : 49
% 0.21/0.28 % Paramodulations : 526
% 0.21/0.28 % Factorizations : 0
% 0.21/0.28 % NegExts : 0
% 0.21/0.28 % Equation resolutions : 0
% 0.21/0.28 % Disequality decompositions : 0
% 0.21/0.28 % Total rewrite steps : 79
% 0.21/0.28 % ...of those cached : 75
% 0.21/0.28 % Propositional unsat checks : 0
% 0.21/0.28 % Propositional check models : 0
% 0.21/0.28 % Propositional check unsatisfiable : 0
% 0.21/0.28 % Propositional clauses : 0
% 0.21/0.28 % Propositional clauses after purity: 0
% 0.21/0.28 % Propositional unsat core size : 0
% 0.21/0.28 % Propositional preprocessing time : 0.000
% 0.21/0.28 % Propositional encoding time : 0.000
% 0.21/0.28 % Propositional solver time : 0.000
% 0.21/0.28 % Success case prop preproc time : 0.000
% 0.21/0.28 % Success case prop encoding time : 0.000
% 0.21/0.28 % Success case prop solver time : 0.000
% 0.21/0.28 % Current number of processed clauses : 81
% 0.21/0.28 % Positive orientable unit clauses : 4
% 0.21/0.28 % Positive unorientable unit clauses: 0
% 0.21/0.28 % Negative unit clauses : 1
% 0.21/0.28 % Non-unit-clauses : 76
% 0.21/0.28 % Current number of unprocessed clauses: 247
% 0.21/0.28 % ...number of literals in the above : 1429
% 0.21/0.28 % Current number of archived formulas : 0
% 0.21/0.28 % Current number of archived clauses : 125
% 0.21/0.28 % Clause-clause subsumption calls (NU) : 1791
% 0.21/0.28 % Rec. Clause-clause subsumption calls : 426
% 0.21/0.28 % Non-unit clause-clause subsumptions : 123
% 0.21/0.28 % Unit Clause-clause subsumption calls : 70
% 0.21/0.28 % Rewrite failures with RHS unbound : 0
% 0.21/0.28 % BW rewrite match attempts : 3
% 0.21/0.28 % BW rewrite match successes : 3
% 0.21/0.28 % Condensation attempts : 0
% 0.21/0.28 % Condensation successes : 0
% 0.21/0.28 % Termbank termtop insertions : 9654
% 0.21/0.28 % Search garbage collected termcells : 141
% 0.21/0.28
% 0.21/0.28 % -------------------------------------------------
% 0.21/0.28 % User time : 0.025 s
% 0.21/0.28 % System time : 0.003 s
% 0.21/0.28 % Total time : 0.028 s
% 0.21/0.28 % Maximum resident set size: 3644 pages
% 0.21/0.28
% 0.21/0.28 % -------------------------------------------------
% 0.21/0.28 % User time : 0.027 s
% 0.21/0.28 % System time : 0.007 s
% 0.21/0.28 % Total time : 0.034 s
% 0.21/0.28 % Maximum resident set size: 4608 pages
% 0.21/0.28 % E exiting
%------------------------------------------------------------------------------