%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ITP062^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 : n020.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:05:24 AM UTC 2026
% Result : Theorem 176.40s 26.92s
% Output : CNFRefutation 176.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 19
% Syntax : Number of formulae : 85 ( 80 unt; 0 typ; 0 def)
% Number of atoms : 93 ( 57 equ; 0 cnn)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 1116 ( 14 ~; 6 |; 0 &;1094 @)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 19 ( 17 usr; 8 con; 0-2 aty)
% Number of variables : 125 ( 5 ^; 120 !; 0 ?; 125 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
nat: $tType ).
thf(decl_sort2,type,
real: $tType ).
thf(decl_sort3,type,
num: $tType ).
thf(decl_24,type,
genClo1144207539le_rho: real ).
thf(decl_30,type,
abs_abs_real: real > real ).
thf(decl_32,type,
minus_minus_real: real > real > real ).
thf(decl_34,type,
one_one_real: real ).
thf(decl_37,type,
plus_plus_real: real > real > real ).
thf(decl_40,type,
times_times_real: real > real > real ).
thf(decl_41,type,
neg_numeral_dbl_real: real > real ).
thf(decl_42,type,
bit0: num > num ).
thf(decl_43,type,
one: num ).
thf(decl_45,type,
numeral_numeral_real: num > real ).
thf(decl_48,type,
ord_less_eq_real: real > real > $o ).
thf(decl_51,type,
c: nat > real > real ).
thf(decl_52,type,
d: nat > real > real ).
thf(decl_53,type,
p: nat ).
thf(decl_54,type,
q: nat ).
thf(decl_55,type,
s: real ).
thf(decl_56,type,
t: real ).
thf(fact_4_Eq4,axiom,
( ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( minus_minus_real @ one_one_real @ genClo1144207539le_rho ) ) )
= ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_4_Eq4) ).
thf(fact_84_one__add__one,axiom,
( ( plus_plus_real @ one_one_real @ one_one_real )
= ( numeral_numeral_real @ ( bit0 @ one ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_84_one__add__one) ).
thf(fact_165_mult_Ocommute,axiom,
( times_times_real
= ( ^ [X76: real,X77: real] : ( times_times_real @ X77 @ X76 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_165_mult_Ocommute) ).
thf(fact_5_Eq3,axiom,
ord_less_eq_real @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( minus_minus_real @ one_one_real @ genClo1144207539le_rho ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_5_Eq3) ).
thf(fact_224_mult__2,axiom,
! [X8: real] :
( ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ X8 )
= ( plus_plus_real @ X8 @ X8 ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_224_mult__2) ).
thf(fact_248_dbl__def,axiom,
( neg_numeral_dbl_real
= ( ^ [X12: real] : ( plus_plus_real @ X12 @ X12 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_248_dbl__def) ).
thf(fact_103_add_Ocommute,axiom,
( plus_plus_real
= ( ^ [X76: real,X77: real] : ( plus_plus_real @ X77 @ X76 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_103_add_Ocommute) ).
thf(fact_152_add__diff__eq,axiom,
! [X1: real,X2: real,X4: real] :
( ( plus_plus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1 @ X2 ) @ X4 ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_152_add__diff__eq) ).
thf(fact_151_diff__diff__eq2,axiom,
! [X1: real,X2: real,X4: real] :
( ( minus_minus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1 @ X4 ) @ X2 ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_151_diff__diff__eq2) ).
thf(conj_0,conjecture,
ord_less_eq_real @ ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',conj_0) ).
thf(fact_163_mult_Oleft__commute,axiom,
! [X2: real,X1: real,X4: real] :
( ( times_times_real @ X2 @ ( times_times_real @ X1 @ X4 ) )
= ( times_times_real @ X1 @ ( times_times_real @ X2 @ X4 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_163_mult_Oleft__commute) ).
thf(fact_149_diff__add__eq__diff__diff__swap,axiom,
! [X1: real,X2: real,X4: real] :
( ( minus_minus_real @ X1 @ ( plus_plus_real @ X2 @ X4 ) )
= ( minus_minus_real @ ( minus_minus_real @ X1 @ X4 ) @ X2 ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_149_diff__add__eq__diff__diff__swap) ).
thf(fact_9_Eq2,axiom,
ord_less_eq_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_9_Eq2) ).
thf(fact_150_diff__add__eq,axiom,
! [X1: real,X2: real,X4: real] :
( ( plus_plus_real @ ( minus_minus_real @ X1 @ X2 ) @ X4 )
= ( minus_minus_real @ ( plus_plus_real @ X1 @ X4 ) @ X2 ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_150_diff__add__eq) ).
thf(fact_222_mult__2__right,axiom,
! [X8: real] :
( ( times_times_real @ X8 @ ( numeral_numeral_real @ ( bit0 @ one ) ) )
= ( plus_plus_real @ X8 @ X8 ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_222_mult__2__right) ).
thf(fact_303_order_Otrans,axiom,
! [X1: real,X2: real,X4: real] :
( ( ord_less_eq_real @ X1 @ X2 )
=> ( ( ord_less_eq_real @ X2 @ X4 )
=> ( ord_less_eq_real @ X1 @ X4 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_303_order_Otrans) ).
thf(fact_3_Eq1,axiom,
( ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) )
= ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_3_Eq1) ).
thf(fact_135_distrib__right,axiom,
! [X1: real,X2: real,X4: real] :
( ( times_times_real @ ( plus_plus_real @ X1 @ X2 ) @ X4 )
= ( plus_plus_real @ ( times_times_real @ X1 @ X4 ) @ ( times_times_real @ X2 @ X4 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_135_distrib__right) ).
thf(fact_167_mult_Oassoc,axiom,
! [X1: real,X2: real,X4: real] :
( ( times_times_real @ ( times_times_real @ X1 @ X2 ) @ X4 )
= ( times_times_real @ X1 @ ( times_times_real @ X2 @ X4 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.LOm4ol46dR/E---3.1_1500343.p',fact_167_mult_Oassoc) ).
thf(c_0_19,plain,
( ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( minus_minus_real @ one_one_real @ genClo1144207539le_rho ) ) )
= ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(split_conjunct,[status(thm)],[fact_4_Eq4]) ).
thf(c_0_20,plain,
( ( plus_plus_real @ one_one_real @ one_one_real )
= ( numeral_numeral_real @ ( bit0 @ one ) ) ),
inference(split_conjunct,[status(thm)],[fact_84_one__add__one]) ).
thf(c_0_21,plain,
! [X1495: real,X1496: real] :
( ( times_times_real @ X1495 @ X1496 )
= ( times_times_real @ X1496 @ X1495 ) ),
inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_165_mult_Ocommute])]) ).
thf(c_0_22,plain,
ord_less_eq_real @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( minus_minus_real @ one_one_real @ genClo1144207539le_rho ) ) ),
inference(split_conjunct,[status(thm)],[fact_5_Eq3]) ).
thf(c_0_23,plain,
( ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( minus_minus_real @ one_one_real @ genClo1144207539le_rho ) ) )
= ( times_times_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ one_one_real ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(rw,[status(thm)],[c_0_19,c_0_20]) ).
thf(c_0_24,plain,
! [X1887: real,X1888: real] :
( ( times_times_real @ X1887 @ X1888 )
= ( times_times_real @ X1888 @ X1887 ) ),
inference(variable_rename,[status(thm)],[c_0_21]) ).
thf(c_0_25,plain,
! [X2051: real] :
( ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ X2051 )
= ( plus_plus_real @ X2051 @ X2051 ) ),
inference(variable_rename,[status(thm)],[fact_224_mult__2]) ).
thf(c_0_26,plain,
! [X1503: real] :
( ( neg_numeral_dbl_real @ X1503 )
= ( plus_plus_real @ X1503 @ X1503 ) ),
inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_248_dbl__def])]) ).
thf(c_0_27,plain,
! [X1488: real,X1489: real] :
( ( plus_plus_real @ X1488 @ X1489 )
= ( plus_plus_real @ X1489 @ X1488 ) ),
inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_103_add_Ocommute])]) ).
thf(c_0_28,plain,
! [X1855: real,X1856: real,X1857: real] :
( ( plus_plus_real @ X1855 @ ( minus_minus_real @ X1856 @ X1857 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1855 @ X1856 ) @ X1857 ) ),
inference(variable_rename,[status(thm)],[fact_152_add__diff__eq]) ).
thf(c_0_29,plain,
! [X1852: real,X1853: real,X1854: real] :
( ( minus_minus_real @ X1852 @ ( minus_minus_real @ X1853 @ X1854 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1852 @ X1854 ) @ X1853 ) ),
inference(variable_rename,[status(thm)],[fact_151_diff__diff__eq2]) ).
thf(c_0_30,negated_conjecture,
~ ( ord_less_eq_real @ ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(c_0_31,plain,
ord_less_eq_real @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( times_times_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ one_one_real ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ),
inference(rw,[status(thm)],[c_0_22,c_0_23]) ).
thf(c_0_32,plain,
! [X2: real,X1: real] :
( ( times_times_real @ X1 @ X2 )
= ( times_times_real @ X2 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
thf(c_0_33,plain,
! [X1881: real,X1882: real,X1883: real] :
( ( times_times_real @ X1881 @ ( times_times_real @ X1882 @ X1883 ) )
= ( times_times_real @ X1882 @ ( times_times_real @ X1881 @ X1883 ) ) ),
inference(variable_rename,[status(thm)],[fact_163_mult_Oleft__commute]) ).
thf(c_0_34,plain,
! [X1: real] :
( ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ X1 )
= ( plus_plus_real @ X1 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
thf(c_0_35,plain,
! [X2095: real] :
( ( neg_numeral_dbl_real @ X2095 )
= ( plus_plus_real @ X2095 @ X2095 ) ),
inference(variable_rename,[status(thm)],[c_0_26]) ).
thf(c_0_36,plain,
! [X1846: real,X1847: real,X1848: real] :
( ( minus_minus_real @ X1846 @ ( plus_plus_real @ X1847 @ X1848 ) )
= ( minus_minus_real @ ( minus_minus_real @ X1846 @ X1848 ) @ X1847 ) ),
inference(variable_rename,[status(thm)],[fact_149_diff__add__eq__diff__diff__swap]) ).
thf(c_0_37,plain,
! [X1709: real,X1710: real] :
( ( plus_plus_real @ X1709 @ X1710 )
= ( plus_plus_real @ X1710 @ X1709 ) ),
inference(variable_rename,[status(thm)],[c_0_27]) ).
thf(c_0_38,plain,
! [X2: real,X1: real,X4: real] :
( ( plus_plus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1 @ X2 ) @ X4 ) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
thf(c_0_39,plain,
! [X4: real,X1: real,X2: real] :
( ( minus_minus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) )
= ( minus_minus_real @ ( plus_plus_real @ X1 @ X4 ) @ X2 ) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
thf(c_0_40,negated_conjecture,
~ ( ord_less_eq_real @ ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(fof_simplification,[status(thm)],[c_0_30]) ).
thf(c_0_41,plain,
ord_less_eq_real @ ( minus_minus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( times_times_real @ genClo1144207539le_rho @ ( plus_plus_real @ one_one_real @ one_one_real ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_32]),c_0_32]),c_0_32]) ).
thf(c_0_42,plain,
! [X2: real,X1: real,X4: real] :
( ( times_times_real @ X1 @ ( times_times_real @ X2 @ X4 ) )
= ( times_times_real @ X2 @ ( times_times_real @ X1 @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_43,plain,
! [X1: real] :
( ( times_times_real @ ( plus_plus_real @ one_one_real @ one_one_real ) @ X1 )
= ( plus_plus_real @ X1 @ X1 ) ),
inference(rw,[status(thm)],[c_0_34,c_0_20]) ).
thf(c_0_44,plain,
! [X1: real] :
( ( neg_numeral_dbl_real @ X1 )
= ( plus_plus_real @ X1 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
thf(c_0_45,plain,
ord_less_eq_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( minus_minus_real @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ),
inference(split_conjunct,[status(thm)],[fact_9_Eq2]) ).
thf(c_0_46,plain,
! [X4: real,X1: real,X2: real] :
( ( minus_minus_real @ X1 @ ( plus_plus_real @ X2 @ X4 ) )
= ( minus_minus_real @ ( minus_minus_real @ X1 @ X4 ) @ X2 ) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
thf(c_0_47,plain,
! [X2: real,X1: real] :
( ( plus_plus_real @ X1 @ X2 )
= ( plus_plus_real @ X2 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
thf(c_0_48,plain,
! [X4: real,X1: real,X2: real] :
( ( minus_minus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) )
= ( plus_plus_real @ X1 @ ( minus_minus_real @ X4 @ X2 ) ) ),
inference(rw,[status(thm)],[c_0_38,c_0_39]) ).
thf(c_0_49,plain,
! [X1849: real,X1850: real,X1851: real] :
( ( plus_plus_real @ ( minus_minus_real @ X1849 @ X1850 ) @ X1851 )
= ( minus_minus_real @ ( plus_plus_real @ X1849 @ X1851 ) @ X1850 ) ),
inference(variable_rename,[status(thm)],[fact_150_diff__add__eq]) ).
thf(c_0_50,plain,
! [X2049: real] :
( ( times_times_real @ X2049 @ ( numeral_numeral_real @ ( bit0 @ one ) ) )
= ( plus_plus_real @ X2049 @ X2049 ) ),
inference(variable_rename,[status(thm)],[fact_222_mult__2__right]) ).
thf(c_0_51,negated_conjecture,
~ ( ord_less_eq_real @ ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(fof_nnf,[status(thm)],[c_0_40]) ).
thf(c_0_52,plain,
! [X2348: real,X2349: real,X2350: real] :
( ~ ( ord_less_eq_real @ X2348 @ X2349 )
| ~ ( ord_less_eq_real @ X2349 @ X2350 )
| ( ord_less_eq_real @ X2348 @ X2350 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_303_order_Otrans])])]) ).
thf(c_0_53,plain,
ord_less_eq_real @ ( minus_minus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( times_times_real @ genClo1144207539le_rho @ ( neg_numeral_dbl_real @ ( minus_minus_real @ t @ s ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41,c_0_42]),c_0_32]),c_0_43]),c_0_44]) ).
thf(c_0_54,plain,
ord_less_eq_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( c @ p @ s ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( minus_minus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45,c_0_46]),c_0_47]),c_0_32]) ).
thf(c_0_55,plain,
! [X2: real,X1: real,X4: real] :
( ( minus_minus_real @ ( plus_plus_real @ X1 @ X2 ) @ X4 )
= ( plus_plus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) ) ),
inference(rw,[status(thm)],[c_0_39,c_0_48]) ).
thf(c_0_56,plain,
! [X4: real,X1: real,X2: real] :
( ( plus_plus_real @ ( minus_minus_real @ X1 @ X2 ) @ X4 )
= ( minus_minus_real @ ( plus_plus_real @ X1 @ X4 ) @ X2 ) ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
thf(c_0_57,plain,
! [X1: real] :
( ( times_times_real @ X1 @ ( numeral_numeral_real @ ( bit0 @ one ) ) )
= ( plus_plus_real @ X1 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
thf(c_0_58,negated_conjecture,
~ ( ord_less_eq_real @ ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( times_times_real @ ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
thf(c_0_59,plain,
( ( abs_abs_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) )
= ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ),
inference(split_conjunct,[status(thm)],[fact_3_Eq1]) ).
thf(c_0_60,plain,
! [X2: real,X1: real,X4: real] :
( ( ord_less_eq_real @ X1 @ X4 )
| ~ ( ord_less_eq_real @ X1 @ X2 )
| ~ ( ord_less_eq_real @ X2 @ X4 ) ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
thf(c_0_61,plain,
ord_less_eq_real @ ( plus_plus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( minus_minus_real @ ( d @ q @ s ) @ ( d @ q @ t ) ) ) @ ( times_times_real @ genClo1144207539le_rho @ ( neg_numeral_dbl_real @ ( minus_minus_real @ t @ s ) ) ),
inference(rw,[status(thm)],[c_0_53,c_0_48]) ).
thf(c_0_62,plain,
ord_less_eq_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( c @ p @ s ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( plus_plus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( minus_minus_real @ ( d @ q @ s ) @ ( d @ q @ t ) ) ),
inference(rw,[status(thm)],[c_0_54,c_0_48]) ).
thf(c_0_63,plain,
! [X2: real,X1: real,X4: real] :
( ( plus_plus_real @ X1 @ ( minus_minus_real @ X2 @ X4 ) )
= ( plus_plus_real @ X2 @ ( minus_minus_real @ X1 @ X4 ) ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_47]),c_0_55]) ).
thf(c_0_64,plain,
! [X4: real,X1: real,X2: real] :
( ( plus_plus_real @ ( minus_minus_real @ X1 @ X2 ) @ X4 )
= ( plus_plus_real @ X1 @ ( minus_minus_real @ X4 @ X2 ) ) ),
inference(rw,[status(thm)],[c_0_56,c_0_55]) ).
thf(c_0_65,plain,
! [X1810: real,X1811: real,X1812: real] :
( ( times_times_real @ ( plus_plus_real @ X1810 @ X1811 ) @ X1812 )
= ( plus_plus_real @ ( times_times_real @ X1810 @ X1812 ) @ ( times_times_real @ X1811 @ X1812 ) ) ),
inference(variable_rename,[status(thm)],[fact_135_distrib__right]) ).
thf(c_0_66,plain,
! [X1891: real,X1892: real,X1893: real] :
( ( times_times_real @ ( times_times_real @ X1891 @ X1892 ) @ X1893 )
= ( times_times_real @ X1891 @ ( times_times_real @ X1892 @ X1893 ) ) ),
inference(variable_rename,[status(thm)],[fact_167_mult_Oassoc]) ).
thf(c_0_67,plain,
! [X1: real] :
( ( times_times_real @ X1 @ ( plus_plus_real @ one_one_real @ one_one_real ) )
= ( plus_plus_real @ X1 @ X1 ) ),
inference(rw,[status(thm)],[c_0_57,c_0_20]) ).
thf(c_0_68,negated_conjecture,
~ ( ord_less_eq_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( times_times_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ one_one_real ) @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_58,c_0_59]),c_0_20]) ).
thf(c_0_69,plain,
! [X1: real] :
( ( ord_less_eq_real @ X1 @ ( times_times_real @ genClo1144207539le_rho @ ( neg_numeral_dbl_real @ ( minus_minus_real @ t @ s ) ) ) )
| ~ ( ord_less_eq_real @ X1 @ ( plus_plus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( minus_minus_real @ ( d @ q @ s ) @ ( d @ q @ t ) ) ) ) ),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
thf(c_0_70,plain,
ord_less_eq_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( d @ q @ t ) @ ( minus_minus_real @ ( c @ p @ s ) @ ( d @ q @ s ) ) ) ) @ ( plus_plus_real @ ( d @ q @ s ) @ ( minus_minus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( d @ q @ t ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_62,c_0_63]),c_0_63]) ).
thf(c_0_71,plain,
! [X1: real,X4: real,X8: real,X2: real] :
( ( minus_minus_real @ X1 @ ( plus_plus_real @ X2 @ ( minus_minus_real @ X4 @ X8 ) ) )
= ( plus_plus_real @ X1 @ ( minus_minus_real @ X8 @ ( plus_plus_real @ X4 @ X2 ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_48]),c_0_64]),c_0_64]),c_0_46]) ).
thf(c_0_72,plain,
! [X2: real,X1: real,X4: real] :
( ( times_times_real @ ( plus_plus_real @ X1 @ X2 ) @ X4 )
= ( plus_plus_real @ ( times_times_real @ X1 @ X4 ) @ ( times_times_real @ X2 @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
thf(c_0_73,plain,
! [X2: real,X1: real,X4: real] :
( ( times_times_real @ ( times_times_real @ X1 @ X2 ) @ X4 )
= ( times_times_real @ X1 @ ( times_times_real @ X2 @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
thf(c_0_74,plain,
! [X1: real] :
( ( times_times_real @ X1 @ ( plus_plus_real @ one_one_real @ one_one_real ) )
= ( neg_numeral_dbl_real @ X1 ) ),
inference(spm,[status(thm)],[c_0_44,c_0_67]) ).
thf(c_0_75,negated_conjecture,
~ ( ord_less_eq_real @ ( minus_minus_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( c @ p @ s ) ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) @ ( times_times_real @ ( minus_minus_real @ t @ s ) @ ( times_times_real @ genClo1144207539le_rho @ ( plus_plus_real @ one_one_real @ one_one_real ) ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68,c_0_32]),c_0_32]) ).
thf(c_0_76,plain,
! [X1: real] :
( ( ord_less_eq_real @ X1 @ ( times_times_real @ genClo1144207539le_rho @ ( neg_numeral_dbl_real @ ( minus_minus_real @ t @ s ) ) ) )
| ~ ( ord_less_eq_real @ X1 @ ( plus_plus_real @ ( d @ q @ s ) @ ( minus_minus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( d @ q @ t ) ) ) ) ),
inference(rw,[status(thm)],[c_0_69,c_0_63]) ).
thf(c_0_77,plain,
ord_less_eq_real @ ( plus_plus_real @ ( d @ q @ s ) @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( d @ q @ t ) @ ( c @ p @ s ) ) ) ) @ ( plus_plus_real @ ( d @ q @ s ) @ ( minus_minus_real @ ( times_times_real @ ( plus_plus_real @ one_one_real @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) @ ( d @ q @ t ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_70,c_0_71]),c_0_47]),c_0_63]) ).
thf(c_0_78,plain,
! [X1: real,X2: real] :
( ( neg_numeral_dbl_real @ ( times_times_real @ X1 @ X2 ) )
= ( times_times_real @ ( plus_plus_real @ X1 @ X1 ) @ X2 ) ),
inference(spm,[status(thm)],[c_0_44,c_0_72]) ).
thf(c_0_79,plain,
! [X1: real,X2: real] :
( ( neg_numeral_dbl_real @ ( times_times_real @ X1 @ X2 ) )
= ( times_times_real @ X1 @ ( neg_numeral_dbl_real @ X2 ) ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_74]),c_0_74]) ).
thf(c_0_80,negated_conjecture,
~ ( ord_less_eq_real @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( c @ p @ s ) @ ( minus_minus_real @ ( d @ q @ t ) @ ( d @ q @ s ) ) ) ) @ ( times_times_real @ ( plus_plus_real @ genClo1144207539le_rho @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_75,c_0_46]),c_0_47]),c_0_67]),c_0_32]) ).
thf(c_0_81,plain,
ord_less_eq_real @ ( plus_plus_real @ ( d @ q @ s ) @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( d @ q @ t ) @ ( c @ p @ s ) ) ) ) @ ( times_times_real @ genClo1144207539le_rho @ ( neg_numeral_dbl_real @ ( minus_minus_real @ t @ s ) ) ),
inference(spm,[status(thm)],[c_0_76,c_0_77]) ).
thf(c_0_82,plain,
! [X1: real,X2: real] :
( ( times_times_real @ X1 @ ( neg_numeral_dbl_real @ X2 ) )
= ( times_times_real @ ( plus_plus_real @ X1 @ X1 ) @ X2 ) ),
inference(rw,[status(thm)],[c_0_78,c_0_79]) ).
thf(c_0_83,negated_conjecture,
~ ( ord_less_eq_real @ ( plus_plus_real @ ( d @ q @ s ) @ ( minus_minus_real @ ( c @ p @ t ) @ ( plus_plus_real @ ( d @ q @ t ) @ ( c @ p @ s ) ) ) ) @ ( times_times_real @ ( plus_plus_real @ genClo1144207539le_rho @ genClo1144207539le_rho ) @ ( minus_minus_real @ t @ s ) ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_80,c_0_71]),c_0_63]) ).
thf(c_0_84,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_81,c_0_82]),c_0_83]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP062^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.16 % Computer : n020.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Tue Sep 29 19:46:04 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.08/0.26 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.LOm4ol46dR/E---3.1_1500343.p
% 176.40/26.92 % Version: 3.5.1-ho
% 176.40/26.92 % Preprocessing class: HSLSSMSMSSSNHFA.
% 176.40/26.92 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 176.40/26.92 % Starting new_ho_10 with 1500s (5) cores
% 176.40/26.92 % Starting new_ho_10_cnf2 with 300s (1) cores
% 176.40/26.92 % Starting full_lambda_6 with 300s (1) cores
% 176.40/26.92 % Starting full_lambda_9 with 300s (1) cores
% 176.40/26.92 % new_ho_10 with pid 1500356 completed with status 0
% 176.40/26.92 % Result found by new_ho_10
% 176.40/26.92 % Preprocessing class: HSLSSMSMSSSNHFA.
% 176.40/26.92 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 176.40/26.92 % Starting new_ho_10 with 1500s (5) cores
% 176.40/26.92 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 176.40/26.92 % No SInE strategy applied
% 176.40/26.92 % Search class: HGUSM-FSLM33-MHFFFFBN
% 176.40/26.92 % partial match(1): HGUSM-FSLM32-MHFFFFBN
% 176.40/26.92 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 176.40/26.92 % Starting SubtermCWHack with 136s (1) cores
% 176.40/26.92 % Starting new_ho_10 with 151s (1) cores
% 176.40/26.92 % Starting full_lambda_10 with 136s (1) cores
% 176.40/26.92 % Starting new_ho_7 with 136s (1) cores
% 176.40/26.92 % Starting full_lambda_2 with 136s (1) cores
% 176.40/26.92 % new_ho_10 with pid 1500364 completed with status 0
% 176.40/26.92 % Result found by new_ho_10
% 176.40/26.92 % Preprocessing class: HSLSSMSMSSSNHFA.
% 176.40/26.92 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 176.40/26.92 % Starting new_ho_10 with 1500s (5) cores
% 176.40/26.92 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 176.40/26.92 % No SInE strategy applied
% 176.40/26.92 % Search class: HGUSM-FSLM33-MHFFFFBN
% 176.40/26.92 % partial match(1): HGUSM-FSLM32-MHFFFFBN
% 176.40/26.92 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 176.40/26.92 % Starting SubtermCWHack with 136s (1) cores
% 176.40/26.92 % Starting new_ho_10 with 151s (1) cores
% 176.40/26.92 % Preprocessing time : 0.012 s
% 176.40/26.92 % Presaturation interreduction done
% 176.40/26.92
% 176.40/26.92 % Proof found!
% 176.40/26.92 % SZS status Theorem
% 176.40/26.92 % SZS output start CNFRefutation
% See solution above
% 176.40/26.92 % Parsed axioms : 391
% 176.40/26.92 % Removed by relevancy pruning/SinE : 0
% 176.40/26.92 % Initial clauses : 701
% 176.40/26.92 % Removed in clause preprocessing : 57
% 176.40/26.92 % Initial clauses in saturation : 644
% 176.40/26.92 % Processed clauses : 10589
% 176.40/26.92 % ...of these trivial : 842
% 176.40/26.92 % ...subsumed : 5307
% 176.40/26.92 % ...remaining for further processing : 4440
% 176.40/26.92 % Other redundant clauses eliminated : 2127
% 176.40/26.92 % Clauses deleted for lack of memory : 0
% 176.40/26.92 % Backward-subsumed : 106
% 176.40/26.92 % Backward-rewritten : 260
% 176.40/26.92 % Generated clauses : 776696
% 176.40/26.92 % ...of the previous two non-redundant : 743339
% 176.40/26.92 % ...aggressively subsumed : 0
% 176.40/26.92 % Contextual simplify-reflections : 75
% 176.40/26.92 % Paramodulations : 774491
% 176.40/26.92 % Factorizations : 8
% 176.40/26.92 % NegExts : 0
% 176.40/26.92 % Equation resolutions : 2180
% 176.40/26.92 % Disequality decompositions : 0
% 176.40/26.92 % Total rewrite steps : 628452
% 176.40/26.92 % ...of those cached : 525830
% 176.40/26.92 % Propositional unsat checks : 0
% 176.40/26.92 % Propositional check models : 0
% 176.40/26.92 % Propositional check unsatisfiable : 0
% 176.40/26.92 % Propositional clauses : 0
% 176.40/26.92 % Propositional clauses after purity: 0
% 176.40/26.92 % Propositional unsat core size : 0
% 176.40/26.92 % Propositional preprocessing time : 0.000
% 176.40/26.92 % Propositional encoding time : 0.000
% 176.40/26.92 % Propositional solver time : 0.000
% 176.40/26.92 % Success case prop preproc time : 0.000
% 176.40/26.92 % Success case prop encoding time : 0.000
% 176.40/26.92 % Success case prop solver time : 0.000
% 176.40/26.92 % Current number of processed clauses : 3695
% 176.40/26.92 % Positive orientable unit clauses : 741
% 176.40/26.92 % Positive unorientable unit clauses: 92
% 176.40/26.92 % Negative unit clauses : 132
% 176.40/26.92 % Non-unit-clauses : 2730
% 176.40/26.92 % Current number of unprocessed clauses: 732533
% 176.40/26.92 % ...number of literals in the above : 2029154
% 176.40/26.92 % Current number of archived formulas : 0
% 176.40/26.92 % Current number of archived clauses : 663
% 176.40/26.92 % Clause-clause subsumption calls (NU) : 1105449
% 176.40/26.92 % Rec. Clause-clause subsumption calls : 873035
% 176.40/26.92 % Non-unit clause-clause subsumptions : 3229
% 176.40/26.92 % Unit Clause-clause subsumption calls : 130746
% 176.40/26.92 % Rewrite failures with RHS unbound : 0
% 176.40/26.92 % BW rewrite match attempts : 5262
% 176.40/26.92 % BW rewrite match successes : 972
% 176.40/26.92 % Condensation attempts : 10589
% 176.40/26.92 % Condensation successes : 42
% 176.40/26.92 % Termbank termtop insertions : 15803037
% 176.40/26.92 % Search garbage collected termcells : 11101
% 176.40/26.92
% 176.40/26.92 % -------------------------------------------------
% 176.40/26.92 % User time : 24.508 s
% 176.40/26.92 % System time : 0.719 s
% 176.40/26.92 % Total time : 25.227 s
% 176.40/26.92 % Maximum resident set size: 6732 pages
% 176.40/26.92
% 176.40/26.92 % -------------------------------------------------
% 176.40/26.92 % User time : 122.204 s
% 176.40/26.92 % System time : 3.574 s
% 176.40/26.92 % Total time : 125.778 s
% 176.40/26.92 % Maximum resident set size: 5376 pages
% 176.40/26.92 % E exiting
%------------------------------------------------------------------------------