%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP280_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 12:55:14 PM UTC 2026
% Result : Theorem 16.36s 5.34s
% Output : CNFRefutation 16.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 25 ( 21 unt; 0 typ; 0 def)
% Number of atoms : 33 ( 13 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 4 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 19 ( 18 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 15 con; 0-2 aty)
% Number of variables : 14 ( 0 sgn 14 !; 0 ?; 14 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
fun_nat_nat: $tType ).
tff(decl_sort2,type,
fun_nat_fun_nat_nat: $tType ).
tff(decl_sort3,type,
fun_real_bool: $tType ).
tff(decl_sort4,type,
fun_nat_bool: $tType ).
tff(decl_sort5,type,
fun_nat_fun_nat_bool: $tType ).
tff(decl_sort6,type,
fun_nat_real: $tType ).
tff(decl_sort7,type,
nat: $tType ).
tff(decl_sort8,type,
real: $tType ).
tff(decl_sort9,type,
num: $tType ).
tff(decl_sort10,type,
fun_re1255401033344146673l_bool: $tType ).
tff(decl_sort11,type,
fun_real_real: $tType ).
tff(decl_sort12,type,
fun_re7681423839302404990l_real: $tType ).
tff(decl_sort13,type,
fun_num_num: $tType ).
tff(decl_sort14,type,
vEBT_VEBT: $tType ).
tff(decl_sort15,type,
fun_num_nat: $tType ).
tff(decl_sort16,type,
bool: $tType ).
tff(decl_sort17,type,
fun_VEBT_VEBT_real: $tType ).
tff(decl_sort18,type,
fun_num_real: $tType ).
tff(decl_510,type,
one_one_nat: nat ).
tff(decl_533,type,
times_times_real: fun_re7681423839302404990l_real ).
tff(decl_669,type,
suc: fun_nat_nat ).
tff(decl_683,type,
semiri5074537144036343181t_real: fun_nat_real ).
tff(decl_728,type,
bit0: fun_num_num ).
tff(decl_729,type,
bit1: fun_num_num ).
tff(decl_730,type,
one: num ).
tff(decl_738,type,
numeral_numeral_nat: fun_num_nat ).
tff(decl_740,type,
numeral_numeral_real: fun_num_real ).
tff(decl_781,type,
ord_less_eq_real: fun_re1255401033344146673l_bool ).
tff(decl_885,type,
divide_divide_nat: fun_nat_fun_nat_nat ).
tff(decl_891,type,
dvd_dvd_nat: fun_nat_fun_nat_bool ).
tff(decl_1016,type,
vEBT_vebt_buildup: nat > vEBT_VEBT ).
tff(decl_1018,type,
vEBT_V8646137997579335489_i_l_d: fun_nat_nat ).
tff(decl_1022,type,
vEBT_VEBT_cnt: fun_VEBT_VEBT_real ).
tff(decl_1080,type,
aa_nat_bool: ( nat * fun_nat_bool ) > bool ).
tff(decl_1082,type,
aa_nat_nat: ( nat * fun_nat_nat ) > nat ).
tff(decl_1087,type,
aa_nat_real: ( nat * fun_nat_real ) > real ).
tff(decl_1094,type,
aa_nat_fun_nat_bool: ( nat * fun_nat_fun_nat_bool ) > fun_nat_bool ).
tff(decl_1095,type,
aa_nat_fun_nat_nat: ( nat * fun_nat_fun_nat_nat ) > fun_nat_nat ).
tff(decl_1111,type,
aa_num_nat: ( num * fun_num_nat ) > nat ).
tff(decl_1112,type,
aa_num_num: ( num * fun_num_num ) > num ).
tff(decl_1115,type,
aa_num_real: ( num * fun_num_real ) > real ).
tff(decl_1144,type,
aa_real_bool: ( real * fun_real_bool ) > bool ).
tff(decl_1149,type,
aa_real_real: ( real * fun_real_real ) > real ).
tff(decl_1153,type,
aa_rea7809428808904475482l_bool: ( real * fun_re1255401033344146673l_bool ) > fun_real_bool ).
tff(decl_1154,type,
aa_rea7340605660300375871l_real: ( real * fun_re7681423839302404990l_real ) > fun_real_real ).
tff(decl_1163,type,
aa_VEBT_VEBT_real: ( vEBT_VEBT * fun_VEBT_VEBT_real ) > real ).
tff(decl_1237,type,
pp: bool > $o ).
tff(decl_1238,type,
va: nat ).
tff(conj_0,conjecture,
pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))),aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(fact_0_False,axiom,
~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_False) ).
tff(fact_1__C3_OIH_C_I3_J,axiom,
! [X1: nat] :
( ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va))))
=> ( ( X1 = aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,va))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) )
=> pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,X1)))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,X1)))),aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__C3_OIH_C_I3_J) ).
tff(fact_5_div2__Suc__Suc,axiom,
! [X3: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,X3))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) = aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,X3),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_div2__Suc__Suc) ).
tff(fact_1045_mult_Ocommute,axiom,
! [X6: real,X4: real] : ( aa_real_real(aa_rea7340605660300375871l_real(times_times_real,X6),X4) = aa_real_real(aa_rea7340605660300375871l_real(times_times_real,X4),X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1045_mult_Ocommute) ).
tff(fact_1296_Suc__1,axiom,
aa_nat_nat(suc,one_one_nat) = aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1296_Suc__1) ).
tff(c_0_6,negated_conjecture,
~ pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))),aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))))),
inference(assume_negation,[status(cth)],[conj_0]) ).
tff(c_0_7,plain,
~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va)))),
inference(fof_simplification,[status(thm)],[fact_0_False]) ).
tff(c_0_8,negated_conjecture,
~ pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))),aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))))),
inference(fof_simplification,[status(thm)],[c_0_6]) ).
tff(c_0_9,plain,
! [X1: nat] :
( ~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va))))
=> ( ( X1 = aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,va))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) )
=> pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,X1)))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,X1)))),aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))))) ) ),
inference(fof_simplification,[status(thm)],[fact_1__C3_OIH_C_I3_J]) ).
tff(c_0_10,plain,
! [X16565: nat] : ( aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,X16565))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) = aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,X16565),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))) ),
inference(variable_rename,[status(thm)],[fact_5_div2__Suc__Suc]) ).
tff(c_0_11,plain,
~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va)))),
inference(fof_nnf,[status(thm)],[c_0_7]) ).
tff(c_0_12,negated_conjecture,
~ pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))),aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))))),
inference(fof_nnf,[status(thm)],[c_0_8]) ).
tff(c_0_13,plain,
! [X16561: nat] :
( pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,X16561)))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,X16561)))),aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one)))))))
| ( X16561 != aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,va))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) )
| pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va)))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])]) ).
tff(c_0_14,plain,
! [X17541: real,X17542: real] : ( aa_real_real(aa_rea7340605660300375871l_real(times_times_real,X17541),X17542) = aa_real_real(aa_rea7340605660300375871l_real(times_times_real,X17542),X17541) ),
inference(variable_rename,[status(thm)],[fact_1045_mult_Ocommute]) ).
tcf(c_0_15,plain,
! [X1: nat] : aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,X1))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) = aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,X1),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tcf(c_0_16,plain,
aa_nat_nat(suc,one_one_nat) = aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)),
inference(split_conjunct,[status(thm)],[fact_1296_Suc__1]) ).
tcf(c_0_17,plain,
~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va)))),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
tcf(c_0_18,negated_conjecture,
~ pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))),aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one)))))))))),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_19,plain,
! [X1: nat] :
( ( X1 != aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,va))),aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))) )
| pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,X1)))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,X1)))),aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one)))))))
| pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_num_nat(numeral_numeral_nat,aa_num_num(bit0,one))),aa_nat_nat(suc,aa_nat_nat(suc,va)))) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
tcf(c_0_20,plain,
! [X6: real,X4: real] : aa_real_real(aa_rea7340605660300375871l_real(times_times_real,X4),X6) = aa_real_real(aa_rea7340605660300375871l_real(times_times_real,X6),X4),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
tcf(c_0_21,plain,
! [X1: nat] : aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,aa_nat_nat(suc,aa_nat_nat(suc,X1))),aa_nat_nat(suc,one_one_nat)) = aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,X1),aa_nat_nat(suc,one_one_nat))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_15,c_0_16]),c_0_16]) ).
tcf(c_0_22,plain,
~ pp(aa_nat_bool(aa_nat_fun_nat_bool(dvd_dvd_nat,aa_nat_nat(suc,one_one_nat)),aa_nat_nat(suc,aa_nat_nat(suc,va)))),
inference(rw,[status(thm)],[c_0_17,c_0_16]) ).
tcf(c_0_23,negated_conjecture,
~ pp(aa_real_bool(aa_rea7809428808904475482l_bool(ord_less_eq_real,aa_nat_real(semiri5074537144036343181t_real,aa_nat_nat(vEBT_V8646137997579335489_i_l_d,aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_nat_nat(suc,one_one_nat))))))),aa_real_real(aa_rea7340605660300375871l_real(times_times_real,aa_num_real(numeral_numeral_real,aa_num_num(bit1,aa_num_num(bit0,aa_num_num(bit1,one))))),aa_VEBT_VEBT_real(vEBT_VEBT_cnt,vEBT_vebt_buildup(aa_nat_nat(suc,aa_nat_nat(suc,aa_nat_nat(aa_nat_fun_nat_nat(divide_divide_nat,va),aa_nat_nat(suc,one_one_nat))))))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_16]),c_0_16]) ).
cnf(c_0_24,plain,
$false,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19,c_0_16]),c_0_20]),c_0_16]),c_0_21]),c_0_22])]),c_0_23]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP280_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n001.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 20 22:33:44 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.51 Running first-order theorem proving
% 0.20/0.51 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
% 16.36/5.34 % Version: 3.5.1
% 16.36/5.34 % Preprocessing class: FMLLSMLLSSSNFFN.
% 16.36/5.34 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 16.36/5.34 % Starting new_bool_3 with 897s (3) cores
% 16.36/5.34 % Starting new_bool_1 with 897s (3) cores
% 16.36/5.34 % Starting sh5l with 299s (1) cores
% 16.36/5.34 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 299s (1) cores
% 16.36/5.34 % new_bool_3 with pid 1545361 completed with status 0
% 16.36/5.34 % Result found by new_bool_3
% 16.36/5.34 % Preprocessing class: FMLLSMLLSSSNFFN.
% 16.36/5.34 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 16.36/5.34 % Starting new_bool_3 with 897s (3) cores
% 16.36/5.34 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 16.36/5.34 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 16.36/5.34 % Search class: FGHSM-SMLM32-DFFFFFNN
% 16.36/5.34 % Scheduled 13 strats onto 3 cores with 895 seconds (895 total)
% 16.36/5.34 % Starting SubtermCWHack with 81s (1) cores
% 16.36/5.34 % Starting new_bool_3 with 90s (1) cores
% 16.36/5.34 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 68s (1) cores
% 16.36/5.34 % new_bool_3 with pid 1545366 completed with status 0
% 16.36/5.34 % Result found by new_bool_3
% 16.36/5.34 % Preprocessing class: FMLLSMLLSSSNFFN.
% 16.36/5.34 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 16.36/5.34 % Starting new_bool_3 with 897s (3) cores
% 16.36/5.34 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 16.36/5.34 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 16.36/5.34 % Search class: FGHSM-SMLM32-DFFFFFNN
% 16.36/5.34 % Scheduled 13 strats onto 3 cores with 895 seconds (895 total)
% 16.36/5.34 % Starting SubtermCWHack with 81s (1) cores
% 16.36/5.34 % Starting new_bool_3 with 90s (1) cores
% 16.36/5.34 % Preprocessing time : 0.314 s
% 16.36/5.34 % Presaturation interreduction done
% 16.36/5.34
% 16.36/5.34 % Proof found!
% 16.36/5.34 % SZS status Theorem
% 16.36/5.34 % SZS output start CNFRefutation
% See solution above
% 16.36/5.34 % Parsed axioms : 11970
% 16.36/5.34 % Removed by relevancy pruning/SinE : 7455
% 16.36/5.34 % Initial clauses : 10455
% 16.36/5.34 % Removed in clause preprocessing : 1619
% 16.36/5.34 % Initial clauses in saturation : 8836
% 16.36/5.34 % Processed clauses : 4030
% 16.36/5.34 % ...of these trivial : 248
% 16.36/5.34 % ...subsumed : 953
% 16.36/5.34 % ...remaining for further processing : 2829
% 16.36/5.34 % Other redundant clauses eliminated : 687
% 16.36/5.34 % Clauses deleted for lack of memory : 0
% 16.36/5.34 % Backward-subsumed : 15
% 16.36/5.34 % Backward-rewritten : 109
% 16.36/5.34 % Generated clauses : 639
% 16.36/5.34 % ...of the previous two non-redundant : 267
% 16.36/5.34 % ...aggressively subsumed : 0
% 16.36/5.34 % Contextual simplify-reflections : 6
% 16.36/5.34 % Paramodulations : 0
% 16.36/5.34 % Factorizations : 0
% 16.36/5.34 % NegExts : 0
% 16.36/5.34 % Equation resolutions : 687
% 16.36/5.34 % Disequality decompositions : 0
% 16.36/5.34 % Total rewrite steps : 1833
% 16.36/5.34 % ...of those cached : 1306
% 16.36/5.34 % Propositional unsat checks : 0
% 16.36/5.34 % Propositional check models : 0
% 16.36/5.34 % Propositional check unsatisfiable : 0
% 16.36/5.34 % Propositional clauses : 0
% 16.36/5.34 % Propositional clauses after purity: 0
% 16.36/5.34 % Propositional unsat core size : 0
% 16.36/5.34 % Propositional preprocessing time : 0.000
% 16.36/5.34 % Propositional encoding time : 0.000
% 16.36/5.34 % Propositional solver time : 0.000
% 16.36/5.34 % Success case prop preproc time : 0.000
% 16.36/5.34 % Success case prop encoding time : 0.000
% 16.36/5.34 % Success case prop solver time : 0.000
% 16.36/5.34 % Current number of processed clauses : 2066
% 16.36/5.34 % Positive orientable unit clauses : 488
% 16.36/5.34 % Positive unorientable unit clauses: 23
% 16.36/5.34 % Negative unit clauses : 150
% 16.36/5.34 % Non-unit-clauses : 1405
% 16.36/5.34 % Current number of unprocessed clauses: 5073
% 16.36/5.34 % ...number of literals in the above : 22123
% 16.36/5.34 % Current number of archived formulas : 0
% 16.36/5.34 % Current number of archived clauses : 124
% 16.36/5.34 % Clause-clause subsumption calls (NU) : 273537
% 16.36/5.34 % Rec. Clause-clause subsumption calls : 176490
% 16.36/5.34 % Non-unit clause-clause subsumptions : 781
% 16.36/5.34 % Unit Clause-clause subsumption calls : 1499
% 16.36/5.34 % Rewrite failures with RHS unbound : 8
% 16.36/5.34 % BW rewrite match attempts : 3949
% 16.36/5.34 % BW rewrite match successes : 338
% 16.36/5.34 % Condensation attempts : 0
% 16.36/5.34 % Condensation successes : 0
% 16.36/5.34 % Termbank termtop insertions : 1199073
% 16.36/5.34 % Search garbage collected termcells : 181563
% 16.36/5.34
% 16.36/5.34 % -------------------------------------------------
% 16.36/5.34 % User time : 2.975 s
% 16.36/5.34 % System time : 0.145 s
% 16.36/5.34 % Total time : 3.120 s
% 16.36/5.34 % Maximum resident set size: 48916 pages
% 16.36/5.34
% 16.36/5.34 % -------------------------------------------------
% 16.36/5.34 % User time : 5.685 s
% 16.36/5.34 % System time : 0.401 s
% 16.36/5.34 % Total time : 6.087 s
% 16.36/5.34 % Maximum resident set size: 28160 pages
% 16.36/5.34 % E exiting
%------------------------------------------------------------------------------