%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NUM925_3 : TPTP v9.3.1. Released v5.3.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 : Thu Sep 24 01:51:02 PM UTC 2026
% Result : Theorem 1.13s 0.65s
% Output : CNFRefutation 1.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 16
% Syntax : Number of formulae : 58 ( 50 unt; 0 typ; 0 def)
% Number of atoms : 66 ( 59 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 24 ( 16 ~; 5 |; 0 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 7 ( 6 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-2 aty)
% Number of variables : 49 ( 0 sgn 49 !; 0 ?; 49 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
fun_int_bool: $tType ).
tff(decl_sort2,type,
int: $tType ).
tff(decl_sort3,type,
nat: $tType ).
tff(decl_sort4,type,
bool: $tType ).
tff(decl_sort5,type,
fun_nat_int: $tType ).
tff(decl_sort6,type,
fun_int_fun_int_bool: $tType ).
tff(decl_25,type,
minus_minus_int: ( int * int ) > int ).
tff(decl_28,type,
one_one_int: int ).
tff(decl_29,type,
one_one_nat: nat ).
tff(decl_31,type,
plus_plus_int: ( int * int ) > int ).
tff(decl_32,type,
plus_plus_nat: ( nat * nat ) > nat ).
tff(decl_37,type,
zero_zero_int: int ).
tff(decl_44,type,
bit0: int > int ).
tff(decl_45,type,
bit1: int > int ).
tff(decl_46,type,
min: int ).
tff(decl_47,type,
pls: int ).
tff(decl_49,type,
number_number_of_int: int > int ).
tff(decl_50,type,
number_number_of_nat: int > nat ).
tff(decl_53,type,
semiri1621563631at_int: fun_nat_int ).
tff(decl_56,type,
ord_less_int: fun_int_fun_int_bool ).
tff(decl_62,type,
power_power_int: int > fun_nat_int ).
tff(decl_72,type,
hAPP_int_bool: ( int * fun_int_bool ) > bool ).
tff(decl_73,type,
hAPP_i1948725293t_bool: ( int * fun_int_fun_int_bool ) > fun_int_bool ).
tff(decl_75,type,
hAPP_nat_int: ( nat * fun_nat_int ) > int ).
tff(decl_81,type,
hBOOL: bool > $o ).
tff(decl_84,type,
n: nat ).
tff(fact_177_number__of__is__id,axiom,
! [X22: int] : ( number_number_of_int(X22) = X22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_number__of__is__id) ).
tff(conj_0,conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(fact_25_semiring__norm_I110_J,axiom,
one_one_int = number_number_of_int(bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_semiring__norm_I110_J) ).
tff(fact_98_Pls__def,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_Pls__def) ).
tff(fact_16_one__add__one__is__two,axiom,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_one__add__one__is__two) ).
tff(fact_231_field__power__not__zero,axiom,
! [X132: nat,X133: int] :
( ( X133 != zero_zero_int )
=> ( hAPP_nat_int(power_power_int(X133),X132) != zero_zero_int ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_field__power__not__zero) ).
tff(fact_103_Bit0__def,axiom,
! [X22: int] : ( bit0(X22) = plus_plus_int(X22,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_Bit0__def) ).
tff(fact_19_semiring__one__add__one__is__two,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_semiring__one__add__one__is__two) ).
tff(fact_1026_diff__bin__simps_I4_J,axiom,
! [X37: int] : ( minus_minus_int(pls,bit1(X37)) = bit1(minus_minus_int(min,X37)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1026_diff__bin__simps_I4_J) ).
tff(fact_606_diff__add__cancel,axiom,
! [X845: int,X846: int] : ( plus_plus_int(minus_minus_int(X845,X846),X846) = X845 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_606_diff__add__cancel) ).
tff(fact_67_zadd__commute,axiom,
! [X18: int,X15: int] : ( plus_plus_int(X18,X15) = plus_plus_int(X15,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_zadd__commute) ).
tff(fact_598_diff__0__right,axiom,
! [X826: int] : ( minus_minus_int(X826,zero_zero_int) = X826 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_598_diff__0__right) ).
tff(fact_319_add__imp__eq,axiom,
! [X223: int,X224: int,X225: int] :
( ( plus_plus_int(X223,X224) = plus_plus_int(X223,X225) )
=> ( X224 = X225 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_319_add__imp__eq) ).
tff(fact_1017_Bit1__Min,axiom,
bit1(min) = min,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1017_Bit1__Min) ).
tff(fact_83_int__less__0__conv,axiom,
! [X35: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X35)),zero_zero_int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_int__less__0__conv) ).
tff(fact_1007_bin__less__0__simps_I2_J,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,min),zero_zero_int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1007_bin__less__0__simps_I2_J) ).
tff(c_0_16,plain,
! [X2584: int] : ( number_number_of_int(X2584) = X2584 ),
inference(variable_rename,[status(thm)],[fact_177_number__of__is__id]) ).
tff(c_0_17,negated_conjecture,
~ ( ( hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
tcf(c_0_18,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(split_conjunct,[status(thm)],[fact_25_semiring__norm_I110_J]) ).
tcf(c_0_19,plain,
pls = zero_zero_int,
inference(split_conjunct,[status(thm)],[fact_98_Pls__def]) ).
tcf(c_0_20,plain,
! [X1: int] : number_number_of_int(X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_16]) ).
tff(c_0_21,negated_conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(fof_simplification,[status(thm)],[c_0_17]) ).
tcf(c_0_22,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(split_conjunct,[status(thm)],[fact_16_one__add__one__is__two]) ).
tcf(c_0_23,plain,
bit1(zero_zero_int) = one_one_int,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_19]),c_0_20]) ).
tff(c_0_24,plain,
! [X132: nat,X133: int] :
( ( X133 != zero_zero_int )
=> ( hAPP_nat_int(power_power_int(X133),X132) != zero_zero_int ) ),
inference(fof_simplification,[status(thm)],[fact_231_field__power__not__zero]) ).
tcf(c_0_25,negated_conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(split_conjunct,[status(thm)],[c_0_21]) ).
tff(c_0_26,plain,
! [X1772: int] : ( bit0(X1772) = plus_plus_int(X1772,X1772) ),
inference(variable_rename,[status(thm)],[fact_103_Bit0__def]) ).
tcf(c_0_27,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(split_conjunct,[status(thm)],[fact_19_semiring__one__add__one__is__two]) ).
tcf(c_0_28,plain,
bit0(one_one_int) = plus_plus_int(one_one_int,one_one_int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_22,c_0_19]),c_0_23]),c_0_20]) ).
tff(c_0_29,plain,
! [X2781: int] : ( minus_minus_int(pls,bit1(X2781)) = bit1(minus_minus_int(min,X2781)) ),
inference(variable_rename,[status(thm)],[fact_1026_diff__bin__simps_I4_J]) ).
tff(c_0_30,plain,
! [X1830: nat,X1831: int] :
( ( hAPP_nat_int(power_power_int(X1831),X1830) != zero_zero_int )
| ( X1831 = zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])]) ).
tcf(c_0_31,negated_conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(zero_zero_int)))) = zero_zero_int,
inference(rw,[status(thm)],[c_0_25,c_0_19]) ).
tcf(c_0_32,plain,
! [X1: int] : bit0(X1) = plus_plus_int(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
tcf(c_0_33,plain,
number_number_of_nat(plus_plus_int(one_one_int,one_one_int)) = plus_plus_nat(one_one_nat,one_one_nat),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_19]),c_0_23]),c_0_28]) ).
tff(c_0_34,plain,
! [X2750: int,X2751: int] : ( plus_plus_int(minus_minus_int(X2750,X2751),X2751) = X2750 ),
inference(variable_rename,[status(thm)],[fact_606_diff__add__cancel]) ).
tff(c_0_35,plain,
! [X1891: int,X1892: int] : ( plus_plus_int(X1891,X1892) = plus_plus_int(X1892,X1891) ),
inference(variable_rename,[status(thm)],[fact_67_zadd__commute]) ).
tcf(c_0_36,plain,
! [X1: int] : minus_minus_int(pls,bit1(X1)) = bit1(minus_minus_int(min,X1)),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tff(c_0_37,plain,
! [X2739: int] : ( minus_minus_int(X2739,zero_zero_int) = X2739 ),
inference(variable_rename,[status(thm)],[fact_598_diff__0__right]) ).
tff(c_0_38,plain,
! [X1905: int,X1906: int,X1907: int] :
( ( X1906 = X1907 )
| ( plus_plus_int(X1905,X1906) != plus_plus_int(X1905,X1907) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_319_add__imp__eq])])]) ).
tcf(c_0_39,plain,
! [X1: int,X16: nat] :
( ( hAPP_nat_int(power_power_int(X1),X16) != zero_zero_int )
| ( X1 = zero_zero_int ) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
tcf(c_0_40,negated_conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),plus_plus_nat(one_one_nat,one_one_nat)) = zero_zero_int,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_23]),c_0_32]),c_0_33]) ).
tcf(c_0_41,plain,
! [X2: int,X1: int] : plus_plus_int(minus_minus_int(X1,X2),X2) = X1,
inference(split_conjunct,[status(thm)],[c_0_34]) ).
tcf(c_0_42,plain,
! [X2: int,X1: int] : plus_plus_int(X1,X2) = plus_plus_int(X2,X1),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
tcf(c_0_43,plain,
! [X1: int] : minus_minus_int(zero_zero_int,bit1(X1)) = bit1(minus_minus_int(min,X1)),
inference(rw,[status(thm)],[c_0_36,c_0_19]) ).
tcf(c_0_44,plain,
! [X1: int] : minus_minus_int(X1,zero_zero_int) = X1,
inference(split_conjunct,[status(thm)],[c_0_37]) ).
tcf(c_0_45,plain,
bit1(min) = min,
inference(split_conjunct,[status(thm)],[fact_1017_Bit1__Min]) ).
tff(c_0_46,plain,
! [X35: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X35)),zero_zero_int)),
inference(fof_simplification,[status(thm)],[fact_83_int__less__0__conv]) ).
tcf(c_0_47,plain,
! [X1: int,X2: int,X5: int] :
( ( plus_plus_int(X1,X2) != plus_plus_int(X1,X5) )
| ( X2 = X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
tcf(c_0_48,negated_conjecture,
plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)) = zero_zero_int,
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
tcf(c_0_49,plain,
! [X1: int,X2: int] : plus_plus_int(X1,minus_minus_int(X2,X1)) = X2,
inference(rw,[status(thm)],[c_0_41,c_0_42]) ).
tcf(c_0_50,plain,
minus_minus_int(zero_zero_int,one_one_int) = min,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_23]),c_0_44]),c_0_45]) ).
tff(c_0_51,plain,
! [X2052: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X2052)),zero_zero_int)),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_46])]) ).
tcf(c_0_52,negated_conjecture,
! [X1: int] :
( ( plus_plus_int(one_one_int,X1) != zero_zero_int )
| ( X1 = hAPP_nat_int(semiri1621563631at_int,n) ) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
tcf(c_0_53,plain,
plus_plus_int(one_one_int,min) = zero_zero_int,
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
tcf(c_0_54,plain,
! [X16: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X16)),zero_zero_int)),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
tcf(c_0_55,negated_conjecture,
hAPP_nat_int(semiri1621563631at_int,n) = min,
inference(spm,[status(thm)],[c_0_52,c_0_53]) ).
tcf(c_0_56,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,min),zero_zero_int)),
inference(split_conjunct,[status(thm)],[fact_1007_bin__less__0__simps_I2_J]) ).
cnf(c_0_57,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_56])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925_3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 03:17:25 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.42 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.13/0.65 % Version: 3.5.1
% 1.13/0.65 % Preprocessing class: FMLSSMSMSSSNFFN.
% 1.13/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.13/0.65 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 1.13/0.65 % Starting new_bool_3 with 600s (2) cores
% 1.13/0.65 % Starting new_bool_1 with 600s (2) cores
% 1.13/0.65 % Starting sh5l with 300s (1) cores
% 1.13/0.65 % new_bool_3 with pid 847565 completed with status 0
% 1.13/0.65 % Result found by new_bool_3
% 1.13/0.65 % Preprocessing class: FMLSSMSMSSSNFFN.
% 1.13/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.13/0.65 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 1.13/0.65 % Starting new_bool_3 with 600s (2) cores
% 1.13/0.65 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 1.13/0.65 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 1.13/0.65 % Search class: FGHSM-SSLM31-DFFFFFNN
% 1.13/0.65 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 1.13/0.65 % Starting SubtermCWHack with 55s (1) cores
% 1.13/0.65 % Starting new_bool_3 with 61s (1) cores
% 1.13/0.65 % new_bool_3 with pid 847571 completed with status 0
% 1.13/0.65 % Result found by new_bool_3
% 1.13/0.65 % Preprocessing class: FMLSSMSMSSSNFFN.
% 1.13/0.65 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.13/0.65 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S4d with 900s (3) cores
% 1.13/0.65 % Starting new_bool_3 with 600s (2) cores
% 1.13/0.65 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 1.13/0.65 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 1.13/0.65 % Search class: FGHSM-SSLM31-DFFFFFNN
% 1.13/0.65 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 1.13/0.65 % Starting SubtermCWHack with 55s (1) cores
% 1.13/0.65 % Starting new_bool_3 with 61s (1) cores
% 1.13/0.65 % Preprocessing time : 0.013 s
% 1.13/0.65 % Presaturation interreduction done
% 1.13/0.65
% 1.13/0.65 % Proof found!
% 1.13/0.65 % SZS status Theorem
% 1.13/0.65 % SZS output start CNFRefutation
% See solution above
% 1.13/0.65 % Parsed axioms : 1286
% 1.13/0.65 % Removed by relevancy pruning/SinE : 428
% 1.13/0.65 % Initial clauses : 1265
% 1.13/0.65 % Removed in clause preprocessing : 98
% 1.13/0.65 % Initial clauses in saturation : 1167
% 1.13/0.65 % Processed clauses : 1437
% 1.13/0.65 % ...of these trivial : 153
% 1.13/0.65 % ...subsumed : 373
% 1.13/0.65 % ...remaining for further processing : 911
% 1.13/0.65 % Other redundant clauses eliminated : 133
% 1.13/0.65 % Clauses deleted for lack of memory : 0
% 1.13/0.65 % Backward-subsumed : 7
% 1.13/0.65 % Backward-rewritten : 31
% 1.13/0.65 % Generated clauses : 451
% 1.13/0.65 % ...of the previous two non-redundant : 312
% 1.13/0.65 % ...aggressively subsumed : 0
% 1.13/0.65 % Contextual simplify-reflections : 1
% 1.13/0.65 % Paramodulations : 323
% 1.13/0.65 % Factorizations : 0
% 1.13/0.65 % NegExts : 0
% 1.13/0.65 % Equation resolutions : 140
% 1.13/0.65 % Disequality decompositions : 0
% 1.13/0.65 % Total rewrite steps : 1182
% 1.13/0.65 % ...of those cached : 972
% 1.13/0.65 % Propositional unsat checks : 0
% 1.13/0.65 % Propositional check models : 0
% 1.13/0.65 % Propositional check unsatisfiable : 0
% 1.13/0.65 % Propositional clauses : 0
% 1.13/0.65 % Propositional clauses after purity: 0
% 1.13/0.65 % Propositional unsat core size : 0
% 1.13/0.65 % Propositional preprocessing time : 0.000
% 1.13/0.65 % Propositional encoding time : 0.000
% 1.13/0.65 % Propositional solver time : 0.000
% 1.13/0.65 % Success case prop preproc time : 0.000
% 1.13/0.65 % Success case prop encoding time : 0.000
% 1.13/0.65 % Success case prop solver time : 0.000
% 1.13/0.65 % Current number of processed clauses : 119
% 1.13/0.65 % Positive orientable unit clauses : 57
% 1.13/0.65 % Positive unorientable unit clauses: 2
% 1.13/0.65 % Negative unit clauses : 24
% 1.13/0.65 % Non-unit-clauses : 36
% 1.13/0.65 % Current number of unprocessed clauses: 678
% 1.13/0.65 % ...number of literals in the above : 1534
% 1.13/0.65 % Current number of archived formulas : 0
% 1.13/0.65 % Current number of archived clauses : 681
% 1.13/0.65 % Clause-clause subsumption calls (NU) : 86688
% 1.13/0.65 % Rec. Clause-clause subsumption calls : 61271
% 1.13/0.65 % Non-unit clause-clause subsumptions : 264
% 1.13/0.65 % Unit Clause-clause subsumption calls : 1065
% 1.13/0.65 % Rewrite failures with RHS unbound : 0
% 1.13/0.65 % BW rewrite match attempts : 353
% 1.13/0.65 % BW rewrite match successes : 153
% 1.13/0.65 % Condensation attempts : 0
% 1.13/0.65 % Condensation successes : 0
% 1.13/0.65 % Termbank termtop insertions : 124504
% 1.13/0.65 % Search garbage collected termcells : 16912
% 1.13/0.65
% 1.13/0.65 % -------------------------------------------------
% 1.13/0.65 % User time : 0.139 s
% 1.13/0.65 % System time : 0.019 s
% 1.13/0.65 % Total time : 0.158 s
% 1.13/0.65 % Maximum resident set size: 9324 pages
% 1.13/0.65
% 1.13/0.65 % -------------------------------------------------
% 1.13/0.65 % User time : 0.258 s
% 1.13/0.65 % System time : 0.037 s
% 1.13/0.65 % Total time : 0.295 s
% 1.13/0.65 % Maximum resident set size: 6912 pages
% 1.13/0.65 % E exiting
%------------------------------------------------------------------------------