%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP129^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:04:27 AM UTC 2026
% Result : Theorem 198.01s 30.04s
% Output : CNFRefutation 198.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 15
% Syntax : Number of formulae : 61 ( 45 unt; 0 typ; 0 def)
% Number of atoms : 79 ( 78 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 388 ( 27 ~; 12 |; 1 &; 343 @)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Number of types : 2 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 53 ( 0 ^; 53 !; 0 ?; 53 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
int: $tType ).
thf(decl_sort2,type,
nat: $tType ).
thf(decl_25,type,
one_one_int: int ).
thf(decl_26,type,
one_one_nat: nat ).
thf(decl_27,type,
plus_plus_int: int > int > int ).
thf(decl_29,type,
times_times_int: int > int > int ).
thf(decl_31,type,
zero_zero_int: int ).
thf(decl_32,type,
zero_zero_nat: nat ).
thf(decl_38,type,
suc: nat > nat ).
thf(decl_39,type,
semiri2019852685at_int: nat > int ).
thf(decl_42,type,
power_power_int: int > nat > int ).
thf(decl_44,type,
divide_divide_int: int > int > int ).
thf(decl_48,type,
pm: nat ).
thf(decl_49,type,
x: int ).
thf(conj_0,conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( power_power_int @ x @ ( suc @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( semiri2019852685at_int @ ( suc @ pm ) ) )
= x ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',conj_0) ).
thf(fact_124_of__nat__Suc,axiom,
! [X1: nat] :
( ( semiri2019852685at_int @ ( suc @ X1 ) )
= ( plus_plus_int @ one_one_int @ ( semiri2019852685at_int @ X1 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_124_of__nat__Suc) ).
thf(fact_122_of__nat__1,axiom,
( ( semiri2019852685at_int @ one_one_nat )
= one_one_int ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_122_of__nat__1) ).
thf(fact_239_One__nat__def,axiom,
( one_one_nat
= ( suc @ zero_zero_nat ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_239_One__nat__def) ).
thf(fact_13_power__Suc,axiom,
! [X6: int,X2: nat] :
( ( power_power_int @ X6 @ ( suc @ X2 ) )
= ( times_times_int @ X6 @ ( power_power_int @ X6 @ X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_13_power__Suc) ).
thf(fact_223_nonzero__mult__div__cancel__right,axiom,
! [X201: int,X6: int] :
( ( X201 != zero_zero_int )
=> ( ( divide_divide_int @ ( times_times_int @ X6 @ X201 ) @ X201 )
= X6 ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_223_nonzero__mult__div__cancel__right) ).
thf(fact_109__092_060open_062_092_060And_062n_O_Ax_A_L_Ax_A_K_An_A_061_Ax_A_K_A_I1_A_L_An_J_092_060close_062,axiom,
! [X126: int] :
( ( plus_plus_int @ x @ ( times_times_int @ x @ X126 ) )
= ( times_times_int @ x @ ( plus_plus_int @ one_one_int @ X126 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_109__092_060open_062_092_060And_062n_O_Ax_A_L_Ax_A_K_An_A_061_Ax_A_K_A_I1_A_L_An_J_092_060close_062) ).
thf(fact_267_power__not__zero,axiom,
! [X6: int,X2: nat] :
( ( X6 != zero_zero_int )
=> ( ( power_power_int @ X6 @ X2 )
!= zero_zero_int ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_267_power__not__zero) ).
thf(fact_271_nat_Odistinct_I1_J,axiom,
! [X11: nat] :
( zero_zero_nat
!= ( suc @ X11 ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_271_nat_Odistinct_I1_J) ).
thf(fact_158_mult__zero__right,axiom,
! [X6: int] :
( ( times_times_int @ X6 @ zero_zero_int )
= zero_zero_int ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_158_mult__zero__right) ).
thf(fact_178_bits__div__by__0,axiom,
! [X6: int] :
( ( divide_divide_int @ X6 @ zero_zero_int )
= zero_zero_int ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_178_bits__div__by__0) ).
thf(fact_163_add_Oleft__neutral,axiom,
! [X6: int] :
( ( plus_plus_int @ zero_zero_int @ X6 )
= X6 ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_163_add_Oleft__neutral) ).
thf(fact_190_of__nat__eq__0__iff,axiom,
! [X1: nat] :
( ( ( semiri2019852685at_int @ X1 )
= zero_zero_int )
<=> ( X1 = zero_zero_nat ) ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_190_of__nat__eq__0__iff) ).
thf(fact_160_mult__zero__left,axiom,
! [X6: int] :
( ( times_times_int @ zero_zero_int @ X6 )
= zero_zero_int ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_160_mult__zero__left) ).
thf(fact_180_bits__div__0,axiom,
! [X6: int] :
( ( divide_divide_int @ zero_zero_int @ X6 )
= zero_zero_int ),
file('/export/starexec/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p',fact_180_bits__div__0) ).
thf(c_0_15,negated_conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( power_power_int @ x @ ( suc @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( semiri2019852685at_int @ ( suc @ pm ) ) )
!= x ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(c_0_16,negated_conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( power_power_int @ x @ ( suc @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( semiri2019852685at_int @ ( suc @ pm ) ) )
!= x ),
inference(fof_simplification,[status(thm)],[c_0_15]) ).
thf(c_0_17,plain,
! [X1177: nat] :
( ( semiri2019852685at_int @ ( suc @ X1177 ) )
= ( plus_plus_int @ one_one_int @ ( semiri2019852685at_int @ X1177 ) ) ),
inference(variable_rename,[status(thm)],[fact_124_of__nat__Suc]) ).
thf(c_0_18,plain,
( ( semiri2019852685at_int @ one_one_nat )
= one_one_int ),
inference(split_conjunct,[status(thm)],[fact_122_of__nat__1]) ).
thf(c_0_19,plain,
( one_one_nat
= ( suc @ zero_zero_nat ) ),
inference(split_conjunct,[status(thm)],[fact_239_One__nat__def]) ).
thf(c_0_20,negated_conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( power_power_int @ x @ ( suc @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( semiri2019852685at_int @ ( suc @ pm ) ) )
!= x ),
inference(fof_nnf,[status(thm)],[c_0_16]) ).
thf(c_0_21,plain,
! [X1: nat] :
( ( semiri2019852685at_int @ ( suc @ X1 ) )
= ( plus_plus_int @ one_one_int @ ( semiri2019852685at_int @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_22,plain,
( one_one_int
= ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) ),
inference(rw,[status(thm)],[c_0_18,c_0_19]) ).
thf(c_0_23,negated_conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( power_power_int @ x @ ( suc @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( semiri2019852685at_int @ ( suc @ pm ) ) )
!= x ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
thf(c_0_24,plain,
! [X1: nat] :
( ( semiri2019852685at_int @ ( suc @ X1 ) )
= ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ X1 ) ) ),
inference(rw,[status(thm)],[c_0_21,c_0_22]) ).
thf(c_0_25,plain,
! [X916: int,X917: nat] :
( ( power_power_int @ X916 @ ( suc @ X917 ) )
= ( times_times_int @ X916 @ ( power_power_int @ X916 @ X917 ) ) ),
inference(variable_rename,[status(thm)],[fact_13_power__Suc]) ).
thf(c_0_26,plain,
! [X201: int,X6: int] :
( ( X201 != zero_zero_int )
=> ( ( divide_divide_int @ ( times_times_int @ X6 @ X201 ) @ X201 )
= X6 ) ),
inference(fof_simplification,[status(thm)],[fact_223_nonzero__mult__div__cancel__right]) ).
thf(c_0_27,plain,
! [X1164: int] :
( ( plus_plus_int @ x @ ( times_times_int @ x @ X1164 ) )
= ( times_times_int @ x @ ( plus_plus_int @ one_one_int @ X1164 ) ) ),
inference(variable_rename,[status(thm)],[fact_109__092_060open_062_092_060And_062n_O_Ax_A_L_Ax_A_K_An_A_061_Ax_A_K_A_I1_A_L_An_J_092_060close_062]) ).
thf(c_0_28,plain,
! [X6: int,X2: nat] :
( ( X6 != zero_zero_int )
=> ( ( power_power_int @ X6 @ X2 )
!= zero_zero_int ) ),
inference(fof_simplification,[status(thm)],[fact_267_power__not__zero]) ).
thf(c_0_29,negated_conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( power_power_int @ x @ ( suc @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x ),
inference(rw,[status(thm)],[c_0_23,c_0_24]) ).
thf(c_0_30,plain,
! [X6: int,X1: nat] :
( ( power_power_int @ X6 @ ( suc @ X1 ) )
= ( times_times_int @ X6 @ ( power_power_int @ X6 @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
thf(c_0_31,plain,
! [X1362: int,X1363: int] :
( ( X1362 = zero_zero_int )
| ( ( divide_divide_int @ ( times_times_int @ X1363 @ X1362 ) @ X1362 )
= X1363 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])]) ).
thf(c_0_32,plain,
! [X6: int] :
( ( plus_plus_int @ x @ ( times_times_int @ x @ X6 ) )
= ( times_times_int @ x @ ( plus_plus_int @ one_one_int @ X6 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
thf(c_0_33,plain,
! [X1437: int,X1438: nat] :
( ( X1437 = zero_zero_int )
| ( ( power_power_int @ X1437 @ X1438 )
!= zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])]) ).
thf(c_0_34,negated_conjecture,
( ( divide_divide_int @ ( plus_plus_int @ ( divide_divide_int @ ( times_times_int @ x @ ( power_power_int @ x @ pm ) ) @ ( power_power_int @ x @ pm ) ) @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x ),
inference(rw,[status(thm)],[c_0_29,c_0_30]) ).
thf(c_0_35,plain,
! [X6: int,X20: int] :
( ( X6 = zero_zero_int )
| ( ( divide_divide_int @ ( times_times_int @ X20 @ X6 ) @ X6 )
= X20 ) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
thf(c_0_36,plain,
! [X6: int] :
( ( plus_plus_int @ x @ ( times_times_int @ x @ X6 ) )
= ( times_times_int @ x @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ X6 ) ) ),
inference(rw,[status(thm)],[c_0_32,c_0_22]) ).
thf(c_0_37,plain,
! [X11: nat] :
( zero_zero_nat
!= ( suc @ X11 ) ),
inference(fof_simplification,[status(thm)],[fact_271_nat_Odistinct_I1_J]) ).
thf(c_0_38,plain,
! [X1263: int] :
( ( times_times_int @ X1263 @ zero_zero_int )
= zero_zero_int ),
inference(variable_rename,[status(thm)],[fact_158_mult__zero__right]) ).
thf(c_0_39,plain,
! [X1293: int] :
( ( divide_divide_int @ X1293 @ zero_zero_int )
= zero_zero_int ),
inference(variable_rename,[status(thm)],[fact_178_bits__div__by__0]) ).
thf(c_0_40,plain,
! [X1268: int] :
( ( plus_plus_int @ zero_zero_int @ X1268 )
= X1268 ),
inference(variable_rename,[status(thm)],[fact_163_add_Oleft__neutral]) ).
thf(c_0_41,plain,
! [X6: int,X1: nat] :
( ( X6 = zero_zero_int )
| ( ( power_power_int @ X6 @ X1 )
!= zero_zero_int ) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_42,negated_conjecture,
( ( ( power_power_int @ x @ pm )
= zero_zero_int )
| ( ( divide_divide_int @ ( times_times_int @ x @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_35]),c_0_36]) ).
thf(c_0_43,plain,
! [X1303: nat] :
( ( ( ( semiri2019852685at_int @ X1303 )
!= zero_zero_int )
| ( X1303 = zero_zero_nat ) )
& ( ( X1303 != zero_zero_nat )
| ( ( semiri2019852685at_int @ X1303 )
= zero_zero_int ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_190_of__nat__eq__0__iff])])]) ).
thf(c_0_44,plain,
! [X1443: nat] :
( zero_zero_nat
!= ( suc @ X1443 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_37])]) ).
thf(c_0_45,plain,
! [X6: int] :
( ( times_times_int @ X6 @ zero_zero_int )
= zero_zero_int ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
thf(c_0_46,plain,
! [X6: int] :
( ( divide_divide_int @ X6 @ zero_zero_int )
= zero_zero_int ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
thf(c_0_47,plain,
! [X6: int] :
( ( plus_plus_int @ zero_zero_int @ X6 )
= X6 ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
thf(c_0_48,negated_conjecture,
( ( x = zero_zero_int )
| ( ( divide_divide_int @ ( times_times_int @ x @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x ) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
thf(c_0_49,plain,
! [X1: nat] :
( ( X1 = zero_zero_nat )
| ( ( semiri2019852685at_int @ X1 )
!= zero_zero_int ) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
thf(c_0_50,plain,
! [X1: nat] :
( zero_zero_nat
!= ( suc @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
thf(c_0_51,negated_conjecture,
( ( ( divide_divide_int @ ( times_times_int @ x @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x )
| ( ( divide_divide_int @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_42]),c_0_45]),c_0_46]),c_0_47]) ).
thf(c_0_52,negated_conjecture,
( ( ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) )
= zero_zero_int )
| ( x = zero_zero_int ) ),
inference(spm,[status(thm)],[c_0_48,c_0_35]) ).
thf(c_0_53,plain,
! [X1: nat] :
( ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ X1 ) )
!= zero_zero_int ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_24]),c_0_50]) ).
thf(c_0_54,plain,
! [X1265: int] :
( ( times_times_int @ zero_zero_int @ X1265 )
= zero_zero_int ),
inference(variable_rename,[status(thm)],[fact_160_mult__zero__left]) ).
thf(c_0_55,plain,
! [X1295: int] :
( ( divide_divide_int @ zero_zero_int @ X1295 )
= zero_zero_int ),
inference(variable_rename,[status(thm)],[fact_180_bits__div__0]) ).
thf(c_0_56,negated_conjecture,
( ( ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) )
= zero_zero_int )
| ( ( divide_divide_int @ ( times_times_int @ x @ ( semiri2019852685at_int @ pm ) ) @ ( plus_plus_int @ ( semiri2019852685at_int @ ( suc @ zero_zero_nat ) ) @ ( semiri2019852685at_int @ pm ) ) )
!= x ) ),
inference(spm,[status(thm)],[c_0_51,c_0_35]) ).
thf(c_0_57,negated_conjecture,
x = zero_zero_int,
inference(sr,[status(thm)],[c_0_52,c_0_53]) ).
thf(c_0_58,plain,
! [X6: int] :
( ( times_times_int @ zero_zero_int @ X6 )
= zero_zero_int ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
thf(c_0_59,plain,
! [X6: int] :
( ( divide_divide_int @ zero_zero_int @ X6 )
= zero_zero_int ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
thf(c_0_60,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_56,c_0_57]),c_0_58]),c_0_59]),c_0_57])]),c_0_53]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP129^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.18 % Computer : n014.cluster.edu
% 0.12/0.18 % Model : x86_64 x86_64
% 0.12/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.18 % Memory : 8046.5625MB
% 0.12/0.18 % OS : Linux 6.8.0-71-generic
% 0.12/0.18 % CPULimit : 300
% 0.12/0.18 % WCLimit : 300
% 0.12/0.18 % DateTime : Tue Sep 29 19:57:44 UTC 2026
% 0.12/0.19 % CPUTime :
% 0.12/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.23 Running higher-order theorem proving
% 0.12/0.27 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.MtGtucuGGA/E---3.1_3134133.p
% 198.01/30.04 % Version: 3.5.1-ho
% 198.01/30.04 % Preprocessing class: HSLSSMSMSSSNSFA.
% 198.01/30.04 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 198.01/30.04 % Starting new_ho_10 with 900s (3) cores
% 198.01/30.04 % Starting sh2lt with 300s (1) cores
% 198.01/30.04 % Starting new_ho_5 with 300s (1) cores
% 198.01/30.04 % Starting full_lambda_5 with 300s (1) cores
% 198.01/30.04 % Starting sh9 with 300s (1) cores
% 198.01/30.04 % Starting ehoh_best8_lambda with 300s (1) cores
% 198.01/30.04 % full_lambda_5 with pid 3134149 completed with status 0
% 198.01/30.04 % Result found by full_lambda_5
% 198.01/30.04 % Preprocessing class: HSLSSMSMSSSNSFA.
% 198.01/30.04 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 198.01/30.04 % Starting new_ho_10 with 900s (3) cores
% 198.01/30.04 % Starting sh2lt with 300s (1) cores
% 198.01/30.04 % Starting new_ho_5 with 300s (1) cores
% 198.01/30.04 % Starting full_lambda_5 with 300s (1) cores
% 198.01/30.04 % (lift_lambdas = 1, lambda_to_forall = 0,unroll_only_formulas = 1, sine = Auto)
% 198.01/30.04 % No SInE strategy applied
% 198.01/30.04 % Search class: HGHSM-FSLM31-MSFFFFBN
% 198.01/30.04 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 198.01/30.04 % Starting SubtermCWHack with 28s (1) cores
% 198.01/30.04 % SubtermCWHack with pid 3134155 completed with status 8
% 198.01/30.04 % Starting full_lambda_5 with 31s (1) cores
% 198.01/30.04 % full_lambda_5 with pid 3134162 completed with status 0
% 198.01/30.04 % Result found by full_lambda_5
% 198.01/30.04 % Preprocessing class: HSLSSMSMSSSNSFA.
% 198.01/30.04 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 198.01/30.04 % Starting new_ho_10 with 900s (3) cores
% 198.01/30.04 % Starting sh2lt with 300s (1) cores
% 198.01/30.04 % Starting new_ho_5 with 300s (1) cores
% 198.01/30.04 % Starting full_lambda_5 with 300s (1) cores
% 198.01/30.04 % (lift_lambdas = 1, lambda_to_forall = 0,unroll_only_formulas = 1, sine = Auto)
% 198.01/30.04 % No SInE strategy applied
% 198.01/30.04 % Search class: HGHSM-FSLM31-MSFFFFBN
% 198.01/30.04 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 198.01/30.04 % Starting SubtermCWHack with 28s (1) cores
% 198.01/30.04 % SubtermCWHack with pid 3134155 completed with status 8
% 198.01/30.04 % Starting full_lambda_5 with 31s (1) cores
% 198.01/30.04 % Preprocessing time : 0.006 s
% 198.01/30.04 % Presaturation interreduction done
% 198.01/30.04
% 198.01/30.04 % Proof found!
% 198.01/30.04 % SZS status Theorem
% 198.01/30.04 % SZS output start CNFRefutation
% See solution above
% 198.01/30.04 % Parsed axioms : 342
% 198.01/30.04 % Removed by relevancy pruning/SinE : 0
% 198.01/30.04 % Initial clauses : 466
% 198.01/30.04 % Removed in clause preprocessing : 71
% 198.01/30.04 % Initial clauses in saturation : 395
% 198.01/30.04 % Processed clauses : 667
% 198.01/30.04 % ...of these trivial : 73
% 198.01/30.04 % ...subsumed : 132
% 198.01/30.04 % ...remaining for further processing : 462
% 198.01/30.04 % Other redundant clauses eliminated : 93
% 198.01/30.04 % Clauses deleted for lack of memory : 0
% 198.01/30.04 % Backward-subsumed : 2
% 198.01/30.04 % Backward-rewritten : 31
% 198.01/30.04 % Generated clauses : 1786
% 198.01/30.04 % ...of the previous two non-redundant : 1411
% 198.01/30.04 % ...aggressively subsumed : 0
% 198.01/30.04 % Contextual simplify-reflections : 0
% 198.01/30.04 % Paramodulations : 1673
% 198.01/30.04 % Factorizations : 0
% 198.01/30.04 % NegExts : 0
% 198.01/30.04 % Equation resolutions : 109
% 198.01/30.04 % Disequality decompositions : 0
% 198.01/30.04 % Total rewrite steps : 1473
% 198.01/30.04 % ...of those cached : 907
% 198.01/30.04 % Propositional unsat checks : 0
% 198.01/30.04 % Propositional check models : 0
% 198.01/30.04 % Propositional check unsatisfiable : 0
% 198.01/30.04 % Propositional clauses : 0
% 198.01/30.04 % Propositional clauses after purity: 0
% 198.01/30.04 % Propositional unsat core size : 0
% 198.01/30.04 % Propositional preprocessing time : 0.000
% 198.01/30.04 % Propositional encoding time : 0.000
% 198.01/30.04 % Propositional solver time : 0.000
% 198.01/30.04 % Success case prop preproc time : 0.000
% 198.01/30.04 % Success case prop encoding time : 0.000
% 198.01/30.04 % Success case prop solver time : 0.000
% 198.01/30.04 % Current number of processed clauses : 173
% 198.01/30.04 % Positive orientable unit clauses : 78
% 198.01/30.04 % Positive unorientable unit clauses: 10
% 198.01/30.04 % Negative unit clauses : 15
% 198.01/30.04 % Non-unit-clauses : 70
% 198.01/30.04 % Current number of unprocessed clauses: 1317
% 198.01/30.04 % ...number of literals in the above : 2445
% 198.01/30.04 % Current number of archived formulas : 0
% 198.01/30.04 % Current number of archived clauses : 212
% 198.01/30.04 % Clause-clause subsumption calls (NU) : 5306
% 198.01/30.04 % Rec. Clause-clause subsumption calls : 3885
% 198.01/30.04 % Non-unit clause-clause subsumptions : 78
% 198.01/30.04 % Unit Clause-clause subsumption calls : 444
% 198.01/30.04 % Rewrite failures with RHS unbound : 0
% 198.01/30.04 % BW rewrite match attempts : 112
% 198.01/30.04 % BW rewrite match successes : 78
% 198.01/30.04 % Condensation attempts : 0
% 198.01/30.04 % Condensation successes : 0
% 198.01/30.04 % Termbank termtop insertions : 42306
% 198.01/30.04 % Search garbage collected termcells : 5566
% 198.01/30.04
% 198.01/30.04 % -------------------------------------------------
% 198.01/30.04 % User time : 27.242 s
% 198.01/30.04 % System time : 0.993 s
% 198.01/30.04 % Total time : 28.235 s
% 198.01/30.04 % Maximum resident set size: 5384 pages
% 198.01/30.04
% 198.01/30.04 % -------------------------------------------------
% 198.01/30.04 % User time : 27.253 s
% 198.01/30.04 % System time : 0.999 s
% 198.01/30.04 % Total time : 28.252 s
% 198.01/30.04 % Maximum resident set size: 5120 pages
% 198.01/30.04 % E exiting
%------------------------------------------------------------------------------