%------------------------------------------------------------------------------
% File : Lash---1.13
% Problem : ITP214^3 : TPTP v9.2.1. Bugfixed v9.2.1.
% Transfm : none
% Format : tptp:raw
% Command : lash -P picomus -M modes -p tstp -t %d %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Feb 28 09:29:47 AM UTC 2026
% Result : Theorem 49.21s 61.68s
% Output : Proof 49.21s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named h2)
% Comments :
%------------------------------------------------------------------------------
thf(ty_a,type,
a: $tType ).
thf(ty_produc7388388658123137530it_nat,type,
produc7388388658123137530it_nat: $tType ).
thf(ty_nat,type,
nat: $tType ).
thf(ty_assn,type,
assn: $tType ).
thf(ty_option4065278094766928714it_nat,type,
option4065278094766928714it_nat: $tType ).
thf(ty_option3562590408128118217it_nat,type,
option3562590408128118217it_nat: $tType ).
thf(ty_set_nat,type,
set_nat: $tType ).
thf(ty_produc3260487557148687353it_nat,type,
produc3260487557148687353it_nat: $tType ).
thf(ty_heap_Time_Heap_a,type,
heap_Time_Heap_a: $tType ).
thf(ty_heap_Time_Heap_b,type,
heap_Time_Heap_b: $tType ).
thf(ty_b,type,
b: $tType ).
thf(ty_heap_e7401611519738050253t_unit,type,
heap_e7401611519738050253t_unit: $tType ).
thf(ty_produc6653097349344004940it_nat,type,
produc6653097349344004940it_nat: $tType ).
thf(ty_produc3658429121746597890et_nat,type,
produc3658429121746597890et_nat: $tType ).
thf(ty_h2,type,
h2: heap_e7401611519738050253t_unit ).
thf(ty_some_P7913643980934408916it_nat,type,
some_P7913643980934408916it_nat: produc3260487557148687353it_nat > option3562590408128118217it_nat ).
thf(ty_produc9178034014595674355it_nat,type,
produc9178034014595674355it_nat: a > produc6653097349344004940it_nat > produc3260487557148687353it_nat ).
thf(ty_eigen__4,type,
eigen__4: heap_e7401611519738050253t_unit ).
thf(ty_as,type,
as: set_nat ).
thf(ty_h,type,
h: heap_e7401611519738050253t_unit ).
thf(ty_eigen__0,type,
eigen__0: a ).
thf(ty_relH,type,
relH: set_nat > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > $o ).
thf(ty_eigen__5,type,
eigen__5: nat ).
thf(ty_g,type,
g: a > heap_Time_Heap_b ).
thf(ty_hoare_new_addrs,type,
hoare_new_addrs: heap_e7401611519738050253t_unit > set_nat > heap_e7401611519738050253t_unit > set_nat ).
thf(ty_some_P2818173045054083285it_nat,type,
some_P2818173045054083285it_nat: produc7388388658123137530it_nat > option4065278094766928714it_nat ).
thf(ty_eigen__1,type,
eigen__1: heap_e7401611519738050253t_unit ).
thf(ty_heap_Time_execute_a,type,
heap_Time_execute_a: heap_Time_Heap_a > heap_e7401611519738050253t_unit > option3562590408128118217it_nat ).
thf(ty_collect_nat,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(ty_lim_Product_unit,type,
lim_Product_unit: heap_e7401611519738050253t_unit > nat ).
thf(ty_member_nat,type,
member_nat: nat > set_nat > $o ).
thf(ty_heap_Time_execute_b,type,
heap_Time_execute_b: heap_Time_Heap_b > heap_e7401611519738050253t_unit > option4065278094766928714it_nat ).
thf(ty_ord_less_eq_nat,type,
ord_less_eq_nat: nat > nat > $o ).
thf(ty_produc7507926704131184380et_nat,type,
produc7507926704131184380et_nat: heap_e7401611519738050253t_unit > set_nat > produc3658429121746597890et_nat ).
thf(ty_eigen__3,type,
eigen__3: b ).
thf(ty_produc584006145561248582it_nat,type,
produc584006145561248582it_nat: heap_e7401611519738050253t_unit > nat > produc6653097349344004940it_nat ).
thf(ty_r,type,
r: a > assn ).
thf(ty_rep_assn,type,
rep_assn: assn > produc3658429121746597890et_nat > $o ).
thf(ty_q,type,
q: b > assn ).
thf(ty_produc4082563078715348724it_nat,type,
produc4082563078715348724it_nat: b > produc6653097349344004940it_nat > produc7388388658123137530it_nat ).
thf(ty_f,type,
f: heap_Time_Heap_a ).
thf(ty_h3,type,
h3: heap_e7401611519738050253t_unit ).
thf(ty_rf,type,
rf: a ).
thf(ty_ord_less_nat,type,
ord_less_nat: nat > nat > $o ).
thf(ty_eigen__2,type,
eigen__2: nat ).
thf(sP1,plain,
( sP1
<=> ( ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h ) )
= ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h3 @ as @ h ) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])]) ).
thf(sP2,plain,
( sP2
<=> ( rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])]) ).
thf(sP3,plain,
( sP3
<=> ( ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h )
= ( hoare_new_addrs @ h3 @ as @ h ) ) ),
introduced(definition,[new_symbols(definition,[sP3])]) ).
thf(sP4,plain,
( sP4
<=> ( rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h3 @ as @ h ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])]) ).
thf(sP5,plain,
( sP5
<=> $false ),
introduced(definition,[new_symbols(definition,[sP5])]) ).
thf(conj_0,conjecture,
sP4 ).
thf(h0,negated_conjecture,
~ sP4,
inference(assume_negation,[status(cth)],[conj_0]) ).
thf(h1,assumption,
~ ! [X1: heap_e7401611519738050253t_unit] :
( ~ ! [X2: nat] :
( ( heap_Time_execute_a @ f @ h3 )
!= ( some_P7913643980934408916it_nat @ ( produc9178034014595674355it_nat @ eigen__0 @ ( produc584006145561248582it_nat @ X1 @ X2 ) ) ) )
=> ( ( rep_assn @ ( r @ eigen__0 ) @ ( produc7507926704131184380et_nat @ X1 @ ( hoare_new_addrs @ h3 @ as @ X1 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X2: nat] :
~ ( ( ord_less_nat @ X2 @ ( lim_Product_unit @ h3 ) )
=> ( member_nat @ X2 @ as ) ) )
@ h3
@ X1 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h3 ) @ ( lim_Product_unit @ X1 ) ) ) ) ),
introduced(assumption,[]) ).
thf(h4,assumption,
~ ( ( rep_assn @ ( r @ eigen__0 ) @ ( produc7507926704131184380et_nat @ eigen__1 @ ( hoare_new_addrs @ h3 @ as @ eigen__1 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h3 ) )
=> ( member_nat @ X1 @ as ) ) )
@ h3
@ eigen__1 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h3 ) @ ( lim_Product_unit @ eigen__1 ) ) ) ),
introduced(assumption,[]) ).
thf(h5,assumption,
( ( heap_Time_execute_a @ f @ h3 )
= ( some_P7913643980934408916it_nat @ ( produc9178034014595674355it_nat @ eigen__0 @ ( produc584006145561248582it_nat @ eigen__1 @ eigen__2 ) ) ) ),
introduced(assumption,[]) ).
thf(h6,assumption,
rep_assn @ ( r @ eigen__0 ) @ ( produc7507926704131184380et_nat @ eigen__1 @ ( hoare_new_addrs @ h3 @ as @ eigen__1 ) ),
introduced(assumption,[]) ).
thf(h7,assumption,
~ ( ( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h3 ) )
=> ( member_nat @ X1 @ as ) ) )
@ h3
@ eigen__1 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h3 ) @ ( lim_Product_unit @ eigen__1 ) ) ),
introduced(assumption,[]) ).
thf(h8,assumption,
( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h3 ) )
=> ( member_nat @ X1 @ as ) ) )
@ h3
@ eigen__1 ),
introduced(assumption,[]) ).
thf(h9,assumption,
ord_less_eq_nat @ ( lim_Product_unit @ h3 ) @ ( lim_Product_unit @ eigen__1 ),
introduced(assumption,[]) ).
thf(h10,assumption,
~ ! [X1: heap_e7401611519738050253t_unit] :
( ~ ! [X2: nat] :
( ( heap_Time_execute_b @ ( g @ rf ) @ h2 )
!= ( some_P2818173045054083285it_nat @ ( produc4082563078715348724it_nat @ eigen__3 @ ( produc584006145561248582it_nat @ X1 @ X2 ) ) ) )
=> ( ( rep_assn @ ( q @ eigen__3 ) @ ( produc7507926704131184380et_nat @ X1 @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ X1 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X2: nat] :
~ ( ( ord_less_nat @ X2 @ ( lim_Product_unit @ h2 ) )
=> ( member_nat @ X2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ) ) )
@ h2
@ X1 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h2 ) @ ( lim_Product_unit @ X1 ) ) ) ) ),
introduced(assumption,[]) ).
thf(h11,assumption,
~ ( ~ ! [X1: nat] :
( ( heap_Time_execute_b @ ( g @ rf ) @ h2 )
!= ( some_P2818173045054083285it_nat @ ( produc4082563078715348724it_nat @ eigen__3 @ ( produc584006145561248582it_nat @ eigen__4 @ X1 ) ) ) )
=> ( ( rep_assn @ ( q @ eigen__3 ) @ ( produc7507926704131184380et_nat @ eigen__4 @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ eigen__4 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h2 ) )
=> ( member_nat @ X1 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ) ) )
@ h2
@ eigen__4 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h2 ) @ ( lim_Product_unit @ eigen__4 ) ) ) ) ),
introduced(assumption,[]) ).
thf(h12,assumption,
~ ! [X1: nat] :
( ( heap_Time_execute_b @ ( g @ rf ) @ h2 )
!= ( some_P2818173045054083285it_nat @ ( produc4082563078715348724it_nat @ eigen__3 @ ( produc584006145561248582it_nat @ eigen__4 @ X1 ) ) ) ),
introduced(assumption,[]) ).
thf(h13,assumption,
~ ( ( rep_assn @ ( q @ eigen__3 ) @ ( produc7507926704131184380et_nat @ eigen__4 @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ eigen__4 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h2 ) )
=> ( member_nat @ X1 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ) ) )
@ h2
@ eigen__4 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h2 ) @ ( lim_Product_unit @ eigen__4 ) ) ) ),
introduced(assumption,[]) ).
thf(h14,assumption,
( ( heap_Time_execute_b @ ( g @ rf ) @ h2 )
= ( some_P2818173045054083285it_nat @ ( produc4082563078715348724it_nat @ eigen__3 @ ( produc584006145561248582it_nat @ eigen__4 @ eigen__5 ) ) ) ),
introduced(assumption,[]) ).
thf(h15,assumption,
rep_assn @ ( q @ eigen__3 ) @ ( produc7507926704131184380et_nat @ eigen__4 @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ eigen__4 ) ),
introduced(assumption,[]) ).
thf(h16,assumption,
~ ( ( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h2 ) )
=> ( member_nat @ X1 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ) ) )
@ h2
@ eigen__4 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h2 ) @ ( lim_Product_unit @ eigen__4 ) ) ),
introduced(assumption,[]) ).
thf(h17,assumption,
( relH
@ ( collect_nat
@ ^ [X1: nat] :
~ ( ( ord_less_nat @ X1 @ ( lim_Product_unit @ h2 ) )
=> ( member_nat @ X1 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ) ) )
@ h2
@ eigen__4 ),
introduced(assumption,[]) ).
thf(h18,assumption,
ord_less_eq_nat @ ( lim_Product_unit @ h2 ) @ ( lim_Product_unit @ eigen__4 ),
introduced(assumption,[]) ).
thf(1,plain,
( sP1
| ~ sP3
| sP5 ),
inference(prop_rule,[status(thm)],[]) ).
thf(2,plain,
~ sP5,
inference(prop_rule,[status(thm)],[]) ).
thf(3,plain,
( ~ sP2
| sP4
| ~ sP1
| sP5 ),
inference(mating_rule,[status(thm)],[]) ).
thf(fact_3_POST__G,axiom,
sP2 ).
thf(fact_0__092_060open_062new__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_A_061_Anew__addrs_Ah_Aas_Ah_H_H_092_060close_062,axiom,
sP3 ).
thf(4,plain,
$false,
inference(prop_unsat,[status(thm),assumptions([h17,h18,h15,h16,h14,h12,h13,h11,h10,h8,h9,h6,h7,h5,h3,h4,h2,h1,h0])],[1,2,3,h0,fact_3_POST__G,fact_0__092_060open_062new__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_A_061_Anew__addrs_Ah_Aas_Ah_H_H_092_060close_062]) ).
thf(5,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h15,h16,h14,h12,h13,h11,h10,h8,h9,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h17,h18])],[h16,4,h17,h18]) ).
thf(6,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h14,h12,h13,h11,h10,h8,h9,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h15,h16])],[h13,5,h15,h16]) ).
thf(7,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h12,h13,h11,h10,h8,h9,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negall(discharge,[h14]),tab_negall(eigenvar,eigen__5)],[h12,6,h14]) ).
thf(8,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h11,h10,h8,h9,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h12,h13])],[h11,7,h12,h13]) ).
thf(9,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h10,h8,h9,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negall(discharge,[h11]),tab_negall(eigenvar,eigen__4)],[h10,8,h11]) ).
thf(fact_133__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rg_Ah_H_H_At_H_H_O_A_092_060lbrakk_062execute_A_Ig_Arf_J_Ah_H_A_061_ASome_A_Irg_M_Ah_H_H_M_At_H_H_J_059_A_Ih_H_H_M_Anew__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_J_A_092_060Turnstile_062_AQ_Arg_059_ArelH_A_123a_O_Aa_A_060_Alim_Ah_H_A_092_060and_062_Aa_A_092_060notin_062_Anew__addrs_Ah_Aas_Ah_H_125_Ah_H_Ah_H_H_059_Alim_Ah_H_A_092_060le_062_Alim_Ah_H_H_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X1: b,X2: heap_e7401611519738050253t_unit] :
( ~ ! [X3: nat] :
( ( heap_Time_execute_b @ ( g @ rf ) @ h2 )
!= ( some_P2818173045054083285it_nat @ ( produc4082563078715348724it_nat @ X1 @ ( produc584006145561248582it_nat @ X2 @ X3 ) ) ) )
=> ( ( rep_assn @ ( q @ X1 ) @ ( produc7507926704131184380et_nat @ X2 @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ X2 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X3: nat] :
~ ( ( ord_less_nat @ X3 @ ( lim_Product_unit @ h2 ) )
=> ( member_nat @ X3 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ) ) )
@ h2
@ X2 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h2 ) @ ( lim_Product_unit @ X2 ) ) ) ) ) ).
thf(10,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h8,h9,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negall(discharge,[h10]),tab_negall(eigenvar,eigen__3)],[fact_133__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rg_Ah_H_H_At_H_H_O_A_092_060lbrakk_062execute_A_Ig_Arf_J_Ah_H_A_061_ASome_A_Irg_M_Ah_H_H_M_At_H_H_J_059_A_Ih_H_H_M_Anew__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_J_A_092_060Turnstile_062_AQ_Arg_059_ArelH_A_123a_O_Aa_A_060_Alim_Ah_H_A_092_060and_062_Aa_A_092_060notin_062_Anew__addrs_Ah_Aas_Ah_H_125_Ah_H_Ah_H_H_059_Alim_Ah_H_A_092_060le_062_Alim_Ah_H_H_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,9,h10]) ).
thf(11,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h6,h7,h5,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h8,h9])],[h7,10,h8,h9]) ).
thf(12,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h5,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h6,h7])],[h4,11,h6,h7]) ).
thf(13,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h3,h4,h2,h1,h0]),tab_negall(discharge,[h5]),tab_negall(eigenvar,eigen__2)],[h3,12,h5]) ).
thf(14,plain,
$false,
inference(tab_negimp,[status(thm),assumptions([h2,h1,h0]),tab_negimp(discharge,[h3,h4])],[h2,13,h3,h4]) ).
thf(15,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[h1,14,h2]) ).
thf(fact_134__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rf_Ah_H_At_H_O_A_092_060lbrakk_062execute_Af_Ah_A_061_ASome_A_Irf_M_Ah_H_M_At_H_J_059_A_Ih_H_M_Anew__addrs_Ah_Aas_Ah_H_J_A_092_060Turnstile_062_AR_Arf_059_ArelH_A_123a_O_Aa_A_060_Alim_Ah_A_092_060and_062_Aa_A_092_060notin_062_Aas_125_Ah_Ah_H_059_Alim_Ah_A_092_060le_062_Alim_Ah_H_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,
~ ! [X1: a,X2: heap_e7401611519738050253t_unit] :
( ~ ! [X3: nat] :
( ( heap_Time_execute_a @ f @ h3 )
!= ( some_P7913643980934408916it_nat @ ( produc9178034014595674355it_nat @ X1 @ ( produc584006145561248582it_nat @ X2 @ X3 ) ) ) )
=> ( ( rep_assn @ ( r @ X1 ) @ ( produc7507926704131184380et_nat @ X2 @ ( hoare_new_addrs @ h3 @ as @ X2 ) ) )
=> ( ( relH
@ ( collect_nat
@ ^ [X3: nat] :
~ ( ( ord_less_nat @ X3 @ ( lim_Product_unit @ h3 ) )
=> ( member_nat @ X3 @ as ) ) )
@ h3
@ X2 )
=> ~ ( ord_less_eq_nat @ ( lim_Product_unit @ h3 ) @ ( lim_Product_unit @ X2 ) ) ) ) ) ).
thf(16,plain,
$false,
inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[fact_134__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rf_Ah_H_At_H_O_A_092_060lbrakk_062execute_Af_Ah_A_061_ASome_A_Irf_M_Ah_H_M_At_H_J_059_A_Ih_H_M_Anew__addrs_Ah_Aas_Ah_H_J_A_092_060Turnstile_062_AR_Arf_059_ArelH_A_123a_O_Aa_A_060_Alim_Ah_A_092_060and_062_Aa_A_092_060notin_062_Aas_125_Ah_Ah_H_059_Alim_Ah_A_092_060le_062_Alim_Ah_H_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,15,h1]) ).
thf(0,theorem,
sP4,
inference(contra,[status(thm),contra(discharge,[h0])],[16,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : ITP214^3 : TPTP v9.2.1. Bugfixed v9.2.1.
% 0.00/0.13 % Command : lash -P picomus -M modes -p tstp -t %d %s
% 0.19/0.38 % Computer : n003.cluster.edu
% 0.19/0.38 % Model : x86_64 x86_64
% 0.19/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.38 % Memory : 8042.1875MB
% 0.19/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.38 % CPULimit : 300
% 0.19/0.38 % WCLimit : 300
% 0.19/0.38 % DateTime : Thu Feb 26 04:13:56 EST 2026
% 0.19/0.38 % CPUTime :
% 49.21/61.68 % SZS status Theorem
% 49.21/61.68 % Mode: cade22sinegrackle2x78f3
% 49.21/61.68 % Steps: 3934
% 49.21/61.68 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------